Theorem zmodeq0 ≪ | index | src | ≫ 

theorem zmodeq0 (a n: nat): $ a %Z n = 0 <-> b0 n |Z a $;
StepHypRefExpression
1 bitr4 
(a %Z n = 0 <-> n || zabs (zfst a + n -ZN zsnd a % n)) -> (b0 n |Z a <-> n || zabs (zfst a + n -ZN zsnd a % n)) -> (a %Z n = 0 <-> b0 n |Z a)
2 modeq0 
zabs (zfst a + n -ZN zsnd a % n) % n = 0 <-> n || zabs (zfst a + n -ZN zsnd a % n)
3 2 conv zmod 
a %Z n = 0 <-> n || zabs (zfst a + n -ZN zsnd a % n)
4 1, 3 ax_mp 
(b0 n |Z a <-> n || zabs (zfst a + n -ZN zsnd a % n)) -> (a %Z n = 0 <-> b0 n |Z a)
5 bitr4 
(b0 n |Z a <-> n || zabs a) -> (n || zabs (zfst a + n -ZN zsnd a % n) <-> n || zabs a) -> (b0 n |Z a <-> n || zabs (zfst a + n -ZN zsnd a % n))
6 zdvdb01 
b0 n |Z a <-> n || zabs a
7 5, 6 ax_mp 
(n || zabs (zfst a + n -ZN zsnd a % n) <-> n || zabs a) -> (b0 n |Z a <-> n || zabs (zfst a + n -ZN zsnd a % n))
8 eqmdvdsub3 
mod(n): zfst a = zsnd a <-> n || zabs a
9 eqmdvdsub2 
mod(n): zsnd a % n = zfst a + n <-> n || zabs (zfst a + n -ZN zsnd a % n)
10 eqmcomb 
mod(n): zsnd a = zfst a <-> mod(n): zfst a = zsnd a
11 eqmmod 
mod(n): zsnd a % n = zsnd a
12 11 a1i 
T. -> mod(n): zsnd a % n = zsnd a
13 eqmaddn 
mod(n): zfst a + n = zfst a
14 13 a1i 
T. -> mod(n): zfst a + n = zfst a
15 12, 14 eqmeqm23d 
T. -> (mod(n): zsnd a % n = zfst a + n <-> mod(n): zsnd a = zfst a)
16 10, 15 syl6bb 
T. -> (mod(n): zsnd a % n = zfst a + n <-> mod(n): zfst a = zsnd a)
17 9, 16 syl5bbr 
T. -> (n || zabs (zfst a + n -ZN zsnd a % n) <-> mod(n): zfst a = zsnd a)
18 8, 17 syl6bb 
T. -> (n || zabs (zfst a + n -ZN zsnd a % n) <-> n || zabs a)
19 18 trud 
n || zabs (zfst a + n -ZN zsnd a % n) <-> n || zabs a
20 7, 19 ax_mp 
b0 n |Z a <-> n || zabs (zfst a + n -ZN zsnd a % n)
21 4, 20 ax_mp 
a %Z n = 0 <-> b0 n |Z 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)