Theorem ssle ≪ | index | src | ≫ 

theorem ssle (a b: nat): $ a C_ b -> a <= b $;
StepHypRefExpression
1 leeq 
a % 2 ^ max a b = a -> b % 2 ^ max a b = b -> (a % 2 ^ max a b <= b % 2 ^ max a b <-> a <= b)
2 modlteq 
a < 2 ^ max a b -> a % 2 ^ max a b = a
3 lelttr 
a <= max a b -> max a b < 2 ^ max a b -> a < 2 ^ max a b
4 lemax1 
a <= max a b
5 3, 4 ax_mp 
max a b < 2 ^ max a b -> a < 2 ^ max a b
6 powltid2 
1 < 2 -> max a b < 2 ^ max a b
7 d1lt2 
1 < 2
8 6, 7 ax_mp 
max a b < 2 ^ max a b
9 5, 8 ax_mp 
a < 2 ^ max a b
10 2, 9 ax_mp 
a % 2 ^ max a b = a
11 1, 10 ax_mp 
b % 2 ^ max a b = b -> (a % 2 ^ max a b <= b % 2 ^ max a b <-> a <= b)
12 modlteq 
b < 2 ^ max a b -> b % 2 ^ max a b = b
13 lelttr 
b <= max a b -> max a b < 2 ^ max a b -> b < 2 ^ max a b
14 lemax2 
b <= max a b
15 13, 14 ax_mp 
max a b < 2 ^ max a b -> b < 2 ^ max a b
16 15, 8 ax_mp 
b < 2 ^ max a b
17 12, 16 ax_mp 
b % 2 ^ max a b = b
18 11, 17 ax_mp 
a % 2 ^ max a b <= b % 2 ^ max a b <-> a <= b
19 bndextle 
A. x (x < max a b -> x e. a -> x e. b) -> a % 2 ^ max a b <= b % 2 ^ max a b
20 ax_1 
(x e. a -> x e. b) -> x < max a b -> x e. a -> x e. b
21 20 alimi 
A. x (x e. a -> x e. b) -> A. x (x < max a b -> x e. a -> x e. b)
22 21 conv subset 
a C_ b -> A. x (x < max a b -> x e. a -> x e. b)
23 19, 22 syl 
a C_ b -> a % 2 ^ max a b <= b % 2 ^ max a b
24 18, 23 sylib 
a C_ 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)