dvdsmulf1o - Metamath Proof Explorer

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

Theorem dvdsmulf1o 27181

Description: If 𝑀 and 𝑁 are two coprime integers, multiplication forms a bijection from the set of pairs ⟨𝑗, 𝑘⟩ where 𝑗 ∥ 𝑀 and 𝑘 ∥ 𝑁, to the set of divisors of 𝑀 · 𝑁. (Contributed by Mario Carneiro, 2-Jul-2015.)

**Hypotheses**
Ref	Expression
dvdsmulf1o.1	⊢ (𝜑 → 𝑀 ∈ ℕ)
dvdsmulf1o.2	⊢ (𝜑 → 𝑁 ∈ ℕ)
dvdsmulf1o.3	⊢ (𝜑 → (𝑀 gcd 𝑁) = 1)
dvdsmulf1o.x	⊢ 𝑋 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀}
dvdsmulf1o.y	⊢ 𝑌 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}
dvdsmulf1o.z	⊢ 𝑍 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑀 · 𝑁)}

**Assertion**
Ref	Expression
dvdsmulf1o	⊢ (𝜑 → ( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1-onto→𝑍)

Distinct variable groups: 𝑥,𝑀 𝑥,𝑁 Allowed substitution hints: 𝜑(𝑥) 𝑋(𝑥) 𝑌(𝑥) 𝑍(𝑥)

Proof of Theorem dvdsmulf1o Dummy variables 𝑖 𝑢 𝑗 𝑚 𝑛 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-mulf 11113	. . . . . . 7 ⊢ · :(ℂ × ℂ)⟶ℂ
2		ffn 6659	. . . . . . 7 ⊢ ( · :(ℂ × ℂ)⟶ℂ → · Fn (ℂ × ℂ))
3	1, 2	ax-mp 5	. . . . . 6 ⊢ · Fn (ℂ × ℂ)
4		dvdsmulf1o.x	. . . . . . . . 9 ⊢ 𝑋 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀}
5	4	ssrab3 4016	. . . . . . . 8 ⊢ 𝑋 ⊆ ℕ
6		nnsscn 12174	. . . . . . . 8 ⊢ ℕ ⊆ ℂ
7	5, 6	sstri 3926	. . . . . . 7 ⊢ 𝑋 ⊆ ℂ
8		dvdsmulf1o.y	. . . . . . . . 9 ⊢ 𝑌 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}
9	8	ssrab3 4016	. . . . . . . 8 ⊢ 𝑌 ⊆ ℕ
10	9, 6	sstri 3926	. . . . . . 7 ⊢ 𝑌 ⊆ ℂ
11		xpss12 5636	. . . . . . 7 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑌 ⊆ ℂ) → (𝑋 × 𝑌) ⊆ (ℂ × ℂ))
12	7, 10, 11	mp2an 699	. . . . . 6 ⊢ (𝑋 × 𝑌) ⊆ (ℂ × ℂ)
13		fnssres 6612	. . . . . 6 ⊢ (( · Fn (ℂ × ℂ) ∧ (𝑋 × 𝑌) ⊆ (ℂ × ℂ)) → ( · ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌))
14	3, 12, 13	mp2an 699	. . . . 5 ⊢ ( · ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌)
15	14	a1i 11	. . . 4 ⊢ (𝜑 → ( · ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌))
16		ovres 7526	. . . . . . 7 ⊢ ((𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌) → (𝑖( · ↾ (𝑋 × 𝑌))𝑗) = (𝑖 · 𝑗))
17	16	adantl 483	. . . . . 6 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖( · ↾ (𝑋 × 𝑌))𝑗) = (𝑖 · 𝑗))
18		breq1 5078	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → (𝑥 ∥ 𝑀 ↔ 𝑖 ∥ 𝑀))
19	18, 4	elrab2 3634	. . . . . . . . . 10 ⊢ (𝑖 ∈ 𝑋 ↔ (𝑖 ∈ ℕ ∧ 𝑖 ∥ 𝑀))
20	19	simplbi 498	. . . . . . . . 9 ⊢ (𝑖 ∈ 𝑋 → 𝑖 ∈ ℕ)
21	20	ad2antrl 735	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑖 ∈ ℕ)
22		breq1 5078	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑗 → (𝑥 ∥ 𝑁 ↔ 𝑗 ∥ 𝑁))
23	22, 8	elrab2 3634	. . . . . . . . . 10 ⊢ (𝑗 ∈ 𝑌 ↔ (𝑗 ∈ ℕ ∧ 𝑗 ∥ 𝑁))
24	23	simplbi 498	. . . . . . . . 9 ⊢ (𝑗 ∈ 𝑌 → 𝑗 ∈ ℕ)
25	24	ad2antll 736	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑗 ∈ ℕ)
26	21, 25	nnmulcld 12225	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 · 𝑗) ∈ ℕ)
27	23	simprbi 499	. . . . . . . . 9 ⊢ (𝑗 ∈ 𝑌 → 𝑗 ∥ 𝑁)
28	27	ad2antll 736	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑗 ∥ 𝑁)
29	19	simprbi 499	. . . . . . . . 9 ⊢ (𝑖 ∈ 𝑋 → 𝑖 ∥ 𝑀)
30	29	ad2antrl 735	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑖 ∥ 𝑀)
31	25	nnzd 12545	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑗 ∈ ℤ)
32		dvdsmulf1o.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℕ)
33	32	adantr 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑁 ∈ ℕ)
34	33	nnzd 12545	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑁 ∈ ℤ)
35	21	nnzd 12545	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑖 ∈ ℤ)
36		dvdscmul 16246	. . . . . . . . . 10 ⊢ ((𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑗 ∥ 𝑁 → (𝑖 · 𝑗) ∥ (𝑖 · 𝑁)))
37	31, 34, 35, 36	syl3anc 1380	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑗 ∥ 𝑁 → (𝑖 · 𝑗) ∥ (𝑖 · 𝑁)))
38		dvdsmulf1o.1	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℕ)
39	38	adantr 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑀 ∈ ℕ)
40	39	nnzd 12545	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑀 ∈ ℤ)
41		dvdsmulc 16247	. . . . . . . . . 10 ⊢ ((𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∥ 𝑀 → (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)))
42	35, 40, 34, 41	syl3anc 1380	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 ∥ 𝑀 → (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)))
43	26	nnzd 12545	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 · 𝑗) ∈ ℤ)
44	35, 34	zmulcld 12634	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 · 𝑁) ∈ ℤ)
45	40, 34	zmulcld 12634	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑀 · 𝑁) ∈ ℤ)
46		dvdstr 16258	. . . . . . . . . 10 ⊢ (((𝑖 · 𝑗) ∈ ℤ ∧ (𝑖 · 𝑁) ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) → (((𝑖 · 𝑗) ∥ (𝑖 · 𝑁) ∧ (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
47	43, 44, 45, 46	syl3anc 1380	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (((𝑖 · 𝑗) ∥ (𝑖 · 𝑁) ∧ (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
48	37, 42, 47	syl2and 615	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → ((𝑗 ∥ 𝑁 ∧ 𝑖 ∥ 𝑀) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
49	28, 30, 48	mp2and 706	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁))
50		breq1 5078	. . . . . . . 8 ⊢ (𝑥 = (𝑖 · 𝑗) → (𝑥 ∥ (𝑀 · 𝑁) ↔ (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
51		dvdsmulf1o.z	. . . . . . . 8 ⊢ 𝑍 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑀 · 𝑁)}
52	50, 51	elrab2 3634	. . . . . . 7 ⊢ ((𝑖 · 𝑗) ∈ 𝑍 ↔ ((𝑖 · 𝑗) ∈ ℕ ∧ (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
53	26, 49, 52	sylanbrc 590	. . . . . 6 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 · 𝑗) ∈ 𝑍)
54	17, 53	eqeltrd 2841	. . . . 5 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖( · ↾ (𝑋 × 𝑌))𝑗) ∈ 𝑍)
55	54	ralrimivva 3184	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑌 (𝑖( · ↾ (𝑋 × 𝑌))𝑗) ∈ 𝑍)
56		ffnov 7486	. . . 4 ⊢ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍 ↔ (( · ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑌 (𝑖( · ↾ (𝑋 × 𝑌))𝑗) ∈ 𝑍))
57	15, 55, 56	sylanbrc 590	. . 3 ⊢ (𝜑 → ( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍)
58	21	adantr 482	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℕ)
59	58	nnnn0d 12493	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℕ₀)
60		simprll 785	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ 𝑋)
61		breq1 5078	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑚 → (𝑥 ∥ 𝑀 ↔ 𝑚 ∥ 𝑀))
62	61, 4	elrab2 3634	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ 𝑋 ↔ (𝑚 ∈ ℕ ∧ 𝑚 ∥ 𝑀))
63	62	simplbi 498	. . . . . . . . . . 11 ⊢ (𝑚 ∈ 𝑋 → 𝑚 ∈ ℕ)
64	60, 63	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℕ)
65	64	nnnn0d 12493	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℕ₀)
66	58	nnzd 12545	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℤ)
67	25	adantr 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∈ ℕ)
68	67	nnzd 12545	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∈ ℤ)
69		dvdsmul1 16241	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ) → 𝑖 ∥ (𝑖 · 𝑗))
70	66, 68, 69	syl2anc 591	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∥ (𝑖 · 𝑗))
71		simprr 779	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑚 · 𝑛))
72	7, 60	sselid 3915	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℂ)
73		simprlr 786	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ 𝑌)
74		breq1 5078	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑛 → (𝑥 ∥ 𝑁 ↔ 𝑛 ∥ 𝑁))
75	74, 8	elrab2 3634	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ 𝑌 ↔ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝑁))
76	75	simplbi 498	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ 𝑌 → 𝑛 ∈ ℕ)
77	73, 76	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ ℕ)
78	77	nncnd 12185	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ ℂ)
79	72, 78	mulcomd 11161	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 · 𝑛) = (𝑛 · 𝑚))
80	71, 79	eqtrd 2776	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑛 · 𝑚))
81	70, 80	breqtrd 5101	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∥ (𝑛 · 𝑚))
82	77	nnzd 12545	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ ℤ)
83	34	adantr 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑁 ∈ ℤ)
84	66, 83	gcdcomd 16478	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 gcd 𝑁) = (𝑁 gcd 𝑖))
85	40	adantr 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑀 ∈ ℤ)
86	32	nnzd 12545	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℤ)
87	38	nnzd 12545	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℤ)
88	86, 87	gcdcomd 16478	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 gcd 𝑀) = (𝑀 gcd 𝑁))
89		dvdsmulf1o.3	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1)
90	88, 89	eqtrd 2776	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 gcd 𝑀) = 1)
91	90	ad2antrr 733	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑁 gcd 𝑀) = 1)
92	30	adantr 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∥ 𝑀)
93		rpdvds 16624	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ((𝑁 gcd 𝑀) = 1 ∧ 𝑖 ∥ 𝑀)) → (𝑁 gcd 𝑖) = 1)
94	83, 66, 85, 91, 92, 93	syl32anc 1387	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑁 gcd 𝑖) = 1)
95	84, 94	eqtrd 2776	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 gcd 𝑁) = 1)
96	75	simprbi 499	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ 𝑌 → 𝑛 ∥ 𝑁)
97	73, 96	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∥ 𝑁)
98		rpdvds 16624	. . . . . . . . . . 11 ⊢ (((𝑖 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑖 gcd 𝑁) = 1 ∧ 𝑛 ∥ 𝑁)) → (𝑖 gcd 𝑛) = 1)
99	66, 82, 83, 95, 97, 98	syl32anc 1387	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 gcd 𝑛) = 1)
100	64	nnzd 12545	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℤ)
101		coprmdvds 16617	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ) → ((𝑖 ∥ (𝑛 · 𝑚) ∧ (𝑖 gcd 𝑛) = 1) → 𝑖 ∥ 𝑚))
102	66, 82, 100, 101	syl3anc 1380	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → ((𝑖 ∥ (𝑛 · 𝑚) ∧ (𝑖 gcd 𝑛) = 1) → 𝑖 ∥ 𝑚))
103	81, 99, 102	mp2and 706	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∥ 𝑚)
104		dvdsmul1 16241	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 𝑚 ∥ (𝑚 · 𝑛))
105	100, 82, 104	syl2anc 591	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∥ (𝑚 · 𝑛))
106	58	nncnd 12185	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℂ)
107	67	nncnd 12185	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∈ ℂ)
108	106, 107	mulcomd 11161	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑗 · 𝑖))
109	71, 108	eqtr3d 2778	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 · 𝑛) = (𝑗 · 𝑖))
110	105, 109	breqtrd 5101	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∥ (𝑗 · 𝑖))
111	100, 83	gcdcomd 16478	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 gcd 𝑁) = (𝑁 gcd 𝑚))
112	62	simprbi 499	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ 𝑋 → 𝑚 ∥ 𝑀)
113	60, 112	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∥ 𝑀)
114		rpdvds 16624	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ((𝑁 gcd 𝑀) = 1 ∧ 𝑚 ∥ 𝑀)) → (𝑁 gcd 𝑚) = 1)
115	83, 100, 85, 91, 113, 114	syl32anc 1387	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑁 gcd 𝑚) = 1)
116	111, 115	eqtrd 2776	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 gcd 𝑁) = 1)
117	28	adantr 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∥ 𝑁)
118		rpdvds 16624	. . . . . . . . . . 11 ⊢ (((𝑚 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑚 gcd 𝑁) = 1 ∧ 𝑗 ∥ 𝑁)) → (𝑚 gcd 𝑗) = 1)
119	100, 68, 83, 116, 117, 118	syl32anc 1387	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 gcd 𝑗) = 1)
120		coprmdvds 16617	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑖 ∈ ℤ) → ((𝑚 ∥ (𝑗 · 𝑖) ∧ (𝑚 gcd 𝑗) = 1) → 𝑚 ∥ 𝑖))
121	100, 68, 66, 120	syl3anc 1380	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → ((𝑚 ∥ (𝑗 · 𝑖) ∧ (𝑚 gcd 𝑗) = 1) → 𝑚 ∥ 𝑖))
122	110, 119, 121	mp2and 706	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∥ 𝑖)
123		dvdseq 16278	. . . . . . . . 9 ⊢ (((𝑖 ∈ ℕ₀ ∧ 𝑚 ∈ ℕ₀) ∧ (𝑖 ∥ 𝑚 ∧ 𝑚 ∥ 𝑖)) → 𝑖 = 𝑚)
124	59, 65, 103, 122, 123	syl22anc 845	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 = 𝑚)
125	58	nnne0d 12222	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ≠ 0)
126	124	oveq1d 7375	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑛) = (𝑚 · 𝑛))
127	71, 126	eqtr4d 2779	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑖 · 𝑛))
128	107, 78, 106, 125, 127	mulcanad 11780	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 = 𝑛)
129	124, 128	opeq12d 4815	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩)
130	129	expr 458	. . . . . 6 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌)) → ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
131	130	ralrimivva 3184	. . . . 5 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
132	131	ralrimivva 3184	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑌 ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
133		fvres 6850	. . . . . . . . 9 ⊢ (𝑢 ∈ (𝑋 × 𝑌) → (( · ↾ (𝑋 × 𝑌))‘𝑢) = ( · ‘𝑢))
134		fvres 6850	. . . . . . . . 9 ⊢ (𝑣 ∈ (𝑋 × 𝑌) → (( · ↾ (𝑋 × 𝑌))‘𝑣) = ( · ‘𝑣))
135	133, 134	eqeqan12d 2755	. . . . . . . 8 ⊢ ((𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) → ((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) ↔ ( · ‘𝑢) = ( · ‘𝑣)))
136	135	imbi1d 343	. . . . . . 7 ⊢ ((𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) → (((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ (( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣)))
137	136	ralbidva 3162	. . . . . 6 ⊢ (𝑢 ∈ (𝑋 × 𝑌) → (∀𝑣 ∈ (𝑋 × 𝑌)((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑣 ∈ (𝑋 × 𝑌)(( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣)))
138	137	ralbiia 3085	. . . . 5 ⊢ (∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)(( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣))
139		fveq2 6831	. . . . . . . . . . 11 ⊢ (𝑣 = ⟨𝑚, 𝑛⟩ → ( · ‘𝑣) = ( · ‘⟨𝑚, 𝑛⟩))
140		df-ov 7363	. . . . . . . . . . 11 ⊢ (𝑚 · 𝑛) = ( · ‘⟨𝑚, 𝑛⟩)
141	139, 140	eqtr4di 2794	. . . . . . . . . 10 ⊢ (𝑣 = ⟨𝑚, 𝑛⟩ → ( · ‘𝑣) = (𝑚 · 𝑛))
142	141	eqeq2d 2752	. . . . . . . . 9 ⊢ (𝑣 = ⟨𝑚, 𝑛⟩ → (( · ‘𝑢) = ( · ‘𝑣) ↔ ( · ‘𝑢) = (𝑚 · 𝑛)))
143		eqeq2 2753	. . . . . . . . 9 ⊢ (𝑣 = ⟨𝑚, 𝑛⟩ → (𝑢 = 𝑣 ↔ 𝑢 = ⟨𝑚, 𝑛⟩))
144	142, 143	imbi12d 346	. . . . . . . 8 ⊢ (𝑣 = ⟨𝑚, 𝑛⟩ → ((( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣) ↔ (( · ‘𝑢) = (𝑚 · 𝑛) → 𝑢 = ⟨𝑚, 𝑛⟩)))
145	144	ralxp 5786	. . . . . . 7 ⊢ (∀𝑣 ∈ (𝑋 × 𝑌)(( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 (( · ‘𝑢) = (𝑚 · 𝑛) → 𝑢 = ⟨𝑚, 𝑛⟩))
146		fveq2 6831	. . . . . . . . . . 11 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → ( · ‘𝑢) = ( · ‘⟨𝑖, 𝑗⟩))
147		df-ov 7363	. . . . . . . . . . 11 ⊢ (𝑖 · 𝑗) = ( · ‘⟨𝑖, 𝑗⟩)
148	146, 147	eqtr4di 2794	. . . . . . . . . 10 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → ( · ‘𝑢) = (𝑖 · 𝑗))
149	148	eqeq1d 2743	. . . . . . . . 9 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (( · ‘𝑢) = (𝑚 · 𝑛) ↔ (𝑖 · 𝑗) = (𝑚 · 𝑛)))
150		eqeq1 2745	. . . . . . . . 9 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (𝑢 = ⟨𝑚, 𝑛⟩ ↔ ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
151	149, 150	imbi12d 346	. . . . . . . 8 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → ((( · ‘𝑢) = (𝑚 · 𝑛) → 𝑢 = ⟨𝑚, 𝑛⟩) ↔ ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩)))
152	151	2ralbidv 3205	. . . . . . 7 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 (( · ‘𝑢) = (𝑚 · 𝑛) → 𝑢 = ⟨𝑚, 𝑛⟩) ↔ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩)))
153	145, 152	bitrid 285	. . . . . 6 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (∀𝑣 ∈ (𝑋 × 𝑌)(( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩)))
154	153	ralxp 5786	. . . . 5 ⊢ (∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)(( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑌 ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
155	138, 154	bitri 277	. . . 4 ⊢ (∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑌 ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
156	132, 155	sylibr 236	. . 3 ⊢ (𝜑 → ∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣))
157		dff13 7202	. . 3 ⊢ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1→𝑍 ↔ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍 ∧ ∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣)))
158	57, 156, 157	sylanbrc 590	. 2 ⊢ (𝜑 → ( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1→𝑍)
159		breq1 5078	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → (𝑥 ∥ (𝑀 · 𝑁) ↔ 𝑤 ∥ (𝑀 · 𝑁)))
160	159, 51	elrab2 3634	. . . . . . . . . . 11 ⊢ (𝑤 ∈ 𝑍 ↔ (𝑤 ∈ ℕ ∧ 𝑤 ∥ (𝑀 · 𝑁)))
161	160	simplbi 498	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑍 → 𝑤 ∈ ℕ)
162	161	adantl 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∈ ℕ)
163	162	nnzd 12545	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∈ ℤ)
164	38	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑀 ∈ ℕ)
165	164	nnzd 12545	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑀 ∈ ℤ)
166	164	nnne0d 12222	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑀 ≠ 0)
167		simpr 486	. . . . . . . . . 10 ⊢ ((𝑤 = 0 ∧ 𝑀 = 0) → 𝑀 = 0)
168	167	necon3ai 2961	. . . . . . . . 9 ⊢ (𝑀 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑀 = 0))
169	166, 168	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ¬ (𝑤 = 0 ∧ 𝑀 = 0))
170		gcdn0cl 16466	. . . . . . . 8 ⊢ (((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ 𝑀 = 0)) → (𝑤 gcd 𝑀) ∈ ℕ)
171	163, 165, 169, 170	syl21anc 844	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑀) ∈ ℕ)
172		gcddvds 16467	. . . . . . . . 9 ⊢ ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
173	163, 165, 172	syl2anc 591	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
174	173	simprd 497	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑀) ∥ 𝑀)
175		breq1 5078	. . . . . . . 8 ⊢ (𝑥 = (𝑤 gcd 𝑀) → (𝑥 ∥ 𝑀 ↔ (𝑤 gcd 𝑀) ∥ 𝑀))
176	175, 4	elrab2 3634	. . . . . . 7 ⊢ ((𝑤 gcd 𝑀) ∈ 𝑋 ↔ ((𝑤 gcd 𝑀) ∈ ℕ ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
177	171, 174, 176	sylanbrc 590	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑀) ∈ 𝑋)
178	32	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑁 ∈ ℕ)
179	178	nnzd 12545	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑁 ∈ ℤ)
180	178	nnne0d 12222	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑁 ≠ 0)
181		simpr 486	. . . . . . . . . 10 ⊢ ((𝑤 = 0 ∧ 𝑁 = 0) → 𝑁 = 0)
182	181	necon3ai 2961	. . . . . . . . 9 ⊢ (𝑁 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑁 = 0))
183	180, 182	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ¬ (𝑤 = 0 ∧ 𝑁 = 0))
184		gcdn0cl 16466	. . . . . . . 8 ⊢ (((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ 𝑁 = 0)) → (𝑤 gcd 𝑁) ∈ ℕ)
185	163, 179, 183, 184	syl21anc 844	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑁) ∈ ℕ)
186		gcddvds 16467	. . . . . . . . 9 ⊢ ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
187	163, 179, 186	syl2anc 591	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
188	187	simprd 497	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑁) ∥ 𝑁)
189		breq1 5078	. . . . . . . 8 ⊢ (𝑥 = (𝑤 gcd 𝑁) → (𝑥 ∥ 𝑁 ↔ (𝑤 gcd 𝑁) ∥ 𝑁))
190	189, 8	elrab2 3634	. . . . . . 7 ⊢ ((𝑤 gcd 𝑁) ∈ 𝑌 ↔ ((𝑤 gcd 𝑁) ∈ ℕ ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
191	185, 188, 190	sylanbrc 590	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑁) ∈ 𝑌)
192	177, 191	opelxpd 5660	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩ ∈ (𝑋 × 𝑌))
193	192	fvresd 6851	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (( · ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩) = ( · ‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
194	89	adantr 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑀 gcd 𝑁) = 1)
195		rpmulgcd2 16620	. . . . . . . 8 ⊢ (((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 gcd 𝑁) = 1) → (𝑤 gcd (𝑀 · 𝑁)) = ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)))
196	163, 165, 179, 194, 195	syl31anc 1382	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd (𝑀 · 𝑁)) = ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)))
197		df-ov 7363	. . . . . . 7 ⊢ ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)) = ( · ‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩)
198	196, 197	eqtrdi 2792	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd (𝑀 · 𝑁)) = ( · ‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
199	160	simprbi 499	. . . . . . . 8 ⊢ (𝑤 ∈ 𝑍 → 𝑤 ∥ (𝑀 · 𝑁))
200	199	adantl 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∥ (𝑀 · 𝑁))
201	38, 32	nnmulcld 12225	. . . . . . . 8 ⊢ (𝜑 → (𝑀 · 𝑁) ∈ ℕ)
202		gcdeq 16517	. . . . . . . 8 ⊢ ((𝑤 ∈ ℕ ∧ (𝑀 · 𝑁) ∈ ℕ) → ((𝑤 gcd (𝑀 · 𝑁)) = 𝑤 ↔ 𝑤 ∥ (𝑀 · 𝑁)))
203	161, 201, 202	syl2anr 604	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ((𝑤 gcd (𝑀 · 𝑁)) = 𝑤 ↔ 𝑤 ∥ (𝑀 · 𝑁)))
204	200, 203	mpbird 259	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd (𝑀 · 𝑁)) = 𝑤)
205	193, 198, 204	3eqtr2rd 2783	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 = (( · ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
206		fveq2 6831	. . . . . 6 ⊢ (𝑢 = ⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩ → (( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
207	206	rspceeqv 3585	. . . . 5 ⊢ ((⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩ ∈ (𝑋 × 𝑌) ∧ 𝑤 = (( · ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩)) → ∃𝑢 ∈ (𝑋 × 𝑌)𝑤 = (( · ↾ (𝑋 × 𝑌))‘𝑢))
208	192, 205, 207	syl2anc 591	. . . 4 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ∃𝑢 ∈ (𝑋 × 𝑌)𝑤 = (( · ↾ (𝑋 × 𝑌))‘𝑢))
209	208	ralrimiva 3133	. . 3 ⊢ (𝜑 → ∀𝑤 ∈ 𝑍 ∃𝑢 ∈ (𝑋 × 𝑌)𝑤 = (( · ↾ (𝑋 × 𝑌))‘𝑢))
210		dffo3 7047	. . 3 ⊢ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–onto→𝑍 ↔ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍 ∧ ∀𝑤 ∈ 𝑍 ∃𝑢 ∈ (𝑋 × 𝑌)𝑤 = (( · ↾ (𝑋 × 𝑌))‘𝑢)))
211	57, 209, 210	sylanbrc 590	. 2 ⊢ (𝜑 → ( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–onto→𝑍)
212		df-f1o 6496	. 2 ⊢ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1-onto→𝑍 ↔ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1→𝑍 ∧ ( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–onto→𝑍))
213	158, 211, 212	sylanbrc 590	1 ⊢ (𝜑 → ( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1-onto→𝑍)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 397 = wceq 1548 ∈ wcel 2121 ≠ wne 2936 ∀wral 3055 ∃wrex 3065 {crab 3393 ⊆ wss 3885 ⟨cop 4564 class class class wbr 5075 × cxp 5619 ↾ cres 5623 Fn wfn 6484 ⟶wf 6485 –1-1→wf1 6486 –onto→wfo 6487 –1-1-onto→wf1o 6488 ‘cfv 6489 (class class class)co 7360 ℂcc 11031 0cc0 11033 1c1 11034 · cmul 11038 ℕcn 12169 ℕ₀cn0 12432 ℤcz 12519 ∥ cdvds 16216 gcd cgcd 16458

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1975 ax-7 2016 ax-8 2123 ax-9 2131 ax-10 2154 ax-11 2170 ax-12 2191 ax-ext 2713 ax-sep 5221 ax-nul 5231 ax-pow 5297 ax-pr 5365 ax-un 7682 ax-cnex 11089 ax-resscn 11090 ax-1cn 11091 ax-icn 11092 ax-addcl 11093 ax-addrcl 11094 ax-mulcl 11095 ax-mulrcl 11096 ax-mulcom 11097 ax-addass 11098 ax-mulass 11099 ax-distr 11100 ax-i2m1 11101 ax-1ne0 11102 ax-1rid 11103 ax-rnegex 11104 ax-rrecex 11105 ax-cnre 11106 ax-pre-lttri 11107 ax-pre-lttrn 11108 ax-pre-ltadd 11109 ax-pre-mulgt0 11110 ax-pre-sup 11111 ax-mulf 11113

This theorem depends on definitions: df-bi 209 df-an 398 df-or 855 df-3or 1094 df-3an 1095 df-tru 1551 df-fal 1561 df-ex 1788 df-nf 1792 df-sb 2075 df-mo 2545 df-eu 2575 df-clab 2720 df-cleq 2733 df-clel 2816 df-nfc 2890 df-ne 2937 df-nel 3041 df-ral 3056 df-rex 3066 df-rmo 3346 df-reu 3347 df-rab 3394 df-v 3435 df-sbc 3726 df-csb 3834 df-dif 3888 df-un 3890 df-in 3892 df-ss 3902 df-pss 3905 df-nul 4265 df-if 4458 df-pw 4534 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4842 df-iun 4926 df-br 5076 df-opab 5138 df-mpt 5157 df-tr 5183 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-we 5576 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-pred 6256 df-ord 6317 df-on 6318 df-lim 6319 df-suc 6320 df-iota 6445 df-fun 6491 df-fn 6492 df-f 6493 df-f1 6494 df-fo 6495 df-f1o 6496 df-fv 6497 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-om 7811 df-2nd 7936 df-frecs 8225 df-wrecs 8256 df-recs 8305 df-rdg 8343 df-er 8637 df-en 8888 df-dom 8889 df-sdom 8890 df-sup 9349 df-inf 9350 df-pnf 11176 df-mnf 11177 df-xr 11178 df-ltxr 11179 df-le 11180 df-sub 11374 df-neg 11375 df-div 11803 df-nn 12170 df-2 12239 df-3 12240 df-n0 12433 df-z 12520 df-uz 12784 df-rp 12938 df-fl 13746 df-mod 13824 df-seq 13959 df-exp 14019 df-cj 15056 df-re 15057 df-im 15058 df-sqrt 15192 df-abs 15193 df-dvds 16217 df-gcd 16459

This theorem is referenced by: (None)

W3C validator