Theorem zfstneg ≪ | index | src | ≫ 

theorem zfstneg (n: nat): $ zfst (-uZ n) = zsnd n $;
StepHypRefExpression
1 eqtr 
zfst (-uZ n) = zfst (-uZ n) -> zfst (-uZ n) = zsnd n -> zfst (-uZ n) = zsnd n
2 zfsteq 
-uZ n = -uZ n -> zfst (-uZ n) = zfst (-uZ n)
3 eqtr3 
-uZ (zfst n -ZN zsnd n) = -uZ n -> -uZ (zfst n -ZN zsnd n) = -uZ n -> -uZ n = -uZ n
4 znegzn 
-uZ (zfst n -ZN zsnd n) = zsnd n -ZN zfst n
5 4 conv zneg 
-uZ (zfst n -ZN zsnd n) = -uZ n
6 3, 5 ax_mp 
-uZ (zfst n -ZN zsnd n) = -uZ n -> -uZ n = -uZ n
7 znegeq 
zfst n -ZN zsnd n = n -> -uZ (zfst n -ZN zsnd n) = -uZ n
8 zfstsnd 
zfst n -ZN zsnd n = n
9 7, 8 ax_mp 
-uZ (zfst n -ZN zsnd n) = -uZ n
10 6, 9 ax_mp 
-uZ n = -uZ n
11 2, 10 ax_mp 
zfst (-uZ n) = zfst (-uZ n)
12 1, 11 ax_mp 
zfst (-uZ n) = zsnd n -> zfst (-uZ n) = zsnd n
13 eqtr 
zfst (-uZ n) = zsnd n - zfst n -> zsnd n - zfst n = zsnd n -> zfst (-uZ n) = zsnd n
14 zfstznsub 
zfst (zsnd n -ZN zfst n) = zsnd n - zfst n
15 14 conv zneg 
zfst (-uZ n) = zsnd n - zfst n
16 13, 15 ax_mp 
zsnd n - zfst n = zsnd n -> zfst (-uZ n) = zsnd n
17 eor 
(zfst n = 0 -> zsnd n - zfst n = zsnd n) -> (zsnd n = 0 -> zsnd n - zfst n = zsnd n) -> zfst n = 0 \/ zsnd n = 0 -> zsnd n - zfst n = zsnd n
18 sub02 
zsnd n - 0 = zsnd n
19 subeq2 
zfst n = 0 -> zsnd n - zfst n = zsnd n - 0
20 18, 19 syl6eq 
zfst n = 0 -> zsnd n - zfst n = zsnd n
21 17, 20 ax_mp 
(zsnd n = 0 -> zsnd n - zfst n = zsnd n) -> zfst n = 0 \/ zsnd n = 0 -> zsnd n - zfst n = zsnd n
22 subeq1 
zsnd n = 0 -> zsnd n - zfst n = 0 - zfst n
23 sub01 
0 - zfst n = 0
24 id 
zsnd n = 0 -> zsnd n = 0
25 23, 24 syl6eqr 
zsnd n = 0 -> zsnd n = 0 - zfst n
26 22, 25 eqtr4d 
zsnd n = 0 -> zsnd n - zfst n = zsnd n
27 21, 26 ax_mp 
zfst n = 0 \/ zsnd n = 0 -> zsnd n - zfst n = zsnd n
28 zfstsnd0 
zfst n = 0 \/ zsnd n = 0
29 27, 28 ax_mp 
zsnd n - zfst n = zsnd n
30 16, 29 ax_mp 
zfst (-uZ n) = zsnd n
31 12, 30 ax_mp 
zfst (-uZ n) = zsnd 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)