Theorem ellt ≪ | index | src | ≫ 

pub theorem ellt (a b: nat): $ a e. b -> a < b $;
StepHypRefExpression
1 elnel 
a e. b <-> odd (shr b a)
2 dfodd2 
odd (shr b a) <-> true (shr b a % 2)
3 con1 
(~a < b -> shr b a % 2 = 0) -> ~shr b a % 2 = 0 -> a < b
4 3 conv ne, true 
(~a < b -> shr b a % 2 = 0) -> true (shr b a % 2) -> a < b
5 lenlt 
b <= a <-> ~a < b
6 mod01 
0 % 2 = 0
7 diveq0 
2 ^ a != 0 -> (b // 2 ^ a = 0 <-> b < 2 ^ a)
8 7 conv shr 
2 ^ a != 0 -> (shr b a = 0 <-> b < 2 ^ a)
9 pow2ne0 
2 ^ a != 0
10 8, 9 ax_mp 
shr b a = 0 <-> b < 2 ^ a
11 powltid2 
1 < 2 -> a < 2 ^ a
12 d1lt2 
1 < 2
13 11, 12 ax_mp 
a < 2 ^ a
14 lelttr 
b <= a -> a < 2 ^ a -> b < 2 ^ a
15 13, 14 mpi 
b <= a -> b < 2 ^ a
16 10, 15 sylibr 
b <= a -> shr b a = 0
17 16 modeq1d 
b <= a -> shr b a % 2 = 0 % 2
18 6, 17 syl6eq 
b <= a -> shr b a % 2 = 0
19 5, 18 sylbir 
~a < b -> shr b a % 2 = 0
20 4, 19 ax_mp 
true (shr b a % 2) -> a < b
21 2, 20 sylbi 
odd (shr b a) -> a < b
22 1, 21 sylbi 
a e. b -> a < b

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)