Theorem leupto | index | src |

theorem leupto (a b: nat): $ a <= b <-> upto a <= upto b $;
StepHypRefExpression
1 bitr4
(a <= b <-> 2 ^ a <= 2 ^ b) -> (upto a <= upto b <-> 2 ^ a <= 2 ^ b) -> (a <= b <-> upto a <= upto b)
2 lepow2
1 < 2 -> (a <= b <-> 2 ^ a <= 2 ^ b)
3 d1lt2
1 < 2
4 2, 3 ax_mp
a <= b <-> 2 ^ a <= 2 ^ b
5 1, 4 ax_mp
(upto a <= upto b <-> 2 ^ a <= 2 ^ b) -> (a <= b <-> upto a <= upto b)
6 bitr
(upto a <= upto b <-> upto a + 1 <= upto b + 1) -> (upto a + 1 <= upto b + 1 <-> 2 ^ a <= 2 ^ b) -> (upto a <= upto b <-> 2 ^ a <= 2 ^ b)
7 leadd1
upto a <= upto b <-> upto a + 1 <= upto b + 1
8 6, 7 ax_mp
(upto a + 1 <= upto b + 1 <-> 2 ^ a <= 2 ^ b) -> (upto a <= upto b <-> 2 ^ a <= 2 ^ b)
9 leeq
upto a + 1 = 2 ^ a -> upto b + 1 = 2 ^ b -> (upto a + 1 <= upto b + 1 <-> 2 ^ a <= 2 ^ b)
10 uptoadd1
upto a + 1 = 2 ^ a
11 9, 10 ax_mp
upto b + 1 = 2 ^ b -> (upto a + 1 <= upto b + 1 <-> 2 ^ a <= 2 ^ b)
12 uptoadd1
upto b + 1 = 2 ^ b
13 11, 12 ax_mp
upto a + 1 <= upto b + 1 <-> 2 ^ a <= 2 ^ b
14 8, 13 ax_mp
upto a <= upto b <-> 2 ^ a <= 2 ^ b
15 5, 14 ax_mp
a <= b <-> upto a <= upto 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)