Theorem mpodvdsmulf1o 15532

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 GG, 18-Apr-2025.)

Hypotheses

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

Assertion

Ref	Expression
mpodvdsmulf1o	⊢ (𝜑 → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1-onto→𝑍)

Distinct variable groups:   𝑥,𝑦,𝑀   𝑥,𝑁,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝑋(𝑥,𝑦)   𝑌(𝑥,𝑦)   𝑍(𝑥,𝑦)

Proof of Theorem mpodvdsmulf1o

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

Step	Hyp	Ref	Expression
1		mpomulf 8077	. . . . . . 7 ⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)):(ℂ × ℂ)⟶ℂ
2		ffn 5434	. . . . . . 7 ⊢ ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)):(ℂ × ℂ)⟶ℂ → (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) Fn (ℂ × ℂ))
3	1, 2	ax-mp 5	. . . . . 6 ⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) Fn (ℂ × ℂ)
4		mpodvdsmulf1o.x	. . . . . . . . 9 ⊢ 𝑋 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀}
5	4	ssrab3 3283	. . . . . . . 8 ⊢ 𝑋 ⊆ ℕ
6		nnsscn 9056	. . . . . . . 8 ⊢ ℕ ⊆ ℂ
7	5, 6	sstri 3206	. . . . . . 7 ⊢ 𝑋 ⊆ ℂ
8		mpodvdsmulf1o.y	. . . . . . . . 9 ⊢ 𝑌 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}
9	8	ssrab3 3283	. . . . . . . 8 ⊢ 𝑌 ⊆ ℕ
10	9, 6	sstri 3206	. . . . . . 7 ⊢ 𝑌 ⊆ ℂ
11		xpss12 4789	. . . . . . 7 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑌 ⊆ ℂ) → (𝑋 × 𝑌) ⊆ (ℂ × ℂ))
12	7, 10, 11	mp2an 426	. . . . . 6 ⊢ (𝑋 × 𝑌) ⊆ (ℂ × ℂ)
13		fnssres 5397	. . . . . 6 ⊢ (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) Fn (ℂ × ℂ) ∧ (𝑋 × 𝑌) ⊆ (ℂ × ℂ)) → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌))
14	3, 12, 13	mp2an 426	. . . . 5 ⊢ ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌)
15	14	a1i 9	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌))
16		ovres 6098	. . . . . . 7 ⊢ ((𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌) → (𝑖((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))𝑗) = (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗))
17	16	adantl 277	. . . . . 6 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))𝑗) = (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗))
18	7	sseli 3193	. . . . . . . . . 10 ⊢ (𝑖 ∈ 𝑋 → 𝑖 ∈ ℂ)
19	18	adantr 276	. . . . . . . . 9 ⊢ ((𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌) → 𝑖 ∈ ℂ)
20	10	sseli 3193	. . . . . . . . . 10 ⊢ (𝑗 ∈ 𝑌 → 𝑗 ∈ ℂ)
21	20	adantl 277	. . . . . . . . 9 ⊢ ((𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌) → 𝑗 ∈ ℂ)
22	19, 21	mulcld 8108	. . . . . . . . 9 ⊢ ((𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌) → (𝑖 · 𝑗) ∈ ℂ)
23		oveq1 5963	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → (𝑥 · 𝑦) = (𝑖 · 𝑦))
24		oveq2 5964	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑗 → (𝑖 · 𝑦) = (𝑖 · 𝑗))
25		eqid 2206	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))
26	23, 24, 25	ovmpog 6092	. . . . . . . . . 10 ⊢ ((𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ ∧ (𝑖 · 𝑗) ∈ ℂ) → (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑖 · 𝑗))
27	26	eqcomd 2212	. . . . . . . . 9 ⊢ ((𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ ∧ (𝑖 · 𝑗) ∈ ℂ) → (𝑖 · 𝑗) = (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗))
28	19, 21, 22, 27	syl3anc 1250	. . . . . . . 8 ⊢ ((𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌) → (𝑖 · 𝑗) = (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗))
29	28	adantl 277	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 · 𝑗) = (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗))
30	5	sseli 3193	. . . . . . . . . 10 ⊢ (𝑖 ∈ 𝑋 → 𝑖 ∈ ℕ)
31	30	ad2antrl 490	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑖 ∈ ℕ)
32	9	sseli 3193	. . . . . . . . . 10 ⊢ (𝑗 ∈ 𝑌 → 𝑗 ∈ ℕ)
33	32	ad2antll 491	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑗 ∈ ℕ)
34	31, 33	nnmulcld 9100	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 · 𝑗) ∈ ℕ)
35		breq1 4053	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑗 → (𝑥 ∥ 𝑁 ↔ 𝑗 ∥ 𝑁))
36	35, 8	elrab2 2936	. . . . . . . . . . 11 ⊢ (𝑗 ∈ 𝑌 ↔ (𝑗 ∈ ℕ ∧ 𝑗 ∥ 𝑁))
37	36	simprbi 275	. . . . . . . . . 10 ⊢ (𝑗 ∈ 𝑌 → 𝑗 ∥ 𝑁)
38	37	ad2antll 491	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑗 ∥ 𝑁)
39		breq1 4053	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑖 → (𝑥 ∥ 𝑀 ↔ 𝑖 ∥ 𝑀))
40	39, 4	elrab2 2936	. . . . . . . . . . 11 ⊢ (𝑖 ∈ 𝑋 ↔ (𝑖 ∈ ℕ ∧ 𝑖 ∥ 𝑀))
41	40	simprbi 275	. . . . . . . . . 10 ⊢ (𝑖 ∈ 𝑋 → 𝑖 ∥ 𝑀)
42	41	ad2antrl 490	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑖 ∥ 𝑀)
43	33	nnzd 9509	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑗 ∈ ℤ)
44		mpodvdsmulf1o.2	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℕ)
45	44	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑁 ∈ ℕ)
46	45	nnzd 9509	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑁 ∈ ℤ)
47	31	nnzd 9509	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑖 ∈ ℤ)
48		dvdscmul 12199	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑗 ∥ 𝑁 → (𝑖 · 𝑗) ∥ (𝑖 · 𝑁)))
49	43, 46, 47, 48	syl3anc 1250	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑗 ∥ 𝑁 → (𝑖 · 𝑗) ∥ (𝑖 · 𝑁)))
50		mpodvdsmulf1o.1	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℕ)
51	50	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑀 ∈ ℕ)
52	51	nnzd 9509	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑀 ∈ ℤ)
53		dvdsmulc 12200	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∥ 𝑀 → (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)))
54	47, 52, 46, 53	syl3anc 1250	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 ∥ 𝑀 → (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)))
55	34	nnzd 9509	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 · 𝑗) ∈ ℤ)
56	47, 46	zmulcld 9516	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 · 𝑁) ∈ ℤ)
57	52, 46	zmulcld 9516	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑀 · 𝑁) ∈ ℤ)
58		dvdstr 12209	. . . . . . . . . . 11 ⊢ (((𝑖 · 𝑗) ∈ ℤ ∧ (𝑖 · 𝑁) ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) → (((𝑖 · 𝑗) ∥ (𝑖 · 𝑁) ∧ (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
59	55, 56, 57, 58	syl3anc 1250	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (((𝑖 · 𝑗) ∥ (𝑖 · 𝑁) ∧ (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
60	49, 54, 59	syl2and 295	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → ((𝑗 ∥ 𝑁 ∧ 𝑖 ∥ 𝑀) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
61	38, 42, 60	mp2and 433	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁))
62		breq1 4053	. . . . . . . . 9 ⊢ (𝑥 = (𝑖 · 𝑗) → (𝑥 ∥ (𝑀 · 𝑁) ↔ (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
63		mpodvdsmulf1o.z	. . . . . . . . 9 ⊢ 𝑍 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑀 · 𝑁)}
64	62, 63	elrab2 2936	. . . . . . . 8 ⊢ ((𝑖 · 𝑗) ∈ 𝑍 ↔ ((𝑖 · 𝑗) ∈ ℕ ∧ (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
65	34, 61, 64	sylanbrc 417	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 · 𝑗) ∈ 𝑍)
66	29, 65	eqeltrrd 2284	. . . . . 6 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) ∈ 𝑍)
67	17, 66	eqeltrd 2283	. . . . 5 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))𝑗) ∈ 𝑍)
68	67	ralrimivva 2589	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑌 (𝑖((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))𝑗) ∈ 𝑍)
69		ffnov 6061	. . . 4 ⊢ (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍 ↔ (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑌 (𝑖((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))𝑗) ∈ 𝑍))
70	15, 68, 69	sylanbrc 417	. . 3 ⊢ (𝜑 → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍)
71	19	ad2antlr 489	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌)) → 𝑖 ∈ ℂ)
72	21	ad2antlr 489	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌)) → 𝑗 ∈ ℂ)
73	22	ad2antlr 489	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌)) → (𝑖 · 𝑗) ∈ ℂ)
74	71, 72, 73, 26	syl3anc 1250	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌)) → (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑖 · 𝑗))
75	7	sseli 3193	. . . . . . . . . 10 ⊢ (𝑚 ∈ 𝑋 → 𝑚 ∈ ℂ)
76	75	ad2antrl 490	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌)) → 𝑚 ∈ ℂ)
77	10	sseli 3193	. . . . . . . . . 10 ⊢ (𝑛 ∈ 𝑌 → 𝑛 ∈ ℂ)
78	77	ad2antll 491	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌)) → 𝑛 ∈ ℂ)
79	76, 78	mulcld 8108	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌)) → (𝑚 · 𝑛) ∈ ℂ)
80		oveq1 5963	. . . . . . . . . 10 ⊢ (𝑥 = 𝑚 → (𝑥 · 𝑦) = (𝑚 · 𝑦))
81		oveq2 5964	. . . . . . . . . 10 ⊢ (𝑦 = 𝑛 → (𝑚 · 𝑦) = (𝑚 · 𝑛))
82	80, 81, 25	ovmpog 6092	. . . . . . . . 9 ⊢ ((𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ ∧ (𝑚 · 𝑛) ∈ ℂ) → (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) = (𝑚 · 𝑛))
83	76, 78, 79, 82	syl3anc 1250	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌)) → (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) = (𝑚 · 𝑛))
84	74, 83	eqeq12d 2221	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌)) → ((𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) ↔ (𝑖 · 𝑗) = (𝑚 · 𝑛)))
85	31	adantr 276	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℕ)
86	85	nnnn0d 9363	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℕ0)
87		simprll 537	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ 𝑋)
88	5, 87	sselid 3195	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℕ)
89	88	nnnn0d 9363	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℕ0)
90	85	nnzd 9509	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℤ)
91	33	adantr 276	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∈ ℕ)
92	91	nnzd 9509	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∈ ℤ)
93		dvdsmul1 12194	. . . . . . . . . . . . 13 ⊢ ((𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ) → 𝑖 ∥ (𝑖 · 𝑗))
94	90, 92, 93	syl2anc 411	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∥ (𝑖 · 𝑗))
95		simprr 531	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑚 · 𝑛))
96	7, 87	sselid 3195	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℂ)
97		simprlr 538	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ 𝑌)
98	10, 97	sselid 3195	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ ℂ)
99	96, 98	mulcomd 8109	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 · 𝑛) = (𝑛 · 𝑚))
100	95, 99	eqtrd 2239	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑛 · 𝑚))
101	94, 100	breqtrd 4076	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∥ (𝑛 · 𝑚))
102	9, 97	sselid 3195	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ ℕ)
103	102	nnzd 9509	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ ℤ)
104	46	adantr 276	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑁 ∈ ℤ)
105	90, 104	gcdcomd 12365	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 gcd 𝑁) = (𝑁 gcd 𝑖))
106	52	adantr 276	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑀 ∈ ℤ)
107	44	nnzd 9509	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ ℤ)
108	50	nnzd 9509	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℤ)
109	107, 108	gcdcomd 12365	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 gcd 𝑀) = (𝑀 gcd 𝑁))
110		mpodvdsmulf1o.3	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1)
111	109, 110	eqtrd 2239	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 gcd 𝑀) = 1)
112	111	ad2antrr 488	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑁 gcd 𝑀) = 1)
113	42	adantr 276	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∥ 𝑀)
114		rpdvds 12491	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ((𝑁 gcd 𝑀) = 1 ∧ 𝑖 ∥ 𝑀)) → (𝑁 gcd 𝑖) = 1)
115	104, 90, 106, 112, 113, 114	syl32anc 1258	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑁 gcd 𝑖) = 1)
116	105, 115	eqtrd 2239	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 gcd 𝑁) = 1)
117		breq1 4053	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑛 → (𝑥 ∥ 𝑁 ↔ 𝑛 ∥ 𝑁))
118	117, 8	elrab2 2936	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ 𝑌 ↔ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝑁))
119	118	simprbi 275	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ 𝑌 → 𝑛 ∥ 𝑁)
120	97, 119	syl 14	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∥ 𝑁)
121		rpdvds 12491	. . . . . . . . . . . 12 ⊢ (((𝑖 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑖 gcd 𝑁) = 1 ∧ 𝑛 ∥ 𝑁)) → (𝑖 gcd 𝑛) = 1)
122	90, 103, 104, 116, 120, 121	syl32anc 1258	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 gcd 𝑛) = 1)
123	88	nnzd 9509	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℤ)
124		coprmdvds 12484	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ) → ((𝑖 ∥ (𝑛 · 𝑚) ∧ (𝑖 gcd 𝑛) = 1) → 𝑖 ∥ 𝑚))
125	90, 103, 123, 124	syl3anc 1250	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → ((𝑖 ∥ (𝑛 · 𝑚) ∧ (𝑖 gcd 𝑛) = 1) → 𝑖 ∥ 𝑚))
126	101, 122, 125	mp2and 433	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∥ 𝑚)
127		dvdsmul1 12194	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 𝑚 ∥ (𝑚 · 𝑛))
128	123, 103, 127	syl2anc 411	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∥ (𝑚 · 𝑛))
129	85	nncnd 9065	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℂ)
130	91	nncnd 9065	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∈ ℂ)
131	129, 130	mulcomd 8109	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑗 · 𝑖))
132	95, 131	eqtr3d 2241	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 · 𝑛) = (𝑗 · 𝑖))
133	128, 132	breqtrd 4076	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∥ (𝑗 · 𝑖))
134	123, 104	gcdcomd 12365	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 gcd 𝑁) = (𝑁 gcd 𝑚))
135		breq1 4053	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑚 → (𝑥 ∥ 𝑀 ↔ 𝑚 ∥ 𝑀))
136	135, 4	elrab2 2936	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ 𝑋 ↔ (𝑚 ∈ ℕ ∧ 𝑚 ∥ 𝑀))
137	136	simprbi 275	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ 𝑋 → 𝑚 ∥ 𝑀)
138	87, 137	syl 14	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∥ 𝑀)
139		rpdvds 12491	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ((𝑁 gcd 𝑀) = 1 ∧ 𝑚 ∥ 𝑀)) → (𝑁 gcd 𝑚) = 1)
140	104, 123, 106, 112, 138, 139	syl32anc 1258	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑁 gcd 𝑚) = 1)
141	134, 140	eqtrd 2239	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 gcd 𝑁) = 1)
142	38	adantr 276	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∥ 𝑁)
143		rpdvds 12491	. . . . . . . . . . . 12 ⊢ (((𝑚 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑚 gcd 𝑁) = 1 ∧ 𝑗 ∥ 𝑁)) → (𝑚 gcd 𝑗) = 1)
144	123, 92, 104, 141, 142, 143	syl32anc 1258	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 gcd 𝑗) = 1)
145		coprmdvds 12484	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑖 ∈ ℤ) → ((𝑚 ∥ (𝑗 · 𝑖) ∧ (𝑚 gcd 𝑗) = 1) → 𝑚 ∥ 𝑖))
146	123, 92, 90, 145	syl3anc 1250	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → ((𝑚 ∥ (𝑗 · 𝑖) ∧ (𝑚 gcd 𝑗) = 1) → 𝑚 ∥ 𝑖))
147	133, 144, 146	mp2and 433	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∥ 𝑖)
148		dvdseq 12229	. . . . . . . . . 10 ⊢ (((𝑖 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0) ∧ (𝑖 ∥ 𝑚 ∧ 𝑚 ∥ 𝑖)) → 𝑖 = 𝑚)
149	86, 89, 126, 147, 148	syl22anc 1251	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 = 𝑚)
150	85	nnap0d 9097	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 # 0)
151	149	oveq1d 5971	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑛) = (𝑚 · 𝑛))
152	95, 151	eqtr4d 2242	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑖 · 𝑛))
153	130, 98, 129, 150, 152	mulcanapad 8751	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 = 𝑛)
154	149, 153	opeq12d 3832	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩)
155	154	expr 375	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌)) → ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
156	84, 155	sylbid 150	. . . . . 6 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌)) → ((𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
157	156	ralrimivva 2589	. . . . 5 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
158	157	ralrimivva 2589	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑌 ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
159		fvres 5612	. . . . . . . . 9 ⊢ (𝑢 ∈ (𝑋 × 𝑌) → (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢))
160		fvres 5612	. . . . . . . . 9 ⊢ (𝑣 ∈ (𝑋 × 𝑌) → (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑣) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣))
161	159, 160	eqeqan12d 2222	. . . . . . . 8 ⊢ ((𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) → ((((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢) = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑣) ↔ ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣)))
162	161	imbi1d 231	. . . . . . 7 ⊢ ((𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) → (((((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢) = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣) → 𝑢 = 𝑣)))
163	162	ralbidva 2503	. . . . . 6 ⊢ (𝑢 ∈ (𝑋 × 𝑌) → (∀𝑣 ∈ (𝑋 × 𝑌)((((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢) = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑣 ∈ (𝑋 × 𝑌)(((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣) → 𝑢 = 𝑣)))
164	163	ralbiia 2521	. . . . 5 ⊢ (∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢) = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)(((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣) → 𝑢 = 𝑣))
165		fveq2 5588	. . . . . . . . . . 11 ⊢ (𝑣 = ⟨𝑚, 𝑛⟩ → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘⟨𝑚, 𝑛⟩))
166		df-ov 5959	. . . . . . . . . . 11 ⊢ (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘⟨𝑚, 𝑛⟩)
167	165, 166	eqtr4di 2257	. . . . . . . . . 10 ⊢ (𝑣 = ⟨𝑚, 𝑛⟩ → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛))
168	167	eqeq2d 2218	. . . . . . . . 9 ⊢ (𝑣 = ⟨𝑚, 𝑛⟩ → (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣) ↔ ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛)))
169		eqeq2 2216	. . . . . . . . 9 ⊢ (𝑣 = ⟨𝑚, 𝑛⟩ → (𝑢 = 𝑣 ↔ 𝑢 = ⟨𝑚, 𝑛⟩))
170	168, 169	imbi12d 234	. . . . . . . 8 ⊢ (𝑣 = ⟨𝑚, 𝑛⟩ → ((((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣) → 𝑢 = 𝑣) ↔ (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → 𝑢 = ⟨𝑚, 𝑛⟩)))
171	170	ralxp 4828	. . . . . . 7 ⊢ (∀𝑣 ∈ (𝑋 × 𝑌)(((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → 𝑢 = ⟨𝑚, 𝑛⟩))
172		fveq2 5588	. . . . . . . . . . 11 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘⟨𝑖, 𝑗⟩))
173		df-ov 5959	. . . . . . . . . . 11 ⊢ (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘⟨𝑖, 𝑗⟩)
174	172, 173	eqtr4di 2257	. . . . . . . . . 10 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗))
175	174	eqeq1d 2215	. . . . . . . . 9 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) ↔ (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛)))
176		eqeq1 2213	. . . . . . . . 9 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (𝑢 = ⟨𝑚, 𝑛⟩ ↔ ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
177	175, 176	imbi12d 234	. . . . . . . 8 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → ((((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → 𝑢 = ⟨𝑚, 𝑛⟩) ↔ ((𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩)))
178	177	2ralbidv 2531	. . . . . . 7 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → 𝑢 = ⟨𝑚, 𝑛⟩) ↔ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩)))
179	171, 178	bitrid 192	. . . . . 6 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (∀𝑣 ∈ (𝑋 × 𝑌)(((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩)))
180	179	ralxp 4828	. . . . 5 ⊢ (∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)(((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑌 ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
181	164, 180	bitri 184	. . . 4 ⊢ (∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢) = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑌 ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
182	158, 181	sylibr 134	. . 3 ⊢ (𝜑 → ∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢) = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣))
183		dff13 5849	. . 3 ⊢ (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1→𝑍 ↔ (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍 ∧ ∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢) = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣)))
184	70, 182, 183	sylanbrc 417	. 2 ⊢ (𝜑 → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1→𝑍)
185		breq1 4053	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → (𝑥 ∥ (𝑀 · 𝑁) ↔ 𝑤 ∥ (𝑀 · 𝑁)))
186	185, 63	elrab2 2936	. . . . . . . . . . 11 ⊢ (𝑤 ∈ 𝑍 ↔ (𝑤 ∈ ℕ ∧ 𝑤 ∥ (𝑀 · 𝑁)))
187	186	simplbi 274	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑍 → 𝑤 ∈ ℕ)
188	187	adantl 277	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∈ ℕ)
189	188	nnzd 9509	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∈ ℤ)
190	50	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑀 ∈ ℕ)
191	190	nnzd 9509	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑀 ∈ ℤ)
192	190	nnne0d 9096	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑀 ≠ 0)
193		simpr 110	. . . . . . . . . 10 ⊢ ((𝑤 = 0 ∧ 𝑀 = 0) → 𝑀 = 0)
194	193	necon3ai 2426	. . . . . . . . 9 ⊢ (𝑀 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑀 = 0))
195	192, 194	syl 14	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ¬ (𝑤 = 0 ∧ 𝑀 = 0))
196		gcdn0cl 12353	. . . . . . . 8 ⊢ (((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ 𝑀 = 0)) → (𝑤 gcd 𝑀) ∈ ℕ)
197	189, 191, 195, 196	syl21anc 1249	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑀) ∈ ℕ)
198		gcddvds 12354	. . . . . . . . 9 ⊢ ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
199	189, 191, 198	syl2anc 411	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
200	199	simprd 114	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑀) ∥ 𝑀)
201		breq1 4053	. . . . . . . 8 ⊢ (𝑥 = (𝑤 gcd 𝑀) → (𝑥 ∥ 𝑀 ↔ (𝑤 gcd 𝑀) ∥ 𝑀))
202	201, 4	elrab2 2936	. . . . . . 7 ⊢ ((𝑤 gcd 𝑀) ∈ 𝑋 ↔ ((𝑤 gcd 𝑀) ∈ ℕ ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
203	197, 200, 202	sylanbrc 417	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑀) ∈ 𝑋)
204	44	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑁 ∈ ℕ)
205	204	nnzd 9509	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑁 ∈ ℤ)
206	204	nnne0d 9096	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑁 ≠ 0)
207		simpr 110	. . . . . . . . . 10 ⊢ ((𝑤 = 0 ∧ 𝑁 = 0) → 𝑁 = 0)
208	207	necon3ai 2426	. . . . . . . . 9 ⊢ (𝑁 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑁 = 0))
209	206, 208	syl 14	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ¬ (𝑤 = 0 ∧ 𝑁 = 0))
210		gcdn0cl 12353	. . . . . . . 8 ⊢ (((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ 𝑁 = 0)) → (𝑤 gcd 𝑁) ∈ ℕ)
211	189, 205, 209, 210	syl21anc 1249	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑁) ∈ ℕ)
212		gcddvds 12354	. . . . . . . . 9 ⊢ ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
213	189, 205, 212	syl2anc 411	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
214	213	simprd 114	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑁) ∥ 𝑁)
215		breq1 4053	. . . . . . . 8 ⊢ (𝑥 = (𝑤 gcd 𝑁) → (𝑥 ∥ 𝑁 ↔ (𝑤 gcd 𝑁) ∥ 𝑁))
216	215, 8	elrab2 2936	. . . . . . 7 ⊢ ((𝑤 gcd 𝑁) ∈ 𝑌 ↔ ((𝑤 gcd 𝑁) ∈ ℕ ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
217	211, 214, 216	sylanbrc 417	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑁) ∈ 𝑌)
218	203, 217	opelxpd 4715	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩ ∈ (𝑋 × 𝑌))
219	218	fvresd 5613	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
220		df-ov 5959	. . . . . . . 8 ⊢ ((𝑤 gcd 𝑀)(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))(𝑤 gcd 𝑁)) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩)
221	197	nncnd 9065	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑀) ∈ ℂ)
222	211	nncnd 9065	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑁) ∈ ℂ)
223	197, 211	nnmulcld 9100	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)) ∈ ℕ)
224		oveq1 5963	. . . . . . . . . 10 ⊢ (𝑥 = (𝑤 gcd 𝑀) → (𝑥 · 𝑦) = ((𝑤 gcd 𝑀) · 𝑦))
225		oveq2 5964	. . . . . . . . . 10 ⊢ (𝑦 = (𝑤 gcd 𝑁) → ((𝑤 gcd 𝑀) · 𝑦) = ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)))
226	224, 225, 25	ovmpog 6092	. . . . . . . . 9 ⊢ (((𝑤 gcd 𝑀) ∈ ℂ ∧ (𝑤 gcd 𝑁) ∈ ℂ ∧ ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)) ∈ ℕ) → ((𝑤 gcd 𝑀)(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))(𝑤 gcd 𝑁)) = ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)))
227	221, 222, 223, 226	syl3anc 1250	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ((𝑤 gcd 𝑀)(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))(𝑤 gcd 𝑁)) = ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)))
228	220, 227	eqtr3id 2253	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩) = ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)))
229		df-ov 5959	. . . . . . . 8 ⊢ ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)) = ( · ‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩)
230	229	a1i 9	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)) = ( · ‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
231	219, 228, 230	3eqtrd 2243	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩) = ( · ‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
232	110	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑀 gcd 𝑁) = 1)
233		rpmulgcd2 12487	. . . . . . . 8 ⊢ (((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 gcd 𝑁) = 1) → (𝑤 gcd (𝑀 · 𝑁)) = ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)))
234	189, 191, 205, 232, 233	syl31anc 1253	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd (𝑀 · 𝑁)) = ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)))
235	234, 229	eqtrdi 2255	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd (𝑀 · 𝑁)) = ( · ‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
236	186	simprbi 275	. . . . . . . 8 ⊢ (𝑤 ∈ 𝑍 → 𝑤 ∥ (𝑀 · 𝑁))
237	236	adantl 277	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∥ (𝑀 · 𝑁))
238	50, 44	nnmulcld 9100	. . . . . . . 8 ⊢ (𝜑 → (𝑀 · 𝑁) ∈ ℕ)
239		gcdeq 12414	. . . . . . . 8 ⊢ ((𝑤 ∈ ℕ ∧ (𝑀 · 𝑁) ∈ ℕ) → ((𝑤 gcd (𝑀 · 𝑁)) = 𝑤 ↔ 𝑤 ∥ (𝑀 · 𝑁)))
240	187, 238, 239	syl2anr 290	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ((𝑤 gcd (𝑀 · 𝑁)) = 𝑤 ↔ 𝑤 ∥ (𝑀 · 𝑁)))
241	237, 240	mpbird 167	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd (𝑀 · 𝑁)) = 𝑤)
242	231, 235, 241	3eqtr2rd 2246	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
243		fveq2 5588	. . . . . 6 ⊢ (𝑢 = ⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩ → (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢) = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
244	243	rspceeqv 2899	. . . . 5 ⊢ ((⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩ ∈ (𝑋 × 𝑌) ∧ 𝑤 = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩)) → ∃𝑢 ∈ (𝑋 × 𝑌)𝑤 = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢))
245	218, 242, 244	syl2anc 411	. . . 4 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ∃𝑢 ∈ (𝑋 × 𝑌)𝑤 = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢))
246	245	ralrimiva 2580	. . 3 ⊢ (𝜑 → ∀𝑤 ∈ 𝑍 ∃𝑢 ∈ (𝑋 × 𝑌)𝑤 = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢))
247		dffo3 5739	. . 3 ⊢ (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–onto→𝑍 ↔ (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍 ∧ ∀𝑤 ∈ 𝑍 ∃𝑢 ∈ (𝑋 × 𝑌)𝑤 = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢)))
248	70, 246, 247	sylanbrc 417	. 2 ⊢ (𝜑 → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–onto→𝑍)
249		df-f1o 5286	. 2 ⊢ (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1-onto→𝑍 ↔ (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1→𝑍 ∧ ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–onto→𝑍))
250	184, 248, 249	sylanbrc 417	1 ⊢ (𝜑 → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1-onto→𝑍)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 981   = wceq 1373   ∈ wcel 2177   ≠ wne 2377  ∀wral 2485  ∃wrex 2486  {crab 2489   ⊆ wss 3170  ⟨cop 3640   class class class wbr 4050   × cxp 4680   ↾ cres 4684   Fn wfn 5274  ⟶wf 5275  –1-1→wf1 5276  –onto→wfo 5277  –1-1-onto→wf1o 5278  ‘cfv 5279  (class class class)co 5956   ∈ cmpo 5958  ℂcc 7938  0cc0 7940  1c1 7941   · cmul 7945  ℕcn 9051  ℕ₀cn0 9310  ℤcz 9387   ∥ cdvds 12168   gcd cgcd 12344

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2179  ax-14 2180  ax-ext 2188  ax-coll 4166  ax-sep 4169  ax-nul 4177  ax-pow 4225  ax-pr 4260  ax-un 4487  ax-setind 4592  ax-iinf 4643  ax-cnex 8031  ax-resscn 8032  ax-1cn 8033  ax-1re 8034  ax-icn 8035  ax-addcl 8036  ax-addrcl 8037  ax-mulcl 8038  ax-mulrcl 8039  ax-addcom 8040  ax-mulcom 8041  ax-addass 8042  ax-mulass 8043  ax-distr 8044  ax-i2m1 8045  ax-0lt1 8046  ax-1rid 8047  ax-0id 8048  ax-rnegex 8049  ax-precex 8050  ax-cnre 8051  ax-pre-ltirr 8052  ax-pre-ltwlin 8053  ax-pre-lttrn 8054  ax-pre-apti 8055  ax-pre-ltadd 8056  ax-pre-mulgt0 8057  ax-pre-mulext 8058  ax-arch 8059  ax-caucvg 8060

This theorem depends on definitions:  df-bi 117  df-stab 833  df-dc 837  df-3or 982  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ne 2378  df-nel 2473  df-ral 2490  df-rex 2491  df-reu 2492  df-rmo 2493  df-rab 2494  df-v 2775  df-sbc 3003  df-csb 3098  df-dif 3172  df-un 3174  df-in 3176  df-ss 3183  df-nul 3465  df-if 3576  df-pw 3622  df-sn 3643  df-pr 3644  df-op 3646  df-uni 3856  df-int 3891  df-iun 3934  df-br 4051  df-opab 4113  df-mpt 4114  df-tr 4150  df-id 4347  df-po 4350  df-iso 4351  df-iord 4420  df-on 4422  df-ilim 4423  df-suc 4425  df-iom 4646  df-xp 4688  df-rel 4689  df-cnv 4690  df-co 4691  df-dm 4692  df-rn 4693  df-res 4694  df-ima 4695  df-iota 5240  df-fun 5281  df-fn 5282  df-f 5283  df-f1 5284  df-fo 5285  df-f1o 5286  df-fv 5287  df-riota 5911  df-ov 5959  df-oprab 5960  df-mpo 5961  df-1st 6238  df-2nd 6239  df-recs 6403  df-frec 6489  df-sup 7100  df-pnf 8124  df-mnf 8125  df-xr 8126  df-ltxr 8127  df-le 8128  df-sub 8260  df-neg 8261  df-reap 8663  df-ap 8670  df-div 8761  df-inn 9052  df-2 9110  df-3 9111  df-4 9112  df-n0 9311  df-z 9388  df-uz 9664  df-q 9756  df-rp 9791  df-fz 10146  df-fzo 10280  df-fl 10430  df-mod 10485  df-seqfrec 10610  df-exp 10701  df-cj 11223  df-re 11224  df-im 11225  df-rsqrt 11379  df-abs 11380  df-dvds 12169  df-gcd 12345

This theorem is referenced by:  fsumdvdsmul  15533