Theorem zmodb0 ≪ | index | src | ≫ 

theorem zmodb0 (a n: nat): $ b0 a %Z n = a % n $;
StepHypRefExpression
1 zmodeq2 
n = 0 -> b0 a %Z n = b0 a %Z 0
2 zmod02 
b0 a %Z 0 = zabs (b0 a)
3 zabsb0 
zabs (b0 a) = a
4 mod0 
a % 0 = a
5 modeq2 
n = 0 -> a % n = a % 0
6 4, 5 syl6eq 
n = 0 -> a % n = a
7 3, 6 syl6eqr 
n = 0 -> a % n = zabs (b0 a)
8 2, 7 syl6eqr 
n = 0 -> a % n = b0 a %Z 0
9 1, 8 eqtr4d 
n = 0 -> b0 a %Z n = a % n
10 eqmaddn 
mod(n): a + n = a
11 10 conv eqm 
(a + n) % n = a % n
12 modeq1 
zfst (b0 a) + n - zsnd (b0 a) % n = a + n -> (zfst (b0 a) + n - zsnd (b0 a) % n) % n = (a + n) % n
13 eqtr 
zfst (b0 a) + n - zsnd (b0 a) % n = a + n - 0 -> a + n - 0 = a + n -> zfst (b0 a) + n - zsnd (b0 a) % n = a + n
14 subeq 
zfst (b0 a) + n = a + n -> zsnd (b0 a) % n = 0 -> zfst (b0 a) + n - zsnd (b0 a) % n = a + n - 0
15 addeq1 
zfst (b0 a) = a -> zfst (b0 a) + n = a + n
16 zfstb0 
zfst (b0 a) = a
17 15, 16 ax_mp 
zfst (b0 a) + n = a + n
18 14, 17 ax_mp 
zsnd (b0 a) % n = 0 -> zfst (b0 a) + n - zsnd (b0 a) % n = a + n - 0
19 eqtr 
zsnd (b0 a) % n = 0 % n -> 0 % n = 0 -> zsnd (b0 a) % n = 0
20 modeq1 
zsnd (b0 a) = 0 -> zsnd (b0 a) % n = 0 % n
21 zsndb0 
zsnd (b0 a) = 0
22 20, 21 ax_mp 
zsnd (b0 a) % n = 0 % n
23 19, 22 ax_mp 
0 % n = 0 -> zsnd (b0 a) % n = 0
24 mod01 
0 % n = 0
25 23, 24 ax_mp 
zsnd (b0 a) % n = 0
26 18, 25 ax_mp 
zfst (b0 a) + n - zsnd (b0 a) % n = a + n - 0
27 13, 26 ax_mp 
a + n - 0 = a + n -> zfst (b0 a) + n - zsnd (b0 a) % n = a + n
28 sub02 
a + n - 0 = a + n
29 27, 28 ax_mp 
zfst (b0 a) + n - zsnd (b0 a) % n = a + n
30 12, 29 ax_mp 
(zfst (b0 a) + n - zsnd (b0 a) % n) % n = (a + n) % n
31 zmodn02 
n != 0 -> b0 a %Z n = (zfst (b0 a) + n - zsnd (b0 a) % n) % n
32 31 conv ne 
~n = 0 -> b0 a %Z n = (zfst (b0 a) + n - zsnd (b0 a) % n) % n
33 30, 32 syl6eq 
~n = 0 -> b0 a %Z n = (a + n) % n
34 11, 33 syl6eq 
~n = 0 -> b0 a %Z n = a % n
35 9, 34 cases 
b0 a %Z n = a % 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)