Theorem zmod02 ≪ | index | src | ≫ 

theorem zmod02 (a: nat): $ a %Z 0 = zabs a $;
StepHypRefExpression
1 eqtr 
a %Z 0 = zabs a % 0 -> zabs a % 0 = zabs a -> a %Z 0 = zabs a
2 modeq1 
zabs (zfst a + 0 -ZN zsnd a % 0) = zabs a -> zabs (zfst a + 0 -ZN zsnd a % 0) % 0 = zabs a % 0
3 2 conv zmod 
zabs (zfst a + 0 -ZN zsnd a % 0) = zabs a -> a %Z 0 = zabs a % 0
4 zabseq 
zfst a + 0 -ZN zsnd a % 0 = a -> zabs (zfst a + 0 -ZN zsnd a % 0) = zabs a
5 eqtr 
zfst a + 0 -ZN zsnd a % 0 = zfst a -ZN zsnd a -> zfst a -ZN zsnd a = a -> zfst a + 0 -ZN zsnd a % 0 = a
6 znsubeq 
zfst a + 0 = zfst a -> zsnd a % 0 = zsnd a -> zfst a + 0 -ZN zsnd a % 0 = zfst a -ZN zsnd a
7 add02 
zfst a + 0 = zfst a
8 6, 7 ax_mp 
zsnd a % 0 = zsnd a -> zfst a + 0 -ZN zsnd a % 0 = zfst a -ZN zsnd a
9 mod0 
zsnd a % 0 = zsnd a
10 8, 9 ax_mp 
zfst a + 0 -ZN zsnd a % 0 = zfst a -ZN zsnd a
11 5, 10 ax_mp 
zfst a -ZN zsnd a = a -> zfst a + 0 -ZN zsnd a % 0 = a
12 zfstsnd 
zfst a -ZN zsnd a = a
13 11, 12 ax_mp 
zfst a + 0 -ZN zsnd a % 0 = a
14 4, 13 ax_mp 
zabs (zfst a + 0 -ZN zsnd a % 0) = zabs a
15 3, 14 ax_mp 
a %Z 0 = zabs a % 0
16 1, 15 ax_mp 
zabs a % 0 = zabs a -> a %Z 0 = zabs a
17 mod0 
zabs a % 0 = zabs a
18 16, 17 ax_mp 
a %Z 0 = zabs a

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)