Theorem ltappendid2 ≪ | index | src | ≫ 

theorem ltappendid2 (a b: nat): $ b != 0 <-> a < b ++ a $;
StepHypRefExpression
1 excons 
b != 0 <-> E. a1 E. a2 b = a1 : a2
2 lelttr 
a <= a2 ++ a -> a2 ++ a < a1 : (a2 ++ a) -> a < a1 : (a2 ++ a)
3 leappendid2 
a <= a2 ++ a
4 2, 3 ax_mp 
a2 ++ a < a1 : (a2 ++ a) -> a < a1 : (a2 ++ a)
5 ltconsid2 
a2 ++ a < a1 : (a2 ++ a)
6 4, 5 ax_mp 
a < a1 : (a2 ++ a)
7 appendS 
a1 : a2 ++ a = a1 : (a2 ++ a)
8 appendeq1 
b = a1 : a2 -> b ++ a = a1 : a2 ++ a
9 7, 8 syl6eq 
b = a1 : a2 -> b ++ a = a1 : (a2 ++ a)
10 9 lteq2d 
b = a1 : a2 -> (a < b ++ a <-> a < a1 : (a2 ++ a))
11 6, 10 mpbiri 
b = a1 : a2 -> a < b ++ a
12 11 eex 
E. a2 b = a1 : a2 -> a < b ++ a
13 12 eex 
E. a1 E. a2 b = a1 : a2 -> a < b ++ a
14 1, 13 sylbi 
b != 0 -> a < b ++ a
15 ltne 
a < b ++ a -> a != b ++ a
16 con3 
(b = 0 -> a = b ++ a) -> ~a = b ++ a -> ~b = 0
17 16 conv ne 
(b = 0 -> a = b ++ a) -> a != b ++ a -> b != 0
18 append0 
0 ++ a = a
19 appendeq1 
b = 0 -> b ++ a = 0 ++ a
20 18, 19 syl6eq 
b = 0 -> b ++ a = a
21 20 eqcomd 
b = 0 -> a = b ++ a
22 17, 21 ax_mp 
a != b ++ a -> b != 0
23 15, 22 rsyl 
a < b ++ a -> b != 0
24 14, 23 ibii 
b != 0 <-> a < b ++ 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)