Theorem pr0 | index | src |

pub theorem pr0: $ 0, 0 = 0 $;
StepHypRefExpression
1 eqtr
0, 0 = 0 + 0 -> 0 + 0 = 0 -> 0, 0 = 0
2 addeq1
(0 + 0) * suc (0 + 0) // 2 = 0 -> (0 + 0) * suc (0 + 0) // 2 + 0 = 0 + 0
3 2 conv pr
(0 + 0) * suc (0 + 0) // 2 = 0 -> 0, 0 = 0 + 0
4 eqtr
(0 + 0) * suc (0 + 0) // 2 = 0 // 2 -> 0 // 2 = 0 -> (0 + 0) * suc (0 + 0) // 2 = 0
5 diveq1
(0 + 0) * suc (0 + 0) = 0 -> (0 + 0) * suc (0 + 0) // 2 = 0 // 2
6 eqtr
(0 + 0) * suc (0 + 0) = 0 * suc (0 + 0) -> 0 * suc (0 + 0) = 0 -> (0 + 0) * suc (0 + 0) = 0
7 muleq1
0 + 0 = 0 -> (0 + 0) * suc (0 + 0) = 0 * suc (0 + 0)
8 add0
0 + 0 = 0
9 7, 8 ax_mp
(0 + 0) * suc (0 + 0) = 0 * suc (0 + 0)
10 6, 9 ax_mp
0 * suc (0 + 0) = 0 -> (0 + 0) * suc (0 + 0) = 0
11 mul01
0 * suc (0 + 0) = 0
12 10, 11 ax_mp
(0 + 0) * suc (0 + 0) = 0
13 5, 12 ax_mp
(0 + 0) * suc (0 + 0) // 2 = 0 // 2
14 4, 13 ax_mp
0 // 2 = 0 -> (0 + 0) * suc (0 + 0) // 2 = 0
15 div01
0 // 2 = 0
16 14, 15 ax_mp
(0 + 0) * suc (0 + 0) // 2 = 0
17 3, 16 ax_mp
0, 0 = 0 + 0
18 1, 17 ax_mp
0 + 0 = 0 -> 0, 0 = 0
19 18, 8 ax_mp
0, 0 = 0

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)