Theorem b1ltb0 | index | src |

theorem b1ltb0 (a b: nat): $ b1 a < b0 b <-> a < b $;
StepHypRefExpression
1 bitr
(b1 a < b0 b <-> suc (b1 a) < suc (b0 b)) -> (suc (b1 a) < suc (b0 b) <-> a < b) -> (b1 a < b0 b <-> a < b)
2 ltsuc
b1 a < b0 b <-> suc (b1 a) < suc (b0 b)
3 1, 2 ax_mp
(suc (b1 a) < suc (b0 b) <-> a < b) -> (b1 a < b0 b <-> a < b)
4 bitr
(suc (b1 a) < suc (b0 b) <-> b0 (suc a) < b1 b) -> (b0 (suc a) < b1 b <-> a < b) -> (suc (b1 a) < suc (b0 b) <-> a < b)
5 lteq
suc (b1 a) = b0 (suc a) -> suc (b0 b) = b1 b -> (suc (b1 a) < suc (b0 b) <-> b0 (suc a) < b1 b)
6 sucb1
suc (b1 a) = b0 (suc a)
7 5, 6 ax_mp
suc (b0 b) = b1 b -> (suc (b1 a) < suc (b0 b) <-> b0 (suc a) < b1 b)
8 sucb0
suc (b0 b) = b1 b
9 7, 8 ax_mp
suc (b1 a) < suc (b0 b) <-> b0 (suc a) < b1 b
10 4, 9 ax_mp
(b0 (suc a) < b1 b <-> a < b) -> (suc (b1 a) < suc (b0 b) <-> a < b)
11 b0ltb1
b0 (suc a) < b1 b <-> suc a <= b
12 11 conv lt
b0 (suc a) < b1 b <-> a < b
13 10, 12 ax_mp
suc (b1 a) < suc (b0 b) <-> a < b
14 3, 13 ax_mp
b1 a < b0 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_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)