Metamath Proof Explorer

Theorem modmulconst

Description: Constant multiplication in a modulo operation, see theorem 5.3 in ApostolNT p. 108. (Contributed by AV, 21-Jul-2021)

Ref Expression
Assertion modmulconst ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) ∧ 𝑀 ∈ ℕ ) → ( ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ↔ ( ( 𝐶 · 𝐴 ) mod ( 𝐶 · 𝑀 ) ) = ( ( 𝐶 · 𝐵 ) mod ( 𝐶 · 𝑀 ) ) ) )

Proof

Step Hyp Ref Expression
1 nnz ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℤ )
2 1 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) ∧ 𝑀 ∈ ℕ ) → 𝑀 ∈ ℤ )
3 zsubcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 − 𝐵 ) ∈ ℤ )
4 3 3adant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( 𝐴 − 𝐵 ) ∈ ℤ )
5 4 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) ∧ 𝑀 ∈ ℕ ) → ( 𝐴 − 𝐵 ) ∈ ℤ )
6 nnz ⊢ ( 𝐶 ∈ ℕ → 𝐶 ∈ ℤ )
7 nnne0 ⊢ ( 𝐶 ∈ ℕ → 𝐶 ≠ 0 )
8 6 7 jca ⊢ ( 𝐶 ∈ ℕ → ( 𝐶 ∈ ℤ ∧ 𝐶 ≠ 0 ) )
9 8 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 ∈ ℤ ∧ 𝐶 ≠ 0 ) )
10 9 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) ∧ 𝑀 ∈ ℕ ) → ( 𝐶 ∈ ℤ ∧ 𝐶 ≠ 0 ) )
11 dvdscmulr ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝐴 − 𝐵 ) ∈ ℤ ∧ ( 𝐶 ∈ ℤ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐶 · 𝑀 ) ∥ ( 𝐶 · ( 𝐴 − 𝐵 ) ) ↔ 𝑀 ∥ ( 𝐴 − 𝐵 ) ) )
12 11 bicomd ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝐴 − 𝐵 ) ∈ ℤ ∧ ( 𝐶 ∈ ℤ ∧ 𝐶 ≠ 0 ) ) → ( 𝑀 ∥ ( 𝐴 − 𝐵 ) ↔ ( 𝐶 · 𝑀 ) ∥ ( 𝐶 · ( 𝐴 − 𝐵 ) ) ) )
13 2 5 10 12 syl3anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) ∧ 𝑀 ∈ ℕ ) → ( 𝑀 ∥ ( 𝐴 − 𝐵 ) ↔ ( 𝐶 · 𝑀 ) ∥ ( 𝐶 · ( 𝐴 − 𝐵 ) ) ) )
14 zcn ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
15 zcn ⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℂ )
16 nncn ⊢ ( 𝐶 ∈ ℕ → 𝐶 ∈ ℂ )
17 14 15 16 3anim123i ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) )
18 3anrot ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ↔ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) )
19 17 18 sylibr ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) )
20 subdi ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐶 · ( 𝐴 − 𝐵 ) ) = ( ( 𝐶 · 𝐴 ) − ( 𝐶 · 𝐵 ) ) )
21 19 20 syl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 · ( 𝐴 − 𝐵 ) ) = ( ( 𝐶 · 𝐴 ) − ( 𝐶 · 𝐵 ) ) )
22 21 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) ∧ 𝑀 ∈ ℕ ) → ( 𝐶 · ( 𝐴 − 𝐵 ) ) = ( ( 𝐶 · 𝐴 ) − ( 𝐶 · 𝐵 ) ) )
23 22 breq2d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) ∧ 𝑀 ∈ ℕ ) → ( ( 𝐶 · 𝑀 ) ∥ ( 𝐶 · ( 𝐴 − 𝐵 ) ) ↔ ( 𝐶 · 𝑀 ) ∥ ( ( 𝐶 · 𝐴 ) − ( 𝐶 · 𝐵 ) ) ) )
24 13 23 bitrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) ∧ 𝑀 ∈ ℕ ) → ( 𝑀 ∥ ( 𝐴 − 𝐵 ) ↔ ( 𝐶 · 𝑀 ) ∥ ( ( 𝐶 · 𝐴 ) − ( 𝐶 · 𝐵 ) ) ) )
25 simpr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) ∧ 𝑀 ∈ ℕ ) → 𝑀 ∈ ℕ )
26 simp1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → 𝐴 ∈ ℤ )
27 26 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) ∧ 𝑀 ∈ ℕ ) → 𝐴 ∈ ℤ )
28 simp2 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → 𝐵 ∈ ℤ )
29 28 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) ∧ 𝑀 ∈ ℕ ) → 𝐵 ∈ ℤ )
30 moddvds ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ↔ 𝑀 ∥ ( 𝐴 − 𝐵 ) ) )
31 25 27 29 30 syl3anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) ∧ 𝑀 ∈ ℕ ) → ( ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ↔ 𝑀 ∥ ( 𝐴 − 𝐵 ) ) )
32 simpl3 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) ∧ 𝑀 ∈ ℕ ) → 𝐶 ∈ ℕ )
33 32 25 nnmulcld ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) ∧ 𝑀 ∈ ℕ ) → ( 𝐶 · 𝑀 ) ∈ ℕ )
34 6 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → 𝐶 ∈ ℤ )
35 34 26 zmulcld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 · 𝐴 ) ∈ ℤ )
36 35 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) ∧ 𝑀 ∈ ℕ ) → ( 𝐶 · 𝐴 ) ∈ ℤ )
37 34 28 zmulcld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 · 𝐵 ) ∈ ℤ )
38 37 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) ∧ 𝑀 ∈ ℕ ) → ( 𝐶 · 𝐵 ) ∈ ℤ )
39 moddvds ⊢ ( ( ( 𝐶 · 𝑀 ) ∈ ℕ ∧ ( 𝐶 · 𝐴 ) ∈ ℤ ∧ ( 𝐶 · 𝐵 ) ∈ ℤ ) → ( ( ( 𝐶 · 𝐴 ) mod ( 𝐶 · 𝑀 ) ) = ( ( 𝐶 · 𝐵 ) mod ( 𝐶 · 𝑀 ) ) ↔ ( 𝐶 · 𝑀 ) ∥ ( ( 𝐶 · 𝐴 ) − ( 𝐶 · 𝐵 ) ) ) )
40 33 36 38 39 syl3anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) ∧ 𝑀 ∈ ℕ ) → ( ( ( 𝐶 · 𝐴 ) mod ( 𝐶 · 𝑀 ) ) = ( ( 𝐶 · 𝐵 ) mod ( 𝐶 · 𝑀 ) ) ↔ ( 𝐶 · 𝑀 ) ∥ ( ( 𝐶 · 𝐴 ) − ( 𝐶 · 𝐵 ) ) ) )
41 24 31 40 3bitr4d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) ∧ 𝑀 ∈ ℕ ) → ( ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ↔ ( ( 𝐶 · 𝐴 ) mod ( 𝐶 · 𝑀 ) ) = ( ( 𝐶 · 𝐵 ) mod ( 𝐶 · 𝑀 ) ) ) )