Theorem letrueb | index | src |

theorem letrueb (a b: nat): $ bool a -> (a <= b <-> true a -> true b) $;
StepHypRefExpression
1 letrue
a <= b -> true a -> true b
2 1 a1i
bool a -> a <= b -> true a -> true b
3 bool01
bool a <-> a = 0 \/ a = 1
4 eor
(a = 0 -> (true a -> true b) -> a <= b) -> (a = 1 -> (true a -> true b) -> a <= b) -> a = 0 \/ a = 1 -> (true a -> true b) -> a <= b
5 le01
0 <= b
6 leeq1
a = 0 -> (a <= b <-> 0 <= b)
7 5, 6 mpbiri
a = 0 -> a <= b
8 7 a1d
a = 0 -> (true a -> true b) -> a <= b
9 4, 8 ax_mp
(a = 1 -> (true a -> true b) -> a <= b) -> a = 0 \/ a = 1 -> (true a -> true b) -> a <= b
10 le11
1 <= b <-> b != 0
11 10 bi2i
b != 0 -> 1 <= b
12 biim1
true a -> (true a -> true b <-> true b)
13 12 conv true
true a -> (true a -> true b <-> b != 0)
14 true1
true 1
15 trueeq
a = 1 -> (true a <-> true 1)
16 14, 15 mpbiri
a = 1 -> true a
17 13, 16 syl
a = 1 -> (true a -> true b <-> b != 0)
18 leeq1
a = 1 -> (a <= b <-> 1 <= b)
19 17, 18 imeqd
a = 1 -> ((true a -> true b) -> a <= b <-> b != 0 -> 1 <= b)
20 11, 19 mpbiri
a = 1 -> (true a -> true b) -> a <= b
21 9, 20 ax_mp
a = 0 \/ a = 1 -> (true a -> true b) -> a <= b
22 3, 21 sylbi
bool a -> (true a -> true b) -> a <= b
23 2, 22 ibid
bool a -> (a <= b <-> true a -> true 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, add0, addS)