cncongr1 - Intuitionistic Logic Explorer

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

Theorem cncongr1 12241

Description: One direction of the bicondition in cncongr 12243. 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 9370	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 · 𝐶) ∈ ℤ)
2	1	3adant2 1018	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 · 𝐶) ∈ ℤ)
3		zmulcl 9370	. . . 4 ⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵 · 𝐶) ∈ ℤ)
4	3	3adant1 1017	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵 · 𝐶) ∈ ℤ)
5		simpl 109	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁))) → 𝑁 ∈ ℕ)
6		congr 12238	. . 3 ⊢ (((𝐴 · 𝐶) ∈ ℤ ∧ (𝐵 · 𝐶) ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐴 · 𝐶) mod 𝑁) = ((𝐵 · 𝐶) mod 𝑁) ↔ ∃𝑘 ∈ ℤ (𝑘 · 𝑁) = ((𝐴 · 𝐶) − (𝐵 · 𝐶))))
7	2, 4, 5, 6	syl2an3an 1309	. 2 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (((𝐴 · 𝐶) mod 𝑁) = ((𝐵 · 𝐶) mod 𝑁) ↔ ∃𝑘 ∈ ℤ (𝑘 · 𝑁) = ((𝐴 · 𝐶) − (𝐵 · 𝐶))))
8		simpl 109	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝐶 ∈ ℤ)
9		nnz 9336	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
10		nnne0 9010	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0)
11	9, 10	jca 306	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0))
12	11	adantl 277	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0))
13		eqidd 2194	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐶 gcd 𝑁) = (𝐶 gcd 𝑁))
14	8, 12, 13	3jca 1179	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐶 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐶 gcd 𝑁) = (𝐶 gcd 𝑁)))
15	14	ex 115	. . . . . . . . . 10 ⊢ (𝐶 ∈ ℤ → (𝑁 ∈ ℕ → (𝐶 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐶 gcd 𝑁) = (𝐶 gcd 𝑁))))
16	15	3ad2ant3 1022	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝑁 ∈ ℕ → (𝐶 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐶 gcd 𝑁) = (𝐶 gcd 𝑁))))
17	16	com12 30	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐶 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐶 gcd 𝑁) = (𝐶 gcd 𝑁))))
18	17	adantr 276	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁))) → ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐶 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐶 gcd 𝑁) = (𝐶 gcd 𝑁))))
19	18	impcom 125	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (𝐶 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐶 gcd 𝑁) = (𝐶 gcd 𝑁)))
20		divgcdcoprmex 12240	. . . . . 6 ⊢ ((𝐶 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐶 gcd 𝑁) = (𝐶 gcd 𝑁)) → ∃𝑟 ∈ ℤ ∃𝑠 ∈ ℤ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1))
21	19, 20	syl 14	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → ∃𝑟 ∈ ℤ ∃𝑠 ∈ ℤ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1))
22	21	adantr 276	. . . 4 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → ∃𝑟 ∈ ℤ ∃𝑠 ∈ ℤ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1))
23		oveq2 5926	. . . . . . . . . 10 ⊢ (𝑁 = ((𝐶 gcd 𝑁) · 𝑠) → (𝑘 · 𝑁) = (𝑘 · ((𝐶 gcd 𝑁) · 𝑠)))
24	23	3ad2ant2 1021	. . . . . . . . 9 ⊢ ((𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1) → (𝑘 · 𝑁) = (𝑘 · ((𝐶 gcd 𝑁) · 𝑠)))
25	24	adantl 277	. . . . . . . 8 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) → (𝑘 · 𝑁) = (𝑘 · ((𝐶 gcd 𝑁) · 𝑠)))
26		oveq2 5926	. . . . . . . . . . 11 ⊢ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) → (𝐴 · 𝐶) = (𝐴 · ((𝐶 gcd 𝑁) · 𝑟)))
27		oveq2 5926	. . . . . . . . . . 11 ⊢ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) → (𝐵 · 𝐶) = (𝐵 · ((𝐶 gcd 𝑁) · 𝑟)))
28	26, 27	oveq12d 5936	. . . . . . . . . 10 ⊢ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) → ((𝐴 · 𝐶) − (𝐵 · 𝐶)) = ((𝐴 · ((𝐶 gcd 𝑁) · 𝑟)) − (𝐵 · ((𝐶 gcd 𝑁) · 𝑟))))
29	28	3ad2ant1 1020	. . . . . . . . 9 ⊢ ((𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1) → ((𝐴 · 𝐶) − (𝐵 · 𝐶)) = ((𝐴 · ((𝐶 gcd 𝑁) · 𝑟)) − (𝐵 · ((𝐶 gcd 𝑁) · 𝑟))))
30	29	adantl 277	. . . . . . . 8 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) → ((𝐴 · 𝐶) − (𝐵 · 𝐶)) = ((𝐴 · ((𝐶 gcd 𝑁) · 𝑟)) − (𝐵 · ((𝐶 gcd 𝑁) · 𝑟))))
31	25, 30	eqeq12d 2208	. . . . . . 7 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) → ((𝑘 · 𝑁) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)) ↔ (𝑘 · ((𝐶 gcd 𝑁) · 𝑠)) = ((𝐴 · ((𝐶 gcd 𝑁) · 𝑟)) − (𝐵 · ((𝐶 gcd 𝑁) · 𝑟)))))
32		simpr 110	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℤ)
33	32	zcnd 9440	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℂ)
34	33	adantr 276	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝑘 ∈ ℂ)
35		simp3 1001	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐶 ∈ ℤ)
36	35	adantr 276	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → 𝐶 ∈ ℤ)
37	9	ad2antrl 490	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → 𝑁 ∈ ℤ)
38	36, 37	gcdcld 12105	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (𝐶 gcd 𝑁) ∈ ℕ₀)
39	38	nn0cnd 9295	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (𝐶 gcd 𝑁) ∈ ℂ)
40	39	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐶 gcd 𝑁) ∈ ℂ)
41		simpr 110	. . . . . . . . . . . . . 14 ⊢ ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ) → 𝑠 ∈ ℤ)
42	41	zcnd 9440	. . . . . . . . . . . . 13 ⊢ ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ) → 𝑠 ∈ ℂ)
43	42	adantl 277	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝑠 ∈ ℂ)
44	34, 40, 43	mul12d 8171	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝑘 · ((𝐶 gcd 𝑁) · 𝑠)) = ((𝐶 gcd 𝑁) · (𝑘 · 𝑠)))
45		simp1 999	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐴 ∈ ℤ)
46	45	zcnd 9440	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐴 ∈ ℂ)
47	46	ad3antrrr 492	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝐴 ∈ ℂ)
48	35	ad2antrr 488	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → 𝐶 ∈ ℤ)
49	5	nnzd 9438	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁))) → 𝑁 ∈ ℤ)
50	49	adantl 277	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → 𝑁 ∈ ℤ)
51	50	adantr 276	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → 𝑁 ∈ ℤ)
52	48, 51	gcdcld 12105	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → (𝐶 gcd 𝑁) ∈ ℕ₀)
53	52	nn0cnd 9295	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → (𝐶 gcd 𝑁) ∈ ℂ)
54	53	adantr 276	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐶 gcd 𝑁) ∈ ℂ)
55		simpl 109	. . . . . . . . . . . . . . 15 ⊢ ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ) → 𝑟 ∈ ℤ)
56	55	zcnd 9440	. . . . . . . . . . . . . 14 ⊢ ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ) → 𝑟 ∈ ℂ)
57	56	adantl 277	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝑟 ∈ ℂ)
58	47, 54, 57	mul12d 8171	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐴 · ((𝐶 gcd 𝑁) · 𝑟)) = ((𝐶 gcd 𝑁) · (𝐴 · 𝑟)))
59		simp2 1000	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐵 ∈ ℤ)
60	59	zcnd 9440	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐵 ∈ ℂ)
61	60	ad3antrrr 492	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝐵 ∈ ℂ)
62	36, 50	gcdcld 12105	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (𝐶 gcd 𝑁) ∈ ℕ₀)
63	62	nn0cnd 9295	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (𝐶 gcd 𝑁) ∈ ℂ)
64	63	ad2antrr 488	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐶 gcd 𝑁) ∈ ℂ)
65	61, 64, 57	mul12d 8171	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐵 · ((𝐶 gcd 𝑁) · 𝑟)) = ((𝐶 gcd 𝑁) · (𝐵 · 𝑟)))
66	58, 65	oveq12d 5936	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝐴 · ((𝐶 gcd 𝑁) · 𝑟)) − (𝐵 · ((𝐶 gcd 𝑁) · 𝑟))) = (((𝐶 gcd 𝑁) · (𝐴 · 𝑟)) − ((𝐶 gcd 𝑁) · (𝐵 · 𝑟))))
67	44, 66	eqeq12d 2208	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝑘 · ((𝐶 gcd 𝑁) · 𝑠)) = ((𝐴 · ((𝐶 gcd 𝑁) · 𝑟)) − (𝐵 · ((𝐶 gcd 𝑁) · 𝑟))) ↔ ((𝐶 gcd 𝑁) · (𝑘 · 𝑠)) = (((𝐶 gcd 𝑁) · (𝐴 · 𝑟)) − ((𝐶 gcd 𝑁) · (𝐵 · 𝑟)))))
68	45	ad3antrrr 492	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝐴 ∈ ℤ)
69	55	adantl 277	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝑟 ∈ ℤ)
70	68, 69	zmulcld 9445	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐴 · 𝑟) ∈ ℤ)
71	70	zcnd 9440	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐴 · 𝑟) ∈ ℂ)
72	59	ad3antrrr 492	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝐵 ∈ ℤ)
73	72, 69	zmulcld 9445	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐵 · 𝑟) ∈ ℤ)
74	73	zcnd 9440	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐵 · 𝑟) ∈ ℂ)
75	64, 71, 74	subdid 8433	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝐶 gcd 𝑁) · ((𝐴 · 𝑟) − (𝐵 · 𝑟))) = (((𝐶 gcd 𝑁) · (𝐴 · 𝑟)) − ((𝐶 gcd 𝑁) · (𝐵 · 𝑟))))
76	75	eqcomd 2199	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (((𝐶 gcd 𝑁) · (𝐴 · 𝑟)) − ((𝐶 gcd 𝑁) · (𝐵 · 𝑟))) = ((𝐶 gcd 𝑁) · ((𝐴 · 𝑟) − (𝐵 · 𝑟))))
77	76	eqeq2d 2205	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (((𝐶 gcd 𝑁) · (𝑘 · 𝑠)) = (((𝐶 gcd 𝑁) · (𝐴 · 𝑟)) − ((𝐶 gcd 𝑁) · (𝐵 · 𝑟))) ↔ ((𝐶 gcd 𝑁) · (𝑘 · 𝑠)) = ((𝐶 gcd 𝑁) · ((𝐴 · 𝑟) − (𝐵 · 𝑟)))))
78	32	adantr 276	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝑘 ∈ ℤ)
79		simprr 531	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝑠 ∈ ℤ)
80	78, 79	zmulcld 9445	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝑘 · 𝑠) ∈ ℤ)
81	80	zcnd 9440	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝑘 · 𝑠) ∈ ℂ)
82		zmulcl 9370	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℤ ∧ 𝑟 ∈ ℤ) → (𝐴 · 𝑟) ∈ ℤ)
83	82	ad2ant2r 509	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐴 · 𝑟) ∈ ℤ)
84		zmulcl 9370	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ ℤ ∧ 𝑟 ∈ ℤ) → (𝐵 · 𝑟) ∈ ℤ)
85	84	ad2ant2lr 510	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐵 · 𝑟) ∈ ℤ)
86	83, 85	zsubcld 9444	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝐴 · 𝑟) − (𝐵 · 𝑟)) ∈ ℤ)
87	86	zcnd 9440	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝐴 · 𝑟) − (𝐵 · 𝑟)) ∈ ℂ)
88	87	ex 115	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ) → ((𝐴 · 𝑟) − (𝐵 · 𝑟)) ∈ ℂ))
89	88	3adant3 1019	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ) → ((𝐴 · 𝑟) − (𝐵 · 𝑟)) ∈ ℂ))
90	89	ad2antrr 488	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ) → ((𝐴 · 𝑟) − (𝐵 · 𝑟)) ∈ ℂ))
91	90	imp 124	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝐴 · 𝑟) − (𝐵 · 𝑟)) ∈ ℂ)
92	10	ad2antrl 490	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → 𝑁 ≠ 0)
93		gcd2n0cl 12106	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐶 gcd 𝑁) ∈ ℕ)
94	36, 50, 92, 93	syl3anc 1249	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (𝐶 gcd 𝑁) ∈ ℕ)
95	94	nnne0d 9027	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (𝐶 gcd 𝑁) ≠ 0)
96	95	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐶 gcd 𝑁) ≠ 0)
97	52	adantr 276	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐶 gcd 𝑁) ∈ ℕ₀)
98	97	nn0zd 9437	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐶 gcd 𝑁) ∈ ℤ)
99		0zd 9329	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 0 ∈ ℤ)
100		zapne 9391	. . . . . . . . . . . . 13 ⊢ (((𝐶 gcd 𝑁) ∈ ℤ ∧ 0 ∈ ℤ) → ((𝐶 gcd 𝑁) # 0 ↔ (𝐶 gcd 𝑁) ≠ 0))
101	98, 99, 100	syl2anc 411	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝐶 gcd 𝑁) # 0 ↔ (𝐶 gcd 𝑁) ≠ 0))
102	96, 101	mpbird 167	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐶 gcd 𝑁) # 0)
103	81, 91, 64, 102	mulcanapd 8680	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (((𝐶 gcd 𝑁) · (𝑘 · 𝑠)) = ((𝐶 gcd 𝑁) · ((𝐴 · 𝑟) − (𝐵 · 𝑟))) ↔ (𝑘 · 𝑠) = ((𝐴 · 𝑟) − (𝐵 · 𝑟))))
104	67, 77, 103	3bitrd 214	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝑘 · ((𝐶 gcd 𝑁) · 𝑠)) = ((𝐴 · ((𝐶 gcd 𝑁) · 𝑟)) − (𝐵 · ((𝐶 gcd 𝑁) · 𝑟))) ↔ (𝑘 · 𝑠) = ((𝐴 · 𝑟) − (𝐵 · 𝑟))))
105	104	adantr 276	. . . . . . . 8 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) → ((𝑘 · ((𝐶 gcd 𝑁) · 𝑠)) = ((𝐴 · ((𝐶 gcd 𝑁) · 𝑟)) − (𝐵 · ((𝐶 gcd 𝑁) · 𝑟))) ↔ (𝑘 · 𝑠) = ((𝐴 · 𝑟) − (𝐵 · 𝑟))))
106		zcn 9322	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℂ)
107		zcn 9322	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ ℤ → 𝐵 ∈ ℂ)
108	106, 107	anim12i 338	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ))
109	108	3adant3 1019	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ))
110	109	ad2antrr 488	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ))
111	110, 56	anim12i 338	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑟 ∈ ℂ))
112		df-3an 982	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑟 ∈ ℂ) ↔ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑟 ∈ ℂ))
113	111, 112	sylibr 134	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑟 ∈ ℂ))
114		subdir 8405	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑟 ∈ ℂ) → ((𝐴 − 𝐵) · 𝑟) = ((𝐴 · 𝑟) − (𝐵 · 𝑟)))
115	113, 114	syl 14	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝐴 − 𝐵) · 𝑟) = ((𝐴 · 𝑟) − (𝐵 · 𝑟)))
116	115	eqcomd 2199	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝐴 · 𝑟) − (𝐵 · 𝑟)) = ((𝐴 − 𝐵) · 𝑟))
117	116	adantr 276	. . . . . . . . . 10 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) → ((𝐴 · 𝑟) − (𝐵 · 𝑟)) = ((𝐴 − 𝐵) · 𝑟))
118	117	eqeq2d 2205	. . . . . . . . 9 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) → ((𝑘 · 𝑠) = ((𝐴 · 𝑟) − (𝐵 · 𝑟)) ↔ (𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟)))
119	5	nncnd 8996	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁))) → 𝑁 ∈ ℂ)
120	119	adantl 277	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → 𝑁 ∈ ℂ)
121	120	ad2antrr 488	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝑁 ∈ ℂ)
122	79	zcnd 9440	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝑠 ∈ ℂ)
123	121, 122, 40, 102	divmulap2d 8843	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝑁 / (𝐶 gcd 𝑁)) = 𝑠 ↔ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠)))
124		simpll 527	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ))
125	69	adantr 276	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → 𝑟 ∈ ℤ)
126	5	adantl 277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → 𝑁 ∈ ℕ)
127		divgcdnnr 12113	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℕ ∧ 𝐶 ∈ ℤ) → (𝑁 / (𝐶 gcd 𝑁)) ∈ ℕ)
128	126, 36, 127	syl2anc 411	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (𝑁 / (𝐶 gcd 𝑁)) ∈ ℕ)
129	128	ad3antrrr 492	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → (𝑁 / (𝐶 gcd 𝑁)) ∈ ℕ)
130		eleq1 2256	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 = (𝑁 / (𝐶 gcd 𝑁)) → (𝑠 ∈ ℕ ↔ (𝑁 / (𝐶 gcd 𝑁)) ∈ ℕ))
131	130	eqcoms 2196	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 / (𝐶 gcd 𝑁)) = 𝑠 → (𝑠 ∈ ℕ ↔ (𝑁 / (𝐶 gcd 𝑁)) ∈ ℕ))
132	131	adantl 277	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → (𝑠 ∈ ℕ ↔ (𝑁 / (𝐶 gcd 𝑁)) ∈ ℕ))
133	129, 132	mpbird 167	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → 𝑠 ∈ ℕ)
134	125, 133	jca 306	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))
135	124, 134	jca 306	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)))
136		simpr 110	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → (𝑁 / (𝐶 gcd 𝑁)) = 𝑠)
137		nnz 9336	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑠 ∈ ℕ → 𝑠 ∈ ℤ)
138	137	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ) → 𝑠 ∈ ℤ)
139	138	anim2i 342	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) → (𝑘 ∈ ℤ ∧ 𝑠 ∈ ℤ))
140	139	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝑘 ∈ ℤ ∧ 𝑠 ∈ ℤ))
141		dvdsmul2 11957	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑘 ∈ ℤ ∧ 𝑠 ∈ ℤ) → 𝑠 ∥ (𝑘 · 𝑠))
142	140, 141	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → 𝑠 ∥ (𝑘 · 𝑠))
143		breq2 4033	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝑠 ∥ (𝑘 · 𝑠) ↔ 𝑠 ∥ ((𝐴 − 𝐵) · 𝑟)))
144		zsubcl 9358	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 − 𝐵) ∈ ℤ)
145	144	zcnd 9440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 − 𝐵) ∈ ℂ)
146	145	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝐴 − 𝐵) ∈ ℂ)
147		zcn 9322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑟 ∈ ℤ → 𝑟 ∈ ℂ)
148	147	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) → 𝑟 ∈ ℂ)
149	148	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → 𝑟 ∈ ℂ)
150	146, 149	mulcomd 8041	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → ((𝐴 − 𝐵) · 𝑟) = (𝑟 · (𝐴 − 𝐵)))
151	150	breq2d 4041	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝑠 ∥ ((𝐴 − 𝐵) · 𝑟) ↔ 𝑠 ∥ (𝑟 · (𝐴 − 𝐵))))
152	137	anim2i 342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ) → (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ))
153		gcdcom 12110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ) → (𝑟 gcd 𝑠) = (𝑠 gcd 𝑟))
154	152, 153	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ) → (𝑟 gcd 𝑠) = (𝑠 gcd 𝑟))
155	154	eqeq1d 2202	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ) → ((𝑟 gcd 𝑠) = 1 ↔ (𝑠 gcd 𝑟) = 1))
156	155	ad2antll 491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → ((𝑟 gcd 𝑠) = 1 ↔ (𝑠 gcd 𝑟) = 1))
157	152	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) → (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ))
158	157	ancomd 267	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) → (𝑠 ∈ ℤ ∧ 𝑟 ∈ ℤ))
159	144, 158	anim12i 338	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → ((𝐴 − 𝐵) ∈ ℤ ∧ (𝑠 ∈ ℤ ∧ 𝑟 ∈ ℤ)))
160	159	ancomd 267	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → ((𝑠 ∈ ℤ ∧ 𝑟 ∈ ℤ) ∧ (𝐴 − 𝐵) ∈ ℤ))
161		df-3an 982	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑠 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ (𝐴 − 𝐵) ∈ ℤ) ↔ ((𝑠 ∈ ℤ ∧ 𝑟 ∈ ℤ) ∧ (𝐴 − 𝐵) ∈ ℤ))
162	160, 161	sylibr 134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝑠 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ (𝐴 − 𝐵) ∈ ℤ))
163		coprmdvds 12230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑠 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ (𝐴 − 𝐵) ∈ ℤ) → ((𝑠 ∥ (𝑟 · (𝐴 − 𝐵)) ∧ (𝑠 gcd 𝑟) = 1) → 𝑠 ∥ (𝐴 − 𝐵)))
164	162, 163	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → ((𝑠 ∥ (𝑟 · (𝐴 − 𝐵)) ∧ (𝑠 gcd 𝑟) = 1) → 𝑠 ∥ (𝐴 − 𝐵)))
165		simprr 531	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) → 𝑠 ∈ ℕ)
166	165	anim2i 342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑠 ∈ ℕ))
167	166	ancomd 267	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝑠 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)))
168		3anass 984	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑠 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ↔ (𝑠 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)))
169	167, 168	sylibr 134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝑠 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ))
170		moddvds 11942	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑠 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 mod 𝑠) = (𝐵 mod 𝑠) ↔ 𝑠 ∥ (𝐴 − 𝐵)))
171	169, 170	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → ((𝐴 mod 𝑠) = (𝐵 mod 𝑠) ↔ 𝑠 ∥ (𝐴 − 𝐵)))
172	164, 171	sylibrd 169	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → ((𝑠 ∥ (𝑟 · (𝐴 − 𝐵)) ∧ (𝑠 gcd 𝑟) = 1) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))
173	172	expcomd 1452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → ((𝑠 gcd 𝑟) = 1 → (𝑠 ∥ (𝑟 · (𝐴 − 𝐵)) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠))))
174	156, 173	sylbid 150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → ((𝑟 gcd 𝑠) = 1 → (𝑠 ∥ (𝑟 · (𝐴 − 𝐵)) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠))))
175	174	com23 78	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝑠 ∥ (𝑟 · (𝐴 − 𝐵)) → ((𝑟 gcd 𝑠) = 1 → (𝐴 mod 𝑠) = (𝐵 mod 𝑠))))
176	151, 175	sylbid 150	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝑠 ∥ ((𝐴 − 𝐵) · 𝑟) → ((𝑟 gcd 𝑠) = 1 → (𝐴 mod 𝑠) = (𝐵 mod 𝑠))))
177	176	com3l 81	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑠 ∥ ((𝐴 − 𝐵) · 𝑟) → ((𝑟 gcd 𝑠) = 1 → (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠))))
178	143, 177	biimtrdi 163	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝑠 ∥ (𝑘 · 𝑠) → ((𝑟 gcd 𝑠) = 1 → (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))))
179	178	com14 88	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝑠 ∥ (𝑘 · 𝑠) → ((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))))
180	142, 179	mpd 13	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → ((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠))))
181	180	ex 115	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) → ((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))))
182	181	3adant3 1019	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) → ((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))))
183	182	adantr 276	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → ((𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) → ((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))))
184	183	impl 380	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) → ((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠))))
185	184	adantr 276	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → ((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠))))
186	185	imp 124	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) ∧ (𝑟 gcd 𝑠) = 1) → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))
187		eqtr2 2212	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑁 / (𝐶 gcd 𝑁)) = 𝑀 ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → 𝑀 = 𝑠)
188		oveq2 5926	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑀 = 𝑠 → (𝐴 mod 𝑀) = (𝐴 mod 𝑠))
189		oveq2 5926	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑀 = 𝑠 → (𝐵 mod 𝑀) = (𝐵 mod 𝑠))
190	188, 189	eqeq12d 2208	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑀 = 𝑠 → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) ↔ (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))
191	187, 190	syl 14	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑁 / (𝐶 gcd 𝑁)) = 𝑀 ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) ↔ (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))
192	191	ex 115	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 / (𝐶 gcd 𝑁)) = 𝑀 → ((𝑁 / (𝐶 gcd 𝑁)) = 𝑠 → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) ↔ (𝐴 mod 𝑠) = (𝐵 mod 𝑠))))
193	192	eqcoms 2196	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 = (𝑁 / (𝐶 gcd 𝑁)) → ((𝑁 / (𝐶 gcd 𝑁)) = 𝑠 → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) ↔ (𝐴 mod 𝑠) = (𝐵 mod 𝑠))))
194	193	ad2antll 491	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → ((𝑁 / (𝐶 gcd 𝑁)) = 𝑠 → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) ↔ (𝐴 mod 𝑠) = (𝐵 mod 𝑠))))
195	194	ad2antrr 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) → ((𝑁 / (𝐶 gcd 𝑁)) = 𝑠 → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) ↔ (𝐴 mod 𝑠) = (𝐵 mod 𝑠))))
196	195	imp 124	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) ↔ (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))
197	196	adantr 276	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) ∧ (𝑟 gcd 𝑠) = 1) → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) ↔ (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))
198	186, 197	sylibrd 169	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) ∧ (𝑟 gcd 𝑠) = 1) → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀)))
199	198	ex 115	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → ((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀))))
200	135, 136, 199	syl2anc 411	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → ((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀))))
201	200	ex 115	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝑁 / (𝐶 gcd 𝑁)) = 𝑠 → ((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀)))))
202	123, 201	sylbird 170	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝑁 = ((𝐶 gcd 𝑁) · 𝑠) → ((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀)))))
203	202	com3l 81	. . . . . . . . . . . 12 ⊢ (𝑁 = ((𝐶 gcd 𝑁) · 𝑠) → ((𝑟 gcd 𝑠) = 1 → (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀)))))
204	203	a1i 9	. . . . . . . . . . 11 ⊢ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) → (𝑁 = ((𝐶 gcd 𝑁) · 𝑠) → ((𝑟 gcd 𝑠) = 1 → (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀))))))
205	204	3imp 1195	. . . . . . . . . 10 ⊢ ((𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1) → (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀))))
206	205	impcom 125	. . . . . . . . 9 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀)))
207	118, 206	sylbid 150	. . . . . . . 8 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) → ((𝑘 · 𝑠) = ((𝐴 · 𝑟) − (𝐵 · 𝑟)) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀)))
208	105, 207	sylbid 150	. . . . . . 7 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) → ((𝑘 · ((𝐶 gcd 𝑁) · 𝑠)) = ((𝐴 · ((𝐶 gcd 𝑁) · 𝑟)) − (𝐵 · ((𝐶 gcd 𝑁) · 𝑟))) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀)))
209	31, 208	sylbid 150	. . . . . 6 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) → ((𝑘 · 𝑁) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀)))
210	209	ex 115	. . . . 5 ⊢ (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1) → ((𝑘 · 𝑁) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀))))
211	210	rexlimdvva 2619	. . . 4 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → (∃𝑟 ∈ ℤ ∃𝑠 ∈ ℤ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1) → ((𝑘 · 𝑁) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀))))
212	22, 211	mpd 13	. . 3 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → ((𝑘 · 𝑁) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀)))
213	212	rexlimdva 2611	. 2 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (∃𝑘 ∈ ℤ (𝑘 · 𝑁) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀)))
214	7, 213	sylbid 150	1 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (((𝐴 · 𝐶) mod 𝑁) = ((𝐵 · 𝐶) mod 𝑁) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀)))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∧ w3a 980 = wceq 1364 ∈ wcel 2164 ≠ wne 2364 ∃wrex 2473 class class class wbr 4029 (class class class)co 5918 ℂcc 7870 0cc0 7872 1c1 7873 · cmul 7877 − cmin 8190 # cap 8600 / cdiv 8691 ℕcn 8982 ℕ₀cn0 9240 ℤcz 9317 mod cmo 10393 ∥ cdvds 11930 gcd cgcd 12079

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2166 ax-14 2167 ax-ext 2175 ax-coll 4144 ax-sep 4147 ax-nul 4155 ax-pow 4203 ax-pr 4238 ax-un 4464 ax-setind 4569 ax-iinf 4620 ax-cnex 7963 ax-resscn 7964 ax-1cn 7965 ax-1re 7966 ax-icn 7967 ax-addcl 7968 ax-addrcl 7969 ax-mulcl 7970 ax-mulrcl 7971 ax-addcom 7972 ax-mulcom 7973 ax-addass 7974 ax-mulass 7975 ax-distr 7976 ax-i2m1 7977 ax-0lt1 7978 ax-1rid 7979 ax-0id 7980 ax-rnegex 7981 ax-precex 7982 ax-cnre 7983 ax-pre-ltirr 7984 ax-pre-ltwlin 7985 ax-pre-lttrn 7986 ax-pre-apti 7987 ax-pre-ltadd 7988 ax-pre-mulgt0 7989 ax-pre-mulext 7990 ax-arch 7991 ax-caucvg 7992

This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2045 df-mo 2046 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ne 2365 df-nel 2460 df-ral 2477 df-rex 2478 df-reu 2479 df-rmo 2480 df-rab 2481 df-v 2762 df-sbc 2986 df-csb 3081 df-dif 3155 df-un 3157 df-in 3159 df-ss 3166 df-nul 3447 df-if 3558 df-pw 3603 df-sn 3624 df-pr 3625 df-op 3627 df-uni 3836 df-int 3871 df-iun 3914 df-br 4030 df-opab 4091 df-mpt 4092 df-tr 4128 df-id 4324 df-po 4327 df-iso 4328 df-iord 4397 df-on 4399 df-ilim 4400 df-suc 4402 df-iom 4623 df-xp 4665 df-rel 4666 df-cnv 4667 df-co 4668 df-dm 4669 df-rn 4670 df-res 4671 df-ima 4672 df-iota 5215 df-fun 5256 df-fn 5257 df-f 5258 df-f1 5259 df-fo 5260 df-f1o 5261 df-fv 5262 df-riota 5873 df-ov 5921 df-oprab 5922 df-mpo 5923 df-1st 6193 df-2nd 6194 df-recs 6358 df-frec 6444 df-sup 7043 df-pnf 8056 df-mnf 8057 df-xr 8058 df-ltxr 8059 df-le 8060 df-sub 8192 df-neg 8193 df-reap 8594 df-ap 8601 df-div 8692 df-inn 8983 df-2 9041 df-3 9042 df-4 9043 df-n0 9241 df-z 9318 df-uz 9593 df-q 9685 df-rp 9720 df-fz 10075 df-fzo 10209 df-fl 10339 df-mod 10394 df-seqfrec 10519 df-exp 10610 df-cj 10986 df-re 10987 df-im 10988 df-rsqrt 11142 df-abs 11143 df-dvds 11931 df-gcd 12080

This theorem is referenced by: cncongr 12243

W3C validator