Theorem modeq0 ≪ | index | src | ≫ 

theorem modeq0 (a n: nat): $ a % n = 0 <-> n || a $;
StepHypRefExpression
1 muleq1 
x = a // n -> x * n = a // n * n
2 1 anwr 
a % n = 0 /\ x = a // n -> x * n = a // n * n
3 mulcom 
a // n * n = n * (a // n)
4 add0 
n * (a // n) + 0 = n * (a // n)
5 addeq2 
a % n = 0 -> n * (a // n) + a % n = n * (a // n) + 0
6 5 anwl 
a % n = 0 /\ x = a // n -> n * (a // n) + a % n = n * (a // n) + 0
7 divmod 
n * (a // n) + a % n = a
8 7 a1i 
a % n = 0 /\ x = a // n -> n * (a // n) + a % n = a
9 6, 8 eqtr3d 
a % n = 0 /\ x = a // n -> n * (a // n) + 0 = a
10 4, 9 syl5eqr 
a % n = 0 /\ x = a // n -> n * (a // n) = a
11 3, 10 syl5eq 
a % n = 0 /\ x = a // n -> a // n * n = a
12 2, 11 eqtrd 
a % n = 0 /\ x = a // n -> x * n = a
13 12 iexde 
a % n = 0 -> E. x x * n = a
14 mulmod2 
x * n % n = 0
15 eqcom 
x * n = a -> a = x * n
16 eqidd 
x * n = a -> n = n
17 15, 16 modeqd 
x * n = a -> a % n = x * n % n
18 14, 17 syl6eq 
x * n = a -> a % n = 0
19 18 eex 
E. x x * n = a -> a % n = 0
20 13, 19 ibii 
a % n = 0 <-> E. x x * n = a
21 20 conv dvd 
a % n = 0 <-> 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)