Theorem znegb1 | index | src |

theorem znegb1 (n: nat): $ -uZ b1 n = b0 (suc n) $;
StepHypRefExpression
1 eqtr
-uZ b1 n = b0 (zsnd (b1 n) - zfst (b1 n)) -> b0 (zsnd (b1 n) - zfst (b1 n)) = b0 (suc n) -> -uZ b1 n = b0 (suc n)
2 znsubpos
zfst (b1 n) <= zsnd (b1 n) -> zsnd (b1 n) -ZN zfst (b1 n) = b0 (zsnd (b1 n) - zfst (b1 n))
3 2 conv zneg
zfst (b1 n) <= zsnd (b1 n) -> -uZ b1 n = b0 (zsnd (b1 n) - zfst (b1 n))
4 leeq1
zfst (b1 n) = 0 -> (zfst (b1 n) <= zsnd (b1 n) <-> 0 <= zsnd (b1 n))
5 zfstb1
zfst (b1 n) = 0
6 4, 5 ax_mp
zfst (b1 n) <= zsnd (b1 n) <-> 0 <= zsnd (b1 n)
7 le01
0 <= zsnd (b1 n)
8 6, 7 mpbir
zfst (b1 n) <= zsnd (b1 n)
9 3, 8 ax_mp
-uZ b1 n = b0 (zsnd (b1 n) - zfst (b1 n))
10 1, 9 ax_mp
b0 (zsnd (b1 n) - zfst (b1 n)) = b0 (suc n) -> -uZ b1 n = b0 (suc n)
11 b0eq
zsnd (b1 n) - zfst (b1 n) = suc n -> b0 (zsnd (b1 n) - zfst (b1 n)) = b0 (suc n)
12 eqtr
zsnd (b1 n) - zfst (b1 n) = suc n - 0 -> suc n - 0 = suc n -> zsnd (b1 n) - zfst (b1 n) = suc n
13 subeq
zsnd (b1 n) = suc n -> zfst (b1 n) = 0 -> zsnd (b1 n) - zfst (b1 n) = suc n - 0
14 zsndb1
zsnd (b1 n) = suc n
15 13, 14 ax_mp
zfst (b1 n) = 0 -> zsnd (b1 n) - zfst (b1 n) = suc n - 0
16 15, 5 ax_mp
zsnd (b1 n) - zfst (b1 n) = suc n - 0
17 12, 16 ax_mp
suc n - 0 = suc n -> zsnd (b1 n) - zfst (b1 n) = suc n
18 sub02
suc n - 0 = suc n
19 17, 18 ax_mp
zsnd (b1 n) - zfst (b1 n) = suc n
20 11, 19 ax_mp
b0 (zsnd (b1 n) - zfst (b1 n)) = b0 (suc n)
21 10, 20 ax_mp
-uZ b1 n = b0 (suc n)

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)