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 26248

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 10882	. . . . . . 7 ⊢ · :(ℂ × ℂ)⟶ℂ
2		ffn 6584	. . . . . . 7 ⊢ ( · :(ℂ × ℂ)⟶ℂ → · Fn (ℂ × ℂ))
3	1, 2	ax-mp 5	. . . . . 6 ⊢ · Fn (ℂ × ℂ)
4		dvdsmulf1o.x	. . . . . . . . 9 ⊢ 𝑋 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀}
5	4	ssrab3 4011	. . . . . . . 8 ⊢ 𝑋 ⊆ ℕ
6		nnsscn 11908	. . . . . . . 8 ⊢ ℕ ⊆ ℂ
7	5, 6	sstri 3926	. . . . . . 7 ⊢ 𝑋 ⊆ ℂ
8		dvdsmulf1o.y	. . . . . . . . 9 ⊢ 𝑌 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}
9	8	ssrab3 4011	. . . . . . . 8 ⊢ 𝑌 ⊆ ℕ
10	9, 6	sstri 3926	. . . . . . 7 ⊢ 𝑌 ⊆ ℂ
11		xpss12 5595	. . . . . . 7 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑌 ⊆ ℂ) → (𝑋 × 𝑌) ⊆ (ℂ × ℂ))
12	7, 10, 11	mp2an 688	. . . . . 6 ⊢ (𝑋 × 𝑌) ⊆ (ℂ × ℂ)
13		fnssres 6539	. . . . . 6 ⊢ (( · Fn (ℂ × ℂ) ∧ (𝑋 × 𝑌) ⊆ (ℂ × ℂ)) → ( · ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌))
14	3, 12, 13	mp2an 688	. . . . 5 ⊢ ( · ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌)
15	14	a1i 11	. . . 4 ⊢ (𝜑 → ( · ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌))
16		ovres 7416	. . . . . . 7 ⊢ ((𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌) → (𝑖( · ↾ (𝑋 × 𝑌))𝑗) = (𝑖 · 𝑗))
17	16	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖( · ↾ (𝑋 × 𝑌))𝑗) = (𝑖 · 𝑗))
18		breq1 5073	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → (𝑥 ∥ 𝑀 ↔ 𝑖 ∥ 𝑀))
19	18, 4	elrab2 3620	. . . . . . . . . 10 ⊢ (𝑖 ∈ 𝑋 ↔ (𝑖 ∈ ℕ ∧ 𝑖 ∥ 𝑀))
20	19	simplbi 497	. . . . . . . . 9 ⊢ (𝑖 ∈ 𝑋 → 𝑖 ∈ ℕ)
21	20	ad2antrl 724	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑖 ∈ ℕ)
22		breq1 5073	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑗 → (𝑥 ∥ 𝑁 ↔ 𝑗 ∥ 𝑁))
23	22, 8	elrab2 3620	. . . . . . . . . 10 ⊢ (𝑗 ∈ 𝑌 ↔ (𝑗 ∈ ℕ ∧ 𝑗 ∥ 𝑁))
24	23	simplbi 497	. . . . . . . . 9 ⊢ (𝑗 ∈ 𝑌 → 𝑗 ∈ ℕ)
25	24	ad2antll 725	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑗 ∈ ℕ)
26	21, 25	nnmulcld 11956	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 · 𝑗) ∈ ℕ)
27	23	simprbi 496	. . . . . . . . 9 ⊢ (𝑗 ∈ 𝑌 → 𝑗 ∥ 𝑁)
28	27	ad2antll 725	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑗 ∥ 𝑁)
29	19	simprbi 496	. . . . . . . . 9 ⊢ (𝑖 ∈ 𝑋 → 𝑖 ∥ 𝑀)
30	29	ad2antrl 724	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑖 ∥ 𝑀)
31	25	nnzd 12354	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑗 ∈ ℤ)
32		dvdsmulf1o.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℕ)
33	32	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑁 ∈ ℕ)
34	33	nnzd 12354	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑁 ∈ ℤ)
35	21	nnzd 12354	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑖 ∈ ℤ)
36		dvdscmul 15920	. . . . . . . . . 10 ⊢ ((𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑗 ∥ 𝑁 → (𝑖 · 𝑗) ∥ (𝑖 · 𝑁)))
37	31, 34, 35, 36	syl3anc 1369	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑗 ∥ 𝑁 → (𝑖 · 𝑗) ∥ (𝑖 · 𝑁)))
38		dvdsmulf1o.1	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℕ)
39	38	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑀 ∈ ℕ)
40	39	nnzd 12354	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑀 ∈ ℤ)
41		dvdsmulc 15921	. . . . . . . . . 10 ⊢ ((𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∥ 𝑀 → (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)))
42	35, 40, 34, 41	syl3anc 1369	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 ∥ 𝑀 → (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)))
43	26	nnzd 12354	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 · 𝑗) ∈ ℤ)
44	35, 34	zmulcld 12361	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 · 𝑁) ∈ ℤ)
45	40, 34	zmulcld 12361	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑀 · 𝑁) ∈ ℤ)
46		dvdstr 15931	. . . . . . . . . 10 ⊢ (((𝑖 · 𝑗) ∈ ℤ ∧ (𝑖 · 𝑁) ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) → (((𝑖 · 𝑗) ∥ (𝑖 · 𝑁) ∧ (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
47	43, 44, 45, 46	syl3anc 1369	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (((𝑖 · 𝑗) ∥ (𝑖 · 𝑁) ∧ (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
48	37, 42, 47	syl2and 607	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → ((𝑗 ∥ 𝑁 ∧ 𝑖 ∥ 𝑀) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
49	28, 30, 48	mp2and 695	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁))
50		breq1 5073	. . . . . . . 8 ⊢ (𝑥 = (𝑖 · 𝑗) → (𝑥 ∥ (𝑀 · 𝑁) ↔ (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
51		dvdsmulf1o.z	. . . . . . . 8 ⊢ 𝑍 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑀 · 𝑁)}
52	50, 51	elrab2 3620	. . . . . . 7 ⊢ ((𝑖 · 𝑗) ∈ 𝑍 ↔ ((𝑖 · 𝑗) ∈ ℕ ∧ (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
53	26, 49, 52	sylanbrc 582	. . . . . 6 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 · 𝑗) ∈ 𝑍)
54	17, 53	eqeltrd 2839	. . . . 5 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖( · ↾ (𝑋 × 𝑌))𝑗) ∈ 𝑍)
55	54	ralrimivva 3114	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑌 (𝑖( · ↾ (𝑋 × 𝑌))𝑗) ∈ 𝑍)
56		ffnov 7379	. . . 4 ⊢ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍 ↔ (( · ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑌 (𝑖( · ↾ (𝑋 × 𝑌))𝑗) ∈ 𝑍))
57	15, 55, 56	sylanbrc 582	. . 3 ⊢ (𝜑 → ( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍)
58	21	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℕ)
59	58	nnnn0d 12223	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℕ₀)
60		simprll 775	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ 𝑋)
61		breq1 5073	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑚 → (𝑥 ∥ 𝑀 ↔ 𝑚 ∥ 𝑀))
62	61, 4	elrab2 3620	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ 𝑋 ↔ (𝑚 ∈ ℕ ∧ 𝑚 ∥ 𝑀))
63	62	simplbi 497	. . . . . . . . . . 11 ⊢ (𝑚 ∈ 𝑋 → 𝑚 ∈ ℕ)
64	60, 63	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℕ)
65	64	nnnn0d 12223	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℕ₀)
66	58	nnzd 12354	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℤ)
67	25	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∈ ℕ)
68	67	nnzd 12354	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∈ ℤ)
69		dvdsmul1 15915	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ) → 𝑖 ∥ (𝑖 · 𝑗))
70	66, 68, 69	syl2anc 583	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∥ (𝑖 · 𝑗))
71		simprr 769	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑚 · 𝑛))
72	7, 60	sselid 3915	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℂ)
73		simprlr 776	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ 𝑌)
74		breq1 5073	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑛 → (𝑥 ∥ 𝑁 ↔ 𝑛 ∥ 𝑁))
75	74, 8	elrab2 3620	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ 𝑌 ↔ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝑁))
76	75	simplbi 497	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ 𝑌 → 𝑛 ∈ ℕ)
77	73, 76	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ ℕ)
78	77	nncnd 11919	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ ℂ)
79	72, 78	mulcomd 10927	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 · 𝑛) = (𝑛 · 𝑚))
80	71, 79	eqtrd 2778	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑛 · 𝑚))
81	70, 80	breqtrd 5096	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∥ (𝑛 · 𝑚))
82	77	nnzd 12354	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ ℤ)
83	34	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑁 ∈ ℤ)
84	66, 83	gcdcomd 16149	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 gcd 𝑁) = (𝑁 gcd 𝑖))
85	40	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑀 ∈ ℤ)
86	32	nnzd 12354	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℤ)
87	38	nnzd 12354	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℤ)
88	86, 87	gcdcomd 16149	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 gcd 𝑀) = (𝑀 gcd 𝑁))
89		dvdsmulf1o.3	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1)
90	88, 89	eqtrd 2778	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 gcd 𝑀) = 1)
91	90	ad2antrr 722	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑁 gcd 𝑀) = 1)
92	30	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∥ 𝑀)
93		rpdvds 16293	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ((𝑁 gcd 𝑀) = 1 ∧ 𝑖 ∥ 𝑀)) → (𝑁 gcd 𝑖) = 1)
94	83, 66, 85, 91, 92, 93	syl32anc 1376	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑁 gcd 𝑖) = 1)
95	84, 94	eqtrd 2778	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 gcd 𝑁) = 1)
96	75	simprbi 496	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ 𝑌 → 𝑛 ∥ 𝑁)
97	73, 96	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∥ 𝑁)
98		rpdvds 16293	. . . . . . . . . . 11 ⊢ (((𝑖 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑖 gcd 𝑁) = 1 ∧ 𝑛 ∥ 𝑁)) → (𝑖 gcd 𝑛) = 1)
99	66, 82, 83, 95, 97, 98	syl32anc 1376	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 gcd 𝑛) = 1)
100	64	nnzd 12354	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℤ)
101		coprmdvds 16286	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ) → ((𝑖 ∥ (𝑛 · 𝑚) ∧ (𝑖 gcd 𝑛) = 1) → 𝑖 ∥ 𝑚))
102	66, 82, 100, 101	syl3anc 1369	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → ((𝑖 ∥ (𝑛 · 𝑚) ∧ (𝑖 gcd 𝑛) = 1) → 𝑖 ∥ 𝑚))
103	81, 99, 102	mp2and 695	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∥ 𝑚)
104		dvdsmul1 15915	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 𝑚 ∥ (𝑚 · 𝑛))
105	100, 82, 104	syl2anc 583	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∥ (𝑚 · 𝑛))
106	58	nncnd 11919	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℂ)
107	67	nncnd 11919	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∈ ℂ)
108	106, 107	mulcomd 10927	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑗 · 𝑖))
109	71, 108	eqtr3d 2780	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 · 𝑛) = (𝑗 · 𝑖))
110	105, 109	breqtrd 5096	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∥ (𝑗 · 𝑖))
111	100, 83	gcdcomd 16149	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 gcd 𝑁) = (𝑁 gcd 𝑚))
112	62	simprbi 496	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ 𝑋 → 𝑚 ∥ 𝑀)
113	60, 112	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∥ 𝑀)
114		rpdvds 16293	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ((𝑁 gcd 𝑀) = 1 ∧ 𝑚 ∥ 𝑀)) → (𝑁 gcd 𝑚) = 1)
115	83, 100, 85, 91, 113, 114	syl32anc 1376	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑁 gcd 𝑚) = 1)
116	111, 115	eqtrd 2778	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 gcd 𝑁) = 1)
117	28	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∥ 𝑁)
118		rpdvds 16293	. . . . . . . . . . 11 ⊢ (((𝑚 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑚 gcd 𝑁) = 1 ∧ 𝑗 ∥ 𝑁)) → (𝑚 gcd 𝑗) = 1)
119	100, 68, 83, 116, 117, 118	syl32anc 1376	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 gcd 𝑗) = 1)
120		coprmdvds 16286	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑖 ∈ ℤ) → ((𝑚 ∥ (𝑗 · 𝑖) ∧ (𝑚 gcd 𝑗) = 1) → 𝑚 ∥ 𝑖))
121	100, 68, 66, 120	syl3anc 1369	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → ((𝑚 ∥ (𝑗 · 𝑖) ∧ (𝑚 gcd 𝑗) = 1) → 𝑚 ∥ 𝑖))
122	110, 119, 121	mp2and 695	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∥ 𝑖)
123		dvdseq 15951	. . . . . . . . 9 ⊢ (((𝑖 ∈ ℕ₀ ∧ 𝑚 ∈ ℕ₀) ∧ (𝑖 ∥ 𝑚 ∧ 𝑚 ∥ 𝑖)) → 𝑖 = 𝑚)
124	59, 65, 103, 122, 123	syl22anc 835	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 = 𝑚)
125	58	nnne0d 11953	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ≠ 0)
126	124	oveq1d 7270	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑛) = (𝑚 · 𝑛))
127	71, 126	eqtr4d 2781	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑖 · 𝑛))
128	107, 78, 106, 125, 127	mulcanad 11540	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 = 𝑛)
129	124, 128	opeq12d 4809	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩)
130	129	expr 456	. . . . . 6 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌)) → ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
131	130	ralrimivva 3114	. . . . 5 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
132	131	ralrimivva 3114	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑌 ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
133		fvres 6775	. . . . . . . . 9 ⊢ (𝑢 ∈ (𝑋 × 𝑌) → (( · ↾ (𝑋 × 𝑌))‘𝑢) = ( · ‘𝑢))
134		fvres 6775	. . . . . . . . 9 ⊢ (𝑣 ∈ (𝑋 × 𝑌) → (( · ↾ (𝑋 × 𝑌))‘𝑣) = ( · ‘𝑣))
135	133, 134	eqeqan12d 2752	. . . . . . . 8 ⊢ ((𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) → ((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) ↔ ( · ‘𝑢) = ( · ‘𝑣)))
136	135	imbi1d 341	. . . . . . 7 ⊢ ((𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) → (((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ (( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣)))
137	136	ralbidva 3119	. . . . . 6 ⊢ (𝑢 ∈ (𝑋 × 𝑌) → (∀𝑣 ∈ (𝑋 × 𝑌)((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑣 ∈ (𝑋 × 𝑌)(( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣)))
138	137	ralbiia 3089	. . . . 5 ⊢ (∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)(( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣))
139		fveq2 6756	. . . . . . . . . . 11 ⊢ (𝑣 = ⟨𝑚, 𝑛⟩ → ( · ‘𝑣) = ( · ‘⟨𝑚, 𝑛⟩))
140		df-ov 7258	. . . . . . . . . . 11 ⊢ (𝑚 · 𝑛) = ( · ‘⟨𝑚, 𝑛⟩)
141	139, 140	eqtr4di 2797	. . . . . . . . . 10 ⊢ (𝑣 = ⟨𝑚, 𝑛⟩ → ( · ‘𝑣) = (𝑚 · 𝑛))
142	141	eqeq2d 2749	. . . . . . . . 9 ⊢ (𝑣 = ⟨𝑚, 𝑛⟩ → (( · ‘𝑢) = ( · ‘𝑣) ↔ ( · ‘𝑢) = (𝑚 · 𝑛)))
143		eqeq2 2750	. . . . . . . . 9 ⊢ (𝑣 = ⟨𝑚, 𝑛⟩ → (𝑢 = 𝑣 ↔ 𝑢 = ⟨𝑚, 𝑛⟩))
144	142, 143	imbi12d 344	. . . . . . . 8 ⊢ (𝑣 = ⟨𝑚, 𝑛⟩ → ((( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣) ↔ (( · ‘𝑢) = (𝑚 · 𝑛) → 𝑢 = ⟨𝑚, 𝑛⟩)))
145	144	ralxp 5739	. . . . . . 7 ⊢ (∀𝑣 ∈ (𝑋 × 𝑌)(( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 (( · ‘𝑢) = (𝑚 · 𝑛) → 𝑢 = ⟨𝑚, 𝑛⟩))
146		fveq2 6756	. . . . . . . . . . 11 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → ( · ‘𝑢) = ( · ‘⟨𝑖, 𝑗⟩))
147		df-ov 7258	. . . . . . . . . . 11 ⊢ (𝑖 · 𝑗) = ( · ‘⟨𝑖, 𝑗⟩)
148	146, 147	eqtr4di 2797	. . . . . . . . . 10 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → ( · ‘𝑢) = (𝑖 · 𝑗))
149	148	eqeq1d 2740	. . . . . . . . 9 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (( · ‘𝑢) = (𝑚 · 𝑛) ↔ (𝑖 · 𝑗) = (𝑚 · 𝑛)))
150		eqeq1 2742	. . . . . . . . 9 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (𝑢 = ⟨𝑚, 𝑛⟩ ↔ ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
151	149, 150	imbi12d 344	. . . . . . . 8 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → ((( · ‘𝑢) = (𝑚 · 𝑛) → 𝑢 = ⟨𝑚, 𝑛⟩) ↔ ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩)))
152	151	2ralbidv 3122	. . . . . . 7 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 (( · ‘𝑢) = (𝑚 · 𝑛) → 𝑢 = ⟨𝑚, 𝑛⟩) ↔ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩)))
153	145, 152	syl5bb 282	. . . . . 6 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (∀𝑣 ∈ (𝑋 × 𝑌)(( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩)))
154	153	ralxp 5739	. . . . 5 ⊢ (∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)(( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑌 ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
155	138, 154	bitri 274	. . . 4 ⊢ (∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑌 ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
156	132, 155	sylibr 233	. . 3 ⊢ (𝜑 → ∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣))
157		dff13 7109	. . 3 ⊢ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1→𝑍 ↔ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍 ∧ ∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣)))
158	57, 156, 157	sylanbrc 582	. 2 ⊢ (𝜑 → ( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1→𝑍)
159		breq1 5073	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → (𝑥 ∥ (𝑀 · 𝑁) ↔ 𝑤 ∥ (𝑀 · 𝑁)))
160	159, 51	elrab2 3620	. . . . . . . . . . 11 ⊢ (𝑤 ∈ 𝑍 ↔ (𝑤 ∈ ℕ ∧ 𝑤 ∥ (𝑀 · 𝑁)))
161	160	simplbi 497	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑍 → 𝑤 ∈ ℕ)
162	161	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∈ ℕ)
163	162	nnzd 12354	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∈ ℤ)
164	38	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑀 ∈ ℕ)
165	164	nnzd 12354	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑀 ∈ ℤ)
166	164	nnne0d 11953	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑀 ≠ 0)
167		simpr 484	. . . . . . . . . 10 ⊢ ((𝑤 = 0 ∧ 𝑀 = 0) → 𝑀 = 0)
168	167	necon3ai 2967	. . . . . . . . 9 ⊢ (𝑀 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑀 = 0))
169	166, 168	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ¬ (𝑤 = 0 ∧ 𝑀 = 0))
170		gcdn0cl 16137	. . . . . . . 8 ⊢ (((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ 𝑀 = 0)) → (𝑤 gcd 𝑀) ∈ ℕ)
171	163, 165, 169, 170	syl21anc 834	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑀) ∈ ℕ)
172		gcddvds 16138	. . . . . . . . 9 ⊢ ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
173	163, 165, 172	syl2anc 583	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
174	173	simprd 495	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑀) ∥ 𝑀)
175		breq1 5073	. . . . . . . 8 ⊢ (𝑥 = (𝑤 gcd 𝑀) → (𝑥 ∥ 𝑀 ↔ (𝑤 gcd 𝑀) ∥ 𝑀))
176	175, 4	elrab2 3620	. . . . . . 7 ⊢ ((𝑤 gcd 𝑀) ∈ 𝑋 ↔ ((𝑤 gcd 𝑀) ∈ ℕ ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
177	171, 174, 176	sylanbrc 582	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑀) ∈ 𝑋)
178	32	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑁 ∈ ℕ)
179	178	nnzd 12354	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑁 ∈ ℤ)
180	178	nnne0d 11953	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑁 ≠ 0)
181		simpr 484	. . . . . . . . . 10 ⊢ ((𝑤 = 0 ∧ 𝑁 = 0) → 𝑁 = 0)
182	181	necon3ai 2967	. . . . . . . . 9 ⊢ (𝑁 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑁 = 0))
183	180, 182	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ¬ (𝑤 = 0 ∧ 𝑁 = 0))
184		gcdn0cl 16137	. . . . . . . 8 ⊢ (((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ 𝑁 = 0)) → (𝑤 gcd 𝑁) ∈ ℕ)
185	163, 179, 183, 184	syl21anc 834	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑁) ∈ ℕ)
186		gcddvds 16138	. . . . . . . . 9 ⊢ ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
187	163, 179, 186	syl2anc 583	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
188	187	simprd 495	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑁) ∥ 𝑁)
189		breq1 5073	. . . . . . . 8 ⊢ (𝑥 = (𝑤 gcd 𝑁) → (𝑥 ∥ 𝑁 ↔ (𝑤 gcd 𝑁) ∥ 𝑁))
190	189, 8	elrab2 3620	. . . . . . 7 ⊢ ((𝑤 gcd 𝑁) ∈ 𝑌 ↔ ((𝑤 gcd 𝑁) ∈ ℕ ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
191	185, 188, 190	sylanbrc 582	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑁) ∈ 𝑌)
192	177, 191	opelxpd 5618	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩ ∈ (𝑋 × 𝑌))
193	192	fvresd 6776	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (( · ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩) = ( · ‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
194	89	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑀 gcd 𝑁) = 1)
195		rpmulgcd2 16289	. . . . . . . 8 ⊢ (((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 gcd 𝑁) = 1) → (𝑤 gcd (𝑀 · 𝑁)) = ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)))
196	163, 165, 179, 194, 195	syl31anc 1371	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd (𝑀 · 𝑁)) = ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)))
197		df-ov 7258	. . . . . . 7 ⊢ ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)) = ( · ‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩)
198	196, 197	eqtrdi 2795	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd (𝑀 · 𝑁)) = ( · ‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
199	160	simprbi 496	. . . . . . . 8 ⊢ (𝑤 ∈ 𝑍 → 𝑤 ∥ (𝑀 · 𝑁))
200	199	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∥ (𝑀 · 𝑁))
201	38, 32	nnmulcld 11956	. . . . . . . 8 ⊢ (𝜑 → (𝑀 · 𝑁) ∈ ℕ)
202		gcdeq 16191	. . . . . . . 8 ⊢ ((𝑤 ∈ ℕ ∧ (𝑀 · 𝑁) ∈ ℕ) → ((𝑤 gcd (𝑀 · 𝑁)) = 𝑤 ↔ 𝑤 ∥ (𝑀 · 𝑁)))
203	161, 201, 202	syl2anr 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ((𝑤 gcd (𝑀 · 𝑁)) = 𝑤 ↔ 𝑤 ∥ (𝑀 · 𝑁)))
204	200, 203	mpbird 256	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd (𝑀 · 𝑁)) = 𝑤)
205	193, 198, 204	3eqtr2rd 2785	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 = (( · ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
206		fveq2 6756	. . . . . 6 ⊢ (𝑢 = ⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩ → (( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
207	206	rspceeqv 3567	. . . . 5 ⊢ ((⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩ ∈ (𝑋 × 𝑌) ∧ 𝑤 = (( · ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩)) → ∃𝑢 ∈ (𝑋 × 𝑌)𝑤 = (( · ↾ (𝑋 × 𝑌))‘𝑢))
208	192, 205, 207	syl2anc 583	. . . 4 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ∃𝑢 ∈ (𝑋 × 𝑌)𝑤 = (( · ↾ (𝑋 × 𝑌))‘𝑢))
209	208	ralrimiva 3107	. . 3 ⊢ (𝜑 → ∀𝑤 ∈ 𝑍 ∃𝑢 ∈ (𝑋 × 𝑌)𝑤 = (( · ↾ (𝑋 × 𝑌))‘𝑢))
210		dffo3 6960	. . 3 ⊢ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–onto→𝑍 ↔ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍 ∧ ∀𝑤 ∈ 𝑍 ∃𝑢 ∈ (𝑋 × 𝑌)𝑤 = (( · ↾ (𝑋 × 𝑌))‘𝑢)))
211	57, 209, 210	sylanbrc 582	. 2 ⊢ (𝜑 → ( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–onto→𝑍)
212		df-f1o 6425	. 2 ⊢ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1-onto→𝑍 ↔ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1→𝑍 ∧ ( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–onto→𝑍))
213	158, 211, 212	sylanbrc 582	1 ⊢ (𝜑 → ( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1-onto→𝑍)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 ∀wral 3063 ∃wrex 3064 {crab 3067 ⊆ wss 3883 ⟨cop 4564 class class class wbr 5070 × cxp 5578 ↾ cres 5582 Fn wfn 6413 ⟶wf 6414 –1-1→wf1 6415 –onto→wfo 6416 –1-1-onto→wf1o 6417 ‘cfv 6418 (class class class)co 7255 ℂcc 10800 0cc0 10802 1c1 10803 · cmul 10807 ℕcn 11903 ℕ₀cn0 12163 ℤcz 12249 ∥ cdvds 15891 gcd cgcd 16129

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880 ax-mulf 10882

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-er 8456 df-en 8692 df-dom 8693 df-sdom 8694 df-sup 9131 df-inf 9132 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-n0 12164 df-z 12250 df-uz 12512 df-rp 12660 df-fl 13440 df-mod 13518 df-seq 13650 df-exp 13711 df-cj 14738 df-re 14739 df-im 14740 df-sqrt 14874 df-abs 14875 df-dvds 15892 df-gcd 16130

This theorem is referenced by: fsumdvdsmul 26249

W3C validator