Theorem lmemnth | index | src |

theorem lmemnth (a l: nat) {n: nat}: $ a IN l <-> E. n nth n l = suc a $;
StepHypRefExpression
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 37, 38 ax_mp
~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 42, 43 ax_mp
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 39, 48 ax_mp
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 51, 52 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)
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 54, 55 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)
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 57, 58 ax_mp
(n = 0 \/ ~n = 0) /\ nth n (a1 : a2) = suc a <-> nth n (a1 : a2) = suc a
60 56, 59 ax_mp
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 53, 61 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
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 63, 72 ax_mp
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 77, 80 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))
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 82, 87 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)
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 88, 94 ax_mp
E. n (~n = 0 /\ nth n (a1 : a2) = suc a) <-> E. a3 nth a3 a2 = suc a
96 81, 95 ax_mp
E. n nth n a2 = suc a <-> E. n (~n = 0 /\ nth n (a1 : a2) = suc a)
97 76, 96 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))
98 75, 97 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))
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

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)