Theorem lmemlt ≪ | index | src | ≫ 

theorem lmemlt (a l: nat): $ a IN l -> a < l $;
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 1, 2 lteqd 
_1 = l -> (a < _1 <-> a < l)
5 3, 4 imeqd 
_1 = l -> (a IN _1 -> a < _1 <-> a IN l -> a < l)
6 eqidd 
_1 = 0 -> a = a
7 id 
_1 = 0 -> _1 = 0
8 6, 7 lmemeqd 
_1 = 0 -> (a IN _1 <-> a IN 0)
9 6, 7 lteqd 
_1 = 0 -> (a < _1 <-> a < 0)
10 8, 9 imeqd 
_1 = 0 -> (a IN _1 -> a < _1 <-> a IN 0 -> a < 0)
11 eqidd 
_1 = a2 -> a = a
12 id 
_1 = a2 -> _1 = a2
13 11, 12 lmemeqd 
_1 = a2 -> (a IN _1 <-> a IN a2)
14 11, 12 lteqd 
_1 = a2 -> (a < _1 <-> a < a2)
15 13, 14 imeqd 
_1 = a2 -> (a IN _1 -> a < _1 <-> a IN a2 -> a < a2)
16 eqidd 
_1 = a1 : a2 -> a = a
17 id 
_1 = a1 : a2 -> _1 = a1 : a2
18 16, 17 lmemeqd 
_1 = a1 : a2 -> (a IN _1 <-> a IN a1 : a2)
19 16, 17 lteqd 
_1 = a1 : a2 -> (a < _1 <-> a < a1 : a2)
20 18, 19 imeqd 
_1 = a1 : a2 -> (a IN _1 -> a < _1 <-> a IN a1 : a2 -> a < a1 : a2)
21 absurd 
~a IN 0 -> a IN 0 -> a < 0
22 lmem0 
~a IN 0
23 21, 22 ax_mp 
a IN 0 -> a < 0
24 lmemS 
a IN a1 : a2 <-> a = a1 \/ a IN a2
25 ltconsid1 
a1 < a1 : a2
26 lteq1 
a = a1 -> (a < a1 : a2 <-> a1 < a1 : a2)
27 25, 26 mpbiri 
a = a1 -> a < a1 : a2
28 27 a1i 
(a IN a2 -> a < a2) -> a = a1 -> a < a1 : a2
29 ltconsid2 
a2 < a1 : a2
30 lttr 
a < a2 -> a2 < a1 : a2 -> a < a1 : a2
31 29, 30 mpi 
a < a2 -> a < a1 : a2
32 31 imim2i 
(a IN a2 -> a < a2) -> a IN a2 -> a < a1 : a2
33 28, 32 eord 
(a IN a2 -> a < a2) -> a = a1 \/ a IN a2 -> a < a1 : a2
34 24, 33 syl5bi 
(a IN a2 -> a < a2) -> a IN a1 : a2 -> a < a1 : a2
35 5, 10, 15, 20, 23, 34 listind 
a IN l -> a < l

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)