cncongr1 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > cncongr1		GIF version

Theorem cncongr1 10485

Description: One direction of the bicondition in cncongr 10487. 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 8404	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 · 𝐶) ∈ ℤ)
2	1	3adant2 957	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 · 𝐶) ∈ ℤ)
3		zmulcl 8404	. . . 4 ⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵 · 𝐶) ∈ ℤ)
4	3	3adant1 956	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵 · 𝐶) ∈ ℤ)
5		simpl 107	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁))) → 𝑁 ∈ ℕ)
6		congr 10482	. . 3 ⊢ (((𝐴 · 𝐶) ∈ ℤ ∧ (𝐵 · 𝐶) ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐴 · 𝐶) mod 𝑁) = ((𝐵 · 𝐶) mod 𝑁) ↔ ∃𝑘 ∈ ℤ (𝑘 · 𝑁) = ((𝐴 · 𝐶) − (𝐵 · 𝐶))))
7	2, 4, 5, 6	syl2an3an 1229	. 2 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (((𝐴 · 𝐶) mod 𝑁) = ((𝐵 · 𝐶) mod 𝑁) ↔ ∃𝑘 ∈ ℤ (𝑘 · 𝑁) = ((𝐴 · 𝐶) − (𝐵 · 𝐶))))
8		simpl 107	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝐶 ∈ ℤ)
9		nnz 8370	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
10		nnne0 8067	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0)
11	9, 10	jca 300	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0))
12	11	adantl 271	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0))
13		eqidd 2082	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐶 gcd 𝑁) = (𝐶 gcd 𝑁))
14	8, 12, 13	3jca 1118	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐶 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐶 gcd 𝑁) = (𝐶 gcd 𝑁)))
15	14	ex 113	. . . . . . . . . 10 ⊢ (𝐶 ∈ ℤ → (𝑁 ∈ ℕ → (𝐶 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐶 gcd 𝑁) = (𝐶 gcd 𝑁))))
16	15	3ad2ant3 961	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝑁 ∈ ℕ → (𝐶 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐶 gcd 𝑁) = (𝐶 gcd 𝑁))))
17	16	com12 30	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐶 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐶 gcd 𝑁) = (𝐶 gcd 𝑁))))
18	17	adantr 270	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁))) → ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐶 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐶 gcd 𝑁) = (𝐶 gcd 𝑁))))
19	18	impcom 123	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (𝐶 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐶 gcd 𝑁) = (𝐶 gcd 𝑁)))
20		divgcdcoprmex 10484	. . . . . 6 ⊢ ((𝐶 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐶 gcd 𝑁) = (𝐶 gcd 𝑁)) → ∃𝑟 ∈ ℤ ∃𝑠 ∈ ℤ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1))
21	19, 20	syl 14	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → ∃𝑟 ∈ ℤ ∃𝑠 ∈ ℤ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1))
22	21	adantr 270	. . . 4 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → ∃𝑟 ∈ ℤ ∃𝑠 ∈ ℤ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1))
23		oveq2 5540	. . . . . . . . . 10 ⊢ (𝑁 = ((𝐶 gcd 𝑁) · 𝑠) → (𝑘 · 𝑁) = (𝑘 · ((𝐶 gcd 𝑁) · 𝑠)))
24	23	3ad2ant2 960	. . . . . . . . 9 ⊢ ((𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1) → (𝑘 · 𝑁) = (𝑘 · ((𝐶 gcd 𝑁) · 𝑠)))
25	24	adantl 271	. . . . . . . 8 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) → (𝑘 · 𝑁) = (𝑘 · ((𝐶 gcd 𝑁) · 𝑠)))
26		oveq2 5540	. . . . . . . . . . 11 ⊢ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) → (𝐴 · 𝐶) = (𝐴 · ((𝐶 gcd 𝑁) · 𝑟)))
27		oveq2 5540	. . . . . . . . . . 11 ⊢ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) → (𝐵 · 𝐶) = (𝐵 · ((𝐶 gcd 𝑁) · 𝑟)))
28	26, 27	oveq12d 5550	. . . . . . . . . 10 ⊢ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) → ((𝐴 · 𝐶) − (𝐵 · 𝐶)) = ((𝐴 · ((𝐶 gcd 𝑁) · 𝑟)) − (𝐵 · ((𝐶 gcd 𝑁) · 𝑟))))
29	28	3ad2ant1 959	. . . . . . . . 9 ⊢ ((𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1) → ((𝐴 · 𝐶) − (𝐵 · 𝐶)) = ((𝐴 · ((𝐶 gcd 𝑁) · 𝑟)) − (𝐵 · ((𝐶 gcd 𝑁) · 𝑟))))
30	29	adantl 271	. . . . . . . 8 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) → ((𝐴 · 𝐶) − (𝐵 · 𝐶)) = ((𝐴 · ((𝐶 gcd 𝑁) · 𝑟)) − (𝐵 · ((𝐶 gcd 𝑁) · 𝑟))))
31	25, 30	eqeq12d 2095	. . . . . . 7 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) → ((𝑘 · 𝑁) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)) ↔ (𝑘 · ((𝐶 gcd 𝑁) · 𝑠)) = ((𝐴 · ((𝐶 gcd 𝑁) · 𝑟)) − (𝐵 · ((𝐶 gcd 𝑁) · 𝑟)))))
32		simpr 108	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℤ)
33	32	zcnd 8470	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℂ)
34	33	adantr 270	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝑘 ∈ ℂ)
35		simp3 940	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐶 ∈ ℤ)
36	35	adantr 270	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → 𝐶 ∈ ℤ)
37	9	ad2antrl 473	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → 𝑁 ∈ ℤ)
38	36, 37	gcdcld 10360	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (𝐶 gcd 𝑁) ∈ ℕ₀)
39	38	nn0cnd 8343	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (𝐶 gcd 𝑁) ∈ ℂ)
40	39	ad2antrr 471	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐶 gcd 𝑁) ∈ ℂ)
41		simpr 108	. . . . . . . . . . . . . 14 ⊢ ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ) → 𝑠 ∈ ℤ)
42	41	zcnd 8470	. . . . . . . . . . . . 13 ⊢ ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ) → 𝑠 ∈ ℂ)
43	42	adantl 271	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝑠 ∈ ℂ)
44	34, 40, 43	mul12d 7260	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝑘 · ((𝐶 gcd 𝑁) · 𝑠)) = ((𝐶 gcd 𝑁) · (𝑘 · 𝑠)))
45		simp1 938	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐴 ∈ ℤ)
46	45	zcnd 8470	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐴 ∈ ℂ)
47	46	ad3antrrr 475	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝐴 ∈ ℂ)
48	35	ad2antrr 471	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → 𝐶 ∈ ℤ)
49	5	nnzd 8468	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁))) → 𝑁 ∈ ℤ)
50	49	adantl 271	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → 𝑁 ∈ ℤ)
51	50	adantr 270	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → 𝑁 ∈ ℤ)
52	48, 51	gcdcld 10360	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → (𝐶 gcd 𝑁) ∈ ℕ₀)
53	52	nn0cnd 8343	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → (𝐶 gcd 𝑁) ∈ ℂ)
54	53	adantr 270	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐶 gcd 𝑁) ∈ ℂ)
55		simpl 107	. . . . . . . . . . . . . . 15 ⊢ ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ) → 𝑟 ∈ ℤ)
56	55	zcnd 8470	. . . . . . . . . . . . . 14 ⊢ ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ) → 𝑟 ∈ ℂ)
57	56	adantl 271	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝑟 ∈ ℂ)
58	47, 54, 57	mul12d 7260	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐴 · ((𝐶 gcd 𝑁) · 𝑟)) = ((𝐶 gcd 𝑁) · (𝐴 · 𝑟)))
59		simp2 939	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐵 ∈ ℤ)
60	59	zcnd 8470	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐵 ∈ ℂ)
61	60	ad3antrrr 475	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝐵 ∈ ℂ)
62	36, 50	gcdcld 10360	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (𝐶 gcd 𝑁) ∈ ℕ₀)
63	62	nn0cnd 8343	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (𝐶 gcd 𝑁) ∈ ℂ)
64	63	ad2antrr 471	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐶 gcd 𝑁) ∈ ℂ)
65	61, 64, 57	mul12d 7260	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐵 · ((𝐶 gcd 𝑁) · 𝑟)) = ((𝐶 gcd 𝑁) · (𝐵 · 𝑟)))
66	58, 65	oveq12d 5550	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝐴 · ((𝐶 gcd 𝑁) · 𝑟)) − (𝐵 · ((𝐶 gcd 𝑁) · 𝑟))) = (((𝐶 gcd 𝑁) · (𝐴 · 𝑟)) − ((𝐶 gcd 𝑁) · (𝐵 · 𝑟))))
67	44, 66	eqeq12d 2095	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝑘 · ((𝐶 gcd 𝑁) · 𝑠)) = ((𝐴 · ((𝐶 gcd 𝑁) · 𝑟)) − (𝐵 · ((𝐶 gcd 𝑁) · 𝑟))) ↔ ((𝐶 gcd 𝑁) · (𝑘 · 𝑠)) = (((𝐶 gcd 𝑁) · (𝐴 · 𝑟)) − ((𝐶 gcd 𝑁) · (𝐵 · 𝑟)))))
68	45	ad3antrrr 475	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝐴 ∈ ℤ)
69	55	adantl 271	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝑟 ∈ ℤ)
70	68, 69	zmulcld 8475	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐴 · 𝑟) ∈ ℤ)
71	70	zcnd 8470	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐴 · 𝑟) ∈ ℂ)
72	59	ad3antrrr 475	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝐵 ∈ ℤ)
73	72, 69	zmulcld 8475	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐵 · 𝑟) ∈ ℤ)
74	73	zcnd 8470	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐵 · 𝑟) ∈ ℂ)
75	64, 71, 74	subdid 7518	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝐶 gcd 𝑁) · ((𝐴 · 𝑟) − (𝐵 · 𝑟))) = (((𝐶 gcd 𝑁) · (𝐴 · 𝑟)) − ((𝐶 gcd 𝑁) · (𝐵 · 𝑟))))
76	75	eqcomd 2086	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (((𝐶 gcd 𝑁) · (𝐴 · 𝑟)) − ((𝐶 gcd 𝑁) · (𝐵 · 𝑟))) = ((𝐶 gcd 𝑁) · ((𝐴 · 𝑟) − (𝐵 · 𝑟))))
77	76	eqeq2d 2092	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (((𝐶 gcd 𝑁) · (𝑘 · 𝑠)) = (((𝐶 gcd 𝑁) · (𝐴 · 𝑟)) − ((𝐶 gcd 𝑁) · (𝐵 · 𝑟))) ↔ ((𝐶 gcd 𝑁) · (𝑘 · 𝑠)) = ((𝐶 gcd 𝑁) · ((𝐴 · 𝑟) − (𝐵 · 𝑟)))))
78	32	adantr 270	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝑘 ∈ ℤ)
79		simprr 498	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝑠 ∈ ℤ)
80	78, 79	zmulcld 8475	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝑘 · 𝑠) ∈ ℤ)
81	80	zcnd 8470	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝑘 · 𝑠) ∈ ℂ)
82		zmulcl 8404	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℤ ∧ 𝑟 ∈ ℤ) → (𝐴 · 𝑟) ∈ ℤ)
83	82	ad2ant2r 492	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐴 · 𝑟) ∈ ℤ)
84		zmulcl 8404	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ ℤ ∧ 𝑟 ∈ ℤ) → (𝐵 · 𝑟) ∈ ℤ)
85	84	ad2ant2lr 493	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐵 · 𝑟) ∈ ℤ)
86	83, 85	zsubcld 8474	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝐴 · 𝑟) − (𝐵 · 𝑟)) ∈ ℤ)
87	86	zcnd 8470	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝐴 · 𝑟) − (𝐵 · 𝑟)) ∈ ℂ)
88	87	ex 113	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ) → ((𝐴 · 𝑟) − (𝐵 · 𝑟)) ∈ ℂ))
89	88	3adant3 958	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ) → ((𝐴 · 𝑟) − (𝐵 · 𝑟)) ∈ ℂ))
90	89	ad2antrr 471	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ) → ((𝐴 · 𝑟) − (𝐵 · 𝑟)) ∈ ℂ))
91	90	imp 122	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝐴 · 𝑟) − (𝐵 · 𝑟)) ∈ ℂ)
92	10	ad2antrl 473	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → 𝑁 ≠ 0)
93		gcd2n0cl 10361	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐶 gcd 𝑁) ∈ ℕ)
94	36, 50, 92, 93	syl3anc 1169	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (𝐶 gcd 𝑁) ∈ ℕ)
95	94	nnne0d 8083	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (𝐶 gcd 𝑁) ≠ 0)
96	95	ad2antrr 471	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐶 gcd 𝑁) ≠ 0)
97	52	adantr 270	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐶 gcd 𝑁) ∈ ℕ₀)
98	97	nn0zd 8467	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐶 gcd 𝑁) ∈ ℤ)
99		0zd 8363	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 0 ∈ ℤ)
100		zapne 8422	. . . . . . . . . . . . 13 ⊢ (((𝐶 gcd 𝑁) ∈ ℤ ∧ 0 ∈ ℤ) → ((𝐶 gcd 𝑁) # 0 ↔ (𝐶 gcd 𝑁) ≠ 0))
101	98, 99, 100	syl2anc 403	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝐶 gcd 𝑁) # 0 ↔ (𝐶 gcd 𝑁) ≠ 0))
102	96, 101	mpbird 165	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐶 gcd 𝑁) # 0)
103	81, 91, 64, 102	mulcanapd 7751	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (((𝐶 gcd 𝑁) · (𝑘 · 𝑠)) = ((𝐶 gcd 𝑁) · ((𝐴 · 𝑟) − (𝐵 · 𝑟))) ↔ (𝑘 · 𝑠) = ((𝐴 · 𝑟) − (𝐵 · 𝑟))))
104	67, 77, 103	3bitrd 212	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝑘 · ((𝐶 gcd 𝑁) · 𝑠)) = ((𝐴 · ((𝐶 gcd 𝑁) · 𝑟)) − (𝐵 · ((𝐶 gcd 𝑁) · 𝑟))) ↔ (𝑘 · 𝑠) = ((𝐴 · 𝑟) − (𝐵 · 𝑟))))
105	104	adantr 270	. . . . . . . 8 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) → ((𝑘 · ((𝐶 gcd 𝑁) · 𝑠)) = ((𝐴 · ((𝐶 gcd 𝑁) · 𝑟)) − (𝐵 · ((𝐶 gcd 𝑁) · 𝑟))) ↔ (𝑘 · 𝑠) = ((𝐴 · 𝑟) − (𝐵 · 𝑟))))
106		zcn 8356	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℂ)
107		zcn 8356	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ ℤ → 𝐵 ∈ ℂ)
108	106, 107	anim12i 331	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ))
109	108	3adant3 958	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ))
110	109	ad2antrr 471	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ))
111	110, 56	anim12i 331	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑟 ∈ ℂ))
112		df-3an 921	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑟 ∈ ℂ) ↔ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑟 ∈ ℂ))
113	111, 112	sylibr 132	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑟 ∈ ℂ))
114		subdir 7490	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑟 ∈ ℂ) → ((𝐴 − 𝐵) · 𝑟) = ((𝐴 · 𝑟) − (𝐵 · 𝑟)))
115	113, 114	syl 14	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝐴 − 𝐵) · 𝑟) = ((𝐴 · 𝑟) − (𝐵 · 𝑟)))
116	115	eqcomd 2086	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝐴 · 𝑟) − (𝐵 · 𝑟)) = ((𝐴 − 𝐵) · 𝑟))
117	116	adantr 270	. . . . . . . . . 10 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) → ((𝐴 · 𝑟) − (𝐵 · 𝑟)) = ((𝐴 − 𝐵) · 𝑟))
118	117	eqeq2d 2092	. . . . . . . . 9 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) → ((𝑘 · 𝑠) = ((𝐴 · 𝑟) − (𝐵 · 𝑟)) ↔ (𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟)))
119	5	nncnd 8053	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁))) → 𝑁 ∈ ℂ)
120	119	adantl 271	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → 𝑁 ∈ ℂ)
121	120	ad2antrr 471	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝑁 ∈ ℂ)
122	79	zcnd 8470	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝑠 ∈ ℂ)
123	121, 122, 40, 102	divmulap2d 7910	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝑁 / (𝐶 gcd 𝑁)) = 𝑠 ↔ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠)))
124		simpll 495	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ))
125	69	adantr 270	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → 𝑟 ∈ ℤ)
126	5	adantl 271	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → 𝑁 ∈ ℕ)
127		divgcdnnr 10367	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℕ ∧ 𝐶 ∈ ℤ) → (𝑁 / (𝐶 gcd 𝑁)) ∈ ℕ)
128	126, 36, 127	syl2anc 403	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (𝑁 / (𝐶 gcd 𝑁)) ∈ ℕ)
129	128	ad3antrrr 475	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → (𝑁 / (𝐶 gcd 𝑁)) ∈ ℕ)
130		eleq1 2141	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 = (𝑁 / (𝐶 gcd 𝑁)) → (𝑠 ∈ ℕ ↔ (𝑁 / (𝐶 gcd 𝑁)) ∈ ℕ))
131	130	eqcoms 2084	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 / (𝐶 gcd 𝑁)) = 𝑠 → (𝑠 ∈ ℕ ↔ (𝑁 / (𝐶 gcd 𝑁)) ∈ ℕ))
132	131	adantl 271	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → (𝑠 ∈ ℕ ↔ (𝑁 / (𝐶 gcd 𝑁)) ∈ ℕ))
133	129, 132	mpbird 165	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → 𝑠 ∈ ℕ)
134	125, 133	jca 300	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))
135	124, 134	jca 300	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)))
136		simpr 108	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → (𝑁 / (𝐶 gcd 𝑁)) = 𝑠)
137		nnz 8370	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑠 ∈ ℕ → 𝑠 ∈ ℤ)
138	137	adantl 271	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ) → 𝑠 ∈ ℤ)
139	138	anim2i 334	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) → (𝑘 ∈ ℤ ∧ 𝑠 ∈ ℤ))
140	139	adantl 271	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝑘 ∈ ℤ ∧ 𝑠 ∈ ℤ))
141		dvdsmul2 10218	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑘 ∈ ℤ ∧ 𝑠 ∈ ℤ) → 𝑠 ∥ (𝑘 · 𝑠))
142	140, 141	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → 𝑠 ∥ (𝑘 · 𝑠))
143		breq2 3789	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝑠 ∥ (𝑘 · 𝑠) ↔ 𝑠 ∥ ((𝐴 − 𝐵) · 𝑟)))
144		zsubcl 8392	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 − 𝐵) ∈ ℤ)
145	144	zcnd 8470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 − 𝐵) ∈ ℂ)
146	145	adantr 270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝐴 − 𝐵) ∈ ℂ)
147		zcn 8356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑟 ∈ ℤ → 𝑟 ∈ ℂ)
148	147	ad2antrl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) → 𝑟 ∈ ℂ)
149	148	adantl 271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → 𝑟 ∈ ℂ)
150	146, 149	mulcomd 7140	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → ((𝐴 − 𝐵) · 𝑟) = (𝑟 · (𝐴 − 𝐵)))
151	150	breq2d 3797	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝑠 ∥ ((𝐴 − 𝐵) · 𝑟) ↔ 𝑠 ∥ (𝑟 · (𝐴 − 𝐵))))
152	137	anim2i 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ) → (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ))
153		gcdcom 10365	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ) → (𝑟 gcd 𝑠) = (𝑠 gcd 𝑟))
154	152, 153	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ) → (𝑟 gcd 𝑠) = (𝑠 gcd 𝑟))
155	154	eqeq1d 2089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ) → ((𝑟 gcd 𝑠) = 1 ↔ (𝑠 gcd 𝑟) = 1))
156	155	ad2antll 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → ((𝑟 gcd 𝑠) = 1 ↔ (𝑠 gcd 𝑟) = 1))
157	152	adantl 271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) → (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ))
158	157	ancomd 263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) → (𝑠 ∈ ℤ ∧ 𝑟 ∈ ℤ))
159	144, 158	anim12i 331	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → ((𝐴 − 𝐵) ∈ ℤ ∧ (𝑠 ∈ ℤ ∧ 𝑟 ∈ ℤ)))
160	159	ancomd 263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → ((𝑠 ∈ ℤ ∧ 𝑟 ∈ ℤ) ∧ (𝐴 − 𝐵) ∈ ℤ))
161		df-3an 921	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑠 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ (𝐴 − 𝐵) ∈ ℤ) ↔ ((𝑠 ∈ ℤ ∧ 𝑟 ∈ ℤ) ∧ (𝐴 − 𝐵) ∈ ℤ))
162	160, 161	sylibr 132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝑠 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ (𝐴 − 𝐵) ∈ ℤ))
163		coprmdvds 10474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑠 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ (𝐴 − 𝐵) ∈ ℤ) → ((𝑠 ∥ (𝑟 · (𝐴 − 𝐵)) ∧ (𝑠 gcd 𝑟) = 1) → 𝑠 ∥ (𝐴 − 𝐵)))
164	162, 163	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → ((𝑠 ∥ (𝑟 · (𝐴 − 𝐵)) ∧ (𝑠 gcd 𝑟) = 1) → 𝑠 ∥ (𝐴 − 𝐵)))
165		simprr 498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) → 𝑠 ∈ ℕ)
166	165	anim2i 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑠 ∈ ℕ))
167	166	ancomd 263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝑠 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)))
168		3anass 923	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑠 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ↔ (𝑠 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)))
169	167, 168	sylibr 132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝑠 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ))
170		moddvds 10204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑠 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 mod 𝑠) = (𝐵 mod 𝑠) ↔ 𝑠 ∥ (𝐴 − 𝐵)))
171	169, 170	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → ((𝐴 mod 𝑠) = (𝐵 mod 𝑠) ↔ 𝑠 ∥ (𝐴 − 𝐵)))
172	164, 171	sylibrd 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → ((𝑠 ∥ (𝑟 · (𝐴 − 𝐵)) ∧ (𝑠 gcd 𝑟) = 1) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))
173	172	expcomd 1370	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → ((𝑠 gcd 𝑟) = 1 → (𝑠 ∥ (𝑟 · (𝐴 − 𝐵)) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠))))
174	156, 173	sylbid 148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → ((𝑟 gcd 𝑠) = 1 → (𝑠 ∥ (𝑟 · (𝐴 − 𝐵)) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠))))
175	174	com23 77	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝑠 ∥ (𝑟 · (𝐴 − 𝐵)) → ((𝑟 gcd 𝑠) = 1 → (𝐴 mod 𝑠) = (𝐵 mod 𝑠))))
176	151, 175	sylbid 148	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝑠 ∥ ((𝐴 − 𝐵) · 𝑟) → ((𝑟 gcd 𝑠) = 1 → (𝐴 mod 𝑠) = (𝐵 mod 𝑠))))
177	176	com3l 80	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑠 ∥ ((𝐴 − 𝐵) · 𝑟) → ((𝑟 gcd 𝑠) = 1 → (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠))))
178	143, 177	syl6bi 161	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝑠 ∥ (𝑘 · 𝑠) → ((𝑟 gcd 𝑠) = 1 → (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))))
179	178	com14 87	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝑠 ∥ (𝑘 · 𝑠) → ((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))))
180	142, 179	mpd 13	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → ((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠))))
181	180	ex 113	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) → ((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))))
182	181	3adant3 958	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) → ((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))))
183	182	adantr 270	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → ((𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) → ((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))))
184	183	impl 372	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) → ((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠))))
185	184	adantr 270	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → ((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠))))
186	185	imp 122	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) ∧ (𝑟 gcd 𝑠) = 1) → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))
187		eqtr2 2099	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑁 / (𝐶 gcd 𝑁)) = 𝑀 ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → 𝑀 = 𝑠)
188		oveq2 5540	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑀 = 𝑠 → (𝐴 mod 𝑀) = (𝐴 mod 𝑠))
189		oveq2 5540	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑀 = 𝑠 → (𝐵 mod 𝑀) = (𝐵 mod 𝑠))
190	188, 189	eqeq12d 2095	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑀 = 𝑠 → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) ↔ (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))
191	187, 190	syl 14	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑁 / (𝐶 gcd 𝑁)) = 𝑀 ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) ↔ (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))
192	191	ex 113	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 / (𝐶 gcd 𝑁)) = 𝑀 → ((𝑁 / (𝐶 gcd 𝑁)) = 𝑠 → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) ↔ (𝐴 mod 𝑠) = (𝐵 mod 𝑠))))
193	192	eqcoms 2084	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 = (𝑁 / (𝐶 gcd 𝑁)) → ((𝑁 / (𝐶 gcd 𝑁)) = 𝑠 → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) ↔ (𝐴 mod 𝑠) = (𝐵 mod 𝑠))))
194	193	ad2antll 474	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → ((𝑁 / (𝐶 gcd 𝑁)) = 𝑠 → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) ↔ (𝐴 mod 𝑠) = (𝐵 mod 𝑠))))
195	194	ad2antrr 471	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) → ((𝑁 / (𝐶 gcd 𝑁)) = 𝑠 → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) ↔ (𝐴 mod 𝑠) = (𝐵 mod 𝑠))))
196	195	imp 122	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) ↔ (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))
197	196	adantr 270	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) ∧ (𝑟 gcd 𝑠) = 1) → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) ↔ (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))
198	186, 197	sylibrd 167	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) ∧ (𝑟 gcd 𝑠) = 1) → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀)))
199	198	ex 113	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → ((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀))))
200	135, 136, 199	syl2anc 403	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → ((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀))))
201	200	ex 113	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝑁 / (𝐶 gcd 𝑁)) = 𝑠 → ((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀)))))
202	123, 201	sylbird 168	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝑁 = ((𝐶 gcd 𝑁) · 𝑠) → ((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀)))))
203	202	com3l 80	. . . . . . . . . . . 12 ⊢ (𝑁 = ((𝐶 gcd 𝑁) · 𝑠) → ((𝑟 gcd 𝑠) = 1 → (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀)))))
204	203	a1i 9	. . . . . . . . . . 11 ⊢ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) → (𝑁 = ((𝐶 gcd 𝑁) · 𝑠) → ((𝑟 gcd 𝑠) = 1 → (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀))))))
205	204	3imp 1132	. . . . . . . . . 10 ⊢ ((𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1) → (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀))))
206	205	impcom 123	. . . . . . . . 9 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀)))
207	118, 206	sylbid 148	. . . . . . . 8 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) → ((𝑘 · 𝑠) = ((𝐴 · 𝑟) − (𝐵 · 𝑟)) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀)))
208	105, 207	sylbid 148	. . . . . . 7 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) → ((𝑘 · ((𝐶 gcd 𝑁) · 𝑠)) = ((𝐴 · ((𝐶 gcd 𝑁) · 𝑟)) − (𝐵 · ((𝐶 gcd 𝑁) · 𝑟))) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀)))
209	31, 208	sylbid 148	. . . . . 6 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) → ((𝑘 · 𝑁) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀)))
210	209	ex 113	. . . . 5 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1) → ((𝑘 · 𝑁) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀))))
211	210	rexlimdvva 2484	. . . 4 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → (∃𝑟 ∈ ℤ ∃𝑠 ∈ ℤ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1) → ((𝑘 · 𝑁) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀))))
212	22, 211	mpd 13	. . 3 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → ((𝑘 · 𝑁) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀)))
213	212	rexlimdva 2477	. 2 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (∃𝑘 ∈ ℤ (𝑘 · 𝑁) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀)))
214	7, 213	sylbid 148	1 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (((𝐴 · 𝐶) mod 𝑁) = ((𝐵 · 𝐶) mod 𝑁) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀)))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 102 ↔ wb 103 ∧ w3a 919 = wceq 1284 ∈ wcel 1433 ≠ wne 2245 ∃wrex 2349 class class class wbr 3785 (class class class)co 5532 ℂcc 6979 0cc0 6981 1c1 6982 · cmul 6986 − cmin 7279 # cap 7681 / cdiv 7760 ℕcn 8039 ℕ₀cn0 8288 ℤcz 8351 mod cmo 9324 ∥ cdvds 10195 gcd cgcd 10338

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 576 ax-in2 577 ax-io 662 ax-5 1376 ax-7 1377 ax-gen 1378 ax-ie1 1422 ax-ie2 1423 ax-8 1435 ax-10 1436 ax-11 1437 ax-i12 1438 ax-bndl 1439 ax-4 1440 ax-13 1444 ax-14 1445 ax-17 1459 ax-i9 1463 ax-ial 1467 ax-i5r 1468 ax-ext 2063 ax-coll 3893 ax-sep 3896 ax-nul 3904 ax-pow 3948 ax-pr 3964 ax-un 4188 ax-setind 4280 ax-iinf 4329 ax-cnex 7067 ax-resscn 7068 ax-1cn 7069 ax-1re 7070 ax-icn 7071 ax-addcl 7072 ax-addrcl 7073 ax-mulcl 7074 ax-mulrcl 7075 ax-addcom 7076 ax-mulcom 7077 ax-addass 7078 ax-mulass 7079 ax-distr 7080 ax-i2m1 7081 ax-0lt1 7082 ax-1rid 7083 ax-0id 7084 ax-rnegex 7085 ax-precex 7086 ax-cnre 7087 ax-pre-ltirr 7088 ax-pre-ltwlin 7089 ax-pre-lttrn 7090 ax-pre-apti 7091 ax-pre-ltadd 7092 ax-pre-mulgt0 7093 ax-pre-mulext 7094 ax-arch 7095 ax-caucvg 7096

This theorem depends on definitions: df-bi 115 df-dc 776 df-3or 920 df-3an 921 df-tru 1287 df-fal 1290 df-nf 1390 df-sb 1686 df-eu 1944 df-mo 1945 df-clab 2068 df-cleq 2074 df-clel 2077 df-nfc 2208 df-ne 2246 df-nel 2340 df-ral 2353 df-rex 2354 df-reu 2355 df-rmo 2356 df-rab 2357 df-v 2603 df-sbc 2816 df-csb 2909 df-dif 2975 df-un 2977 df-in 2979 df-ss 2986 df-nul 3252 df-if 3352 df-pw 3384 df-sn 3404 df-pr 3405 df-op 3407 df-uni 3602 df-int 3637 df-iun 3680 df-br 3786 df-opab 3840 df-mpt 3841 df-tr 3876 df-id 4048 df-po 4051 df-iso 4052 df-iord 4121 df-on 4123 df-suc 4126 df-iom 4332 df-xp 4369 df-rel 4370 df-cnv 4371 df-co 4372 df-dm 4373 df-rn 4374 df-res 4375 df-ima 4376 df-iota 4887 df-fun 4924 df-fn 4925 df-f 4926 df-f1 4927 df-fo 4928 df-f1o 4929 df-fv 4930 df-riota 5488 df-ov 5535 df-oprab 5536 df-mpt2 5537 df-1st 5787 df-2nd 5788 df-recs 5943 df-frec 6001 df-sup 6397 df-pnf 7155 df-mnf 7156 df-xr 7157 df-ltxr 7158 df-le 7159 df-sub 7281 df-neg 7282 df-reap 7675 df-ap 7682 df-div 7761 df-inn 8040 df-2 8098 df-3 8099 df-4 8100 df-n0 8289 df-z 8352 df-uz 8620 df-q 8705 df-rp 8735 df-fz 9030 df-fzo 9153 df-fl 9274 df-mod 9325 df-iseq 9432 df-iexp 9476 df-cj 9729 df-re 9730 df-im 9731 df-rsqrt 9884 df-abs 9885 df-dvds 10196 df-gcd 10339

This theorem is referenced by: cncongr 10487

W3C validator