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 24720

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 9895	. . . . . . 7 ⊢ · :(ℂ × ℂ)⟶ℂ
2		ffn 5958	. . . . . . 7 ⊢ ( · :(ℂ × ℂ)⟶ℂ → · Fn (ℂ × ℂ))
3	1, 2	ax-mp 5	. . . . . 6 ⊢ · Fn (ℂ × ℂ)
4		dvdsmulf1o.x	. . . . . . . . 9 ⊢ 𝑋 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀}
5		ssrab2 3650	. . . . . . . . 9 ⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀} ⊆ ℕ
6	4, 5	eqsstri 3598	. . . . . . . 8 ⊢ 𝑋 ⊆ ℕ
7		nnsscn 10902	. . . . . . . 8 ⊢ ℕ ⊆ ℂ
8	6, 7	sstri 3577	. . . . . . 7 ⊢ 𝑋 ⊆ ℂ
9		dvdsmulf1o.y	. . . . . . . . 9 ⊢ 𝑌 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}
10		ssrab2 3650	. . . . . . . . 9 ⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ⊆ ℕ
11	9, 10	eqsstri 3598	. . . . . . . 8 ⊢ 𝑌 ⊆ ℕ
12	11, 7	sstri 3577	. . . . . . 7 ⊢ 𝑌 ⊆ ℂ
13		xpss12 5148	. . . . . . 7 ⊢ ((𝑋 ⊆ ℂ ∧ 𝑌 ⊆ ℂ) → (𝑋 × 𝑌) ⊆ (ℂ × ℂ))
14	8, 12, 13	mp2an 704	. . . . . 6 ⊢ (𝑋 × 𝑌) ⊆ (ℂ × ℂ)
15		fnssres 5918	. . . . . 6 ⊢ (( · Fn (ℂ × ℂ) ∧ (𝑋 × 𝑌) ⊆ (ℂ × ℂ)) → ( · ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌))
16	3, 14, 15	mp2an 704	. . . . 5 ⊢ ( · ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌)
17	16	a1i 11	. . . 4 ⊢ (𝜑 → ( · ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌))
18		ovres 6698	. . . . . . 7 ⊢ ((𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌) → (𝑖( · ↾ (𝑋 × 𝑌))𝑗) = (𝑖 · 𝑗))
19	18	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖( · ↾ (𝑋 × 𝑌))𝑗) = (𝑖 · 𝑗))
20		breq1 4586	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → (𝑥 ∥ 𝑀 ↔ 𝑖 ∥ 𝑀))
21	20, 4	elrab2 3333	. . . . . . . . . 10 ⊢ (𝑖 ∈ 𝑋 ↔ (𝑖 ∈ ℕ ∧ 𝑖 ∥ 𝑀))
22	21	simplbi 475	. . . . . . . . 9 ⊢ (𝑖 ∈ 𝑋 → 𝑖 ∈ ℕ)
23	22	ad2antrl 760	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑖 ∈ ℕ)
24		breq1 4586	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑗 → (𝑥 ∥ 𝑁 ↔ 𝑗 ∥ 𝑁))
25	24, 9	elrab2 3333	. . . . . . . . . 10 ⊢ (𝑗 ∈ 𝑌 ↔ (𝑗 ∈ ℕ ∧ 𝑗 ∥ 𝑁))
26	25	simplbi 475	. . . . . . . . 9 ⊢ (𝑗 ∈ 𝑌 → 𝑗 ∈ ℕ)
27	26	ad2antll 761	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑗 ∈ ℕ)
28	23, 27	nnmulcld 10945	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 · 𝑗) ∈ ℕ)
29	25	simprbi 479	. . . . . . . . 9 ⊢ (𝑗 ∈ 𝑌 → 𝑗 ∥ 𝑁)
30	29	ad2antll 761	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑗 ∥ 𝑁)
31	21	simprbi 479	. . . . . . . . 9 ⊢ (𝑖 ∈ 𝑋 → 𝑖 ∥ 𝑀)
32	31	ad2antrl 760	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑖 ∥ 𝑀)
33	27	nnzd 11357	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑗 ∈ ℤ)
34		dvdsmulf1o.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℕ)
35	34	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑁 ∈ ℕ)
36	35	nnzd 11357	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑁 ∈ ℤ)
37	23	nnzd 11357	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑖 ∈ ℤ)
38		dvdscmul 14846	. . . . . . . . . 10 ⊢ ((𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑗 ∥ 𝑁 → (𝑖 · 𝑗) ∥ (𝑖 · 𝑁)))
39	33, 36, 37, 38	syl3anc 1318	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑗 ∥ 𝑁 → (𝑖 · 𝑗) ∥ (𝑖 · 𝑁)))
40		dvdsmulf1o.1	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℕ)
41	40	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑀 ∈ ℕ)
42	41	nnzd 11357	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑀 ∈ ℤ)
43		dvdsmulc 14847	. . . . . . . . . 10 ⊢ ((𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∥ 𝑀 → (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)))
44	37, 42, 36, 43	syl3anc 1318	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 ∥ 𝑀 → (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)))
45	28	nnzd 11357	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 · 𝑗) ∈ ℤ)
46	37, 36	zmulcld 11364	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 · 𝑁) ∈ ℤ)
47	42, 36	zmulcld 11364	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑀 · 𝑁) ∈ ℤ)
48		dvdstr 14856	. . . . . . . . . 10 ⊢ (((𝑖 · 𝑗) ∈ ℤ ∧ (𝑖 · 𝑁) ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) → (((𝑖 · 𝑗) ∥ (𝑖 · 𝑁) ∧ (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
49	45, 46, 47, 48	syl3anc 1318	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (((𝑖 · 𝑗) ∥ (𝑖 · 𝑁) ∧ (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
50	39, 44, 49	syl2and 499	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → ((𝑗 ∥ 𝑁 ∧ 𝑖 ∥ 𝑀) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
51	30, 32, 50	mp2and 711	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁))
52		breq1 4586	. . . . . . . 8 ⊢ (𝑥 = (𝑖 · 𝑗) → (𝑥 ∥ (𝑀 · 𝑁) ↔ (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
53		dvdsmulf1o.z	. . . . . . . 8 ⊢ 𝑍 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑀 · 𝑁)}
54	52, 53	elrab2 3333	. . . . . . 7 ⊢ ((𝑖 · 𝑗) ∈ 𝑍 ↔ ((𝑖 · 𝑗) ∈ ℕ ∧ (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
55	28, 51, 54	sylanbrc 695	. . . . . 6 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 · 𝑗) ∈ 𝑍)
56	19, 55	eqeltrd 2688	. . . . 5 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖( · ↾ (𝑋 × 𝑌))𝑗) ∈ 𝑍)
57	56	ralrimivva 2954	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑌 (𝑖( · ↾ (𝑋 × 𝑌))𝑗) ∈ 𝑍)
58		ffnov 6662	. . . 4 ⊢ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍 ↔ (( · ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑌 (𝑖( · ↾ (𝑋 × 𝑌))𝑗) ∈ 𝑍))
59	17, 57, 58	sylanbrc 695	. . 3 ⊢ (𝜑 → ( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍)
60	23	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℕ)
61	60	nnnn0d 11228	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℕ₀)
62		simprll 798	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ 𝑋)
63		breq1 4586	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑚 → (𝑥 ∥ 𝑀 ↔ 𝑚 ∥ 𝑀))
64	63, 4	elrab2 3333	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ 𝑋 ↔ (𝑚 ∈ ℕ ∧ 𝑚 ∥ 𝑀))
65	64	simplbi 475	. . . . . . . . . . 11 ⊢ (𝑚 ∈ 𝑋 → 𝑚 ∈ ℕ)
66	62, 65	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℕ)
67	66	nnnn0d 11228	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℕ₀)
68	60	nnzd 11357	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℤ)
69	27	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∈ ℕ)
70	69	nnzd 11357	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∈ ℤ)
71		dvdsmul1 14841	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ) → 𝑖 ∥ (𝑖 · 𝑗))
72	68, 70, 71	syl2anc 691	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∥ (𝑖 · 𝑗))
73		simprr 792	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑚 · 𝑛))
74	8, 62	sseldi 3566	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℂ)
75		simprlr 799	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ 𝑌)
76		breq1 4586	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑛 → (𝑥 ∥ 𝑁 ↔ 𝑛 ∥ 𝑁))
77	76, 9	elrab2 3333	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ 𝑌 ↔ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝑁))
78	77	simplbi 475	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ 𝑌 → 𝑛 ∈ ℕ)
79	75, 78	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ ℕ)
80	79	nncnd 10913	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ ℂ)
81	74, 80	mulcomd 9940	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 · 𝑛) = (𝑛 · 𝑚))
82	73, 81	eqtrd 2644	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑛 · 𝑚))
83	72, 82	breqtrd 4609	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∥ (𝑛 · 𝑚))
84	79	nnzd 11357	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ ℤ)
85	36	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑁 ∈ ℤ)
86		gcdcom 15073	. . . . . . . . . . . . 13 ⊢ ((𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 gcd 𝑁) = (𝑁 gcd 𝑖))
87	68, 85, 86	syl2anc 691	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 gcd 𝑁) = (𝑁 gcd 𝑖))
88	42	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑀 ∈ ℤ)
89	34	nnzd 11357	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℤ)
90	40	nnzd 11357	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℤ)
91		gcdcom 15073	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁 gcd 𝑀) = (𝑀 gcd 𝑁))
92	89, 90, 91	syl2anc 691	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 gcd 𝑀) = (𝑀 gcd 𝑁))
93		dvdsmulf1o.3	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1)
94	92, 93	eqtrd 2644	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 gcd 𝑀) = 1)
95	94	ad2antrr 758	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑁 gcd 𝑀) = 1)
96	32	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∥ 𝑀)
97		rpdvds 15212	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ((𝑁 gcd 𝑀) = 1 ∧ 𝑖 ∥ 𝑀)) → (𝑁 gcd 𝑖) = 1)
98	85, 68, 88, 95, 96, 97	syl32anc 1326	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑁 gcd 𝑖) = 1)
99	87, 98	eqtrd 2644	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 gcd 𝑁) = 1)
100	77	simprbi 479	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ 𝑌 → 𝑛 ∥ 𝑁)
101	75, 100	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∥ 𝑁)
102		rpdvds 15212	. . . . . . . . . . 11 ⊢ (((𝑖 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑖 gcd 𝑁) = 1 ∧ 𝑛 ∥ 𝑁)) → (𝑖 gcd 𝑛) = 1)
103	68, 84, 85, 99, 101, 102	syl32anc 1326	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 gcd 𝑛) = 1)
104	66	nnzd 11357	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℤ)
105		coprmdvds 15204	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ) → ((𝑖 ∥ (𝑛 · 𝑚) ∧ (𝑖 gcd 𝑛) = 1) → 𝑖 ∥ 𝑚))
106	68, 84, 104, 105	syl3anc 1318	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → ((𝑖 ∥ (𝑛 · 𝑚) ∧ (𝑖 gcd 𝑛) = 1) → 𝑖 ∥ 𝑚))
107	83, 103, 106	mp2and 711	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∥ 𝑚)
108		dvdsmul1 14841	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 𝑚 ∥ (𝑚 · 𝑛))
109	104, 84, 108	syl2anc 691	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∥ (𝑚 · 𝑛))
110	60	nncnd 10913	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℂ)
111	69	nncnd 10913	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∈ ℂ)
112	110, 111	mulcomd 9940	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑗 · 𝑖))
113	73, 112	eqtr3d 2646	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 · 𝑛) = (𝑗 · 𝑖))
114	109, 113	breqtrd 4609	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∥ (𝑗 · 𝑖))
115		gcdcom 15073	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑚 gcd 𝑁) = (𝑁 gcd 𝑚))
116	104, 85, 115	syl2anc 691	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 gcd 𝑁) = (𝑁 gcd 𝑚))
117	64	simprbi 479	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ 𝑋 → 𝑚 ∥ 𝑀)
118	62, 117	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∥ 𝑀)
119		rpdvds 15212	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ((𝑁 gcd 𝑀) = 1 ∧ 𝑚 ∥ 𝑀)) → (𝑁 gcd 𝑚) = 1)
120	85, 104, 88, 95, 118, 119	syl32anc 1326	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑁 gcd 𝑚) = 1)
121	116, 120	eqtrd 2644	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 gcd 𝑁) = 1)
122	30	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∥ 𝑁)
123		rpdvds 15212	. . . . . . . . . . 11 ⊢ (((𝑚 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑚 gcd 𝑁) = 1 ∧ 𝑗 ∥ 𝑁)) → (𝑚 gcd 𝑗) = 1)
124	104, 70, 85, 121, 122, 123	syl32anc 1326	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 gcd 𝑗) = 1)
125		coprmdvds 15204	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑖 ∈ ℤ) → ((𝑚 ∥ (𝑗 · 𝑖) ∧ (𝑚 gcd 𝑗) = 1) → 𝑚 ∥ 𝑖))
126	104, 70, 68, 125	syl3anc 1318	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → ((𝑚 ∥ (𝑗 · 𝑖) ∧ (𝑚 gcd 𝑗) = 1) → 𝑚 ∥ 𝑖))
127	114, 124, 126	mp2and 711	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∥ 𝑖)
128		dvdseq 14874	. . . . . . . . 9 ⊢ (((𝑖 ∈ ℕ₀ ∧ 𝑚 ∈ ℕ₀) ∧ (𝑖 ∥ 𝑚 ∧ 𝑚 ∥ 𝑖)) → 𝑖 = 𝑚)
129	61, 67, 107, 127, 128	syl22anc 1319	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 = 𝑚)
130	60	nnne0d 10942	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ≠ 0)
131	129	oveq1d 6564	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑛) = (𝑚 · 𝑛))
132	73, 131	eqtr4d 2647	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑖 · 𝑛))
133	111, 80, 110, 130, 132	mulcanad 10541	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 = 𝑛)
134	129, 133	opeq12d 4348	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩)
135	134	expr 641	. . . . . 6 ⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌)) → ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
136	135	ralrimivva 2954	. . . . 5 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
137	136	ralrimivva 2954	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑌 ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
138		fvres 6117	. . . . . . . . 9 ⊢ (𝑢 ∈ (𝑋 × 𝑌) → (( · ↾ (𝑋 × 𝑌))‘𝑢) = ( · ‘𝑢))
139		fvres 6117	. . . . . . . . 9 ⊢ (𝑣 ∈ (𝑋 × 𝑌) → (( · ↾ (𝑋 × 𝑌))‘𝑣) = ( · ‘𝑣))
140	138, 139	eqeqan12d 2626	. . . . . . . 8 ⊢ ((𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) → ((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) ↔ ( · ‘𝑢) = ( · ‘𝑣)))
141	140	imbi1d 330	. . . . . . 7 ⊢ ((𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) → (((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ (( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣)))
142	141	ralbidva 2968	. . . . . 6 ⊢ (𝑢 ∈ (𝑋 × 𝑌) → (∀𝑣 ∈ (𝑋 × 𝑌)((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑣 ∈ (𝑋 × 𝑌)(( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣)))
143	142	ralbiia 2962	. . . . 5 ⊢ (∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)(( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣))
144		fveq2 6103	. . . . . . . . . . 11 ⊢ (𝑣 = ⟨𝑚, 𝑛⟩ → ( · ‘𝑣) = ( · ‘⟨𝑚, 𝑛⟩))
145		df-ov 6552	. . . . . . . . . . 11 ⊢ (𝑚 · 𝑛) = ( · ‘⟨𝑚, 𝑛⟩)
146	144, 145	syl6eqr 2662	. . . . . . . . . 10 ⊢ (𝑣 = ⟨𝑚, 𝑛⟩ → ( · ‘𝑣) = (𝑚 · 𝑛))
147	146	eqeq2d 2620	. . . . . . . . 9 ⊢ (𝑣 = ⟨𝑚, 𝑛⟩ → (( · ‘𝑢) = ( · ‘𝑣) ↔ ( · ‘𝑢) = (𝑚 · 𝑛)))
148		eqeq2 2621	. . . . . . . . 9 ⊢ (𝑣 = ⟨𝑚, 𝑛⟩ → (𝑢 = 𝑣 ↔ 𝑢 = ⟨𝑚, 𝑛⟩))
149	147, 148	imbi12d 333	. . . . . . . 8 ⊢ (𝑣 = ⟨𝑚, 𝑛⟩ → ((( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣) ↔ (( · ‘𝑢) = (𝑚 · 𝑛) → 𝑢 = ⟨𝑚, 𝑛⟩)))
150	149	ralxp 5185	. . . . . . 7 ⊢ (∀𝑣 ∈ (𝑋 × 𝑌)(( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 (( · ‘𝑢) = (𝑚 · 𝑛) → 𝑢 = ⟨𝑚, 𝑛⟩))
151		fveq2 6103	. . . . . . . . . . 11 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → ( · ‘𝑢) = ( · ‘⟨𝑖, 𝑗⟩))
152		df-ov 6552	. . . . . . . . . . 11 ⊢ (𝑖 · 𝑗) = ( · ‘⟨𝑖, 𝑗⟩)
153	151, 152	syl6eqr 2662	. . . . . . . . . 10 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → ( · ‘𝑢) = (𝑖 · 𝑗))
154	153	eqeq1d 2612	. . . . . . . . 9 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (( · ‘𝑢) = (𝑚 · 𝑛) ↔ (𝑖 · 𝑗) = (𝑚 · 𝑛)))
155		eqeq1 2614	. . . . . . . . 9 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (𝑢 = ⟨𝑚, 𝑛⟩ ↔ ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
156	154, 155	imbi12d 333	. . . . . . . 8 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → ((( · ‘𝑢) = (𝑚 · 𝑛) → 𝑢 = ⟨𝑚, 𝑛⟩) ↔ ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩)))
157	156	2ralbidv 2972	. . . . . . 7 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 (( · ‘𝑢) = (𝑚 · 𝑛) → 𝑢 = ⟨𝑚, 𝑛⟩) ↔ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩)))
158	150, 157	syl5bb 271	. . . . . 6 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (∀𝑣 ∈ (𝑋 × 𝑌)(( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩)))
159	158	ralxp 5185	. . . . 5 ⊢ (∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)(( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑌 ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
160	143, 159	bitri 263	. . . 4 ⊢ (∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑌 ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
161	137, 160	sylibr 223	. . 3 ⊢ (𝜑 → ∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣))
162		dff13 6416	. . 3 ⊢ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1→𝑍 ↔ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍 ∧ ∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣)))
163	59, 161, 162	sylanbrc 695	. 2 ⊢ (𝜑 → ( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1→𝑍)
164		breq1 4586	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → (𝑥 ∥ (𝑀 · 𝑁) ↔ 𝑤 ∥ (𝑀 · 𝑁)))
165	164, 53	elrab2 3333	. . . . . . . . . . 11 ⊢ (𝑤 ∈ 𝑍 ↔ (𝑤 ∈ ℕ ∧ 𝑤 ∥ (𝑀 · 𝑁)))
166	165	simplbi 475	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑍 → 𝑤 ∈ ℕ)
167	166	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∈ ℕ)
168	167	nnzd 11357	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∈ ℤ)
169	40	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑀 ∈ ℕ)
170	169	nnzd 11357	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑀 ∈ ℤ)
171	169	nnne0d 10942	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑀 ≠ 0)
172		simpr 476	. . . . . . . . . 10 ⊢ ((𝑤 = 0 ∧ 𝑀 = 0) → 𝑀 = 0)
173	172	necon3ai 2807	. . . . . . . . 9 ⊢ (𝑀 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑀 = 0))
174	171, 173	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ¬ (𝑤 = 0 ∧ 𝑀 = 0))
175		gcdn0cl 15062	. . . . . . . 8 ⊢ (((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ 𝑀 = 0)) → (𝑤 gcd 𝑀) ∈ ℕ)
176	168, 170, 174, 175	syl21anc 1317	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑀) ∈ ℕ)
177		gcddvds 15063	. . . . . . . . 9 ⊢ ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
178	168, 170, 177	syl2anc 691	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
179	178	simprd 478	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑀) ∥ 𝑀)
180		breq1 4586	. . . . . . . 8 ⊢ (𝑥 = (𝑤 gcd 𝑀) → (𝑥 ∥ 𝑀 ↔ (𝑤 gcd 𝑀) ∥ 𝑀))
181	180, 4	elrab2 3333	. . . . . . 7 ⊢ ((𝑤 gcd 𝑀) ∈ 𝑋 ↔ ((𝑤 gcd 𝑀) ∈ ℕ ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
182	176, 179, 181	sylanbrc 695	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑀) ∈ 𝑋)
183	34	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑁 ∈ ℕ)
184	183	nnzd 11357	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑁 ∈ ℤ)
185	183	nnne0d 10942	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑁 ≠ 0)
186		simpr 476	. . . . . . . . . 10 ⊢ ((𝑤 = 0 ∧ 𝑁 = 0) → 𝑁 = 0)
187	186	necon3ai 2807	. . . . . . . . 9 ⊢ (𝑁 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑁 = 0))
188	185, 187	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ¬ (𝑤 = 0 ∧ 𝑁 = 0))
189		gcdn0cl 15062	. . . . . . . 8 ⊢ (((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ 𝑁 = 0)) → (𝑤 gcd 𝑁) ∈ ℕ)
190	168, 184, 188, 189	syl21anc 1317	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑁) ∈ ℕ)
191		gcddvds 15063	. . . . . . . . 9 ⊢ ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
192	168, 184, 191	syl2anc 691	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
193	192	simprd 478	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑁) ∥ 𝑁)
194		breq1 4586	. . . . . . . 8 ⊢ (𝑥 = (𝑤 gcd 𝑁) → (𝑥 ∥ 𝑁 ↔ (𝑤 gcd 𝑁) ∥ 𝑁))
195	194, 9	elrab2 3333	. . . . . . 7 ⊢ ((𝑤 gcd 𝑁) ∈ 𝑌 ↔ ((𝑤 gcd 𝑁) ∈ ℕ ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
196	190, 193, 195	sylanbrc 695	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑁) ∈ 𝑌)
197		opelxpi 5072	. . . . . 6 ⊢ (((𝑤 gcd 𝑀) ∈ 𝑋 ∧ (𝑤 gcd 𝑁) ∈ 𝑌) → ⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩ ∈ (𝑋 × 𝑌))
198	182, 196, 197	syl2anc 691	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩ ∈ (𝑋 × 𝑌))
199		fvres 6117	. . . . . . 7 ⊢ (⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩ ∈ (𝑋 × 𝑌) → (( · ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩) = ( · ‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
200	198, 199	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (( · ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩) = ( · ‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
201	93	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑀 gcd 𝑁) = 1)
202		rpmulgcd2 15208	. . . . . . . 8 ⊢ (((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 gcd 𝑁) = 1) → (𝑤 gcd (𝑀 · 𝑁)) = ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)))
203	168, 170, 184, 201, 202	syl31anc 1321	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd (𝑀 · 𝑁)) = ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)))
204		df-ov 6552	. . . . . . 7 ⊢ ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)) = ( · ‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩)
205	203, 204	syl6eq 2660	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd (𝑀 · 𝑁)) = ( · ‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
206	165	simprbi 479	. . . . . . . 8 ⊢ (𝑤 ∈ 𝑍 → 𝑤 ∥ (𝑀 · 𝑁))
207	206	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∥ (𝑀 · 𝑁))
208	40, 34	nnmulcld 10945	. . . . . . . 8 ⊢ (𝜑 → (𝑀 · 𝑁) ∈ ℕ)
209		gcdeq 15110	. . . . . . . 8 ⊢ ((𝑤 ∈ ℕ ∧ (𝑀 · 𝑁) ∈ ℕ) → ((𝑤 gcd (𝑀 · 𝑁)) = 𝑤 ↔ 𝑤 ∥ (𝑀 · 𝑁)))
210	166, 208, 209	syl2anr 494	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ((𝑤 gcd (𝑀 · 𝑁)) = 𝑤 ↔ 𝑤 ∥ (𝑀 · 𝑁)))
211	207, 210	mpbird 246	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd (𝑀 · 𝑁)) = 𝑤)
212	200, 205, 211	3eqtr2rd 2651	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 = (( · ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
213		fveq2 6103	. . . . . . 7 ⊢ (𝑢 = ⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩ → (( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
214	213	eqeq2d 2620	. . . . . 6 ⊢ (𝑢 = ⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩ → (𝑤 = (( · ↾ (𝑋 × 𝑌))‘𝑢) ↔ 𝑤 = (( · ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩)))
215	214	rspcev 3282	. . . . 5 ⊢ ((⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩ ∈ (𝑋 × 𝑌) ∧ 𝑤 = (( · ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩)) → ∃𝑢 ∈ (𝑋 × 𝑌)𝑤 = (( · ↾ (𝑋 × 𝑌))‘𝑢))
216	198, 212, 215	syl2anc 691	. . . 4 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ∃𝑢 ∈ (𝑋 × 𝑌)𝑤 = (( · ↾ (𝑋 × 𝑌))‘𝑢))
217	216	ralrimiva 2949	. . 3 ⊢ (𝜑 → ∀𝑤 ∈ 𝑍 ∃𝑢 ∈ (𝑋 × 𝑌)𝑤 = (( · ↾ (𝑋 × 𝑌))‘𝑢))
218		dffo3 6282	. . 3 ⊢ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–onto→𝑍 ↔ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍 ∧ ∀𝑤 ∈ 𝑍 ∃𝑢 ∈ (𝑋 × 𝑌)𝑤 = (( · ↾ (𝑋 × 𝑌))‘𝑢)))
219	59, 217, 218	sylanbrc 695	. 2 ⊢ (𝜑 → ( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–onto→𝑍)
220		df-f1o 5811	. 2 ⊢ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1-onto→𝑍 ↔ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1→𝑍 ∧ ( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–onto→𝑍))
221	163, 219, 220	sylanbrc 695	1 ⊢ (𝜑 → ( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1-onto→𝑍)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 ∈ wcel 1977 ≠ wne 2780 ∀wral 2896 ∃wrex 2897 {crab 2900 ⊆ wss 3540 ⟨cop 4131 class class class wbr 4583 × cxp 5036 ↾ cres 5040 Fn wfn 5799 ⟶wf 5800 –1-1→wf1 5801 –onto→wfo 5802 –1-1-onto→wf1o 5803 ‘cfv 5804 (class class class)co 6549 ℂcc 9813 0cc0 9815 1c1 9816 · cmul 9820 ℕcn 10897 ℕ₀cn0 11169 ℤcz 11254 ∥ cdvds 14821 gcd cgcd 15054

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892 ax-pre-sup 9893 ax-mulf 9895

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-er 7629 df-en 7842 df-dom 7843 df-sdom 7844 df-sup 8231 df-inf 8232 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-2 10956 df-3 10957 df-n0 11170 df-z 11255 df-uz 11564 df-rp 11709 df-fl 12455 df-mod 12531 df-seq 12664 df-exp 12723 df-cj 13687 df-re 13688 df-im 13689 df-sqrt 13823 df-abs 13824 df-dvds 14822 df-gcd 15055

This theorem is referenced by: fsumdvdsmul 24721

W3C validator