Metamath Proof Explorer

Theorem cncongr1

Description: One direction of the bicondition in cncongr . Theorem 5.4 in ApostolNT p. 109. (Contributed by AV, 13-Jul-2021)

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

Proof

Step Hyp Ref Expression
1 zmulcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 · 𝐶 ) ∈ ℤ )
2 1 3adant2 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 · 𝐶 ) ∈ ℤ )
3 zmulcl ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐵 · 𝐶 ) ∈ ℤ )
4 3 3adant1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐵 · 𝐶 ) ∈ ℤ )
5 simpl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) → 𝑁 ∈ ℕ )
6 congr ⊢ ( ( ( 𝐴 · 𝐶 ) ∈ ℤ ∧ ( 𝐵 · 𝐶 ) ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 · 𝐶 ) mod 𝑁 ) = ( ( 𝐵 · 𝐶 ) mod 𝑁 ) ↔ ∃ 𝑘 ∈ ℤ ( 𝑘 · 𝑁 ) = ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐶 ) ) ) )
7 2 4 5 6 syl2an3an ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( ( ( 𝐴 · 𝐶 ) mod 𝑁 ) = ( ( 𝐵 · 𝐶 ) mod 𝑁 ) ↔ ∃ 𝑘 ∈ ℤ ( 𝑘 · 𝑁 ) = ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐶 ) ) ) )
8 simpl ⊢ ( ( 𝐶 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝐶 ∈ ℤ )
9 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
10 nnne0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
11 9 10 jca ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) )
12 11 adantl ⊢ ( ( 𝐶 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) )
13 eqidd ⊢ ( ( 𝐶 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐶 gcd 𝑁 ) = ( 𝐶 gcd 𝑁 ) )
14 8 12 13 3jca ⊢ ( ( 𝐶 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐶 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ ( 𝐶 gcd 𝑁 ) = ( 𝐶 gcd 𝑁 ) ) )
15 14 ex ⊢ ( 𝐶 ∈ ℤ → ( 𝑁 ∈ ℕ → ( 𝐶 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ ( 𝐶 gcd 𝑁 ) = ( 𝐶 gcd 𝑁 ) ) ) )
16 15 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝑁 ∈ ℕ → ( 𝐶 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ ( 𝐶 gcd 𝑁 ) = ( 𝐶 gcd 𝑁 ) ) ) )
17 16 com12 ⊢ ( 𝑁 ∈ ℕ → ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐶 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ ( 𝐶 gcd 𝑁 ) = ( 𝐶 gcd 𝑁 ) ) ) )
18 17 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) → ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐶 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ ( 𝐶 gcd 𝑁 ) = ( 𝐶 gcd 𝑁 ) ) ) )
19 18 impcom ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( 𝐶 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ ( 𝐶 gcd 𝑁 ) = ( 𝐶 gcd 𝑁 ) ) )
20 divgcdcoprmex ⊢ ( ( 𝐶 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ∧ ( 𝐶 gcd 𝑁 ) = ( 𝐶 gcd 𝑁 ) ) → ∃ 𝑟 ∈ ℤ ∃ 𝑠 ∈ ℤ ( 𝐶 = ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ∧ 𝑁 = ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) ∧ ( 𝑟 gcd 𝑠 ) = 1 ) )
21 19 20 syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ∃ 𝑟 ∈ ℤ ∃ 𝑠 ∈ ℤ ( 𝐶 = ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ∧ 𝑁 = ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) ∧ ( 𝑟 gcd 𝑠 ) = 1 ) )
22 21 adantr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) → ∃ 𝑟 ∈ ℤ ∃ 𝑠 ∈ ℤ ( 𝐶 = ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ∧ 𝑁 = ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) ∧ ( 𝑟 gcd 𝑠 ) = 1 ) )
23 oveq2 ⊢ ( 𝑁 = ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) → ( 𝑘 · 𝑁 ) = ( 𝑘 · ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) ) )
24 23 3ad2ant2 ⊢ ( ( 𝐶 = ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ∧ 𝑁 = ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) ∧ ( 𝑟 gcd 𝑠 ) = 1 ) → ( 𝑘 · 𝑁 ) = ( 𝑘 · ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) ) )
25 24 adantl ⊢ ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) ∧ ( 𝐶 = ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ∧ 𝑁 = ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) ∧ ( 𝑟 gcd 𝑠 ) = 1 ) ) → ( 𝑘 · 𝑁 ) = ( 𝑘 · ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) ) )
26 oveq2 ⊢ ( 𝐶 = ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) → ( 𝐴 · 𝐶 ) = ( 𝐴 · ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ) )
27 oveq2 ⊢ ( 𝐶 = ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) → ( 𝐵 · 𝐶 ) = ( 𝐵 · ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ) )
28 26 27 oveq12d ⊢ ( 𝐶 = ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) → ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 · ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ) − ( 𝐵 · ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ) ) )
29 28 3ad2ant1 ⊢ ( ( 𝐶 = ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ∧ 𝑁 = ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) ∧ ( 𝑟 gcd 𝑠 ) = 1 ) → ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 · ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ) − ( 𝐵 · ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ) ) )
30 29 adantl ⊢ ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) ∧ ( 𝐶 = ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ∧ 𝑁 = ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) ∧ ( 𝑟 gcd 𝑠 ) = 1 ) ) → ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 · ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ) − ( 𝐵 · ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ) ) )
31 25 30 eqeq12d ⊢ ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) ∧ ( 𝐶 = ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ∧ 𝑁 = ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) ∧ ( 𝑟 gcd 𝑠 ) = 1 ) ) → ( ( 𝑘 · 𝑁 ) = ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐶 ) ) ↔ ( 𝑘 · ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) ) = ( ( 𝐴 · ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ) − ( 𝐵 · ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ) ) ) )
32 simpr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) → 𝑘 ∈ ℤ )
33 32 zcnd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) → 𝑘 ∈ ℂ )
34 33 adantr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → 𝑘 ∈ ℂ )
35 simp3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐶 ∈ ℤ )
36 35 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → 𝐶 ∈ ℤ )
37 9 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) → 𝑁 ∈ ℤ )
38 37 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → 𝑁 ∈ ℤ )
39 36 38 gcdcld ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( 𝐶 gcd 𝑁 ) ∈ ℕ0 )
40 39 nn0cnd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( 𝐶 gcd 𝑁 ) ∈ ℂ )
41 40 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( 𝐶 gcd 𝑁 ) ∈ ℂ )
42 simpr ⊢ ( ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) → 𝑠 ∈ ℤ )
43 42 zcnd ⊢ ( ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) → 𝑠 ∈ ℂ )
44 43 adantl ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → 𝑠 ∈ ℂ )
45 34 41 44 mul12d ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( 𝑘 · ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) ) = ( ( 𝐶 gcd 𝑁 ) · ( 𝑘 · 𝑠 ) ) )
46 simp1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐴 ∈ ℤ )
47 46 zcnd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐴 ∈ ℂ )
48 47 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → 𝐴 ∈ ℂ )
49 48 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → 𝐴 ∈ ℂ )
50 35 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) → 𝐶 ∈ ℤ )
51 5 nnzd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) → 𝑁 ∈ ℤ )
52 51 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → 𝑁 ∈ ℤ )
53 52 adantr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) → 𝑁 ∈ ℤ )
54 50 53 gcdcld ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) → ( 𝐶 gcd 𝑁 ) ∈ ℕ0 )
55 54 nn0cnd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) → ( 𝐶 gcd 𝑁 ) ∈ ℂ )
56 55 adantr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( 𝐶 gcd 𝑁 ) ∈ ℂ )
57 simpl ⊢ ( ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) → 𝑟 ∈ ℤ )
58 57 zcnd ⊢ ( ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) → 𝑟 ∈ ℂ )
59 58 adantl ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → 𝑟 ∈ ℂ )
60 49 56 59 mul12d ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( 𝐴 · ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ) = ( ( 𝐶 gcd 𝑁 ) · ( 𝐴 · 𝑟 ) ) )
61 simp2 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐵 ∈ ℤ )
62 61 zcnd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐵 ∈ ℂ )
63 62 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → 𝐵 ∈ ℂ )
64 63 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → 𝐵 ∈ ℂ )
65 36 52 gcdcld ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( 𝐶 gcd 𝑁 ) ∈ ℕ0 )
66 65 nn0cnd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( 𝐶 gcd 𝑁 ) ∈ ℂ )
67 66 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( 𝐶 gcd 𝑁 ) ∈ ℂ )
68 64 67 59 mul12d ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( 𝐵 · ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ) = ( ( 𝐶 gcd 𝑁 ) · ( 𝐵 · 𝑟 ) ) )
69 60 68 oveq12d ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( ( 𝐴 · ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ) − ( 𝐵 · ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ) ) = ( ( ( 𝐶 gcd 𝑁 ) · ( 𝐴 · 𝑟 ) ) − ( ( 𝐶 gcd 𝑁 ) · ( 𝐵 · 𝑟 ) ) ) )
70 45 69 eqeq12d ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( ( 𝑘 · ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) ) = ( ( 𝐴 · ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ) − ( 𝐵 · ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ) ) ↔ ( ( 𝐶 gcd 𝑁 ) · ( 𝑘 · 𝑠 ) ) = ( ( ( 𝐶 gcd 𝑁 ) · ( 𝐴 · 𝑟 ) ) − ( ( 𝐶 gcd 𝑁 ) · ( 𝐵 · 𝑟 ) ) ) ) )
71 46 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → 𝐴 ∈ ℤ )
72 71 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → 𝐴 ∈ ℤ )
73 57 adantl ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → 𝑟 ∈ ℤ )
74 72 73 zmulcld ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( 𝐴 · 𝑟 ) ∈ ℤ )
75 74 zcnd ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( 𝐴 · 𝑟 ) ∈ ℂ )
76 61 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → 𝐵 ∈ ℤ )
77 76 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → 𝐵 ∈ ℤ )
78 77 73 zmulcld ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( 𝐵 · 𝑟 ) ∈ ℤ )
79 78 zcnd ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( 𝐵 · 𝑟 ) ∈ ℂ )
80 67 75 79 subdid ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( ( 𝐶 gcd 𝑁 ) · ( ( 𝐴 · 𝑟 ) − ( 𝐵 · 𝑟 ) ) ) = ( ( ( 𝐶 gcd 𝑁 ) · ( 𝐴 · 𝑟 ) ) − ( ( 𝐶 gcd 𝑁 ) · ( 𝐵 · 𝑟 ) ) ) )
81 80 eqcomd ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( ( ( 𝐶 gcd 𝑁 ) · ( 𝐴 · 𝑟 ) ) − ( ( 𝐶 gcd 𝑁 ) · ( 𝐵 · 𝑟 ) ) ) = ( ( 𝐶 gcd 𝑁 ) · ( ( 𝐴 · 𝑟 ) − ( 𝐵 · 𝑟 ) ) ) )
82 81 eqeq2d ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( ( ( 𝐶 gcd 𝑁 ) · ( 𝑘 · 𝑠 ) ) = ( ( ( 𝐶 gcd 𝑁 ) · ( 𝐴 · 𝑟 ) ) − ( ( 𝐶 gcd 𝑁 ) · ( 𝐵 · 𝑟 ) ) ) ↔ ( ( 𝐶 gcd 𝑁 ) · ( 𝑘 · 𝑠 ) ) = ( ( 𝐶 gcd 𝑁 ) · ( ( 𝐴 · 𝑟 ) − ( 𝐵 · 𝑟 ) ) ) ) )
83 32 adantr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → 𝑘 ∈ ℤ )
84 42 adantl ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → 𝑠 ∈ ℤ )
85 83 84 zmulcld ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( 𝑘 · 𝑠 ) ∈ ℤ )
86 85 zcnd ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( 𝑘 · 𝑠 ) ∈ ℂ )
87 simpl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐴 ∈ ℤ )
88 87 57 anim12i ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( 𝐴 ∈ ℤ ∧ 𝑟 ∈ ℤ ) )
89 zmulcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑟 ∈ ℤ ) → ( 𝐴 · 𝑟 ) ∈ ℤ )
90 88 89 syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( 𝐴 · 𝑟 ) ∈ ℤ )
91 simpr ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐵 ∈ ℤ )
92 91 57 anim12i ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( 𝐵 ∈ ℤ ∧ 𝑟 ∈ ℤ ) )
93 zmulcl ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝑟 ∈ ℤ ) → ( 𝐵 · 𝑟 ) ∈ ℤ )
94 92 93 syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( 𝐵 · 𝑟 ) ∈ ℤ )
95 90 94 zsubcld ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( ( 𝐴 · 𝑟 ) − ( 𝐵 · 𝑟 ) ) ∈ ℤ )
96 95 zcnd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( ( 𝐴 · 𝑟 ) − ( 𝐵 · 𝑟 ) ) ∈ ℂ )
97 96 ex ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) → ( ( 𝐴 · 𝑟 ) − ( 𝐵 · 𝑟 ) ) ∈ ℂ ) )
98 97 3adant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) → ( ( 𝐴 · 𝑟 ) − ( 𝐵 · 𝑟 ) ) ∈ ℂ ) )
99 98 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) → ( ( 𝐴 · 𝑟 ) − ( 𝐵 · 𝑟 ) ) ∈ ℂ ) )
100 99 imp ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( ( 𝐴 · 𝑟 ) − ( 𝐵 · 𝑟 ) ) ∈ ℂ )
101 10 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) → 𝑁 ≠ 0 )
102 101 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → 𝑁 ≠ 0 )
103 gcd2n0cl ⊢ ( ( 𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝐶 gcd 𝑁 ) ∈ ℕ )
104 36 52 102 103 syl3anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( 𝐶 gcd 𝑁 ) ∈ ℕ )
105 nnne0 ⊢ ( ( 𝐶 gcd 𝑁 ) ∈ ℕ → ( 𝐶 gcd 𝑁 ) ≠ 0 )
106 104 105 syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( 𝐶 gcd 𝑁 ) ≠ 0 )
107 106 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( 𝐶 gcd 𝑁 ) ≠ 0 )
108 86 100 67 107 mulcand ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( ( ( 𝐶 gcd 𝑁 ) · ( 𝑘 · 𝑠 ) ) = ( ( 𝐶 gcd 𝑁 ) · ( ( 𝐴 · 𝑟 ) − ( 𝐵 · 𝑟 ) ) ) ↔ ( 𝑘 · 𝑠 ) = ( ( 𝐴 · 𝑟 ) − ( 𝐵 · 𝑟 ) ) ) )
109 70 82 108 3bitrd ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( ( 𝑘 · ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) ) = ( ( 𝐴 · ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ) − ( 𝐵 · ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ) ) ↔ ( 𝑘 · 𝑠 ) = ( ( 𝐴 · 𝑟 ) − ( 𝐵 · 𝑟 ) ) ) )
110 109 adantr ⊢ ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) ∧ ( 𝐶 = ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ∧ 𝑁 = ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) ∧ ( 𝑟 gcd 𝑠 ) = 1 ) ) → ( ( 𝑘 · ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) ) = ( ( 𝐴 · ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ) − ( 𝐵 · ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ) ) ↔ ( 𝑘 · 𝑠 ) = ( ( 𝐴 · 𝑟 ) − ( 𝐵 · 𝑟 ) ) ) )
111 zcn ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
112 zcn ⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℂ )
113 111 112 anim12i ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) )
114 113 3adant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) )
115 114 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) )
116 115 58 anim12i ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑟 ∈ ℂ ) )
117 df-3an ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑟 ∈ ℂ ) ↔ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑟 ∈ ℂ ) )
118 116 117 sylibr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑟 ∈ ℂ ) )
119 subdir ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑟 ∈ ℂ ) → ( ( 𝐴 − 𝐵 ) · 𝑟 ) = ( ( 𝐴 · 𝑟 ) − ( 𝐵 · 𝑟 ) ) )
120 118 119 syl ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( ( 𝐴 − 𝐵 ) · 𝑟 ) = ( ( 𝐴 · 𝑟 ) − ( 𝐵 · 𝑟 ) ) )
121 120 eqcomd ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( ( 𝐴 · 𝑟 ) − ( 𝐵 · 𝑟 ) ) = ( ( 𝐴 − 𝐵 ) · 𝑟 ) )
122 121 adantr ⊢ ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) ∧ ( 𝐶 = ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ∧ 𝑁 = ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) ∧ ( 𝑟 gcd 𝑠 ) = 1 ) ) → ( ( 𝐴 · 𝑟 ) − ( 𝐵 · 𝑟 ) ) = ( ( 𝐴 − 𝐵 ) · 𝑟 ) )
123 122 eqeq2d ⊢ ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) ∧ ( 𝐶 = ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ∧ 𝑁 = ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) ∧ ( 𝑟 gcd 𝑠 ) = 1 ) ) → ( ( 𝑘 · 𝑠 ) = ( ( 𝐴 · 𝑟 ) − ( 𝐵 · 𝑟 ) ) ↔ ( 𝑘 · 𝑠 ) = ( ( 𝐴 − 𝐵 ) · 𝑟 ) ) )
124 5 nncnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) → 𝑁 ∈ ℂ )
125 124 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → 𝑁 ∈ ℂ )
126 125 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → 𝑁 ∈ ℂ )
127 84 zcnd ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → 𝑠 ∈ ℂ )
128 66 106 jca ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( ( 𝐶 gcd 𝑁 ) ∈ ℂ ∧ ( 𝐶 gcd 𝑁 ) ≠ 0 ) )
129 128 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( ( 𝐶 gcd 𝑁 ) ∈ ℂ ∧ ( 𝐶 gcd 𝑁 ) ≠ 0 ) )
130 divmul2 ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ ( ( 𝐶 gcd 𝑁 ) ∈ ℂ ∧ ( 𝐶 gcd 𝑁 ) ≠ 0 ) ) → ( ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = 𝑠 ↔ 𝑁 = ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) ) )
131 126 127 129 130 syl3anc ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = 𝑠 ↔ 𝑁 = ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) ) )
132 simpll ⊢ ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) ∧ ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = 𝑠 ) → ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) )
133 73 adantr ⊢ ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) ∧ ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = 𝑠 ) → 𝑟 ∈ ℤ )
134 5 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → 𝑁 ∈ ℕ )
135 134 36 jca ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( 𝑁 ∈ ℕ ∧ 𝐶 ∈ ℤ ) )
136 divgcdnnr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐶 ∈ ℤ ) → ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ∈ ℕ )
137 135 136 syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ∈ ℕ )
138 137 adantr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) → ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ∈ ℕ )
139 138 ad2antrr ⊢ ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) ∧ ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = 𝑠 ) → ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ∈ ℕ )
140 eleq1 ⊢ ( 𝑠 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) → ( 𝑠 ∈ ℕ ↔ ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ∈ ℕ ) )
141 140 eqcoms ⊢ ( ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = 𝑠 → ( 𝑠 ∈ ℕ ↔ ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ∈ ℕ ) )
142 141 adantl ⊢ ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) ∧ ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = 𝑠 ) → ( 𝑠 ∈ ℕ ↔ ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ∈ ℕ ) )
143 139 142 mpbird ⊢ ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) ∧ ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = 𝑠 ) → 𝑠 ∈ ℕ )
144 133 143 jca ⊢ ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) ∧ ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = 𝑠 ) → ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) )
145 132 144 jca ⊢ ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) ∧ ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = 𝑠 ) → ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) )
146 simpr ⊢ ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) ∧ ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = 𝑠 ) → ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = 𝑠 )
147 145 146 jca ⊢ ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) ∧ ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = 𝑠 ) → ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) ∧ ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = 𝑠 ) )
148 nnz ⊢ ( 𝑠 ∈ ℕ → 𝑠 ∈ ℤ )
149 148 adantl ⊢ ( ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → 𝑠 ∈ ℤ )
150 149 anim2i ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) → ( 𝑘 ∈ ℤ ∧ 𝑠 ∈ ℤ ) )
151 150 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) ) → ( 𝑘 ∈ ℤ ∧ 𝑠 ∈ ℤ ) )
152 dvdsmul2 ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑠 ∈ ℤ ) → 𝑠 ∥ ( 𝑘 · 𝑠 ) )
153 151 152 syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) ) → 𝑠 ∥ ( 𝑘 · 𝑠 ) )
154 breq2 ⊢ ( ( 𝑘 · 𝑠 ) = ( ( 𝐴 − 𝐵 ) · 𝑟 ) → ( 𝑠 ∥ ( 𝑘 · 𝑠 ) ↔ 𝑠 ∥ ( ( 𝐴 − 𝐵 ) · 𝑟 ) ) )
155 zsubcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 − 𝐵 ) ∈ ℤ )
156 155 zcnd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
157 156 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
158 zcn ⊢ ( 𝑟 ∈ ℤ → 𝑟 ∈ ℂ )
159 158 adantr ⊢ ( ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → 𝑟 ∈ ℂ )
160 159 adantl ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) → 𝑟 ∈ ℂ )
161 160 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) ) → 𝑟 ∈ ℂ )
162 157 161 mulcomd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) ) → ( ( 𝐴 − 𝐵 ) · 𝑟 ) = ( 𝑟 · ( 𝐴 − 𝐵 ) ) )
163 162 breq2d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) ) → ( 𝑠 ∥ ( ( 𝐴 − 𝐵 ) · 𝑟 ) ↔ 𝑠 ∥ ( 𝑟 · ( 𝐴 − 𝐵 ) ) ) )
164 148 anim2i ⊢ ( ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) )
165 gcdcom ⊢ ( ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) → ( 𝑟 gcd 𝑠 ) = ( 𝑠 gcd 𝑟 ) )
166 164 165 syl ⊢ ( ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( 𝑟 gcd 𝑠 ) = ( 𝑠 gcd 𝑟 ) )
167 166 eqeq1d ⊢ ( ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → ( ( 𝑟 gcd 𝑠 ) = 1 ↔ ( 𝑠 gcd 𝑟 ) = 1 ) )
168 167 adantl ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) → ( ( 𝑟 gcd 𝑠 ) = 1 ↔ ( 𝑠 gcd 𝑟 ) = 1 ) )
169 168 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) ) → ( ( 𝑟 gcd 𝑠 ) = 1 ↔ ( 𝑠 gcd 𝑟 ) = 1 ) )
170 164 adantl ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) → ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) )
171 170 ancomd ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) → ( 𝑠 ∈ ℤ ∧ 𝑟 ∈ ℤ ) )
172 155 171 anim12i ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) ) → ( ( 𝐴 − 𝐵 ) ∈ ℤ ∧ ( 𝑠 ∈ ℤ ∧ 𝑟 ∈ ℤ ) ) )
173 172 ancomd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) ) → ( ( 𝑠 ∈ ℤ ∧ 𝑟 ∈ ℤ ) ∧ ( 𝐴 − 𝐵 ) ∈ ℤ ) )
174 df-3an ⊢ ( ( 𝑠 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ ( 𝐴 − 𝐵 ) ∈ ℤ ) ↔ ( ( 𝑠 ∈ ℤ ∧ 𝑟 ∈ ℤ ) ∧ ( 𝐴 − 𝐵 ) ∈ ℤ ) )
175 173 174 sylibr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) ) → ( 𝑠 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ ( 𝐴 − 𝐵 ) ∈ ℤ ) )
176 coprmdvds ⊢ ( ( 𝑠 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ ( 𝐴 − 𝐵 ) ∈ ℤ ) → ( ( 𝑠 ∥ ( 𝑟 · ( 𝐴 − 𝐵 ) ) ∧ ( 𝑠 gcd 𝑟 ) = 1 ) → 𝑠 ∥ ( 𝐴 − 𝐵 ) ) )
177 175 176 syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) ) → ( ( 𝑠 ∥ ( 𝑟 · ( 𝐴 − 𝐵 ) ) ∧ ( 𝑠 gcd 𝑟 ) = 1 ) → 𝑠 ∥ ( 𝐴 − 𝐵 ) ) )
178 simpr ⊢ ( ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) → 𝑠 ∈ ℕ )
179 178 adantl ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) → 𝑠 ∈ ℕ )
180 179 anim2i ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) ) → ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝑠 ∈ ℕ ) )
181 180 ancomd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) ) → ( 𝑠 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) )
182 3anass ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ↔ ( 𝑠 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) )
183 181 182 sylibr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) ) → ( 𝑠 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) )
184 moddvds ⊢ ( ( 𝑠 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 mod 𝑠 ) = ( 𝐵 mod 𝑠 ) ↔ 𝑠 ∥ ( 𝐴 − 𝐵 ) ) )
185 183 184 syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) ) → ( ( 𝐴 mod 𝑠 ) = ( 𝐵 mod 𝑠 ) ↔ 𝑠 ∥ ( 𝐴 − 𝐵 ) ) )
186 177 185 sylibrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) ) → ( ( 𝑠 ∥ ( 𝑟 · ( 𝐴 − 𝐵 ) ) ∧ ( 𝑠 gcd 𝑟 ) = 1 ) → ( 𝐴 mod 𝑠 ) = ( 𝐵 mod 𝑠 ) ) )
187 186 expcomd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) ) → ( ( 𝑠 gcd 𝑟 ) = 1 → ( 𝑠 ∥ ( 𝑟 · ( 𝐴 − 𝐵 ) ) → ( 𝐴 mod 𝑠 ) = ( 𝐵 mod 𝑠 ) ) ) )
188 169 187 sylbid ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) ) → ( ( 𝑟 gcd 𝑠 ) = 1 → ( 𝑠 ∥ ( 𝑟 · ( 𝐴 − 𝐵 ) ) → ( 𝐴 mod 𝑠 ) = ( 𝐵 mod 𝑠 ) ) ) )
189 188 com23 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) ) → ( 𝑠 ∥ ( 𝑟 · ( 𝐴 − 𝐵 ) ) → ( ( 𝑟 gcd 𝑠 ) = 1 → ( 𝐴 mod 𝑠 ) = ( 𝐵 mod 𝑠 ) ) ) )
190 163 189 sylbid ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) ) → ( 𝑠 ∥ ( ( 𝐴 − 𝐵 ) · 𝑟 ) → ( ( 𝑟 gcd 𝑠 ) = 1 → ( 𝐴 mod 𝑠 ) = ( 𝐵 mod 𝑠 ) ) ) )
191 190 com3l ⊢ ( 𝑠 ∥ ( ( 𝐴 − 𝐵 ) · 𝑟 ) → ( ( 𝑟 gcd 𝑠 ) = 1 → ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) ) → ( 𝐴 mod 𝑠 ) = ( 𝐵 mod 𝑠 ) ) ) )
192 154 191 biimtrdi ⊢ ( ( 𝑘 · 𝑠 ) = ( ( 𝐴 − 𝐵 ) · 𝑟 ) → ( 𝑠 ∥ ( 𝑘 · 𝑠 ) → ( ( 𝑟 gcd 𝑠 ) = 1 → ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) ) → ( 𝐴 mod 𝑠 ) = ( 𝐵 mod 𝑠 ) ) ) ) )
193 192 com14 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) ) → ( 𝑠 ∥ ( 𝑘 · 𝑠 ) → ( ( 𝑟 gcd 𝑠 ) = 1 → ( ( 𝑘 · 𝑠 ) = ( ( 𝐴 − 𝐵 ) · 𝑟 ) → ( 𝐴 mod 𝑠 ) = ( 𝐵 mod 𝑠 ) ) ) ) )
194 153 193 mpd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) ) → ( ( 𝑟 gcd 𝑠 ) = 1 → ( ( 𝑘 · 𝑠 ) = ( ( 𝐴 − 𝐵 ) · 𝑟 ) → ( 𝐴 mod 𝑠 ) = ( 𝐵 mod 𝑠 ) ) ) )
195 194 ex ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) → ( ( 𝑟 gcd 𝑠 ) = 1 → ( ( 𝑘 · 𝑠 ) = ( ( 𝐴 − 𝐵 ) · 𝑟 ) → ( 𝐴 mod 𝑠 ) = ( 𝐵 mod 𝑠 ) ) ) ) )
196 195 3adant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) → ( ( 𝑟 gcd 𝑠 ) = 1 → ( ( 𝑘 · 𝑠 ) = ( ( 𝐴 − 𝐵 ) · 𝑟 ) → ( 𝐴 mod 𝑠 ) = ( 𝐵 mod 𝑠 ) ) ) ) )
197 196 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( ( 𝑘 ∈ ℤ ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) → ( ( 𝑟 gcd 𝑠 ) = 1 → ( ( 𝑘 · 𝑠 ) = ( ( 𝐴 − 𝐵 ) · 𝑟 ) → ( 𝐴 mod 𝑠 ) = ( 𝐵 mod 𝑠 ) ) ) ) )
198 197 impl ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) → ( ( 𝑟 gcd 𝑠 ) = 1 → ( ( 𝑘 · 𝑠 ) = ( ( 𝐴 − 𝐵 ) · 𝑟 ) → ( 𝐴 mod 𝑠 ) = ( 𝐵 mod 𝑠 ) ) ) )
199 198 adantr ⊢ ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) ∧ ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = 𝑠 ) → ( ( 𝑟 gcd 𝑠 ) = 1 → ( ( 𝑘 · 𝑠 ) = ( ( 𝐴 − 𝐵 ) · 𝑟 ) → ( 𝐴 mod 𝑠 ) = ( 𝐵 mod 𝑠 ) ) ) )
200 199 imp ⊢ ( ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) ∧ ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = 𝑠 ) ∧ ( 𝑟 gcd 𝑠 ) = 1 ) → ( ( 𝑘 · 𝑠 ) = ( ( 𝐴 − 𝐵 ) · 𝑟 ) → ( 𝐴 mod 𝑠 ) = ( 𝐵 mod 𝑠 ) ) )
201 eqtr2 ⊢ ( ( ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = 𝑀 ∧ ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = 𝑠 ) → 𝑀 = 𝑠 )
202 oveq2 ⊢ ( 𝑀 = 𝑠 → ( 𝐴 mod 𝑀 ) = ( 𝐴 mod 𝑠 ) )
203 oveq2 ⊢ ( 𝑀 = 𝑠 → ( 𝐵 mod 𝑀 ) = ( 𝐵 mod 𝑠 ) )
204 202 203 eqeq12d ⊢ ( 𝑀 = 𝑠 → ( ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ↔ ( 𝐴 mod 𝑠 ) = ( 𝐵 mod 𝑠 ) ) )
205 201 204 syl ⊢ ( ( ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = 𝑀 ∧ ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = 𝑠 ) → ( ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ↔ ( 𝐴 mod 𝑠 ) = ( 𝐵 mod 𝑠 ) ) )
206 205 ex ⊢ ( ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = 𝑀 → ( ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = 𝑠 → ( ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ↔ ( 𝐴 mod 𝑠 ) = ( 𝐵 mod 𝑠 ) ) ) )
207 206 eqcoms ⊢ ( 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) → ( ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = 𝑠 → ( ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ↔ ( 𝐴 mod 𝑠 ) = ( 𝐵 mod 𝑠 ) ) ) )
208 207 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) → ( ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = 𝑠 → ( ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ↔ ( 𝐴 mod 𝑠 ) = ( 𝐵 mod 𝑠 ) ) ) )
209 208 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = 𝑠 → ( ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ↔ ( 𝐴 mod 𝑠 ) = ( 𝐵 mod 𝑠 ) ) ) )
210 209 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) → ( ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = 𝑠 → ( ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ↔ ( 𝐴 mod 𝑠 ) = ( 𝐵 mod 𝑠 ) ) ) )
211 210 imp ⊢ ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) ∧ ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = 𝑠 ) → ( ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ↔ ( 𝐴 mod 𝑠 ) = ( 𝐵 mod 𝑠 ) ) )
212 211 adantr ⊢ ( ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) ∧ ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = 𝑠 ) ∧ ( 𝑟 gcd 𝑠 ) = 1 ) → ( ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ↔ ( 𝐴 mod 𝑠 ) = ( 𝐵 mod 𝑠 ) ) )
213 200 212 sylibrd ⊢ ( ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) ∧ ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = 𝑠 ) ∧ ( 𝑟 gcd 𝑠 ) = 1 ) → ( ( 𝑘 · 𝑠 ) = ( ( 𝐴 − 𝐵 ) · 𝑟 ) → ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ) )
214 213 ex ⊢ ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ ) ) ∧ ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = 𝑠 ) → ( ( 𝑟 gcd 𝑠 ) = 1 → ( ( 𝑘 · 𝑠 ) = ( ( 𝐴 − 𝐵 ) · 𝑟 ) → ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ) ) )
215 147 214 syl ⊢ ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) ∧ ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = 𝑠 ) → ( ( 𝑟 gcd 𝑠 ) = 1 → ( ( 𝑘 · 𝑠 ) = ( ( 𝐴 − 𝐵 ) · 𝑟 ) → ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ) ) )
216 215 ex ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) = 𝑠 → ( ( 𝑟 gcd 𝑠 ) = 1 → ( ( 𝑘 · 𝑠 ) = ( ( 𝐴 − 𝐵 ) · 𝑟 ) → ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ) ) ) )
217 131 216 sylbird ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( 𝑁 = ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) → ( ( 𝑟 gcd 𝑠 ) = 1 → ( ( 𝑘 · 𝑠 ) = ( ( 𝐴 − 𝐵 ) · 𝑟 ) → ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ) ) ) )
218 217 com3l ⊢ ( 𝑁 = ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) → ( ( 𝑟 gcd 𝑠 ) = 1 → ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( ( 𝑘 · 𝑠 ) = ( ( 𝐴 − 𝐵 ) · 𝑟 ) → ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ) ) ) )
219 218 a1i ⊢ ( 𝐶 = ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) → ( 𝑁 = ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) → ( ( 𝑟 gcd 𝑠 ) = 1 → ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( ( 𝑘 · 𝑠 ) = ( ( 𝐴 − 𝐵 ) · 𝑟 ) → ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ) ) ) ) )
220 219 3imp ⊢ ( ( 𝐶 = ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ∧ 𝑁 = ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) ∧ ( 𝑟 gcd 𝑠 ) = 1 ) → ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( ( 𝑘 · 𝑠 ) = ( ( 𝐴 − 𝐵 ) · 𝑟 ) → ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ) ) )
221 220 impcom ⊢ ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) ∧ ( 𝐶 = ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ∧ 𝑁 = ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) ∧ ( 𝑟 gcd 𝑠 ) = 1 ) ) → ( ( 𝑘 · 𝑠 ) = ( ( 𝐴 − 𝐵 ) · 𝑟 ) → ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ) )
222 123 221 sylbid ⊢ ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) ∧ ( 𝐶 = ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ∧ 𝑁 = ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) ∧ ( 𝑟 gcd 𝑠 ) = 1 ) ) → ( ( 𝑘 · 𝑠 ) = ( ( 𝐴 · 𝑟 ) − ( 𝐵 · 𝑟 ) ) → ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ) )
223 110 222 sylbid ⊢ ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) ∧ ( 𝐶 = ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ∧ 𝑁 = ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) ∧ ( 𝑟 gcd 𝑠 ) = 1 ) ) → ( ( 𝑘 · ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) ) = ( ( 𝐴 · ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ) − ( 𝐵 · ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ) ) → ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ) )
224 31 223 sylbid ⊢ ( ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) ∧ ( 𝐶 = ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ∧ 𝑁 = ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) ∧ ( 𝑟 gcd 𝑠 ) = 1 ) ) → ( ( 𝑘 · 𝑁 ) = ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐶 ) ) → ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ) )
225 224 ex ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ ) ) → ( ( 𝐶 = ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ∧ 𝑁 = ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) ∧ ( 𝑟 gcd 𝑠 ) = 1 ) → ( ( 𝑘 · 𝑁 ) = ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐶 ) ) → ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ) ) )
226 225 rexlimdvva ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) → ( ∃ 𝑟 ∈ ℤ ∃ 𝑠 ∈ ℤ ( 𝐶 = ( ( 𝐶 gcd 𝑁 ) · 𝑟 ) ∧ 𝑁 = ( ( 𝐶 gcd 𝑁 ) · 𝑠 ) ∧ ( 𝑟 gcd 𝑠 ) = 1 ) → ( ( 𝑘 · 𝑁 ) = ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐶 ) ) → ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ) ) )
227 22 226 mpd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝑘 · 𝑁 ) = ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐶 ) ) → ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ) )
228 227 rexlimdva ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( ∃ 𝑘 ∈ ℤ ( 𝑘 · 𝑁 ) = ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐶 ) ) → ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ) )
229 7 228 sylbid ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝑁 ∈ ℕ ∧ 𝑀 = ( 𝑁 / ( 𝐶 gcd 𝑁 ) ) ) ) → ( ( ( 𝐴 · 𝐶 ) mod 𝑁 ) = ( ( 𝐵 · 𝐶 ) mod 𝑁 ) → ( 𝐴 mod 𝑀 ) = ( 𝐵 mod 𝑀 ) ) )