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	syl6bi	⊢ ( ( 𝑘 · 𝑠 ) = ( ( 𝐴 − 𝐵 ) · 𝑟 ) → ( 𝑠 ∥ ( 𝑘 · 𝑠 ) → ( ( 𝑟 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 𝑀 ) ) )