Theorem zeqmmod ≪ | index | src | ≫ 

theorem zeqmmod (a n: nat): $ n != 0 -> modZ(n): b0 (a %Z n) = a $;
StepHypRefExpression
1 zeqmtr 
modZ(n): b0 (a %Z n) = b0 (zabs (zfst a + n -ZN zsnd a % n)) -> modZ(n): b0 (zabs (zfst a + n -ZN zsnd a % n)) = a -> modZ(n): b0 (a %Z n) = a
2 zeqmeqm 
modZ(n): b0 (a %Z n) = b0 (zabs (zfst a + n -ZN zsnd a % n)) <-> mod(n): a %Z n = zabs (zfst a + n -ZN zsnd a % n)
3 eqmmod 
mod(n): zabs (zfst a + n -ZN zsnd a % n) % n = zabs (zfst a + n -ZN zsnd a % n)
4 3 conv zmod 
mod(n): a %Z n = zabs (zfst a + n -ZN zsnd a % n)
5 2, 4 mpbir 
modZ(n): b0 (a %Z n) = b0 (zabs (zfst a + n -ZN zsnd a % n))
6 1, 5 ax_mp 
modZ(n): b0 (zabs (zfst a + n -ZN zsnd a % n)) = a -> modZ(n): b0 (a %Z n) = a
7 b0zabs 
b0 (zabs (zfst a + n -ZN zsnd a % n)) = zfst a + n -ZN zsnd a % n <-> 0 <=Z zfst a + n -ZN zsnd a % n
8 zle0znsub 
0 <=Z zfst a + n -ZN zsnd a % n <-> zsnd a % n <= zfst a + n
9 ltle 
zsnd a % n < n -> zsnd a % n <= n
10 modlt 
n != 0 -> zsnd a % n < n
11 9, 10 syl 
n != 0 -> zsnd a % n <= n
12 leaddid2 
n <= zfst a + n
13 12 a1i 
n != 0 -> n <= zfst a + n
14 11, 13 letrd 
n != 0 -> zsnd a % n <= zfst a + n
15 8, 14 sylibr 
n != 0 -> 0 <=Z zfst a + n -ZN zsnd a % n
16 7, 15 sylibr 
n != 0 -> b0 (zabs (zfst a + n -ZN zsnd a % n)) = zfst a + n -ZN zsnd a % n
17 16 zeqmeq2d 
n != 0 -> (modZ(n): b0 (zabs (zfst a + n -ZN zsnd a % n)) = a <-> modZ(n): zfst a + n -ZN zsnd a % n = a)
18 zeqmeq3 
zfst a -ZN zsnd a = a -> (modZ(n): zfst a + n -ZN zsnd a % n = zfst a -ZN zsnd a <-> modZ(n): zfst a + n -ZN zsnd a % n = a)
19 zfstsnd 
zfst a -ZN zsnd a = a
20 18, 19 ax_mp 
modZ(n): zfst a + n -ZN zsnd a % n = zfst a -ZN zsnd a <-> modZ(n): zfst a + n -ZN zsnd a % n = a
21 eqmaddn 
mod(n): zfst a + n = zfst a
22 21 a1i 
n != 0 -> mod(n): zfst a + n = zfst a
23 eqmmod 
mod(n): zsnd a % n = zsnd a
24 23 a1i 
n != 0 -> mod(n): zsnd a % n = zsnd a
25 22, 24 zeqmznsubd 
n != 0 -> modZ(n): zfst a + n -ZN zsnd a % n = zfst a -ZN zsnd a
26 20, 25 sylib 
n != 0 -> modZ(n): zfst a + n -ZN zsnd a % n = a
27 17, 26 mpbird 
n != 0 -> modZ(n): b0 (zabs (zfst a + n -ZN zsnd a % n)) = a
28 6, 27 syl 
n != 0 -> modZ(n): b0 (a %Z n) = 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)