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 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℕ ∧ M ∈ ℕ → A mod M = B mod M ↔ C ⁢ A mod C ⋅ M = C ⁢ B mod C ⋅ M

Proof

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