lmemnth - ../examples/peano.mm1

Step	Hyp	Ref	Expression
1		eqidd	_1 = l -> a = a
2		id	_1 = l -> _1 = l
3	1, 2	lmemeqd	_1 = l -> (a IN _1 <-> a IN l)
4		eqidd	_1 = l -> n = n
5	4, 2	ntheqd	_1 = l -> nth n _1 = nth n l
6		eqidd	_1 = l -> suc a = suc a
7	5, 6	eqeqd	_1 = l -> (nth n _1 = suc a <-> nth n l = suc a)
8	7	exeqd	_1 = l -> (E. n nth n _1 = suc a <-> E. n nth n l = suc a)
9	3, 8	bieqd	_1 = l -> (a IN _1 <-> E. n nth n _1 = suc a <-> (a IN l <-> E. n nth n l = suc a))
10		eqidd	_1 = 0 -> a = a
11		id	_1 = 0 -> _1 = 0
12	10, 11	lmemeqd	_1 = 0 -> (a IN _1 <-> a IN 0)
13		eqidd	_1 = 0 -> n = n
14	13, 11	ntheqd	_1 = 0 -> nth n _1 = nth n 0
15		eqidd	_1 = 0 -> suc a = suc a
16	14, 15	eqeqd	_1 = 0 -> (nth n _1 = suc a <-> nth n 0 = suc a)
17	16	exeqd	_1 = 0 -> (E. n nth n _1 = suc a <-> E. n nth n 0 = suc a)
18	12, 17	bieqd	_1 = 0 -> (a IN _1 <-> E. n nth n _1 = suc a <-> (a IN 0 <-> E. n nth n 0 = suc a))
19		eqidd	_1 = a2 -> a = a
20		id	_1 = a2 -> _1 = a2
21	19, 20	lmemeqd	_1 = a2 -> (a IN _1 <-> a IN a2)
22		eqidd	_1 = a2 -> n = n
23	22, 20	ntheqd	_1 = a2 -> nth n _1 = nth n a2
24		eqidd	_1 = a2 -> suc a = suc a
25	23, 24	eqeqd	_1 = a2 -> (nth n _1 = suc a <-> nth n a2 = suc a)
26	25	exeqd	_1 = a2 -> (E. n nth n _1 = suc a <-> E. n nth n a2 = suc a)
27	21, 26	bieqd	_1 = a2 -> (a IN _1 <-> E. n nth n _1 = suc a <-> (a IN a2 <-> E. n nth n a2 = suc a))
28		eqidd	_1 = a1 : a2 -> a = a
29		id	_1 = a1 : a2 -> _1 = a1 : a2
30	28, 29	lmemeqd	_1 = a1 : a2 -> (a IN _1 <-> a IN a1 : a2)
31		eqidd	_1 = a1 : a2 -> n = n
32	31, 29	ntheqd	_1 = a1 : a2 -> nth n _1 = nth n (a1 : a2)
33		eqidd	_1 = a1 : a2 -> suc a = suc a
34	32, 33	eqeqd	_1 = a1 : a2 -> (nth n _1 = suc a <-> nth n (a1 : a2) = suc a)
35	34	exeqd	_1 = a1 : a2 -> (E. n nth n _1 = suc a <-> E. n nth n (a1 : a2) = suc a)
36	30, 35	bieqd	_1 = a1 : a2 -> (a IN _1 <-> E. n nth n _1 = suc a <-> (a IN a1 : a2 <-> E. n nth n (a1 : a2) = suc a))
37		binth	~a IN 0 -> ~E. n nth n 0 = suc a -> (a IN 0 <-> E. n nth n 0 = suc a)
38		lmem0	~a IN 0
39	38	binth*	~E. n nth n 0 = suc a -> (a IN 0 <-> E. n nth n 0 = suc a)
40		necom	suc a != nth n 0 -> nth n 0 != suc a
41	40	conv ne	suc a != nth n 0 -> ~nth n 0 = suc a
42		neeq2	nth n 0 = 0 -> (suc a != nth n 0 <-> suc a != 0)
43		nth0	nth n 0 = 0
44	43	neeq2*	suc a != nth n 0 <-> suc a != 0
45		peano1	suc a != 0
46	44, 45	mpbir	suc a != nth n 0
47	41, 46	ax_mp	~nth n 0 = suc a
48	47	nexi	~E. n nth n 0 = suc a
49	38, 48	binth*	a IN 0 <-> E. n nth n 0 = suc a
50		lmemS	a IN a1 : a2 <-> a = a1 \/ a IN a2
51		bitr3	(E. n (n = 0 /\ nth n (a1 : a2) = suc a \/ ~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. n (n = 0 /\ nth n (a1 : a2) = suc a) \/ E. n (~n = 0 /\ nth n (a1 : a2) = suc a)) -> (E. n (n = 0 /\ nth n (a1 : a2) = suc a \/ ~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. n nth n (a1 : a2) = suc a) -> (E. n (n = 0 /\ nth n (a1 : a2) = suc a) \/ E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. n nth n (a1 : a2) = suc a)
52		exor	E. n (n = 0 /\ nth n (a1 : a2) = suc a \/ ~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. n (n = 0 /\ nth n (a1 : a2) = suc a) \/ E. n (~n = 0 /\ nth n (a1 : a2) = suc a)
53	52	bitr3*	(E. n (n = 0 /\ nth n (a1 : a2) = suc a \/ ~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. n nth n (a1 : a2) = suc a) -> (E. n (n = 0 /\ nth n (a1 : a2) = suc a) \/ E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. n nth n (a1 : a2) = suc a)
54		bitr3	((n = 0 \/ ~n = 0) /\ nth n (a1 : a2) = suc a <-> n = 0 /\ nth n (a1 : a2) = suc a \/ ~n = 0 /\ nth n (a1 : a2) = suc a) -> ((n = 0 \/ ~n = 0) /\ nth n (a1 : a2) = suc a <-> nth n (a1 : a2) = suc a) -> (n = 0 /\ nth n (a1 : a2) = suc a \/ ~n = 0 /\ nth n (a1 : a2) = suc a <-> nth n (a1 : a2) = suc a)
55		andir	(n = 0 \/ ~n = 0) /\ nth n (a1 : a2) = suc a <-> n = 0 /\ nth n (a1 : a2) = suc a \/ ~n = 0 /\ nth n (a1 : a2) = suc a
56	55	bitr3*	((n = 0 \/ ~n = 0) /\ nth n (a1 : a2) = suc a <-> nth n (a1 : a2) = suc a) -> (n = 0 /\ nth n (a1 : a2) = suc a \/ ~n = 0 /\ nth n (a1 : a2) = suc a <-> nth n (a1 : a2) = suc a)
57		bian1	n = 0 \/ ~n = 0 -> ((n = 0 \/ ~n = 0) /\ nth n (a1 : a2) = suc a <-> nth n (a1 : a2) = suc a)
58		em	n = 0 \/ ~n = 0
59	58	bian1*	(n = 0 \/ ~n = 0) /\ nth n (a1 : a2) = suc a <-> nth n (a1 : a2) = suc a
60	55, 59	bitr3*	n = 0 /\ nth n (a1 : a2) = suc a \/ ~n = 0 /\ nth n (a1 : a2) = suc a <-> nth n (a1 : a2) = suc a
61	60	exeqi	E. n (n = 0 /\ nth n (a1 : a2) = suc a \/ ~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. n nth n (a1 : a2) = suc a
62	52, 61	bitr3*	E. n (n = 0 /\ nth n (a1 : a2) = suc a) \/ E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. n nth n (a1 : a2) = suc a
63		bicom	(E. n (n = 0 /\ nth n (a1 : a2) = suc a) <-> a = a1) -> (a = a1 <-> E. n (n = 0 /\ nth n (a1 : a2) = suc a))
64		eqcomb	a1 = a <-> a = a1
65		peano2	suc a1 = suc a <-> a1 = a
66		nthZ	nth 0 (a1 : a2) = suc a1
67		ntheq1	n = 0 -> nth n (a1 : a2) = nth 0 (a1 : a2)
68	66, 67	syl6eq	n = 0 -> nth n (a1 : a2) = suc a1
69	68	eqeq1d	n = 0 -> (nth n (a1 : a2) = suc a <-> suc a1 = suc a)
70	65, 69	syl6bb	n = 0 -> (nth n (a1 : a2) = suc a <-> a1 = a)
71	64, 70	syl6bb	n = 0 -> (nth n (a1 : a2) = suc a <-> a = a1)
72	71	exeqe	E. n (n = 0 /\ nth n (a1 : a2) = suc a) <-> a = a1
73	72	bicom*	a = a1 <-> E. n (n = 0 /\ nth n (a1 : a2) = suc a)
74	73	a1i	(a IN a2 <-> E. n nth n a2 = suc a) -> (a = a1 <-> E. n (n = 0 /\ nth n (a1 : a2) = suc a))
75		bi1	(a IN a2 <-> E. n nth n a2 = suc a <-> (a IN a2 <-> E. n (~n = 0 /\ nth n (a1 : a2) = suc a))) -> (a IN a2 <-> E. n nth n a2 = suc a) -> (a IN a2 <-> E. n (~n = 0 /\ nth n (a1 : a2) = suc a))
76		bieq2	(E. n nth n a2 = suc a <-> E. n (~n = 0 /\ nth n (a1 : a2) = suc a)) -> (a IN a2 <-> E. n nth n a2 = suc a <-> (a IN a2 <-> E. n (~n = 0 /\ nth n (a1 : a2) = suc a)))
77		bitr4	(E. n nth n a2 = suc a <-> E. a3 nth a3 a2 = suc a) -> (E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. a3 nth a3 a2 = suc a) -> (E. n nth n a2 = suc a <-> E. n (~n = 0 /\ nth n (a1 : a2) = suc a))
78		ntheq1	n = a3 -> nth n a2 = nth a3 a2
79	78	eqeq1d	n = a3 -> (nth n a2 = suc a <-> nth a3 a2 = suc a)
80	79	cbvex	E. n nth n a2 = suc a <-> E. a3 nth a3 a2 = suc a
81	80	bitr4*	(E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. a3 nth a3 a2 = suc a) -> (E. n nth n a2 = suc a <-> E. n (~n = 0 /\ nth n (a1 : a2) = suc a))
82		bitr	(E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. a3 E. n (n = suc a3 /\ nth n (a1 : a2) = suc a)) -> (E. a3 E. n (n = suc a3 /\ nth n (a1 : a2) = suc a) <-> E. a3 nth a3 a2 = suc a) -> (E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. a3 nth a3 a2 = suc a)
83		exsuc	n != 0 <-> E. a3 n = suc a3
84	83	conv ne	~n = 0 <-> E. a3 n = suc a3
85	84	a1i	nth n (a1 : a2) = suc a -> (~n = 0 <-> E. a3 n = suc a3)
86	85	biexan1a	~n = 0 /\ nth n (a1 : a2) = suc a <-> E. a3 (n = suc a3 /\ nth n (a1 : a2) = suc a)
87	86	biexexi	E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. a3 E. n (n = suc a3 /\ nth n (a1 : a2) = suc a)
88	87	bitr*	(E. a3 E. n (n = suc a3 /\ nth n (a1 : a2) = suc a) <-> E. a3 nth a3 a2 = suc a) -> (E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. a3 nth a3 a2 = suc a)
89		nthS	nth (suc a3) (a1 : a2) = nth a3 a2
90		ntheq1	n = suc a3 -> nth n (a1 : a2) = nth (suc a3) (a1 : a2)
91	89, 90	syl6eq	n = suc a3 -> nth n (a1 : a2) = nth a3 a2
92	91	eqeq1d	n = suc a3 -> (nth n (a1 : a2) = suc a <-> nth a3 a2 = suc a)
93	92	exeqe	E. n (n = suc a3 /\ nth n (a1 : a2) = suc a) <-> nth a3 a2 = suc a
94	93	exeqi	E. a3 E. n (n = suc a3 /\ nth n (a1 : a2) = suc a) <-> E. a3 nth a3 a2 = suc a
95	87, 94	bitr*	E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. a3 nth a3 a2 = suc a
96	80, 95	bitr4*	E. n nth n a2 = suc a <-> E. n (~n = 0 /\ nth n (a1 : a2) = suc a)
97	96	bieq2*	a IN a2 <-> E. n nth n a2 = suc a <-> (a IN a2 <-> E. n (~n = 0 /\ nth n (a1 : a2) = suc a))
98	97	bi1*	(a IN a2 <-> E. n nth n a2 = suc a) -> (a IN a2 <-> E. n (~n = 0 /\ nth n (a1 : a2) = suc a))
99	74, 98	oreqd	(a IN a2 <-> E. n nth n a2 = suc a) -> (a = a1 \/ a IN a2 <-> E. n (n = 0 /\ nth n (a1 : a2) = suc a) \/ E. n (~n = 0 /\ nth n (a1 : a2) = suc a))
100	62, 99	syl6bb	(a IN a2 <-> E. n nth n a2 = suc a) -> (a = a1 \/ a IN a2 <-> E. n nth n (a1 : a2) = suc a)
101	50, 100	syl5bb	(a IN a2 <-> E. n nth n a2 = suc a) -> (a IN a1 : a2 <-> E. n nth n (a1 : a2) = suc a)
102	9, 18, 27, 36, 49, 101	listind	a IN l <-> E. n nth n l = suc a

1

_1 = l -> a = a

2

id

_1 = l -> _1 = l

3

1, 2

lmemeqd

_1 = l -> (a IN _1 <-> a IN l)

4

eqidd

_1 = l -> n = n

5

4, 2

ntheqd

_1 = l -> nth n _1 = nth n l

6

eqidd

_1 = l -> suc a = suc a

7

5, 6

eqeqd

_1 = l -> (nth n _1 = suc a <-> nth n l = suc a)

8

7

exeqd

_1 = l -> (E. n nth n _1 = suc a <-> E. n nth n l = suc a)

9

3, 8

bieqd

_1 = l -> (a IN _1 <-> E. n nth n _1 = suc a <-> (a IN l <-> E. n nth n l = suc a))

10

eqidd

_1 = 0 -> a = a

11

id

_1 = 0 -> _1 = 0

12

10, 11

lmemeqd

_1 = 0 -> (a IN _1 <-> a IN 0)

13

eqidd

_1 = 0 -> n = n

14

13, 11

ntheqd

_1 = 0 -> nth n _1 = nth n 0

15

eqidd

_1 = 0 -> suc a = suc a

16

14, 15

eqeqd

_1 = 0 -> (nth n _1 = suc a <-> nth n 0 = suc a)

17

16

exeqd

_1 = 0 -> (E. n nth n _1 = suc a <-> E. n nth n 0 = suc a)

18

12, 17

bieqd

_1 = 0 -> (a IN _1 <-> E. n nth n _1 = suc a <-> (a IN 0 <-> E. n nth n 0 = suc a))

19

eqidd

_1 = a2 -> a = a

20

id

_1 = a2 -> _1 = a2

21

19, 20

lmemeqd

_1 = a2 -> (a IN _1 <-> a IN a2)

22

eqidd

_1 = a2 -> n = n

23

22, 20

ntheqd

_1 = a2 -> nth n _1 = nth n a2

24

eqidd

_1 = a2 -> suc a = suc a

25

23, 24

eqeqd

_1 = a2 -> (nth n _1 = suc a <-> nth n a2 = suc a)

26

25

exeqd

_1 = a2 -> (E. n nth n _1 = suc a <-> E. n nth n a2 = suc a)

27

21, 26

bieqd

_1 = a2 -> (a IN _1 <-> E. n nth n _1 = suc a <-> (a IN a2 <-> E. n nth n a2 = suc a))

28

eqidd

_1 = a1 : a2 -> a = a

29

id

_1 = a1 : a2 -> _1 = a1 : a2

30

28, 29

lmemeqd

_1 = a1 : a2 -> (a IN _1 <-> a IN a1 : a2)

31

eqidd

_1 = a1 : a2 -> n = n

32

31, 29

ntheqd

_1 = a1 : a2 -> nth n _1 = nth n (a1 : a2)

33

eqidd

_1 = a1 : a2 -> suc a = suc a

34

32, 33

eqeqd

_1 = a1 : a2 -> (nth n _1 = suc a <-> nth n (a1 : a2) = suc a)

35

34

exeqd

_1 = a1 : a2 -> (E. n nth n _1 = suc a <-> E. n nth n (a1 : a2) = suc a)

36

30, 35

bieqd

_1 = a1 : a2 -> (a IN _1 <-> E. n nth n _1 = suc a <-> (a IN a1 : a2 <-> E. n nth n (a1 : a2) = suc a))

37

binth

~a IN 0 -> ~E. n nth n 0 = suc a -> (a IN 0 <-> E. n nth n 0 = suc a)

38

lmem0

~a IN 0

39

38

binth*

~E. n nth n 0 = suc a -> (a IN 0 <-> E. n nth n 0 = suc a)

40

necom

suc a != nth n 0 -> nth n 0 != suc a

42

neeq2

nth n 0 = 0 -> (suc a != nth n 0 <-> suc a != 0)

43

nth0

nth n 0 = 0

44

43

neeq2*

suc a != nth n 0 <-> suc a != 0

45

peano1

suc a != 0

46

44, 45

mpbir

suc a != nth n 0

47

41, 46

ax_mp

~nth n 0 = suc a

48

47

nexi

~E. n nth n 0 = suc a

49

38, 48

binth*

a IN 0 <-> E. n nth n 0 = suc a

50

lmemS

a IN a1 : a2 <-> a = a1 \/ a IN a2

51

bitr3

(E. n (n = 0 /\ nth n (a1 : a2) = suc a \/ ~n = 0 /\ nth n (a1 : a2) = suc a) <->
    E. n (n = 0 /\ nth n (a1 : a2) = suc a) \/ E. n (~n = 0 /\ nth n (a1 : a2) = suc a)) ->
  (E. n (n = 0 /\ nth n (a1 : a2) = suc a \/ ~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. n nth n (a1 : a2) = suc a) ->
  (E. n (n = 0 /\ nth n (a1 : a2) = suc a) \/ E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. n nth n (a1 : a2) = suc a)

52

exor

E. n (n = 0 /\ nth n (a1 : a2) = suc a \/ ~n = 0 /\ nth n (a1 : a2) = suc a) <->
  E. n (n = 0 /\ nth n (a1 : a2) = suc a) \/ E. n (~n = 0 /\ nth n (a1 : a2) = suc a)

53

52

bitr3*

(E. n (n = 0 /\ nth n (a1 : a2) = suc a \/ ~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. n nth n (a1 : a2) = suc a) ->
  (E. n (n = 0 /\ nth n (a1 : a2) = suc a) \/ E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. n nth n (a1 : a2) = suc a)

54

bitr3

((n = 0 \/ ~n = 0) /\ nth n (a1 : a2) = suc a <-> n = 0 /\ nth n (a1 : a2) = suc a \/ ~n = 0 /\ nth n (a1 : a2) = suc a) ->
  ((n = 0 \/ ~n = 0) /\ nth n (a1 : a2) = suc a <-> nth n (a1 : a2) = suc a) ->
  (n = 0 /\ nth n (a1 : a2) = suc a \/ ~n = 0 /\ nth n (a1 : a2) = suc a <-> nth n (a1 : a2) = suc a)

55

andir

(n = 0 \/ ~n = 0) /\ nth n (a1 : a2) = suc a <-> n = 0 /\ nth n (a1 : a2) = suc a \/ ~n = 0 /\ nth n (a1 : a2) = suc a

56

55

bitr3*

((n = 0 \/ ~n = 0) /\ nth n (a1 : a2) = suc a <-> nth n (a1 : a2) = suc a) ->
  (n = 0 /\ nth n (a1 : a2) = suc a \/ ~n = 0 /\ nth n (a1 : a2) = suc a <-> nth n (a1 : a2) = suc a)

57

bian1

n = 0 \/ ~n = 0 -> ((n = 0 \/ ~n = 0) /\ nth n (a1 : a2) = suc a <-> nth n (a1 : a2) = suc a)

58

em

n = 0 \/ ~n = 0

59

58

bian1*

(n = 0 \/ ~n = 0) /\ nth n (a1 : a2) = suc a <-> nth n (a1 : a2) = suc a

60

55, 59

bitr3*

n = 0 /\ nth n (a1 : a2) = suc a \/ ~n = 0 /\ nth n (a1 : a2) = suc a <-> nth n (a1 : a2) = suc a

61

60

exeqi

E. n (n = 0 /\ nth n (a1 : a2) = suc a \/ ~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. n nth n (a1 : a2) = suc a

62

52, 61

bitr3*

E. n (n = 0 /\ nth n (a1 : a2) = suc a) \/ E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. n nth n (a1 : a2) = suc a

63

bicom

(E. n (n = 0 /\ nth n (a1 : a2) = suc a) <-> a = a1) -> (a = a1 <-> E. n (n = 0 /\ nth n (a1 : a2) = suc a))

64

eqcomb

a1 = a <-> a = a1

65

peano2

suc a1 = suc a <-> a1 = a

66

nthZ

nth 0 (a1 : a2) = suc a1

67

ntheq1

n = 0 -> nth n (a1 : a2) = nth 0 (a1 : a2)

68

66, 67

syl6eq

n = 0 -> nth n (a1 : a2) = suc a1

69

68

eqeq1d

n = 0 -> (nth n (a1 : a2) = suc a <-> suc a1 = suc a)

70

65, 69

syl6bb

n = 0 -> (nth n (a1 : a2) = suc a <-> a1 = a)

71

64, 70

syl6bb

n = 0 -> (nth n (a1 : a2) = suc a <-> a = a1)

72

71

exeqe

E. n (n = 0 /\ nth n (a1 : a2) = suc a) <-> a = a1

73

72

bicom*

a = a1 <-> E. n (n = 0 /\ nth n (a1 : a2) = suc a)

74

73

a1i

(a IN a2 <-> E. n nth n a2 = suc a) -> (a = a1 <-> E. n (n = 0 /\ nth n (a1 : a2) = suc a))

75

bi1

(a IN a2 <-> E. n nth n a2 = suc a <-> (a IN a2 <-> E. n (~n = 0 /\ nth n (a1 : a2) = suc a))) ->
  (a IN a2 <-> E. n nth n a2 = suc a) ->
  (a IN a2 <-> E. n (~n = 0 /\ nth n (a1 : a2) = suc a))

76

bieq2

(E. n nth n a2 = suc a <-> E. n (~n = 0 /\ nth n (a1 : a2) = suc a)) ->
  (a IN a2 <-> E. n nth n a2 = suc a <-> (a IN a2 <-> E. n (~n = 0 /\ nth n (a1 : a2) = suc a)))

77

bitr4

(E. n nth n a2 = suc a <-> E. a3 nth a3 a2 = suc a) ->
  (E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. a3 nth a3 a2 = suc a) ->
  (E. n nth n a2 = suc a <-> E. n (~n = 0 /\ nth n (a1 : a2) = suc a))

78

ntheq1

n = a3 -> nth n a2 = nth a3 a2

79

78

eqeq1d

n = a3 -> (nth n a2 = suc a <-> nth a3 a2 = suc a)

80

79

cbvex

E. n nth n a2 = suc a <-> E. a3 nth a3 a2 = suc a

81

80

bitr4*

(E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. a3 nth a3 a2 = suc a) -> (E. n nth n a2 = suc a <-> E. n (~n = 0 /\ nth n (a1 : a2) = suc a))

82

bitr

(E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. a3 E. n (n = suc a3 /\ nth n (a1 : a2) = suc a)) ->
  (E. a3 E. n (n = suc a3 /\ nth n (a1 : a2) = suc a) <-> E. a3 nth a3 a2 = suc a) ->
  (E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. a3 nth a3 a2 = suc a)

83

exsuc

n != 0 <-> E. a3 n = suc a3

85

84

a1i

nth n (a1 : a2) = suc a -> (~n = 0 <-> E. a3 n = suc a3)

86

85

biexan1a

~n = 0 /\ nth n (a1 : a2) = suc a <-> E. a3 (n = suc a3 /\ nth n (a1 : a2) = suc a)

87

86

biexexi

E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. a3 E. n (n = suc a3 /\ nth n (a1 : a2) = suc a)

88

87

bitr*

(E. a3 E. n (n = suc a3 /\ nth n (a1 : a2) = suc a) <-> E. a3 nth a3 a2 = suc a) -> (E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. a3 nth a3 a2 = suc a)

89

nthS

nth (suc a3) (a1 : a2) = nth a3 a2

90

ntheq1

n = suc a3 -> nth n (a1 : a2) = nth (suc a3) (a1 : a2)

91

89, 90

syl6eq

n = suc a3 -> nth n (a1 : a2) = nth a3 a2

92

91

eqeq1d

n = suc a3 -> (nth n (a1 : a2) = suc a <-> nth a3 a2 = suc a)

93

92

exeqe

E. n (n = suc a3 /\ nth n (a1 : a2) = suc a) <-> nth a3 a2 = suc a

94

93

exeqi

E. a3 E. n (n = suc a3 /\ nth n (a1 : a2) = suc a) <-> E. a3 nth a3 a2 = suc a

95

87, 94

bitr*

E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. a3 nth a3 a2 = suc a

96

80, 95

bitr4*

E. n nth n a2 = suc a <-> E. n (~n = 0 /\ nth n (a1 : a2) = suc a)

97

96

bieq2*

a IN a2 <-> E. n nth n a2 = suc a <-> (a IN a2 <-> E. n (~n = 0 /\ nth n (a1 : a2) = suc a))

98

97

bi1*

(a IN a2 <-> E. n nth n a2 = suc a) -> (a IN a2 <-> E. n (~n = 0 /\ nth n (a1 : a2) = suc a))

99

74, 98

oreqd

(a IN a2 <-> E. n nth n a2 = suc a) -> (a = a1 \/ a IN a2 <-> E. n (n = 0 /\ nth n (a1 : a2) = suc a) \/ E. n (~n = 0 /\ nth n (a1 : a2) = suc a))

100

62, 99

syl6bb

(a IN a2 <-> E. n nth n a2 = suc a) -> (a = a1 \/ a IN a2 <-> E. n nth n (a1 : a2) = suc a)

101

50, 100

syl5bb

(a IN a2 <-> E. n nth n a2 = suc a) -> (a IN a1 : a2 <-> E. n nth n (a1 : a2) = suc a)

102

9, 18, 27, 36, 49, 101

listind

a IN l <-> E. n nth n l = suc a

Theorem lmemnth ≪ | index | src | ≫

Axiom use