Theorem lmemnth ≪ | index | src | ≫ 

theorem lmemnth (a l: nat) {n: nat}: $ a IN l <-> E. n nth n l = suc a $;
StepHypRefExpression
1 id 
_1 = l -> _1 = l
2 1 lmemeq2d 
_1 = l -> (a IN _1 <-> a IN l)
3 1 ntheq2d 
_1 = l -> nth n _1 = nth n l
4 3 eqeq1d 
_1 = l -> (nth n _1 = suc a <-> nth n l = suc a)
5 4 exeqd 
_1 = l -> (E. n nth n _1 = suc a <-> E. n nth n l = suc a)
6 2, 5 bieqd 
_1 = l -> (a IN _1 <-> E. n nth n _1 = suc a <-> (a IN l <-> E. n nth n l = suc a))
7 id 
_1 = 0 -> _1 = 0
8 7 lmemeq2d 
_1 = 0 -> (a IN _1 <-> a IN 0)
9 7 ntheq2d 
_1 = 0 -> nth n _1 = nth n 0
10 9 eqeq1d 
_1 = 0 -> (nth n _1 = suc a <-> nth n 0 = suc a)
11 10 exeqd 
_1 = 0 -> (E. n nth n _1 = suc a <-> E. n nth n 0 = suc a)
12 8, 11 bieqd 
_1 = 0 -> (a IN _1 <-> E. n nth n _1 = suc a <-> (a IN 0 <-> E. n nth n 0 = suc a))
13 id 
_1 = a2 -> _1 = a2
14 13 lmemeq2d 
_1 = a2 -> (a IN _1 <-> a IN a2)
15 13 ntheq2d 
_1 = a2 -> nth n _1 = nth n a2
16 15 eqeq1d 
_1 = a2 -> (nth n _1 = suc a <-> nth n a2 = suc a)
17 16 exeqd 
_1 = a2 -> (E. n nth n _1 = suc a <-> E. n nth n a2 = suc a)
18 14, 17 bieqd 
_1 = a2 -> (a IN _1 <-> E. n nth n _1 = suc a <-> (a IN a2 <-> E. n nth n a2 = suc a))
19 id 
_1 = a1 : a2 -> _1 = a1 : a2
20 19 lmemeq2d 
_1 = a1 : a2 -> (a IN _1 <-> a IN a1 : a2)
21 19 ntheq2d 
_1 = a1 : a2 -> nth n _1 = nth n (a1 : a2)
22 21 eqeq1d 
_1 = a1 : a2 -> (nth n _1 = suc a <-> nth n (a1 : a2) = suc a)
23 22 exeqd 
_1 = a1 : a2 -> (E. n nth n _1 = suc a <-> E. n nth n (a1 : a2) = suc a)
24 20, 23 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))
25 binth 
~a IN 0 -> ~E. n nth n 0 = suc a -> (a IN 0 <-> E. n nth n 0 = suc a)
26 lmem0 
~a IN 0
27 25, 26 ax_mp 
~E. n nth n 0 = suc a -> (a IN 0 <-> E. n nth n 0 = suc a)
28 necom 
suc a != nth n 0 -> nth n 0 != suc a
29 28 conv ne 
suc a != nth n 0 -> ~nth n 0 = suc a
30 neeq2 
nth n 0 = 0 -> (suc a != nth n 0 <-> suc a != 0)
31 nth0 
nth n 0 = 0
32 30, 31 ax_mp 
suc a != nth n 0 <-> suc a != 0
33 peano1 
suc a != 0
34 32, 33 mpbir 
suc a != nth n 0
35 29, 34 ax_mp 
~nth n 0 = suc a
36 35 nexi 
~E. n nth n 0 = suc a
37 27, 36 ax_mp 
a IN 0 <-> E. n nth n 0 = suc a
38 lmemS 
a IN a1 : a2 <-> a = a1 \/ a IN a2
39 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)
40 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)
41 39, 40 ax_mp 
(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)
42 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)
43 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
44 42, 43 ax_mp 
((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)
45 bian1 
n = 0 \/ ~n = 0 -> ((n = 0 \/ ~n = 0) /\ nth n (a1 : a2) = suc a <-> nth n (a1 : a2) = suc a)
46 em 
n = 0 \/ ~n = 0
47 45, 46 ax_mp 
(n = 0 \/ ~n = 0) /\ nth n (a1 : a2) = suc a <-> nth n (a1 : a2) = suc a
48 44, 47 ax_mp 
n = 0 /\ nth n (a1 : a2) = suc a \/ ~n = 0 /\ nth n (a1 : a2) = suc a <-> nth n (a1 : a2) = suc a
49 48 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
50 41, 49 ax_mp 
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
51 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))
52 eqcomb 
a1 = a <-> a = a1
53 peano2 
suc a1 = suc a <-> a1 = a
54 nthZ 
nth 0 (a1 : a2) = suc a1
55 ntheq1 
n = 0 -> nth n (a1 : a2) = nth 0 (a1 : a2)
56 54, 55 syl6eq 
n = 0 -> nth n (a1 : a2) = suc a1
57 56 eqeq1d 
n = 0 -> (nth n (a1 : a2) = suc a <-> suc a1 = suc a)
58 53, 57 syl6bb 
n = 0 -> (nth n (a1 : a2) = suc a <-> a1 = a)
59 52, 58 syl6bb 
n = 0 -> (nth n (a1 : a2) = suc a <-> a = a1)
60 59 exeqe 
E. n (n = 0 /\ nth n (a1 : a2) = suc a) <-> a = a1
61 51, 60 ax_mp 
a = a1 <-> E. n (n = 0 /\ nth n (a1 : a2) = suc a)
62 61 a1i 
(a IN a2 <-> E. n nth n a2 = suc a) -> (a = a1 <-> E. n (n = 0 /\ nth n (a1 : a2) = suc a))
63 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))
64 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)))
65 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))
66 ntheq1 
n = a3 -> nth n a2 = nth a3 a2
67 66 eqeq1d 
n = a3 -> (nth n a2 = suc a <-> nth a3 a2 = suc a)
68 67 cbvex 
E. n nth n a2 = suc a <-> E. a3 nth a3 a2 = suc a
69 65, 68 ax_mp 
(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))
70 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)
71 exsuc 
n != 0 <-> E. a3 n = suc a3
72 71 conv ne 
~n = 0 <-> E. a3 n = suc a3
73 72 a1i 
nth n (a1 : a2) = suc a -> (~n = 0 <-> E. a3 n = suc a3)
74 73 biexan1a 
~n = 0 /\ nth n (a1 : a2) = suc a <-> E. a3 (n = suc a3 /\ nth n (a1 : a2) = suc a)
75 74 biexexi 
E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. a3 E. n (n = suc a3 /\ nth n (a1 : a2) = suc a)
76 70, 75 ax_mp 
(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)
77 nthS 
nth (suc a3) (a1 : a2) = nth a3 a2
78 ntheq1 
n = suc a3 -> nth n (a1 : a2) = nth (suc a3) (a1 : a2)
79 77, 78 syl6eq 
n = suc a3 -> nth n (a1 : a2) = nth a3 a2
80 79 eqeq1d 
n = suc a3 -> (nth n (a1 : a2) = suc a <-> nth a3 a2 = suc a)
81 80 exeqe 
E. n (n = suc a3 /\ nth n (a1 : a2) = suc a) <-> nth a3 a2 = suc a
82 81 exeqi 
E. a3 E. n (n = suc a3 /\ nth n (a1 : a2) = suc a) <-> E. a3 nth a3 a2 = suc a
83 76, 82 ax_mp 
E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. a3 nth a3 a2 = suc a
84 69, 83 ax_mp 
E. n nth n a2 = suc a <-> E. n (~n = 0 /\ nth n (a1 : a2) = suc a)
85 64, 84 ax_mp 
a IN a2 <-> E. n nth n a2 = suc a <-> (a IN a2 <-> E. n (~n = 0 /\ nth n (a1 : a2) = suc a))
86 63, 85 ax_mp 
(a IN a2 <-> E. n nth n a2 = suc a) -> (a IN a2 <-> E. n (~n = 0 /\ nth n (a1 : a2) = suc a))
87 62, 86 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))
88 50, 87 syl6bb 
(a IN a2 <-> E. n nth n a2 = suc a) -> (a = a1 \/ a IN a2 <-> E. n nth n (a1 : a2) = suc a)
89 38, 88 syl5bb 
(a IN a2 <-> E. n nth n a2 = suc a) -> (a IN a1 : a2 <-> E. n nth n (a1 : a2) = suc a)
90 6, 12, 18, 24, 37, 89 listind 
a IN l <-> E. n nth n l = suc a

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)