This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cncongr2

Description: The other direction of the bicondition in cncongr . (Contributed by AV, 11-Jul-2021)

Ref Expression
Assertion cncongr2 ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) → ( ( 𝐴 · 𝐶 ) mod 𝑁 ) = ( ( 𝐵 · 𝐶 ) mod 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 zcn ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
2 1 mul01d ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 · 0 ) = 0 )
3 2 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 · 0 ) = 0 )
4 zcn ⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℂ )
5 4 mul01d ⊢ ( 𝐵 ∈ ℤ → ( 𝐵 · 0 ) = 0 )
6 5 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐵 · 0 ) = 0 )
7 3 6 eqtr4d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 · 0 ) = ( 𝐵 · 0 ) )
8 7 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( 𝐴 · 0 ) = ( 𝐵 · 0 ) )
9 8 oveq1d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( ( 𝐴 · 0 ) mod 𝑁 ) = ( ( 𝐵 · 0 ) mod 𝑁 ) )
10 9 adantr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ) → ( ( 𝐴 · 0 ) mod 𝑁 ) = ( ( 𝐵 · 0 ) mod 𝑁 ) )
11 oveq2 ⊢ ( 𝐶 = 0 → ( 𝐴 · 𝐶 ) = ( 𝐴 · 0 ) )
12 11 oveq1d ⊢ ( 𝐶 = 0 → ( ( 𝐴 · 𝐶 ) mod 𝑁 ) = ( ( 𝐴 · 0 ) mod 𝑁 ) )
13 oveq2 ⊢ ( 𝐶 = 0 → ( 𝐵 · 𝐶 ) = ( 𝐵 · 0 ) )
14 13 oveq1d ⊢ ( 𝐶 = 0 → ( ( 𝐵 · 𝐶 ) mod 𝑁 ) = ( ( 𝐵 · 0 ) mod 𝑁 ) )
15 12 14 eqeq12d ⊢ ( 𝐶 = 0 → ( ( ( 𝐴 · 𝐶 ) mod 𝑁 ) = ( ( 𝐵 · 𝐶 ) mod 𝑁 ) ↔ ( ( 𝐴 · 0 ) mod 𝑁 ) = ( ( 𝐵 · 0 ) mod 𝑁 ) ) )
16 10 15 imbitrrid ⊢ ( 𝐶 = 0 → ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ) → ( ( 𝐴 · 𝐶 ) mod 𝑁 ) = ( ( 𝐵 · 𝐶 ) mod 𝑁 ) ) )
17 oveq2 ⊢ ( 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) → ( 𝐴 mod 𝑀 ) = ( 𝐴 mod ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) )
18 oveq2 ⊢ ( 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) → ( 𝐵 mod 𝑀 ) = ( 𝐵 mod ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) )
19 17 18 eqeq12d ⊢ ( 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) → ( ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ↔ ( 𝐴 mod ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) = ( 𝐵 mod ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) )
20 19 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) → ( ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ↔ ( 𝐴 mod ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) = ( 𝐵 mod ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) )
21 20 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ↔ ( 𝐴 mod ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) = ( 𝐵 mod ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) )
22 simpl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) → 𝑁 ∈ ℕ )
23 simp3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐶 ∈ ℤ )
24 divgcdnnr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐶 ∈ ℤ ) → ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ∈ ℕ )
25 22 23 24 syl2anr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ∈ ℕ )
26 simpl1 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → 𝐴 ∈ ℤ )
27 simpl2 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → 𝐵 ∈ ℤ )
28 moddvds ⊢ ( ( ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 mod ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) = ( 𝐵 mod ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ↔ ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ∥ ( 𝐴 − 𝐵 ) ) )
29 25 26 27 28 syl3anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( ( 𝐴 mod ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) = ( 𝐵 mod ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ↔ ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ∥ ( 𝐴 − 𝐵 ) ) )
30 25 nnzd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ∈ ℤ )
31 zsubcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 − 𝐵 ) ∈ ℤ )
32 31 3adant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 − 𝐵 ) ∈ ℤ )
33 32 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( 𝐴 − 𝐵 ) ∈ ℤ )
34 30 33 jca ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ∈ ℤ ∧ ( 𝐴 − 𝐵 ) ∈ ℤ ) )
35 divides ⊢ ( ( ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ∈ ℤ ∧ ( 𝐴 − 𝐵 ) ∈ ℤ ) → ( ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ∥ ( 𝐴 − 𝐵 ) ↔ ∃ 𝑘 ∈ ℤ ( 𝑘 · ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) = ( 𝐴 − 𝐵 ) ) )
36 34 35 syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ∥ ( 𝐴 − 𝐵 ) ↔ ∃ 𝑘 ∈ ℤ ( 𝑘 · ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) = ( 𝐴 − 𝐵 ) ) )
37 21 29 36 3bitrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ↔ ∃ 𝑘 ∈ ℤ ( 𝑘 · ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) = ( 𝐴 − 𝐵 ) ) )
38 simpr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝐶 ≠ 0 ) ∧ 𝑘 ∈ ℤ ) → 𝑘 ∈ ℤ )
39 30 adantr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝐶 ≠ 0 ) → ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ∈ ℤ )
40 39 adantr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝐶 ≠ 0 ) ∧ 𝑘 ∈ ℤ ) → ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ∈ ℤ )
41 38 40 zmulcld ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝐶 ≠ 0 ) ∧ 𝑘 ∈ ℤ ) → ( 𝑘 · ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ∈ ℤ )
42 41 zcnd ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝐶 ≠ 0 ) ∧ 𝑘 ∈ ℤ ) → ( 𝑘 · ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ∈ ℂ )
43 31 zcnd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
44 43 3adant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
45 44 ad3antrrr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝐶 ≠ 0 ) ∧ 𝑘 ∈ ℤ ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
46 23 zcnd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐶 ∈ ℂ )
47 46 ad3antrrr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝐶 ≠ 0 ) ∧ 𝑘 ∈ ℤ ) → 𝐶 ∈ ℂ )
48 simpr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝐶 ≠ 0 ) → 𝐶 ≠ 0 )
49 48 adantr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝐶 ≠ 0 ) ∧ 𝑘 ∈ ℤ ) → 𝐶 ≠ 0 )
50 42 45 47 49 mulcan2d ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝐶 ≠ 0 ) ∧ 𝑘 ∈ ℤ ) → ( ( ( 𝑘 · ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) · 𝐶 ) = ( ( 𝐴 − 𝐵 ) · 𝐶 ) ↔ ( 𝑘 · ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) = ( 𝐴 − 𝐵 ) ) )
51 zcn ⊢ ( 𝐶 ∈ ℤ → 𝐶 ∈ ℂ )
52 subdir ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 − 𝐵 ) · 𝐶 ) = ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐶 ) ) )
53 1 4 51 52 syl3an ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( ( 𝐴 − 𝐵 ) · 𝐶 ) = ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐶 ) ) )
54 53 ad3antrrr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝐶 ≠ 0 ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝐴 − 𝐵 ) · 𝐶 ) = ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐶 ) ) )
55 54 eqeq2d ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝐶 ≠ 0 ) ∧ 𝑘 ∈ ℤ ) → ( ( ( 𝑘 · ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) · 𝐶 ) = ( ( 𝐴 − 𝐵 ) · 𝐶 ) ↔ ( ( 𝑘 · ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) · 𝐶 ) = ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐶 ) ) ) )
56 50 55 bitr3d ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝐶 ≠ 0 ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝑘 · ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) = ( 𝐴 − 𝐵 ) ↔ ( ( 𝑘 · ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) · 𝐶 ) = ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐶 ) ) ) )
57 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
58 57 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ ) → 𝑁 ∈ ℤ )
59 simpr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ ) → 𝑘 ∈ ℤ )
60 59 zcnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ ) → 𝑘 ∈ ℂ )
61 60 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ ) ) → 𝑘 ∈ ℂ )
62 46 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ ) ) → 𝐶 ∈ ℂ )
63 simpl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ ) → 𝑁 ∈ ℕ )
64 63 nnzd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ ) → 𝑁 ∈ ℤ )
65 23 64 anim12i ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ ) ) → ( 𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
66 gcdcl ⊢ ( ( 𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐶 gcd 𝑁 ) ∈ ℕ0 )
67 65 66 syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ ) ) → ( 𝐶 gcd 𝑁 ) ∈ ℕ0 )
68 67 nn0cnd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ ) ) → ( 𝐶 gcd 𝑁 ) ∈ ℂ )
69 nnne0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
70 69 neneqd ⊢ ( 𝑁 ∈ ℕ → ¬ 𝑁 = 0 )
71 70 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ ) → ¬ 𝑁 = 0 )
72 71 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ ) ) → ¬ 𝑁 = 0 )
73 72 intnand ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ ) ) → ¬ ( 𝐶 = 0 ∧ 𝑁 = 0 ) )
74 gcdeq0 ⊢ ( ( 𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐶 gcd 𝑁 ) = 0 ↔ ( 𝐶 = 0 ∧ 𝑁 = 0 ) ) )
75 65 74 syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝐶 gcd 𝑁 ) = 0 ↔ ( 𝐶 = 0 ∧ 𝑁 = 0 ) ) )
76 75 necon3abid ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝐶 gcd 𝑁 ) ≠ 0 ↔ ¬ ( 𝐶 = 0 ∧ 𝑁 = 0 ) ) )
77 73 76 mpbird ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ ) ) → ( 𝐶 gcd 𝑁 ) ≠ 0 )
78 61 62 68 77 divassd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑘 · 𝐶 ) / ( 𝐶 gcd 𝑁 ) ) = ( 𝑘 · ( 𝐶 / ( 𝐶 gcd 𝑁 ) ) ) )
79 59 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ ) ) → 𝑘 ∈ ℤ )
80 57 69 jca ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) )
81 80 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ ) → ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) )
82 23 81 anim12i ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ ) ) → ( 𝐶 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) )
83 3anass ⊢ ( ( 𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ↔ ( 𝐶 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) )
84 82 83 sylibr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ ) ) → ( 𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) )
85 divgcdz ⊢ ( ( 𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝐶 / ( 𝐶 gcd 𝑁 ) ) ∈ ℤ )
86 84 85 syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ ) ) → ( 𝐶 / ( 𝐶 gcd 𝑁 ) ) ∈ ℤ )
87 79 86 zmulcld ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑘 · ( 𝐶 / ( 𝐶 gcd 𝑁 ) ) ) ∈ ℤ )
88 78 87 eqeltrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑘 · 𝐶 ) / ( 𝐶 gcd 𝑁 ) ) ∈ ℤ )
89 dvdsmul1 ⊢ ( ( 𝑁 ∈ ℤ ∧ ( ( 𝑘 · 𝐶 ) / ( 𝐶 gcd 𝑁 ) ) ∈ ℤ ) → 𝑁 ∥ ( 𝑁 · ( ( 𝑘 · 𝐶 ) / ( 𝐶 gcd 𝑁 ) ) ) )
90 58 88 89 syl2an2 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ ) ) → 𝑁 ∥ ( 𝑁 · ( ( 𝑘 · 𝐶 ) / ( 𝐶 gcd 𝑁 ) ) ) )
91 63 nncnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ ) → 𝑁 ∈ ℂ )
92 91 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ ) ) → 𝑁 ∈ ℂ )
93 divmulasscom ⊢ ( ( ( 𝑘 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( ( 𝐶 gcd 𝑁 ) ∈ ℂ ∧ ( 𝐶 gcd 𝑁 ) ≠ 0 ) ) → ( ( 𝑘 · ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) · 𝐶 ) = ( 𝑁 · ( ( 𝑘 · 𝐶 ) / ( 𝐶 gcd 𝑁 ) ) ) )
94 61 92 62 68 77 93 syl32anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑘 · ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) · 𝐶 ) = ( 𝑁 · ( ( 𝑘 · 𝐶 ) / ( 𝐶 gcd 𝑁 ) ) ) )
95 90 94 breqtrrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ ) ) → 𝑁 ∥ ( ( 𝑘 · ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) · 𝐶 ) )
96 95 exp32 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝑁 ∈ ℕ → ( 𝑘 ∈ ℤ → 𝑁 ∥ ( ( 𝑘 · ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) · 𝐶 ) ) ) )
97 96 adantrd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) → ( 𝑘 ∈ ℤ → 𝑁 ∥ ( ( 𝑘 · ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) · 𝐶 ) ) ) )
98 97 imp ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( 𝑘 ∈ ℤ → 𝑁 ∥ ( ( 𝑘 · ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) · 𝐶 ) ) )
99 98 adantr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝐶 ≠ 0 ) → ( 𝑘 ∈ ℤ → 𝑁 ∥ ( ( 𝑘 · ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) · 𝐶 ) ) )
100 99 imp ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝐶 ≠ 0 ) ∧ 𝑘 ∈ ℤ ) → 𝑁 ∥ ( ( 𝑘 · ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) · 𝐶 ) )
101 breq2 ⊢ ( ( ( 𝑘 · ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) · 𝐶 ) = ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐶 ) ) → ( 𝑁 ∥ ( ( 𝑘 · ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) · 𝐶 ) ↔ 𝑁 ∥ ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐶 ) ) ) )
102 100 101 syl5ibcom ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝐶 ≠ 0 ) ∧ 𝑘 ∈ ℤ ) → ( ( ( 𝑘 · ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) · 𝐶 ) = ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐶 ) ) → 𝑁 ∥ ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐶 ) ) ) )
103 56 102 sylbid ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝐶 ≠ 0 ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝑘 · ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) = ( 𝐴 − 𝐵 ) → 𝑁 ∥ ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐶 ) ) ) )
104 103 rexlimdva ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝐶 ≠ 0 ) → ( ∃ 𝑘 ∈ ℤ ( 𝑘 · ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) = ( 𝐴 − 𝐵 ) → 𝑁 ∥ ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐶 ) ) ) )
105 22 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → 𝑁 ∈ ℕ )
106 zmulcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 · 𝐶 ) ∈ ℤ )
107 106 3adant2 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 · 𝐶 ) ∈ ℤ )
108 107 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( 𝐴 · 𝐶 ) ∈ ℤ )
109 zmulcl ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐵 · 𝐶 ) ∈ ℤ )
110 109 3adant1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐵 · 𝐶 ) ∈ ℤ )
111 110 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( 𝐵 · 𝐶 ) ∈ ℤ )
112 moddvds ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 · 𝐶 ) ∈ ℤ ∧ ( 𝐵 · 𝐶 ) ∈ ℤ ) → ( ( ( 𝐴 · 𝐶 ) mod 𝑁 ) = ( ( 𝐵 · 𝐶 ) mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐶 ) ) ) )
113 105 108 111 112 syl3anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( ( ( 𝐴 · 𝐶 ) mod 𝑁 ) = ( ( 𝐵 · 𝐶 ) mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐶 ) ) ) )
114 113 adantr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝐶 ≠ 0 ) → ( ( ( 𝐴 · 𝐶 ) mod 𝑁 ) = ( ( 𝐵 · 𝐶 ) mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐶 ) ) ) )
115 104 114 sylibrd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝐶 ≠ 0 ) → ( ∃ 𝑘 ∈ ℤ ( 𝑘 · ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) = ( 𝐴 − 𝐵 ) → ( ( 𝐴 · 𝐶 ) mod 𝑁 ) = ( ( 𝐵 · 𝐶 ) mod 𝑁 ) ) )
116 115 ex ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( 𝐶 ≠ 0 → ( ∃ 𝑘 ∈ ℤ ( 𝑘 · ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) = ( 𝐴 − 𝐵 ) → ( ( 𝐴 · 𝐶 ) mod 𝑁 ) = ( ( 𝐵 · 𝐶 ) mod 𝑁 ) ) ) )
117 116 com23 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( ∃ 𝑘 ∈ ℤ ( 𝑘 · ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) = ( 𝐴 − 𝐵 ) → ( 𝐶 ≠ 0 → ( ( 𝐴 · 𝐶 ) mod 𝑁 ) = ( ( 𝐵 · 𝐶 ) mod 𝑁 ) ) ) )
118 37 117 sylbid ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) → ( 𝐶 ≠ 0 → ( ( 𝐴 · 𝐶 ) mod 𝑁 ) = ( ( 𝐵 · 𝐶 ) mod 𝑁 ) ) ) )
119 118 imp ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ) → ( 𝐶 ≠ 0 → ( ( 𝐴 · 𝐶 ) mod 𝑁 ) = ( ( 𝐵 · 𝐶 ) mod 𝑁 ) ) )
120 119 com12 ⊢ ( 𝐶 ≠ 0 → ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ) → ( ( 𝐴 · 𝐶 ) mod 𝑁 ) = ( ( 𝐵 · 𝐶 ) mod 𝑁 ) ) )
121 16 120 pm2.61ine ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ) → ( ( 𝐴 · 𝐶 ) mod 𝑁 ) = ( ( 𝐵 · 𝐶 ) mod 𝑁 ) )
122 121 ex ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) → ( ( 𝐴 · 𝐶 ) mod 𝑁 ) = ( ( 𝐵 · 𝐶 ) mod 𝑁 ) ) )