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 27179

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 11120	. . . . . . 7 ⊢ · :(ℂ × ℂ)⟶ℂ
2		ffn 6672	. . . . . . 7 ⊢ ( · :(ℂ × ℂ)⟶ℂ → · Fn (ℂ × ℂ))
3	1, 2	ax-mp 5	. . . . . 6 ⊢ · Fn (ℂ × ℂ)
4		dvdsmulf1o.x	. . . . . . . . 9 ⊢ 𝑋 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀}
5	4	ssrab3 4036	. . . . . . . 8 ⊢ 𝑋 ⊆ ℕ
6		nnsscn 12164	. . . . . . . 8 ⊢ ℕ ⊆ ℂ
7	5, 6	sstri 3945	. . . . . . 7 ⊢ 𝑋 ⊆ ℂ
8		dvdsmulf1o.y	. . . . . . . . 9 ⊢ 𝑌 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}
9	8	ssrab3 4036	. . . . . . . 8 ⊢ 𝑌 ⊆ ℕ
10	9, 6	sstri 3945	. . . . . . 7 ⊢ 𝑌 ⊆ ℂ
11		xpss12 5649	. . . . . . 7 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑌 ⊆ ℂ) → (𝑋 × 𝑌) ⊆ (ℂ × ℂ))
12	7, 10, 11	mp2an 693	. . . . . 6 ⊢ (𝑋 × 𝑌) ⊆ (ℂ × ℂ)
13		fnssres 6625	. . . . . 6 ⊢ (( · Fn (ℂ × ℂ) ∧ (𝑋 × 𝑌) ⊆ (ℂ × ℂ)) → ( · ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌))
14	3, 12, 13	mp2an 693	. . . . 5 ⊢ ( · ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌)
15	14	a1i 11	. . . 4 ⊢ (𝜑 → ( · ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌))
16		ovres 7536	. . . . . . 7 ⊢ ((𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌) → (𝑖( · ↾ (𝑋 × 𝑌))𝑗) = (𝑖 · 𝑗))
17	16	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖( · ↾ (𝑋 × 𝑌))𝑗) = (𝑖 · 𝑗))
18		breq1 5103	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → (𝑥 ∥ 𝑀 ↔ 𝑖 ∥ 𝑀))
19	18, 4	elrab2 3651	. . . . . . . . . 10 ⊢ (𝑖 ∈ 𝑋 ↔ (𝑖 ∈ ℕ ∧ 𝑖 ∥ 𝑀))
20	19	simplbi 496	. . . . . . . . 9 ⊢ (𝑖 ∈ 𝑋 → 𝑖 ∈ ℕ)
21	20	ad2antrl 729	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑖 ∈ ℕ)
22		breq1 5103	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑗 → (𝑥 ∥ 𝑁 ↔ 𝑗 ∥ 𝑁))
23	22, 8	elrab2 3651	. . . . . . . . . 10 ⊢ (𝑗 ∈ 𝑌 ↔ (𝑗 ∈ ℕ ∧ 𝑗 ∥ 𝑁))
24	23	simplbi 496	. . . . . . . . 9 ⊢ (𝑗 ∈ 𝑌 → 𝑗 ∈ ℕ)
25	24	ad2antll 730	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑗 ∈ ℕ)
26	21, 25	nnmulcld 12212	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 · 𝑗) ∈ ℕ)
27	23	simprbi 497	. . . . . . . . 9 ⊢ (𝑗 ∈ 𝑌 → 𝑗 ∥ 𝑁)
28	27	ad2antll 730	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑗 ∥ 𝑁)
29	19	simprbi 497	. . . . . . . . 9 ⊢ (𝑖 ∈ 𝑋 → 𝑖 ∥ 𝑀)
30	29	ad2antrl 729	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑖 ∥ 𝑀)
31	25	nnzd 12528	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑗 ∈ ℤ)
32		dvdsmulf1o.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℕ)
33	32	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑁 ∈ ℕ)
34	33	nnzd 12528	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑁 ∈ ℤ)
35	21	nnzd 12528	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑖 ∈ ℤ)
36		dvdscmul 16223	. . . . . . . . . 10 ⊢ ((𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑗 ∥ 𝑁 → (𝑖 · 𝑗) ∥ (𝑖 · 𝑁)))
37	31, 34, 35, 36	syl3anc 1374	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑗 ∥ 𝑁 → (𝑖 · 𝑗) ∥ (𝑖 · 𝑁)))
38		dvdsmulf1o.1	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℕ)
39	38	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑀 ∈ ℕ)
40	39	nnzd 12528	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑀 ∈ ℤ)
41		dvdsmulc 16224	. . . . . . . . . 10 ⊢ ((𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∥ 𝑀 → (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)))
42	35, 40, 34, 41	syl3anc 1374	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 ∥ 𝑀 → (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)))
43	26	nnzd 12528	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 · 𝑗) ∈ ℤ)
44	35, 34	zmulcld 12616	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 · 𝑁) ∈ ℤ)
45	40, 34	zmulcld 12616	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑀 · 𝑁) ∈ ℤ)
46		dvdstr 16235	. . . . . . . . . 10 ⊢ (((𝑖 · 𝑗) ∈ ℤ ∧ (𝑖 · 𝑁) ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) → (((𝑖 · 𝑗) ∥ (𝑖 · 𝑁) ∧ (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
47	43, 44, 45, 46	syl3anc 1374	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (((𝑖 · 𝑗) ∥ (𝑖 · 𝑁) ∧ (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
48	37, 42, 47	syl2and 609	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → ((𝑗 ∥ 𝑁 ∧ 𝑖 ∥ 𝑀) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
49	28, 30, 48	mp2and 700	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁))
50		breq1 5103	. . . . . . . 8 ⊢ (𝑥 = (𝑖 · 𝑗) → (𝑥 ∥ (𝑀 · 𝑁) ↔ (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
51		dvdsmulf1o.z	. . . . . . . 8 ⊢ 𝑍 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑀 · 𝑁)}
52	50, 51	elrab2 3651	. . . . . . 7 ⊢ ((𝑖 · 𝑗) ∈ 𝑍 ↔ ((𝑖 · 𝑗) ∈ ℕ ∧ (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
53	26, 49, 52	sylanbrc 584	. . . . . 6 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 · 𝑗) ∈ 𝑍)
54	17, 53	eqeltrd 2837	. . . . 5 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖( · ↾ (𝑋 × 𝑌))𝑗) ∈ 𝑍)
55	54	ralrimivva 3181	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑌 (𝑖( · ↾ (𝑋 × 𝑌))𝑗) ∈ 𝑍)
56		ffnov 7496	. . . 4 ⊢ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍 ↔ (( · ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑌 (𝑖( · ↾ (𝑋 × 𝑌))𝑗) ∈ 𝑍))
57	15, 55, 56	sylanbrc 584	. . 3 ⊢ (𝜑 → ( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍)
58	21	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℕ)
59	58	nnnn0d 12476	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℕ₀)
60		simprll 779	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ 𝑋)
61		breq1 5103	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑚 → (𝑥 ∥ 𝑀 ↔ 𝑚 ∥ 𝑀))
62	61, 4	elrab2 3651	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ 𝑋 ↔ (𝑚 ∈ ℕ ∧ 𝑚 ∥ 𝑀))
63	62	simplbi 496	. . . . . . . . . . 11 ⊢ (𝑚 ∈ 𝑋 → 𝑚 ∈ ℕ)
64	60, 63	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℕ)
65	64	nnnn0d 12476	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℕ₀)
66	58	nnzd 12528	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℤ)
67	25	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∈ ℕ)
68	67	nnzd 12528	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∈ ℤ)
69		dvdsmul1 16218	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ) → 𝑖 ∥ (𝑖 · 𝑗))
70	66, 68, 69	syl2anc 585	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∥ (𝑖 · 𝑗))
71		simprr 773	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑚 · 𝑛))
72	7, 60	sselid 3933	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℂ)
73		simprlr 780	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ 𝑌)
74		breq1 5103	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑛 → (𝑥 ∥ 𝑁 ↔ 𝑛 ∥ 𝑁))
75	74, 8	elrab2 3651	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ 𝑌 ↔ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝑁))
76	75	simplbi 496	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ 𝑌 → 𝑛 ∈ ℕ)
77	73, 76	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ ℕ)
78	77	nncnd 12175	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ ℂ)
79	72, 78	mulcomd 11167	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 · 𝑛) = (𝑛 · 𝑚))
80	71, 79	eqtrd 2772	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑛 · 𝑚))
81	70, 80	breqtrd 5126	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∥ (𝑛 · 𝑚))
82	77	nnzd 12528	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ ℤ)
83	34	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑁 ∈ ℤ)
84	66, 83	gcdcomd 16455	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 gcd 𝑁) = (𝑁 gcd 𝑖))
85	40	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑀 ∈ ℤ)
86	32	nnzd 12528	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℤ)
87	38	nnzd 12528	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℤ)
88	86, 87	gcdcomd 16455	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 gcd 𝑀) = (𝑀 gcd 𝑁))
89		dvdsmulf1o.3	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1)
90	88, 89	eqtrd 2772	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 gcd 𝑀) = 1)
91	90	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑁 gcd 𝑀) = 1)
92	30	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∥ 𝑀)
93		rpdvds 16601	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ((𝑁 gcd 𝑀) = 1 ∧ 𝑖 ∥ 𝑀)) → (𝑁 gcd 𝑖) = 1)
94	83, 66, 85, 91, 92, 93	syl32anc 1381	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑁 gcd 𝑖) = 1)
95	84, 94	eqtrd 2772	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 gcd 𝑁) = 1)
96	75	simprbi 497	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ 𝑌 → 𝑛 ∥ 𝑁)
97	73, 96	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∥ 𝑁)
98		rpdvds 16601	. . . . . . . . . . 11 ⊢ (((𝑖 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑖 gcd 𝑁) = 1 ∧ 𝑛 ∥ 𝑁)) → (𝑖 gcd 𝑛) = 1)
99	66, 82, 83, 95, 97, 98	syl32anc 1381	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 gcd 𝑛) = 1)
100	64	nnzd 12528	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℤ)
101		coprmdvds 16594	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ) → ((𝑖 ∥ (𝑛 · 𝑚) ∧ (𝑖 gcd 𝑛) = 1) → 𝑖 ∥ 𝑚))
102	66, 82, 100, 101	syl3anc 1374	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → ((𝑖 ∥ (𝑛 · 𝑚) ∧ (𝑖 gcd 𝑛) = 1) → 𝑖 ∥ 𝑚))
103	81, 99, 102	mp2and 700	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∥ 𝑚)
104		dvdsmul1 16218	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 𝑚 ∥ (𝑚 · 𝑛))
105	100, 82, 104	syl2anc 585	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∥ (𝑚 · 𝑛))
106	58	nncnd 12175	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℂ)
107	67	nncnd 12175	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∈ ℂ)
108	106, 107	mulcomd 11167	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑗 · 𝑖))
109	71, 108	eqtr3d 2774	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 · 𝑛) = (𝑗 · 𝑖))
110	105, 109	breqtrd 5126	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∥ (𝑗 · 𝑖))
111	100, 83	gcdcomd 16455	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 gcd 𝑁) = (𝑁 gcd 𝑚))
112	62	simprbi 497	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ 𝑋 → 𝑚 ∥ 𝑀)
113	60, 112	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∥ 𝑀)
114		rpdvds 16601	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ((𝑁 gcd 𝑀) = 1 ∧ 𝑚 ∥ 𝑀)) → (𝑁 gcd 𝑚) = 1)
115	83, 100, 85, 91, 113, 114	syl32anc 1381	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑁 gcd 𝑚) = 1)
116	111, 115	eqtrd 2772	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 gcd 𝑁) = 1)
117	28	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∥ 𝑁)
118		rpdvds 16601	. . . . . . . . . . 11 ⊢ (((𝑚 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑚 gcd 𝑁) = 1 ∧ 𝑗 ∥ 𝑁)) → (𝑚 gcd 𝑗) = 1)
119	100, 68, 83, 116, 117, 118	syl32anc 1381	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 gcd 𝑗) = 1)
120		coprmdvds 16594	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑖 ∈ ℤ) → ((𝑚 ∥ (𝑗 · 𝑖) ∧ (𝑚 gcd 𝑗) = 1) → 𝑚 ∥ 𝑖))
121	100, 68, 66, 120	syl3anc 1374	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → ((𝑚 ∥ (𝑗 · 𝑖) ∧ (𝑚 gcd 𝑗) = 1) → 𝑚 ∥ 𝑖))
122	110, 119, 121	mp2and 700	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∥ 𝑖)
123		dvdseq 16255	. . . . . . . . 9 ⊢ (((𝑖 ∈ ℕ₀ ∧ 𝑚 ∈ ℕ₀) ∧ (𝑖 ∥ 𝑚 ∧ 𝑚 ∥ 𝑖)) → 𝑖 = 𝑚)
124	59, 65, 103, 122, 123	syl22anc 839	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 = 𝑚)
125	58	nnne0d 12209	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ≠ 0)
126	124	oveq1d 7385	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑛) = (𝑚 · 𝑛))
127	71, 126	eqtr4d 2775	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑖 · 𝑛))
128	107, 78, 106, 125, 127	mulcanad 11786	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 = 𝑛)
129	124, 128	opeq12d 4839	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩)
130	129	expr 456	. . . . . 6 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌)) → ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
131	130	ralrimivva 3181	. . . . 5 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
132	131	ralrimivva 3181	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑌 ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
133		fvres 6863	. . . . . . . . 9 ⊢ (𝑢 ∈ (𝑋 × 𝑌) → (( · ↾ (𝑋 × 𝑌))‘𝑢) = ( · ‘𝑢))
134		fvres 6863	. . . . . . . . 9 ⊢ (𝑣 ∈ (𝑋 × 𝑌) → (( · ↾ (𝑋 × 𝑌))‘𝑣) = ( · ‘𝑣))
135	133, 134	eqeqan12d 2751	. . . . . . . 8 ⊢ ((𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) → ((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) ↔ ( · ‘𝑢) = ( · ‘𝑣)))
136	135	imbi1d 341	. . . . . . 7 ⊢ ((𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) → (((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ (( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣)))
137	136	ralbidva 3159	. . . . . 6 ⊢ (𝑢 ∈ (𝑋 × 𝑌) → (∀𝑣 ∈ (𝑋 × 𝑌)((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑣 ∈ (𝑋 × 𝑌)(( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣)))
138	137	ralbiia 3082	. . . . 5 ⊢ (∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)(( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣))
139		fveq2 6844	. . . . . . . . . . 11 ⊢ (𝑣 = ⟨𝑚, 𝑛⟩ → ( · ‘𝑣) = ( · ‘⟨𝑚, 𝑛⟩))
140		df-ov 7373	. . . . . . . . . . 11 ⊢ (𝑚 · 𝑛) = ( · ‘⟨𝑚, 𝑛⟩)
141	139, 140	eqtr4di 2790	. . . . . . . . . 10 ⊢ (𝑣 = ⟨𝑚, 𝑛⟩ → ( · ‘𝑣) = (𝑚 · 𝑛))
142	141	eqeq2d 2748	. . . . . . . . 9 ⊢ (𝑣 = ⟨𝑚, 𝑛⟩ → (( · ‘𝑢) = ( · ‘𝑣) ↔ ( · ‘𝑢) = (𝑚 · 𝑛)))
143		eqeq2 2749	. . . . . . . . 9 ⊢ (𝑣 = ⟨𝑚, 𝑛⟩ → (𝑢 = 𝑣 ↔ 𝑢 = ⟨𝑚, 𝑛⟩))
144	142, 143	imbi12d 344	. . . . . . . 8 ⊢ (𝑣 = ⟨𝑚, 𝑛⟩ → ((( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣) ↔ (( · ‘𝑢) = (𝑚 · 𝑛) → 𝑢 = ⟨𝑚, 𝑛⟩)))
145	144	ralxp 5800	. . . . . . 7 ⊢ (∀𝑣 ∈ (𝑋 × 𝑌)(( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 (( · ‘𝑢) = (𝑚 · 𝑛) → 𝑢 = ⟨𝑚, 𝑛⟩))
146		fveq2 6844	. . . . . . . . . . 11 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → ( · ‘𝑢) = ( · ‘⟨𝑖, 𝑗⟩))
147		df-ov 7373	. . . . . . . . . . 11 ⊢ (𝑖 · 𝑗) = ( · ‘⟨𝑖, 𝑗⟩)
148	146, 147	eqtr4di 2790	. . . . . . . . . 10 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → ( · ‘𝑢) = (𝑖 · 𝑗))
149	148	eqeq1d 2739	. . . . . . . . 9 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (( · ‘𝑢) = (𝑚 · 𝑛) ↔ (𝑖 · 𝑗) = (𝑚 · 𝑛)))
150		eqeq1 2741	. . . . . . . . 9 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (𝑢 = ⟨𝑚, 𝑛⟩ ↔ ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
151	149, 150	imbi12d 344	. . . . . . . 8 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → ((( · ‘𝑢) = (𝑚 · 𝑛) → 𝑢 = ⟨𝑚, 𝑛⟩) ↔ ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩)))
152	151	2ralbidv 3202	. . . . . . 7 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 (( · ‘𝑢) = (𝑚 · 𝑛) → 𝑢 = ⟨𝑚, 𝑛⟩) ↔ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩)))
153	145, 152	bitrid 283	. . . . . 6 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (∀𝑣 ∈ (𝑋 × 𝑌)(( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩)))
154	153	ralxp 5800	. . . . 5 ⊢ (∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)(( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑌 ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
155	138, 154	bitri 275	. . . 4 ⊢ (∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑌 ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
156	132, 155	sylibr 234	. . 3 ⊢ (𝜑 → ∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣))
157		dff13 7212	. . 3 ⊢ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1→𝑍 ↔ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍 ∧ ∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣)))
158	57, 156, 157	sylanbrc 584	. 2 ⊢ (𝜑 → ( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1→𝑍)
159		breq1 5103	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → (𝑥 ∥ (𝑀 · 𝑁) ↔ 𝑤 ∥ (𝑀 · 𝑁)))
160	159, 51	elrab2 3651	. . . . . . . . . . 11 ⊢ (𝑤 ∈ 𝑍 ↔ (𝑤 ∈ ℕ ∧ 𝑤 ∥ (𝑀 · 𝑁)))
161	160	simplbi 496	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑍 → 𝑤 ∈ ℕ)
162	161	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∈ ℕ)
163	162	nnzd 12528	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∈ ℤ)
164	38	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑀 ∈ ℕ)
165	164	nnzd 12528	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑀 ∈ ℤ)
166	164	nnne0d 12209	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑀 ≠ 0)
167		simpr 484	. . . . . . . . . 10 ⊢ ((𝑤 = 0 ∧ 𝑀 = 0) → 𝑀 = 0)
168	167	necon3ai 2958	. . . . . . . . 9 ⊢ (𝑀 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑀 = 0))
169	166, 168	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ¬ (𝑤 = 0 ∧ 𝑀 = 0))
170		gcdn0cl 16443	. . . . . . . 8 ⊢ (((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ 𝑀 = 0)) → (𝑤 gcd 𝑀) ∈ ℕ)
171	163, 165, 169, 170	syl21anc 838	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑀) ∈ ℕ)
172		gcddvds 16444	. . . . . . . . 9 ⊢ ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
173	163, 165, 172	syl2anc 585	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
174	173	simprd 495	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑀) ∥ 𝑀)
175		breq1 5103	. . . . . . . 8 ⊢ (𝑥 = (𝑤 gcd 𝑀) → (𝑥 ∥ 𝑀 ↔ (𝑤 gcd 𝑀) ∥ 𝑀))
176	175, 4	elrab2 3651	. . . . . . 7 ⊢ ((𝑤 gcd 𝑀) ∈ 𝑋 ↔ ((𝑤 gcd 𝑀) ∈ ℕ ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
177	171, 174, 176	sylanbrc 584	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑀) ∈ 𝑋)
178	32	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑁 ∈ ℕ)
179	178	nnzd 12528	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑁 ∈ ℤ)
180	178	nnne0d 12209	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑁 ≠ 0)
181		simpr 484	. . . . . . . . . 10 ⊢ ((𝑤 = 0 ∧ 𝑁 = 0) → 𝑁 = 0)
182	181	necon3ai 2958	. . . . . . . . 9 ⊢ (𝑁 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑁 = 0))
183	180, 182	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ¬ (𝑤 = 0 ∧ 𝑁 = 0))
184		gcdn0cl 16443	. . . . . . . 8 ⊢ (((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ 𝑁 = 0)) → (𝑤 gcd 𝑁) ∈ ℕ)
185	163, 179, 183, 184	syl21anc 838	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑁) ∈ ℕ)
186		gcddvds 16444	. . . . . . . . 9 ⊢ ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
187	163, 179, 186	syl2anc 585	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
188	187	simprd 495	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑁) ∥ 𝑁)
189		breq1 5103	. . . . . . . 8 ⊢ (𝑥 = (𝑤 gcd 𝑁) → (𝑥 ∥ 𝑁 ↔ (𝑤 gcd 𝑁) ∥ 𝑁))
190	189, 8	elrab2 3651	. . . . . . 7 ⊢ ((𝑤 gcd 𝑁) ∈ 𝑌 ↔ ((𝑤 gcd 𝑁) ∈ ℕ ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
191	185, 188, 190	sylanbrc 584	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑁) ∈ 𝑌)
192	177, 191	opelxpd 5673	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩ ∈ (𝑋 × 𝑌))
193	192	fvresd 6864	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (( · ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩) = ( · ‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
194	89	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑀 gcd 𝑁) = 1)
195		rpmulgcd2 16597	. . . . . . . 8 ⊢ (((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 gcd 𝑁) = 1) → (𝑤 gcd (𝑀 · 𝑁)) = ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)))
196	163, 165, 179, 194, 195	syl31anc 1376	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd (𝑀 · 𝑁)) = ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)))
197		df-ov 7373	. . . . . . 7 ⊢ ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)) = ( · ‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩)
198	196, 197	eqtrdi 2788	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd (𝑀 · 𝑁)) = ( · ‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
199	160	simprbi 497	. . . . . . . 8 ⊢ (𝑤 ∈ 𝑍 → 𝑤 ∥ (𝑀 · 𝑁))
200	199	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∥ (𝑀 · 𝑁))
201	38, 32	nnmulcld 12212	. . . . . . . 8 ⊢ (𝜑 → (𝑀 · 𝑁) ∈ ℕ)
202		gcdeq 16494	. . . . . . . 8 ⊢ ((𝑤 ∈ ℕ ∧ (𝑀 · 𝑁) ∈ ℕ) → ((𝑤 gcd (𝑀 · 𝑁)) = 𝑤 ↔ 𝑤 ∥ (𝑀 · 𝑁)))
203	161, 201, 202	syl2anr 598	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ((𝑤 gcd (𝑀 · 𝑁)) = 𝑤 ↔ 𝑤 ∥ (𝑀 · 𝑁)))
204	200, 203	mpbird 257	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd (𝑀 · 𝑁)) = 𝑤)
205	193, 198, 204	3eqtr2rd 2779	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 = (( · ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
206		fveq2 6844	. . . . . 6 ⊢ (𝑢 = ⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩ → (( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
207	206	rspceeqv 3601	. . . . 5 ⊢ ((⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩ ∈ (𝑋 × 𝑌) ∧ 𝑤 = (( · ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩)) → ∃𝑢 ∈ (𝑋 × 𝑌)𝑤 = (( · ↾ (𝑋 × 𝑌))‘𝑢))
208	192, 205, 207	syl2anc 585	. . . 4 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ∃𝑢 ∈ (𝑋 × 𝑌)𝑤 = (( · ↾ (𝑋 × 𝑌))‘𝑢))
209	208	ralrimiva 3130	. . 3 ⊢ (𝜑 → ∀𝑤 ∈ 𝑍 ∃𝑢 ∈ (𝑋 × 𝑌)𝑤 = (( · ↾ (𝑋 × 𝑌))‘𝑢))
210		dffo3 7058	. . 3 ⊢ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–onto→𝑍 ↔ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍 ∧ ∀𝑤 ∈ 𝑍 ∃𝑢 ∈ (𝑋 × 𝑌)𝑤 = (( · ↾ (𝑋 × 𝑌))‘𝑢)))
211	57, 209, 210	sylanbrc 584	. 2 ⊢ (𝜑 → ( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–onto→𝑍)
212		df-f1o 6509	. 2 ⊢ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1-onto→𝑍 ↔ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1→𝑍 ∧ ( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–onto→𝑍))
213	158, 211, 212	sylanbrc 584	1 ⊢ (𝜑 → ( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1-onto→𝑍)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ∀wral 3052 ∃wrex 3062 {crab 3401 ⊆ wss 3903 ⟨cop 4588 class class class wbr 5100 × cxp 5632 ↾ cres 5636 Fn wfn 6497 ⟶wf 6498 –1-1→wf1 6499 –onto→wfo 6500 –1-1-onto→wf1o 6501 ‘cfv 6502 (class class class)co 7370 ℂcc 11038 0cc0 11040 1c1 11041 · cmul 11045 ℕcn 12159 ℕ₀cn0 12415 ℤcz 12502 ∥ cdvds 16193 gcd cgcd 16435

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5245 ax-nul 5255 ax-pow 5314 ax-pr 5381 ax-un 7692 ax-cnex 11096 ax-resscn 11097 ax-1cn 11098 ax-icn 11099 ax-addcl 11100 ax-addrcl 11101 ax-mulcl 11102 ax-mulrcl 11103 ax-mulcom 11104 ax-addass 11105 ax-mulass 11106 ax-distr 11107 ax-i2m1 11108 ax-1ne0 11109 ax-1rid 11110 ax-rnegex 11111 ax-rrecex 11112 ax-cnre 11113 ax-pre-lttri 11114 ax-pre-lttrn 11115 ax-pre-ltadd 11116 ax-pre-mulgt0 11117 ax-pre-sup 11118 ax-mulf 11120

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5529 df-eprel 5534 df-po 5542 df-so 5543 df-fr 5587 df-we 5589 df-xp 5640 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-rn 5645 df-res 5646 df-ima 5647 df-pred 6269 df-ord 6330 df-on 6331 df-lim 6332 df-suc 6333 df-iota 6458 df-fun 6504 df-fn 6505 df-f 6506 df-f1 6507 df-fo 6508 df-f1o 6509 df-fv 6510 df-riota 7327 df-ov 7373 df-oprab 7374 df-mpo 7375 df-om 7821 df-2nd 7946 df-frecs 8235 df-wrecs 8266 df-recs 8315 df-rdg 8353 df-er 8647 df-en 8898 df-dom 8899 df-sdom 8900 df-sup 9359 df-inf 9360 df-pnf 11182 df-mnf 11183 df-xr 11184 df-ltxr 11185 df-le 11186 df-sub 11380 df-neg 11381 df-div 11809 df-nn 12160 df-2 12222 df-3 12223 df-n0 12416 df-z 12503 df-uz 12766 df-rp 12920 df-fl 13726 df-mod 13804 df-seq 13939 df-exp 13999 df-cj 15036 df-re 15037 df-im 15038 df-sqrt 15172 df-abs 15173 df-dvds 16194 df-gcd 16436

This theorem is referenced by: fsumdvdsmulOLD 27180

W3C validator