Metamath Proof Explorer

Theorem moddvds

Description: Two ways to say A == B (mod N ), see also definition in ApostolNT p. 106. (Contributed by Mario Carneiro, 18-Feb-2014)

Ref Expression
Assertion moddvds ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 mod 𝑁 ) = ( 𝐵 mod 𝑁 ) ↔ 𝑁 ∥ ( 𝐴 − 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 nnrp ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
2 1 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → 𝑁 ∈ ℝ+ )
3 0mod ⊢ ( 𝑁 ∈ ℝ+ → ( 0 mod 𝑁 ) = 0 )
4 2 3 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( 0 mod 𝑁 ) = 0 )
5 4 eqeq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = ( 0 mod 𝑁 ) ↔ ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = 0 ) )
6 zre ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
7 6 ad2antrl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → 𝐴 ∈ ℝ )
8 zre ⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℝ )
9 8 ad2antll ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → 𝐵 ∈ ℝ )
10 9 renegcld ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → - 𝐵 ∈ ℝ )
11 modadd1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( - 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑁 ) = ( 𝐵 mod 𝑁 ) ) → ( ( 𝐴 + - 𝐵 ) mod 𝑁 ) = ( ( 𝐵 + - 𝐵 ) mod 𝑁 ) )
12 11 3expia ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( - 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ) → ( ( 𝐴 mod 𝑁 ) = ( 𝐵 mod 𝑁 ) → ( ( 𝐴 + - 𝐵 ) mod 𝑁 ) = ( ( 𝐵 + - 𝐵 ) mod 𝑁 ) ) )
13 7 9 10 2 12 syl22anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( ( 𝐴 mod 𝑁 ) = ( 𝐵 mod 𝑁 ) → ( ( 𝐴 + - 𝐵 ) mod 𝑁 ) = ( ( 𝐵 + - 𝐵 ) mod 𝑁 ) ) )
14 7 recnd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → 𝐴 ∈ ℂ )
15 9 recnd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → 𝐵 ∈ ℂ )
16 14 15 negsubd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( 𝐴 + - 𝐵 ) = ( 𝐴 − 𝐵 ) )
17 16 oveq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( ( 𝐴 + - 𝐵 ) mod 𝑁 ) = ( ( 𝐴 − 𝐵 ) mod 𝑁 ) )
18 15 negidd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( 𝐵 + - 𝐵 ) = 0 )
19 18 oveq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( ( 𝐵 + - 𝐵 ) mod 𝑁 ) = ( 0 mod 𝑁 ) )
20 17 19 eqeq12d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( ( ( 𝐴 + - 𝐵 ) mod 𝑁 ) = ( ( 𝐵 + - 𝐵 ) mod 𝑁 ) ↔ ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = ( 0 mod 𝑁 ) ) )
21 13 20 sylibd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( ( 𝐴 mod 𝑁 ) = ( 𝐵 mod 𝑁 ) → ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = ( 0 mod 𝑁 ) ) )
22 7 9 resubcld ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( 𝐴 − 𝐵 ) ∈ ℝ )
23 0red ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → 0 ∈ ℝ )
24 modadd1 ⊢ ( ( ( ( 𝐴 − 𝐵 ) ∈ ℝ ∧ 0 ∈ ℝ ) ∧ ( 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ∧ ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = ( 0 mod 𝑁 ) ) → ( ( ( 𝐴 − 𝐵 ) + 𝐵 ) mod 𝑁 ) = ( ( 0 + 𝐵 ) mod 𝑁 ) )
25 24 3expia ⊢ ( ( ( ( 𝐴 − 𝐵 ) ∈ ℝ ∧ 0 ∈ ℝ ) ∧ ( 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ) → ( ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = ( 0 mod 𝑁 ) → ( ( ( 𝐴 − 𝐵 ) + 𝐵 ) mod 𝑁 ) = ( ( 0 + 𝐵 ) mod 𝑁 ) ) )
26 22 23 9 2 25 syl22anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = ( 0 mod 𝑁 ) → ( ( ( 𝐴 − 𝐵 ) + 𝐵 ) mod 𝑁 ) = ( ( 0 + 𝐵 ) mod 𝑁 ) ) )
27 14 15 npcand ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( ( 𝐴 − 𝐵 ) + 𝐵 ) = 𝐴 )
28 27 oveq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( ( ( 𝐴 − 𝐵 ) + 𝐵 ) mod 𝑁 ) = ( 𝐴 mod 𝑁 ) )
29 15 addlidd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( 0 + 𝐵 ) = 𝐵 )
30 29 oveq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( ( 0 + 𝐵 ) mod 𝑁 ) = ( 𝐵 mod 𝑁 ) )
31 28 30 eqeq12d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( ( ( ( 𝐴 − 𝐵 ) + 𝐵 ) mod 𝑁 ) = ( ( 0 + 𝐵 ) mod 𝑁 ) ↔ ( 𝐴 mod 𝑁 ) = ( 𝐵 mod 𝑁 ) ) )
32 26 31 sylibd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = ( 0 mod 𝑁 ) → ( 𝐴 mod 𝑁 ) = ( 𝐵 mod 𝑁 ) ) )
33 21 32 impbid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( ( 𝐴 mod 𝑁 ) = ( 𝐵 mod 𝑁 ) ↔ ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = ( 0 mod 𝑁 ) ) )
34 zsubcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 − 𝐵 ) ∈ ℤ )
35 dvdsval3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 − 𝐵 ) ∈ ℤ ) → ( 𝑁 ∥ ( 𝐴 − 𝐵 ) ↔ ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = 0 ) )
36 34 35 sylan2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( 𝑁 ∥ ( 𝐴 − 𝐵 ) ↔ ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = 0 ) )
37 5 33 36 3bitr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( ( 𝐴 mod 𝑁 ) = ( 𝐵 mod 𝑁 ) ↔ 𝑁 ∥ ( 𝐴 − 𝐵 ) ) )
38 37 3impb ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 mod 𝑁 ) = ( 𝐵 mod 𝑁 ) ↔ 𝑁 ∥ ( 𝐴 − 𝐵 ) ) )