cncongr1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cncongr1		Structured version Visualization version GIF version

Theorem cncongr1 16360

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

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

Proof of Theorem cncongr1 Dummy variables 𝑘 𝑟 𝑠 are mutually distinct and distinct from all other variables.

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 ≠ wne 2943 ∃wrex 3065 class class class wbr 5074 (class class class)co 7268 ℂcc 10857 0cc0 10859 1c1 10860 · cmul 10864 − cmin 11193 / cdiv 11620 ℕcn 11961 ℤcz 12307 mod cmo 13577 ∥ cdvds 15951 gcd cgcd 16189

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-sep 5222 ax-nul 5229 ax-pow 5287 ax-pr 5351 ax-un 7579 ax-cnex 10915 ax-resscn 10916 ax-1cn 10917 ax-icn 10918 ax-addcl 10919 ax-addrcl 10920 ax-mulcl 10921 ax-mulrcl 10922 ax-mulcom 10923 ax-addass 10924 ax-mulass 10925 ax-distr 10926 ax-i2m1 10927 ax-1ne0 10928 ax-1rid 10929 ax-rnegex 10930 ax-rrecex 10931 ax-cnre 10932 ax-pre-lttri 10933 ax-pre-lttrn 10934 ax-pre-ltadd 10935 ax-pre-mulgt0 10936 ax-pre-sup 10937

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-reu 3071 df-rmo 3072 df-rab 3073 df-v 3432 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4258 df-if 4461 df-pw 4536 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4841 df-iun 4927 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5485 df-eprel 5491 df-po 5499 df-so 5500 df-fr 5540 df-we 5542 df-xp 5591 df-rel 5592 df-cnv 5593 df-co 5594 df-dm 5595 df-rn 5596 df-res 5597 df-ima 5598 df-pred 6196 df-ord 6263 df-on 6264 df-lim 6265 df-suc 6266 df-iota 6385 df-fun 6429 df-fn 6430 df-f 6431 df-f1 6432 df-fo 6433 df-f1o 6434 df-fv 6435 df-riota 7225 df-ov 7271 df-oprab 7272 df-mpo 7273 df-om 7704 df-2nd 7822 df-frecs 8085 df-wrecs 8116 df-recs 8190 df-rdg 8229 df-er 8486 df-en 8722 df-dom 8723 df-sdom 8724 df-sup 9189 df-inf 9190 df-pnf 10999 df-mnf 11000 df-xr 11001 df-ltxr 11002 df-le 11003 df-sub 11195 df-neg 11196 df-div 11621 df-nn 11962 df-2 12024 df-3 12025 df-n0 12222 df-z 12308 df-uz 12571 df-rp 12719 df-fl 13500 df-mod 13578 df-seq 13710 df-exp 13771 df-cj 14798 df-re 14799 df-im 14800 df-sqrt 14934 df-abs 14935 df-dvds 15952 df-gcd 16190

This theorem is referenced by: cncongr 16362

W3C validator