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

Theorem dvdsmulf1o 25140
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.
StepHypRef Expression
1 ax-mulf 10228 . . . . . . 7 · :(ℂ × ℂ)⟶ℂ
2 ffn 6206 . . . . . . 7 ( · :(ℂ × ℂ)⟶ℂ → · Fn (ℂ × ℂ))
31, 2ax-mp 5 . . . . . 6 · Fn (ℂ × ℂ)
4 dvdsmulf1o.x . . . . . . . . 9 𝑋 = {𝑥 ∈ ℕ ∣ 𝑥𝑀}
5 ssrab2 3828 . . . . . . . . 9 {𝑥 ∈ ℕ ∣ 𝑥𝑀} ⊆ ℕ
64, 5eqsstri 3776 . . . . . . . 8 𝑋 ⊆ ℕ
7 nnsscn 11237 . . . . . . . 8 ℕ ⊆ ℂ
86, 7sstri 3753 . . . . . . 7 𝑋 ⊆ ℂ
9 dvdsmulf1o.y . . . . . . . . 9 𝑌 = {𝑥 ∈ ℕ ∣ 𝑥𝑁}
10 ssrab2 3828 . . . . . . . . 9 {𝑥 ∈ ℕ ∣ 𝑥𝑁} ⊆ ℕ
119, 10eqsstri 3776 . . . . . . . 8 𝑌 ⊆ ℕ
1211, 7sstri 3753 . . . . . . 7 𝑌 ⊆ ℂ
13 xpss12 5281 . . . . . . 7 ((𝑋 ⊆ ℂ ∧ 𝑌 ⊆ ℂ) → (𝑋 × 𝑌) ⊆ (ℂ × ℂ))
148, 12, 13mp2an 710 . . . . . 6 (𝑋 × 𝑌) ⊆ (ℂ × ℂ)
15 fnssres 6165 . . . . . 6 (( · Fn (ℂ × ℂ) ∧ (𝑋 × 𝑌) ⊆ (ℂ × ℂ)) → ( · ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌))
163, 14, 15mp2an 710 . . . . 5 ( · ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌)
1716a1i 11 . . . 4 (𝜑 → ( · ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌))
18 ovres 6966 . . . . . . 7 ((𝑖𝑋𝑗𝑌) → (𝑖( · ↾ (𝑋 × 𝑌))𝑗) = (𝑖 · 𝑗))
1918adantl 473 . . . . . 6 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (𝑖( · ↾ (𝑋 × 𝑌))𝑗) = (𝑖 · 𝑗))
20 breq1 4807 . . . . . . . . . . 11 (𝑥 = 𝑖 → (𝑥𝑀𝑖𝑀))
2120, 4elrab2 3507 . . . . . . . . . 10 (𝑖𝑋 ↔ (𝑖 ∈ ℕ ∧ 𝑖𝑀))
2221simplbi 478 . . . . . . . . 9 (𝑖𝑋𝑖 ∈ ℕ)
2322ad2antrl 766 . . . . . . . 8 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → 𝑖 ∈ ℕ)
24 breq1 4807 . . . . . . . . . . 11 (𝑥 = 𝑗 → (𝑥𝑁𝑗𝑁))
2524, 9elrab2 3507 . . . . . . . . . 10 (𝑗𝑌 ↔ (𝑗 ∈ ℕ ∧ 𝑗𝑁))
2625simplbi 478 . . . . . . . . 9 (𝑗𝑌𝑗 ∈ ℕ)
2726ad2antll 767 . . . . . . . 8 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → 𝑗 ∈ ℕ)
2823, 27nnmulcld 11280 . . . . . . 7 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (𝑖 · 𝑗) ∈ ℕ)
2925simprbi 483 . . . . . . . . 9 (𝑗𝑌𝑗𝑁)
3029ad2antll 767 . . . . . . . 8 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → 𝑗𝑁)
3121simprbi 483 . . . . . . . . 9 (𝑖𝑋𝑖𝑀)
3231ad2antrl 766 . . . . . . . 8 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → 𝑖𝑀)
3327nnzd 11693 . . . . . . . . . 10 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → 𝑗 ∈ ℤ)
34 dvdsmulf1o.2 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℕ)
3534adantr 472 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → 𝑁 ∈ ℕ)
3635nnzd 11693 . . . . . . . . . 10 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → 𝑁 ∈ ℤ)
3723nnzd 11693 . . . . . . . . . 10 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → 𝑖 ∈ ℤ)
38 dvdscmul 15230 . . . . . . . . . 10 ((𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑗𝑁 → (𝑖 · 𝑗) ∥ (𝑖 · 𝑁)))
3933, 36, 37, 38syl3anc 1477 . . . . . . . . 9 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (𝑗𝑁 → (𝑖 · 𝑗) ∥ (𝑖 · 𝑁)))
40 dvdsmulf1o.1 . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℕ)
4140adantr 472 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → 𝑀 ∈ ℕ)
4241nnzd 11693 . . . . . . . . . 10 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → 𝑀 ∈ ℤ)
43 dvdsmulc 15231 . . . . . . . . . 10 ((𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖𝑀 → (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)))
4437, 42, 36, 43syl3anc 1477 . . . . . . . . 9 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (𝑖𝑀 → (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)))
4528nnzd 11693 . . . . . . . . . 10 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (𝑖 · 𝑗) ∈ ℤ)
4637, 36zmulcld 11700 . . . . . . . . . 10 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (𝑖 · 𝑁) ∈ ℤ)
4742, 36zmulcld 11700 . . . . . . . . . 10 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (𝑀 · 𝑁) ∈ ℤ)
48 dvdstr 15240 . . . . . . . . . 10 (((𝑖 · 𝑗) ∈ ℤ ∧ (𝑖 · 𝑁) ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) → (((𝑖 · 𝑗) ∥ (𝑖 · 𝑁) ∧ (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
4945, 46, 47, 48syl3anc 1477 . . . . . . . . 9 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (((𝑖 · 𝑗) ∥ (𝑖 · 𝑁) ∧ (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
5039, 44, 49syl2and 501 . . . . . . . 8 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → ((𝑗𝑁𝑖𝑀) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
5130, 32, 50mp2and 717 . . . . . . 7 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁))
52 breq1 4807 . . . . . . . 8 (𝑥 = (𝑖 · 𝑗) → (𝑥 ∥ (𝑀 · 𝑁) ↔ (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
53 dvdsmulf1o.z . . . . . . . 8 𝑍 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑀 · 𝑁)}
5452, 53elrab2 3507 . . . . . . 7 ((𝑖 · 𝑗) ∈ 𝑍 ↔ ((𝑖 · 𝑗) ∈ ℕ ∧ (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
5528, 51, 54sylanbrc 701 . . . . . 6 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (𝑖 · 𝑗) ∈ 𝑍)
5619, 55eqeltrd 2839 . . . . 5 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (𝑖( · ↾ (𝑋 × 𝑌))𝑗) ∈ 𝑍)
5756ralrimivva 3109 . . . 4 (𝜑 → ∀𝑖𝑋𝑗𝑌 (𝑖( · ↾ (𝑋 × 𝑌))𝑗) ∈ 𝑍)
58 ffnov 6930 . . . 4 (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍 ↔ (( · ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌) ∧ ∀𝑖𝑋𝑗𝑌 (𝑖( · ↾ (𝑋 × 𝑌))𝑗) ∈ 𝑍))
5917, 57, 58sylanbrc 701 . . 3 (𝜑 → ( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍)
6023adantr 472 . . . . . . . . . 10 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℕ)
6160nnnn0d 11563 . . . . . . . . 9 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℕ0)
62 simprll 821 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚𝑋)
63 breq1 4807 . . . . . . . . . . . . 13 (𝑥 = 𝑚 → (𝑥𝑀𝑚𝑀))
6463, 4elrab2 3507 . . . . . . . . . . . 12 (𝑚𝑋 ↔ (𝑚 ∈ ℕ ∧ 𝑚𝑀))
6564simplbi 478 . . . . . . . . . . 11 (𝑚𝑋𝑚 ∈ ℕ)
6662, 65syl 17 . . . . . . . . . 10 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℕ)
6766nnnn0d 11563 . . . . . . . . 9 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℕ0)
6860nnzd 11693 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℤ)
6927adantr 472 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∈ ℕ)
7069nnzd 11693 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∈ ℤ)
71 dvdsmul1 15225 . . . . . . . . . . . 12 ((𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ) → 𝑖 ∥ (𝑖 · 𝑗))
7268, 70, 71syl2anc 696 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∥ (𝑖 · 𝑗))
73 simprr 813 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑚 · 𝑛))
748, 62sseldi 3742 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℂ)
75 simprlr 822 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛𝑌)
76 breq1 4807 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑛 → (𝑥𝑁𝑛𝑁))
7776, 9elrab2 3507 . . . . . . . . . . . . . . . 16 (𝑛𝑌 ↔ (𝑛 ∈ ℕ ∧ 𝑛𝑁))
7877simplbi 478 . . . . . . . . . . . . . . 15 (𝑛𝑌𝑛 ∈ ℕ)
7975, 78syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ ℕ)
8079nncnd 11248 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ ℂ)
8174, 80mulcomd 10273 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 · 𝑛) = (𝑛 · 𝑚))
8273, 81eqtrd 2794 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑛 · 𝑚))
8372, 82breqtrd 4830 . . . . . . . . . 10 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∥ (𝑛 · 𝑚))
8479nnzd 11693 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ ℤ)
8536adantr 472 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑁 ∈ ℤ)
86 gcdcom 15457 . . . . . . . . . . . . 13 ((𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 gcd 𝑁) = (𝑁 gcd 𝑖))
8768, 85, 86syl2anc 696 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 gcd 𝑁) = (𝑁 gcd 𝑖))
8842adantr 472 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑀 ∈ ℤ)
8934nnzd 11693 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℤ)
9040nnzd 11693 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℤ)
91 gcdcom 15457 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁 gcd 𝑀) = (𝑀 gcd 𝑁))
9289, 90, 91syl2anc 696 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 gcd 𝑀) = (𝑀 gcd 𝑁))
93 dvdsmulf1o.3 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀 gcd 𝑁) = 1)
9492, 93eqtrd 2794 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 gcd 𝑀) = 1)
9594ad2antrr 764 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑁 gcd 𝑀) = 1)
9632adantr 472 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖𝑀)
97 rpdvds 15596 . . . . . . . . . . . . 13 (((𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ((𝑁 gcd 𝑀) = 1 ∧ 𝑖𝑀)) → (𝑁 gcd 𝑖) = 1)
9885, 68, 88, 95, 96, 97syl32anc 1485 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑁 gcd 𝑖) = 1)
9987, 98eqtrd 2794 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 gcd 𝑁) = 1)
10077simprbi 483 . . . . . . . . . . . 12 (𝑛𝑌𝑛𝑁)
10175, 100syl 17 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛𝑁)
102 rpdvds 15596 . . . . . . . . . . 11 (((𝑖 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑖 gcd 𝑁) = 1 ∧ 𝑛𝑁)) → (𝑖 gcd 𝑛) = 1)
10368, 84, 85, 99, 101, 102syl32anc 1485 . . . . . . . . . 10 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 gcd 𝑛) = 1)
10466nnzd 11693 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℤ)
105 coprmdvds 15588 . . . . . . . . . . 11 ((𝑖 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ) → ((𝑖 ∥ (𝑛 · 𝑚) ∧ (𝑖 gcd 𝑛) = 1) → 𝑖𝑚))
10668, 84, 104, 105syl3anc 1477 . . . . . . . . . 10 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → ((𝑖 ∥ (𝑛 · 𝑚) ∧ (𝑖 gcd 𝑛) = 1) → 𝑖𝑚))
10783, 103, 106mp2and 717 . . . . . . . . 9 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖𝑚)
108 dvdsmul1 15225 . . . . . . . . . . . 12 ((𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 𝑚 ∥ (𝑚 · 𝑛))
109104, 84, 108syl2anc 696 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∥ (𝑚 · 𝑛))
11060nncnd 11248 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℂ)
11169nncnd 11248 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∈ ℂ)
112110, 111mulcomd 10273 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑗 · 𝑖))
11373, 112eqtr3d 2796 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 · 𝑛) = (𝑗 · 𝑖))
114109, 113breqtrd 4830 . . . . . . . . . 10 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∥ (𝑗 · 𝑖))
115 gcdcom 15457 . . . . . . . . . . . . 13 ((𝑚 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑚 gcd 𝑁) = (𝑁 gcd 𝑚))
116104, 85, 115syl2anc 696 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 gcd 𝑁) = (𝑁 gcd 𝑚))
11764simprbi 483 . . . . . . . . . . . . . 14 (𝑚𝑋𝑚𝑀)
11862, 117syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚𝑀)
119 rpdvds 15596 . . . . . . . . . . . . 13 (((𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ((𝑁 gcd 𝑀) = 1 ∧ 𝑚𝑀)) → (𝑁 gcd 𝑚) = 1)
12085, 104, 88, 95, 118, 119syl32anc 1485 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑁 gcd 𝑚) = 1)
121116, 120eqtrd 2794 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 gcd 𝑁) = 1)
12230adantr 472 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗𝑁)
123 rpdvds 15596 . . . . . . . . . . 11 (((𝑚 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑚 gcd 𝑁) = 1 ∧ 𝑗𝑁)) → (𝑚 gcd 𝑗) = 1)
124104, 70, 85, 121, 122, 123syl32anc 1485 . . . . . . . . . 10 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 gcd 𝑗) = 1)
125 coprmdvds 15588 . . . . . . . . . . 11 ((𝑚 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑖 ∈ ℤ) → ((𝑚 ∥ (𝑗 · 𝑖) ∧ (𝑚 gcd 𝑗) = 1) → 𝑚𝑖))
126104, 70, 68, 125syl3anc 1477 . . . . . . . . . 10 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → ((𝑚 ∥ (𝑗 · 𝑖) ∧ (𝑚 gcd 𝑗) = 1) → 𝑚𝑖))
127114, 124, 126mp2and 717 . . . . . . . . 9 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚𝑖)
128 dvdseq 15258 . . . . . . . . 9 (((𝑖 ∈ ℕ0𝑚 ∈ ℕ0) ∧ (𝑖𝑚𝑚𝑖)) → 𝑖 = 𝑚)
12961, 67, 107, 127, 128syl22anc 1478 . . . . . . . 8 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 = 𝑚)
13060nnne0d 11277 . . . . . . . . 9 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ≠ 0)
131129oveq1d 6829 . . . . . . . . . 10 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑛) = (𝑚 · 𝑛))
13273, 131eqtr4d 2797 . . . . . . . . 9 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑖 · 𝑛))
133111, 80, 110, 130, 132mulcanad 10874 . . . . . . . 8 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 = 𝑛)
134129, 133opeq12d 4561 . . . . . . 7 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩)
135134expr 644 . . . . . 6 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ (𝑚𝑋𝑛𝑌)) → ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
136135ralrimivva 3109 . . . . 5 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → ∀𝑚𝑋𝑛𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
137136ralrimivva 3109 . . . 4 (𝜑 → ∀𝑖𝑋𝑗𝑌𝑚𝑋𝑛𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
138 fvres 6369 . . . . . . . . 9 (𝑢 ∈ (𝑋 × 𝑌) → (( · ↾ (𝑋 × 𝑌))‘𝑢) = ( · ‘𝑢))
139 fvres 6369 . . . . . . . . 9 (𝑣 ∈ (𝑋 × 𝑌) → (( · ↾ (𝑋 × 𝑌))‘𝑣) = ( · ‘𝑣))
140138, 139eqeqan12d 2776 . . . . . . . 8 ((𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) → ((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) ↔ ( · ‘𝑢) = ( · ‘𝑣)))
141140imbi1d 330 . . . . . . 7 ((𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) → (((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ (( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣)))
142141ralbidva 3123 . . . . . 6 (𝑢 ∈ (𝑋 × 𝑌) → (∀𝑣 ∈ (𝑋 × 𝑌)((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑣 ∈ (𝑋 × 𝑌)(( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣)))
143142ralbiia 3117 . . . . 5 (∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)(( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣))
144 fveq2 6353 . . . . . . . . . . 11 (𝑣 = ⟨𝑚, 𝑛⟩ → ( · ‘𝑣) = ( · ‘⟨𝑚, 𝑛⟩))
145 df-ov 6817 . . . . . . . . . . 11 (𝑚 · 𝑛) = ( · ‘⟨𝑚, 𝑛⟩)
146144, 145syl6eqr 2812 . . . . . . . . . 10 (𝑣 = ⟨𝑚, 𝑛⟩ → ( · ‘𝑣) = (𝑚 · 𝑛))
147146eqeq2d 2770 . . . . . . . . 9 (𝑣 = ⟨𝑚, 𝑛⟩ → (( · ‘𝑢) = ( · ‘𝑣) ↔ ( · ‘𝑢) = (𝑚 · 𝑛)))
148 eqeq2 2771 . . . . . . . . 9 (𝑣 = ⟨𝑚, 𝑛⟩ → (𝑢 = 𝑣𝑢 = ⟨𝑚, 𝑛⟩))
149147, 148imbi12d 333 . . . . . . . 8 (𝑣 = ⟨𝑚, 𝑛⟩ → ((( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣) ↔ (( · ‘𝑢) = (𝑚 · 𝑛) → 𝑢 = ⟨𝑚, 𝑛⟩)))
150149ralxp 5419 . . . . . . 7 (∀𝑣 ∈ (𝑋 × 𝑌)(( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑚𝑋𝑛𝑌 (( · ‘𝑢) = (𝑚 · 𝑛) → 𝑢 = ⟨𝑚, 𝑛⟩))
151 fveq2 6353 . . . . . . . . . . 11 (𝑢 = ⟨𝑖, 𝑗⟩ → ( · ‘𝑢) = ( · ‘⟨𝑖, 𝑗⟩))
152 df-ov 6817 . . . . . . . . . . 11 (𝑖 · 𝑗) = ( · ‘⟨𝑖, 𝑗⟩)
153151, 152syl6eqr 2812 . . . . . . . . . 10 (𝑢 = ⟨𝑖, 𝑗⟩ → ( · ‘𝑢) = (𝑖 · 𝑗))
154153eqeq1d 2762 . . . . . . . . 9 (𝑢 = ⟨𝑖, 𝑗⟩ → (( · ‘𝑢) = (𝑚 · 𝑛) ↔ (𝑖 · 𝑗) = (𝑚 · 𝑛)))
155 eqeq1 2764 . . . . . . . . 9 (𝑢 = ⟨𝑖, 𝑗⟩ → (𝑢 = ⟨𝑚, 𝑛⟩ ↔ ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
156154, 155imbi12d 333 . . . . . . . 8 (𝑢 = ⟨𝑖, 𝑗⟩ → ((( · ‘𝑢) = (𝑚 · 𝑛) → 𝑢 = ⟨𝑚, 𝑛⟩) ↔ ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩)))
1571562ralbidv 3127 . . . . . . 7 (𝑢 = ⟨𝑖, 𝑗⟩ → (∀𝑚𝑋𝑛𝑌 (( · ‘𝑢) = (𝑚 · 𝑛) → 𝑢 = ⟨𝑚, 𝑛⟩) ↔ ∀𝑚𝑋𝑛𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩)))
158150, 157syl5bb 272 . . . . . 6 (𝑢 = ⟨𝑖, 𝑗⟩ → (∀𝑣 ∈ (𝑋 × 𝑌)(( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑚𝑋𝑛𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩)))
159158ralxp 5419 . . . . 5 (∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)(( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑖𝑋𝑗𝑌𝑚𝑋𝑛𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
160143, 159bitri 264 . . . 4 (∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑖𝑋𝑗𝑌𝑚𝑋𝑛𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
161137, 160sylibr 224 . . 3 (𝜑 → ∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣))
162 dff13 6676 . . 3 (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1𝑍 ↔ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍 ∧ ∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣)))
16359, 161, 162sylanbrc 701 . 2 (𝜑 → ( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1𝑍)
164 breq1 4807 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (𝑥 ∥ (𝑀 · 𝑁) ↔ 𝑤 ∥ (𝑀 · 𝑁)))
165164, 53elrab2 3507 . . . . . . . . . . 11 (𝑤𝑍 ↔ (𝑤 ∈ ℕ ∧ 𝑤 ∥ (𝑀 · 𝑁)))
166165simplbi 478 . . . . . . . . . 10 (𝑤𝑍𝑤 ∈ ℕ)
167166adantl 473 . . . . . . . . 9 ((𝜑𝑤𝑍) → 𝑤 ∈ ℕ)
168167nnzd 11693 . . . . . . . 8 ((𝜑𝑤𝑍) → 𝑤 ∈ ℤ)
16940adantr 472 . . . . . . . . 9 ((𝜑𝑤𝑍) → 𝑀 ∈ ℕ)
170169nnzd 11693 . . . . . . . 8 ((𝜑𝑤𝑍) → 𝑀 ∈ ℤ)
171169nnne0d 11277 . . . . . . . . 9 ((𝜑𝑤𝑍) → 𝑀 ≠ 0)
172 simpr 479 . . . . . . . . . 10 ((𝑤 = 0 ∧ 𝑀 = 0) → 𝑀 = 0)
173172necon3ai 2957 . . . . . . . . 9 (𝑀 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑀 = 0))
174171, 173syl 17 . . . . . . . 8 ((𝜑𝑤𝑍) → ¬ (𝑤 = 0 ∧ 𝑀 = 0))
175 gcdn0cl 15446 . . . . . . . 8 (((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ 𝑀 = 0)) → (𝑤 gcd 𝑀) ∈ ℕ)
176168, 170, 174, 175syl21anc 1476 . . . . . . 7 ((𝜑𝑤𝑍) → (𝑤 gcd 𝑀) ∈ ℕ)
177 gcddvds 15447 . . . . . . . . 9 ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
178168, 170, 177syl2anc 696 . . . . . . . 8 ((𝜑𝑤𝑍) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
179178simprd 482 . . . . . . 7 ((𝜑𝑤𝑍) → (𝑤 gcd 𝑀) ∥ 𝑀)
180 breq1 4807 . . . . . . . 8 (𝑥 = (𝑤 gcd 𝑀) → (𝑥𝑀 ↔ (𝑤 gcd 𝑀) ∥ 𝑀))
181180, 4elrab2 3507 . . . . . . 7 ((𝑤 gcd 𝑀) ∈ 𝑋 ↔ ((𝑤 gcd 𝑀) ∈ ℕ ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
182176, 179, 181sylanbrc 701 . . . . . 6 ((𝜑𝑤𝑍) → (𝑤 gcd 𝑀) ∈ 𝑋)
18334adantr 472 . . . . . . . . 9 ((𝜑𝑤𝑍) → 𝑁 ∈ ℕ)
184183nnzd 11693 . . . . . . . 8 ((𝜑𝑤𝑍) → 𝑁 ∈ ℤ)
185183nnne0d 11277 . . . . . . . . 9 ((𝜑𝑤𝑍) → 𝑁 ≠ 0)
186 simpr 479 . . . . . . . . . 10 ((𝑤 = 0 ∧ 𝑁 = 0) → 𝑁 = 0)
187186necon3ai 2957 . . . . . . . . 9 (𝑁 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑁 = 0))
188185, 187syl 17 . . . . . . . 8 ((𝜑𝑤𝑍) → ¬ (𝑤 = 0 ∧ 𝑁 = 0))
189 gcdn0cl 15446 . . . . . . . 8 (((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ 𝑁 = 0)) → (𝑤 gcd 𝑁) ∈ ℕ)
190168, 184, 188, 189syl21anc 1476 . . . . . . 7 ((𝜑𝑤𝑍) → (𝑤 gcd 𝑁) ∈ ℕ)
191 gcddvds 15447 . . . . . . . . 9 ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
192168, 184, 191syl2anc 696 . . . . . . . 8 ((𝜑𝑤𝑍) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
193192simprd 482 . . . . . . 7 ((𝜑𝑤𝑍) → (𝑤 gcd 𝑁) ∥ 𝑁)
194 breq1 4807 . . . . . . . 8 (𝑥 = (𝑤 gcd 𝑁) → (𝑥𝑁 ↔ (𝑤 gcd 𝑁) ∥ 𝑁))
195194, 9elrab2 3507 . . . . . . 7 ((𝑤 gcd 𝑁) ∈ 𝑌 ↔ ((𝑤 gcd 𝑁) ∈ ℕ ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
196190, 193, 195sylanbrc 701 . . . . . 6 ((𝜑𝑤𝑍) → (𝑤 gcd 𝑁) ∈ 𝑌)
197 opelxpi 5305 . . . . . 6 (((𝑤 gcd 𝑀) ∈ 𝑋 ∧ (𝑤 gcd 𝑁) ∈ 𝑌) → ⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩ ∈ (𝑋 × 𝑌))
198182, 196, 197syl2anc 696 . . . . 5 ((𝜑𝑤𝑍) → ⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩ ∈ (𝑋 × 𝑌))
199 fvres 6369 . . . . . . 7 (⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩ ∈ (𝑋 × 𝑌) → (( · ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩) = ( · ‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
200198, 199syl 17 . . . . . 6 ((𝜑𝑤𝑍) → (( · ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩) = ( · ‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
20193adantr 472 . . . . . . . 8 ((𝜑𝑤𝑍) → (𝑀 gcd 𝑁) = 1)
202 rpmulgcd2 15592 . . . . . . . 8 (((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 gcd 𝑁) = 1) → (𝑤 gcd (𝑀 · 𝑁)) = ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)))
203168, 170, 184, 201, 202syl31anc 1480 . . . . . . 7 ((𝜑𝑤𝑍) → (𝑤 gcd (𝑀 · 𝑁)) = ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)))
204 df-ov 6817 . . . . . . 7 ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)) = ( · ‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩)
205203, 204syl6eq 2810 . . . . . 6 ((𝜑𝑤𝑍) → (𝑤 gcd (𝑀 · 𝑁)) = ( · ‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
206165simprbi 483 . . . . . . . 8 (𝑤𝑍𝑤 ∥ (𝑀 · 𝑁))
207206adantl 473 . . . . . . 7 ((𝜑𝑤𝑍) → 𝑤 ∥ (𝑀 · 𝑁))
20840, 34nnmulcld 11280 . . . . . . . 8 (𝜑 → (𝑀 · 𝑁) ∈ ℕ)
209 gcdeq 15494 . . . . . . . 8 ((𝑤 ∈ ℕ ∧ (𝑀 · 𝑁) ∈ ℕ) → ((𝑤 gcd (𝑀 · 𝑁)) = 𝑤𝑤 ∥ (𝑀 · 𝑁)))
210166, 208, 209syl2anr 496 . . . . . . 7 ((𝜑𝑤𝑍) → ((𝑤 gcd (𝑀 · 𝑁)) = 𝑤𝑤 ∥ (𝑀 · 𝑁)))
211207, 210mpbird 247 . . . . . 6 ((𝜑𝑤𝑍) → (𝑤 gcd (𝑀 · 𝑁)) = 𝑤)
212200, 205, 2113eqtr2rd 2801 . . . . 5 ((𝜑𝑤𝑍) → 𝑤 = (( · ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
213 fveq2 6353 . . . . . . 7 (𝑢 = ⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩ → (( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
214213eqeq2d 2770 . . . . . 6 (𝑢 = ⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩ → (𝑤 = (( · ↾ (𝑋 × 𝑌))‘𝑢) ↔ 𝑤 = (( · ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩)))
215214rspcev 3449 . . . . 5 ((⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩ ∈ (𝑋 × 𝑌) ∧ 𝑤 = (( · ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩)) → ∃𝑢 ∈ (𝑋 × 𝑌)𝑤 = (( · ↾ (𝑋 × 𝑌))‘𝑢))
216198, 212, 215syl2anc 696 . . . 4 ((𝜑𝑤𝑍) → ∃𝑢 ∈ (𝑋 × 𝑌)𝑤 = (( · ↾ (𝑋 × 𝑌))‘𝑢))
217216ralrimiva 3104 . . 3 (𝜑 → ∀𝑤𝑍𝑢 ∈ (𝑋 × 𝑌)𝑤 = (( · ↾ (𝑋 × 𝑌))‘𝑢))
218 dffo3 6538 . . 3 (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–onto𝑍 ↔ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍 ∧ ∀𝑤𝑍𝑢 ∈ (𝑋 × 𝑌)𝑤 = (( · ↾ (𝑋 × 𝑌))‘𝑢)))
21959, 217, 218sylanbrc 701 . 2 (𝜑 → ( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–onto𝑍)
220 df-f1o 6056 . 2 (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1-onto𝑍 ↔ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1𝑍 ∧ ( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–onto𝑍))
221163, 219, 220sylanbrc 701 1 (𝜑 → ( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1-onto𝑍)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383   = wceq 1632  wcel 2139  wne 2932  wral 3050  wrex 3051  {crab 3054  wss 3715  cop 4327   class class class wbr 4804   × cxp 5264  cres 5268   Fn wfn 6044  wf 6045  1-1wf1 6046  ontowfo 6047  1-1-ontowf1o 6048  cfv 6049  (class class class)co 6814  cc 10146  0cc0 10148  1c1 10149   · cmul 10153  cn 11232  0cn0 11504  cz 11589  cdvds 15202   gcd cgcd 15438
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115  ax-cnex 10204  ax-resscn 10205  ax-1cn 10206  ax-icn 10207  ax-addcl 10208  ax-addrcl 10209  ax-mulcl 10210  ax-mulrcl 10211  ax-mulcom 10212  ax-addass 10213  ax-mulass 10214  ax-distr 10215  ax-i2m1 10216  ax-1ne0 10217  ax-1rid 10218  ax-rnegex 10219  ax-rrecex 10220  ax-cnre 10221  ax-pre-lttri 10222  ax-pre-lttrn 10223  ax-pre-ltadd 10224  ax-pre-mulgt0 10225  ax-pre-sup 10226  ax-mulf 10228
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6775  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-om 7232  df-2nd 7335  df-wrecs 7577  df-recs 7638  df-rdg 7676  df-er 7913  df-en 8124  df-dom 8125  df-sdom 8126  df-sup 8515  df-inf 8516  df-pnf 10288  df-mnf 10289  df-xr 10290  df-ltxr 10291  df-le 10292  df-sub 10480  df-neg 10481  df-div 10897  df-nn 11233  df-2 11291  df-3 11292  df-n0 11505  df-z 11590  df-uz 11900  df-rp 12046  df-fl 12807  df-mod 12883  df-seq 13016  df-exp 13075  df-cj 14058  df-re 14059  df-im 14060  df-sqrt 14194  df-abs 14195  df-dvds 15203  df-gcd 15439
This theorem is referenced by:  fsumdvdsmul  25141
  Copyright terms: Public domain W3C validator