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

Theorem dvdsmulf1o 25770
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 10604 . . . . . . 7 · :(ℂ × ℂ)⟶ℂ
2 ffn 6497 . . . . . . 7 ( · :(ℂ × ℂ)⟶ℂ → · Fn (ℂ × ℂ))
31, 2ax-mp 5 . . . . . 6 · Fn (ℂ × ℂ)
4 dvdsmulf1o.x . . . . . . . . 9 𝑋 = {𝑥 ∈ ℕ ∣ 𝑥𝑀}
54ssrab3 4041 . . . . . . . 8 𝑋 ⊆ ℕ
6 nnsscn 11630 . . . . . . . 8 ℕ ⊆ ℂ
75, 6sstri 3960 . . . . . . 7 𝑋 ⊆ ℂ
8 dvdsmulf1o.y . . . . . . . . 9 𝑌 = {𝑥 ∈ ℕ ∣ 𝑥𝑁}
98ssrab3 4041 . . . . . . . 8 𝑌 ⊆ ℕ
109, 6sstri 3960 . . . . . . 7 𝑌 ⊆ ℂ
11 xpss12 5553 . . . . . . 7 ((𝑋 ⊆ ℂ ∧ 𝑌 ⊆ ℂ) → (𝑋 × 𝑌) ⊆ (ℂ × ℂ))
127, 10, 11mp2an 691 . . . . . 6 (𝑋 × 𝑌) ⊆ (ℂ × ℂ)
13 fnssres 6453 . . . . . 6 (( · Fn (ℂ × ℂ) ∧ (𝑋 × 𝑌) ⊆ (ℂ × ℂ)) → ( · ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌))
143, 12, 13mp2an 691 . . . . 5 ( · ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌)
1514a1i 11 . . . 4 (𝜑 → ( · ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌))
16 ovres 7299 . . . . . . 7 ((𝑖𝑋𝑗𝑌) → (𝑖( · ↾ (𝑋 × 𝑌))𝑗) = (𝑖 · 𝑗))
1716adantl 485 . . . . . 6 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (𝑖( · ↾ (𝑋 × 𝑌))𝑗) = (𝑖 · 𝑗))
18 breq1 5052 . . . . . . . . . . 11 (𝑥 = 𝑖 → (𝑥𝑀𝑖𝑀))
1918, 4elrab2 3668 . . . . . . . . . 10 (𝑖𝑋 ↔ (𝑖 ∈ ℕ ∧ 𝑖𝑀))
2019simplbi 501 . . . . . . . . 9 (𝑖𝑋𝑖 ∈ ℕ)
2120ad2antrl 727 . . . . . . . 8 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → 𝑖 ∈ ℕ)
22 breq1 5052 . . . . . . . . . . 11 (𝑥 = 𝑗 → (𝑥𝑁𝑗𝑁))
2322, 8elrab2 3668 . . . . . . . . . 10 (𝑗𝑌 ↔ (𝑗 ∈ ℕ ∧ 𝑗𝑁))
2423simplbi 501 . . . . . . . . 9 (𝑗𝑌𝑗 ∈ ℕ)
2524ad2antll 728 . . . . . . . 8 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → 𝑗 ∈ ℕ)
2621, 25nnmulcld 11678 . . . . . . 7 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (𝑖 · 𝑗) ∈ ℕ)
2723simprbi 500 . . . . . . . . 9 (𝑗𝑌𝑗𝑁)
2827ad2antll 728 . . . . . . . 8 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → 𝑗𝑁)
2919simprbi 500 . . . . . . . . 9 (𝑖𝑋𝑖𝑀)
3029ad2antrl 727 . . . . . . . 8 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → 𝑖𝑀)
3125nnzd 12074 . . . . . . . . . 10 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → 𝑗 ∈ ℤ)
32 dvdsmulf1o.2 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℕ)
3332adantr 484 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → 𝑁 ∈ ℕ)
3433nnzd 12074 . . . . . . . . . 10 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → 𝑁 ∈ ℤ)
3521nnzd 12074 . . . . . . . . . 10 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → 𝑖 ∈ ℤ)
36 dvdscmul 15627 . . . . . . . . . 10 ((𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑗𝑁 → (𝑖 · 𝑗) ∥ (𝑖 · 𝑁)))
3731, 34, 35, 36syl3anc 1368 . . . . . . . . 9 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (𝑗𝑁 → (𝑖 · 𝑗) ∥ (𝑖 · 𝑁)))
38 dvdsmulf1o.1 . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℕ)
3938adantr 484 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → 𝑀 ∈ ℕ)
4039nnzd 12074 . . . . . . . . . 10 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → 𝑀 ∈ ℤ)
41 dvdsmulc 15628 . . . . . . . . . 10 ((𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖𝑀 → (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)))
4235, 40, 34, 41syl3anc 1368 . . . . . . . . 9 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (𝑖𝑀 → (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)))
4326nnzd 12074 . . . . . . . . . 10 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (𝑖 · 𝑗) ∈ ℤ)
4435, 34zmulcld 12081 . . . . . . . . . 10 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (𝑖 · 𝑁) ∈ ℤ)
4540, 34zmulcld 12081 . . . . . . . . . 10 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (𝑀 · 𝑁) ∈ ℤ)
46 dvdstr 15637 . . . . . . . . . 10 (((𝑖 · 𝑗) ∈ ℤ ∧ (𝑖 · 𝑁) ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) → (((𝑖 · 𝑗) ∥ (𝑖 · 𝑁) ∧ (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
4743, 44, 45, 46syl3anc 1368 . . . . . . . . 9 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (((𝑖 · 𝑗) ∥ (𝑖 · 𝑁) ∧ (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
4837, 42, 47syl2and 610 . . . . . . . 8 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → ((𝑗𝑁𝑖𝑀) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
4928, 30, 48mp2and 698 . . . . . . 7 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁))
50 breq1 5052 . . . . . . . 8 (𝑥 = (𝑖 · 𝑗) → (𝑥 ∥ (𝑀 · 𝑁) ↔ (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
51 dvdsmulf1o.z . . . . . . . 8 𝑍 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑀 · 𝑁)}
5250, 51elrab2 3668 . . . . . . 7 ((𝑖 · 𝑗) ∈ 𝑍 ↔ ((𝑖 · 𝑗) ∈ ℕ ∧ (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
5326, 49, 52sylanbrc 586 . . . . . 6 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (𝑖 · 𝑗) ∈ 𝑍)
5417, 53eqeltrd 2916 . . . . 5 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (𝑖( · ↾ (𝑋 × 𝑌))𝑗) ∈ 𝑍)
5554ralrimivva 3185 . . . 4 (𝜑 → ∀𝑖𝑋𝑗𝑌 (𝑖( · ↾ (𝑋 × 𝑌))𝑗) ∈ 𝑍)
56 ffnov 7262 . . . 4 (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍 ↔ (( · ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌) ∧ ∀𝑖𝑋𝑗𝑌 (𝑖( · ↾ (𝑋 × 𝑌))𝑗) ∈ 𝑍))
5715, 55, 56sylanbrc 586 . . 3 (𝜑 → ( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍)
5821adantr 484 . . . . . . . . . 10 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℕ)
5958nnnn0d 11943 . . . . . . . . 9 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℕ0)
60 simprll 778 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚𝑋)
61 breq1 5052 . . . . . . . . . . . . 13 (𝑥 = 𝑚 → (𝑥𝑀𝑚𝑀))
6261, 4elrab2 3668 . . . . . . . . . . . 12 (𝑚𝑋 ↔ (𝑚 ∈ ℕ ∧ 𝑚𝑀))
6362simplbi 501 . . . . . . . . . . 11 (𝑚𝑋𝑚 ∈ ℕ)
6460, 63syl 17 . . . . . . . . . 10 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℕ)
6564nnnn0d 11943 . . . . . . . . 9 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℕ0)
6658nnzd 12074 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℤ)
6725adantr 484 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∈ ℕ)
6867nnzd 12074 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∈ ℤ)
69 dvdsmul1 15622 . . . . . . . . . . . 12 ((𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ) → 𝑖 ∥ (𝑖 · 𝑗))
7066, 68, 69syl2anc 587 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∥ (𝑖 · 𝑗))
71 simprr 772 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑚 · 𝑛))
727, 60sseldi 3949 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℂ)
73 simprlr 779 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛𝑌)
74 breq1 5052 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑛 → (𝑥𝑁𝑛𝑁))
7574, 8elrab2 3668 . . . . . . . . . . . . . . . 16 (𝑛𝑌 ↔ (𝑛 ∈ ℕ ∧ 𝑛𝑁))
7675simplbi 501 . . . . . . . . . . . . . . 15 (𝑛𝑌𝑛 ∈ ℕ)
7773, 76syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ ℕ)
7877nncnd 11641 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ ℂ)
7972, 78mulcomd 10649 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 · 𝑛) = (𝑛 · 𝑚))
8071, 79eqtrd 2859 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑛 · 𝑚))
8170, 80breqtrd 5075 . . . . . . . . . 10 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∥ (𝑛 · 𝑚))
8277nnzd 12074 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ ℤ)
8334adantr 484 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑁 ∈ ℤ)
84 gcdcom 15851 . . . . . . . . . . . . 13 ((𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 gcd 𝑁) = (𝑁 gcd 𝑖))
8566, 83, 84syl2anc 587 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 gcd 𝑁) = (𝑁 gcd 𝑖))
8640adantr 484 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑀 ∈ ℤ)
8732nnzd 12074 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℤ)
8838nnzd 12074 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℤ)
89 gcdcom 15851 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁 gcd 𝑀) = (𝑀 gcd 𝑁))
9087, 88, 89syl2anc 587 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 gcd 𝑀) = (𝑀 gcd 𝑁))
91 dvdsmulf1o.3 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀 gcd 𝑁) = 1)
9290, 91eqtrd 2859 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 gcd 𝑀) = 1)
9392ad2antrr 725 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑁 gcd 𝑀) = 1)
9430adantr 484 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖𝑀)
95 rpdvds 15993 . . . . . . . . . . . . 13 (((𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ((𝑁 gcd 𝑀) = 1 ∧ 𝑖𝑀)) → (𝑁 gcd 𝑖) = 1)
9683, 66, 86, 93, 94, 95syl32anc 1375 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑁 gcd 𝑖) = 1)
9785, 96eqtrd 2859 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 gcd 𝑁) = 1)
9875simprbi 500 . . . . . . . . . . . 12 (𝑛𝑌𝑛𝑁)
9973, 98syl 17 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛𝑁)
100 rpdvds 15993 . . . . . . . . . . 11 (((𝑖 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑖 gcd 𝑁) = 1 ∧ 𝑛𝑁)) → (𝑖 gcd 𝑛) = 1)
10166, 82, 83, 97, 99, 100syl32anc 1375 . . . . . . . . . 10 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 gcd 𝑛) = 1)
10264nnzd 12074 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℤ)
103 coprmdvds 15986 . . . . . . . . . . 11 ((𝑖 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ) → ((𝑖 ∥ (𝑛 · 𝑚) ∧ (𝑖 gcd 𝑛) = 1) → 𝑖𝑚))
10466, 82, 102, 103syl3anc 1368 . . . . . . . . . 10 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → ((𝑖 ∥ (𝑛 · 𝑚) ∧ (𝑖 gcd 𝑛) = 1) → 𝑖𝑚))
10581, 101, 104mp2and 698 . . . . . . . . 9 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖𝑚)
106 dvdsmul1 15622 . . . . . . . . . . . 12 ((𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 𝑚 ∥ (𝑚 · 𝑛))
107102, 82, 106syl2anc 587 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∥ (𝑚 · 𝑛))
10858nncnd 11641 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℂ)
10967nncnd 11641 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∈ ℂ)
110108, 109mulcomd 10649 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑗 · 𝑖))
11171, 110eqtr3d 2861 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 · 𝑛) = (𝑗 · 𝑖))
112107, 111breqtrd 5075 . . . . . . . . . 10 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∥ (𝑗 · 𝑖))
113 gcdcom 15851 . . . . . . . . . . . . 13 ((𝑚 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑚 gcd 𝑁) = (𝑁 gcd 𝑚))
114102, 83, 113syl2anc 587 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 gcd 𝑁) = (𝑁 gcd 𝑚))
11562simprbi 500 . . . . . . . . . . . . . 14 (𝑚𝑋𝑚𝑀)
11660, 115syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚𝑀)
117 rpdvds 15993 . . . . . . . . . . . . 13 (((𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ((𝑁 gcd 𝑀) = 1 ∧ 𝑚𝑀)) → (𝑁 gcd 𝑚) = 1)
11883, 102, 86, 93, 116, 117syl32anc 1375 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑁 gcd 𝑚) = 1)
119114, 118eqtrd 2859 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 gcd 𝑁) = 1)
12028adantr 484 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗𝑁)
121 rpdvds 15993 . . . . . . . . . . 11 (((𝑚 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑚 gcd 𝑁) = 1 ∧ 𝑗𝑁)) → (𝑚 gcd 𝑗) = 1)
122102, 68, 83, 119, 120, 121syl32anc 1375 . . . . . . . . . 10 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 gcd 𝑗) = 1)
123 coprmdvds 15986 . . . . . . . . . . 11 ((𝑚 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑖 ∈ ℤ) → ((𝑚 ∥ (𝑗 · 𝑖) ∧ (𝑚 gcd 𝑗) = 1) → 𝑚𝑖))
124102, 68, 66, 123syl3anc 1368 . . . . . . . . . 10 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → ((𝑚 ∥ (𝑗 · 𝑖) ∧ (𝑚 gcd 𝑗) = 1) → 𝑚𝑖))
125112, 122, 124mp2and 698 . . . . . . . . 9 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚𝑖)
126 dvdseq 15655 . . . . . . . . 9 (((𝑖 ∈ ℕ0𝑚 ∈ ℕ0) ∧ (𝑖𝑚𝑚𝑖)) → 𝑖 = 𝑚)
12759, 65, 105, 125, 126syl22anc 837 . . . . . . . 8 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 = 𝑚)
12858nnne0d 11675 . . . . . . . . 9 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ≠ 0)
129127oveq1d 7155 . . . . . . . . . 10 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑛) = (𝑚 · 𝑛))
13071, 129eqtr4d 2862 . . . . . . . . 9 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑖 · 𝑛))
131109, 78, 108, 128, 130mulcanad 11262 . . . . . . . 8 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 = 𝑛)
132127, 131opeq12d 4794 . . . . . . 7 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩)
133132expr 460 . . . . . 6 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ (𝑚𝑋𝑛𝑌)) → ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
134133ralrimivva 3185 . . . . 5 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → ∀𝑚𝑋𝑛𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
135134ralrimivva 3185 . . . 4 (𝜑 → ∀𝑖𝑋𝑗𝑌𝑚𝑋𝑛𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
136 fvres 6672 . . . . . . . . 9 (𝑢 ∈ (𝑋 × 𝑌) → (( · ↾ (𝑋 × 𝑌))‘𝑢) = ( · ‘𝑢))
137 fvres 6672 . . . . . . . . 9 (𝑣 ∈ (𝑋 × 𝑌) → (( · ↾ (𝑋 × 𝑌))‘𝑣) = ( · ‘𝑣))
138136, 137eqeqan12d 2841 . . . . . . . 8 ((𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) → ((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) ↔ ( · ‘𝑢) = ( · ‘𝑣)))
139138imbi1d 345 . . . . . . 7 ((𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) → (((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ (( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣)))
140139ralbidva 3190 . . . . . 6 (𝑢 ∈ (𝑋 × 𝑌) → (∀𝑣 ∈ (𝑋 × 𝑌)((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑣 ∈ (𝑋 × 𝑌)(( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣)))
141140ralbiia 3158 . . . . 5 (∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)(( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣))
142 fveq2 6653 . . . . . . . . . . 11 (𝑣 = ⟨𝑚, 𝑛⟩ → ( · ‘𝑣) = ( · ‘⟨𝑚, 𝑛⟩))
143 df-ov 7143 . . . . . . . . . . 11 (𝑚 · 𝑛) = ( · ‘⟨𝑚, 𝑛⟩)
144142, 143syl6eqr 2877 . . . . . . . . . 10 (𝑣 = ⟨𝑚, 𝑛⟩ → ( · ‘𝑣) = (𝑚 · 𝑛))
145144eqeq2d 2835 . . . . . . . . 9 (𝑣 = ⟨𝑚, 𝑛⟩ → (( · ‘𝑢) = ( · ‘𝑣) ↔ ( · ‘𝑢) = (𝑚 · 𝑛)))
146 eqeq2 2836 . . . . . . . . 9 (𝑣 = ⟨𝑚, 𝑛⟩ → (𝑢 = 𝑣𝑢 = ⟨𝑚, 𝑛⟩))
147145, 146imbi12d 348 . . . . . . . 8 (𝑣 = ⟨𝑚, 𝑛⟩ → ((( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣) ↔ (( · ‘𝑢) = (𝑚 · 𝑛) → 𝑢 = ⟨𝑚, 𝑛⟩)))
148147ralxp 5695 . . . . . . 7 (∀𝑣 ∈ (𝑋 × 𝑌)(( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑚𝑋𝑛𝑌 (( · ‘𝑢) = (𝑚 · 𝑛) → 𝑢 = ⟨𝑚, 𝑛⟩))
149 fveq2 6653 . . . . . . . . . . 11 (𝑢 = ⟨𝑖, 𝑗⟩ → ( · ‘𝑢) = ( · ‘⟨𝑖, 𝑗⟩))
150 df-ov 7143 . . . . . . . . . . 11 (𝑖 · 𝑗) = ( · ‘⟨𝑖, 𝑗⟩)
151149, 150syl6eqr 2877 . . . . . . . . . 10 (𝑢 = ⟨𝑖, 𝑗⟩ → ( · ‘𝑢) = (𝑖 · 𝑗))
152151eqeq1d 2826 . . . . . . . . 9 (𝑢 = ⟨𝑖, 𝑗⟩ → (( · ‘𝑢) = (𝑚 · 𝑛) ↔ (𝑖 · 𝑗) = (𝑚 · 𝑛)))
153 eqeq1 2828 . . . . . . . . 9 (𝑢 = ⟨𝑖, 𝑗⟩ → (𝑢 = ⟨𝑚, 𝑛⟩ ↔ ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
154152, 153imbi12d 348 . . . . . . . 8 (𝑢 = ⟨𝑖, 𝑗⟩ → ((( · ‘𝑢) = (𝑚 · 𝑛) → 𝑢 = ⟨𝑚, 𝑛⟩) ↔ ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩)))
1551542ralbidv 3193 . . . . . . 7 (𝑢 = ⟨𝑖, 𝑗⟩ → (∀𝑚𝑋𝑛𝑌 (( · ‘𝑢) = (𝑚 · 𝑛) → 𝑢 = ⟨𝑚, 𝑛⟩) ↔ ∀𝑚𝑋𝑛𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩)))
156148, 155syl5bb 286 . . . . . 6 (𝑢 = ⟨𝑖, 𝑗⟩ → (∀𝑣 ∈ (𝑋 × 𝑌)(( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑚𝑋𝑛𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩)))
157156ralxp 5695 . . . . 5 (∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)(( · ‘𝑢) = ( · ‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑖𝑋𝑗𝑌𝑚𝑋𝑛𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
158141, 157bitri 278 . . . 4 (∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑖𝑋𝑗𝑌𝑚𝑋𝑛𝑌 ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
159135, 158sylibr 237 . . 3 (𝜑 → ∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣))
160 dff13 6997 . . 3 (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1𝑍 ↔ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍 ∧ ∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣)))
16157, 159, 160sylanbrc 586 . 2 (𝜑 → ( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1𝑍)
162 breq1 5052 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (𝑥 ∥ (𝑀 · 𝑁) ↔ 𝑤 ∥ (𝑀 · 𝑁)))
163162, 51elrab2 3668 . . . . . . . . . . 11 (𝑤𝑍 ↔ (𝑤 ∈ ℕ ∧ 𝑤 ∥ (𝑀 · 𝑁)))
164163simplbi 501 . . . . . . . . . 10 (𝑤𝑍𝑤 ∈ ℕ)
165164adantl 485 . . . . . . . . 9 ((𝜑𝑤𝑍) → 𝑤 ∈ ℕ)
166165nnzd 12074 . . . . . . . 8 ((𝜑𝑤𝑍) → 𝑤 ∈ ℤ)
16738adantr 484 . . . . . . . . 9 ((𝜑𝑤𝑍) → 𝑀 ∈ ℕ)
168167nnzd 12074 . . . . . . . 8 ((𝜑𝑤𝑍) → 𝑀 ∈ ℤ)
169167nnne0d 11675 . . . . . . . . 9 ((𝜑𝑤𝑍) → 𝑀 ≠ 0)
170 simpr 488 . . . . . . . . . 10 ((𝑤 = 0 ∧ 𝑀 = 0) → 𝑀 = 0)
171170necon3ai 3038 . . . . . . . . 9 (𝑀 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑀 = 0))
172169, 171syl 17 . . . . . . . 8 ((𝜑𝑤𝑍) → ¬ (𝑤 = 0 ∧ 𝑀 = 0))
173 gcdn0cl 15840 . . . . . . . 8 (((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ 𝑀 = 0)) → (𝑤 gcd 𝑀) ∈ ℕ)
174166, 168, 172, 173syl21anc 836 . . . . . . 7 ((𝜑𝑤𝑍) → (𝑤 gcd 𝑀) ∈ ℕ)
175 gcddvds 15841 . . . . . . . . 9 ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
176166, 168, 175syl2anc 587 . . . . . . . 8 ((𝜑𝑤𝑍) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
177176simprd 499 . . . . . . 7 ((𝜑𝑤𝑍) → (𝑤 gcd 𝑀) ∥ 𝑀)
178 breq1 5052 . . . . . . . 8 (𝑥 = (𝑤 gcd 𝑀) → (𝑥𝑀 ↔ (𝑤 gcd 𝑀) ∥ 𝑀))
179178, 4elrab2 3668 . . . . . . 7 ((𝑤 gcd 𝑀) ∈ 𝑋 ↔ ((𝑤 gcd 𝑀) ∈ ℕ ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
180174, 177, 179sylanbrc 586 . . . . . 6 ((𝜑𝑤𝑍) → (𝑤 gcd 𝑀) ∈ 𝑋)
18132adantr 484 . . . . . . . . 9 ((𝜑𝑤𝑍) → 𝑁 ∈ ℕ)
182181nnzd 12074 . . . . . . . 8 ((𝜑𝑤𝑍) → 𝑁 ∈ ℤ)
183181nnne0d 11675 . . . . . . . . 9 ((𝜑𝑤𝑍) → 𝑁 ≠ 0)
184 simpr 488 . . . . . . . . . 10 ((𝑤 = 0 ∧ 𝑁 = 0) → 𝑁 = 0)
185184necon3ai 3038 . . . . . . . . 9 (𝑁 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑁 = 0))
186183, 185syl 17 . . . . . . . 8 ((𝜑𝑤𝑍) → ¬ (𝑤 = 0 ∧ 𝑁 = 0))
187 gcdn0cl 15840 . . . . . . . 8 (((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ 𝑁 = 0)) → (𝑤 gcd 𝑁) ∈ ℕ)
188166, 182, 186, 187syl21anc 836 . . . . . . 7 ((𝜑𝑤𝑍) → (𝑤 gcd 𝑁) ∈ ℕ)
189 gcddvds 15841 . . . . . . . . 9 ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
190166, 182, 189syl2anc 587 . . . . . . . 8 ((𝜑𝑤𝑍) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
191190simprd 499 . . . . . . 7 ((𝜑𝑤𝑍) → (𝑤 gcd 𝑁) ∥ 𝑁)
192 breq1 5052 . . . . . . . 8 (𝑥 = (𝑤 gcd 𝑁) → (𝑥𝑁 ↔ (𝑤 gcd 𝑁) ∥ 𝑁))
193192, 8elrab2 3668 . . . . . . 7 ((𝑤 gcd 𝑁) ∈ 𝑌 ↔ ((𝑤 gcd 𝑁) ∈ ℕ ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
194188, 191, 193sylanbrc 586 . . . . . 6 ((𝜑𝑤𝑍) → (𝑤 gcd 𝑁) ∈ 𝑌)
195180, 194opelxpd 5576 . . . . 5 ((𝜑𝑤𝑍) → ⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩ ∈ (𝑋 × 𝑌))
196195fvresd 6673 . . . . . 6 ((𝜑𝑤𝑍) → (( · ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩) = ( · ‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
19791adantr 484 . . . . . . . 8 ((𝜑𝑤𝑍) → (𝑀 gcd 𝑁) = 1)
198 rpmulgcd2 15989 . . . . . . . 8 (((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 gcd 𝑁) = 1) → (𝑤 gcd (𝑀 · 𝑁)) = ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)))
199166, 168, 182, 197, 198syl31anc 1370 . . . . . . 7 ((𝜑𝑤𝑍) → (𝑤 gcd (𝑀 · 𝑁)) = ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)))
200 df-ov 7143 . . . . . . 7 ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)) = ( · ‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩)
201199, 200syl6eq 2875 . . . . . 6 ((𝜑𝑤𝑍) → (𝑤 gcd (𝑀 · 𝑁)) = ( · ‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
202163simprbi 500 . . . . . . . 8 (𝑤𝑍𝑤 ∥ (𝑀 · 𝑁))
203202adantl 485 . . . . . . 7 ((𝜑𝑤𝑍) → 𝑤 ∥ (𝑀 · 𝑁))
20438, 32nnmulcld 11678 . . . . . . . 8 (𝜑 → (𝑀 · 𝑁) ∈ ℕ)
205 gcdeq 15892 . . . . . . . 8 ((𝑤 ∈ ℕ ∧ (𝑀 · 𝑁) ∈ ℕ) → ((𝑤 gcd (𝑀 · 𝑁)) = 𝑤𝑤 ∥ (𝑀 · 𝑁)))
206164, 204, 205syl2anr 599 . . . . . . 7 ((𝜑𝑤𝑍) → ((𝑤 gcd (𝑀 · 𝑁)) = 𝑤𝑤 ∥ (𝑀 · 𝑁)))
207203, 206mpbird 260 . . . . . 6 ((𝜑𝑤𝑍) → (𝑤 gcd (𝑀 · 𝑁)) = 𝑤)
208196, 201, 2073eqtr2rd 2866 . . . . 5 ((𝜑𝑤𝑍) → 𝑤 = (( · ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
209 fveq2 6653 . . . . . 6 (𝑢 = ⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩ → (( · ↾ (𝑋 × 𝑌))‘𝑢) = (( · ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
210209rspceeqv 3623 . . . . 5 ((⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩ ∈ (𝑋 × 𝑌) ∧ 𝑤 = (( · ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩)) → ∃𝑢 ∈ (𝑋 × 𝑌)𝑤 = (( · ↾ (𝑋 × 𝑌))‘𝑢))
211195, 208, 210syl2anc 587 . . . 4 ((𝜑𝑤𝑍) → ∃𝑢 ∈ (𝑋 × 𝑌)𝑤 = (( · ↾ (𝑋 × 𝑌))‘𝑢))
212211ralrimiva 3176 . . 3 (𝜑 → ∀𝑤𝑍𝑢 ∈ (𝑋 × 𝑌)𝑤 = (( · ↾ (𝑋 × 𝑌))‘𝑢))
213 dffo3 6851 . . 3 (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–onto𝑍 ↔ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍 ∧ ∀𝑤𝑍𝑢 ∈ (𝑋 × 𝑌)𝑤 = (( · ↾ (𝑋 × 𝑌))‘𝑢)))
21457, 212, 213sylanbrc 586 . 2 (𝜑 → ( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–onto𝑍)
215 df-f1o 6345 . 2 (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1-onto𝑍 ↔ (( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1𝑍 ∧ ( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–onto𝑍))
216161, 214, 215sylanbrc 586 1 (𝜑 → ( · ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1-onto𝑍)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399   = wceq 1538  wcel 2115  wne 3013  wral 3132  wrex 3133  {crab 3136  wss 3918  cop 4554   class class class wbr 5049   × cxp 5536  cres 5540   Fn wfn 6333  wf 6334  1-1wf1 6335  ontowfo 6336  1-1-ontowf1o 6337  cfv 6338  (class class class)co 7140  cc 10522  0cc0 10524  1c1 10525   · cmul 10529  cn 11625  0cn0 11885  cz 11969  cdvds 15598   gcd cgcd 15832
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5186  ax-nul 5193  ax-pow 5249  ax-pr 5313  ax-un 7446  ax-cnex 10580  ax-resscn 10581  ax-1cn 10582  ax-icn 10583  ax-addcl 10584  ax-addrcl 10585  ax-mulcl 10586  ax-mulrcl 10587  ax-mulcom 10588  ax-addass 10589  ax-mulass 10590  ax-distr 10591  ax-i2m1 10592  ax-1ne0 10593  ax-1rid 10594  ax-rnegex 10595  ax-rrecex 10596  ax-cnre 10597  ax-pre-lttri 10598  ax-pre-lttrn 10599  ax-pre-ltadd 10600  ax-pre-mulgt0 10601  ax-pre-sup 10602  ax-mulf 10604
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3014  df-nel 3118  df-ral 3137  df-rex 3138  df-reu 3139  df-rmo 3140  df-rab 3141  df-v 3481  df-sbc 3758  df-csb 3866  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-pss 3937  df-nul 4275  df-if 4449  df-pw 4522  df-sn 4549  df-pr 4551  df-tp 4553  df-op 4555  df-uni 4822  df-iun 4904  df-br 5050  df-opab 5112  df-mpt 5130  df-tr 5156  df-id 5443  df-eprel 5448  df-po 5457  df-so 5458  df-fr 5497  df-we 5499  df-xp 5544  df-rel 5545  df-cnv 5546  df-co 5547  df-dm 5548  df-rn 5549  df-res 5550  df-ima 5551  df-pred 6131  df-ord 6177  df-on 6178  df-lim 6179  df-suc 6180  df-iota 6297  df-fun 6340  df-fn 6341  df-f 6342  df-f1 6343  df-fo 6344  df-f1o 6345  df-fv 6346  df-riota 7098  df-ov 7143  df-oprab 7144  df-mpo 7145  df-om 7566  df-2nd 7675  df-wrecs 7932  df-recs 7993  df-rdg 8031  df-er 8274  df-en 8495  df-dom 8496  df-sdom 8497  df-sup 8892  df-inf 8893  df-pnf 10664  df-mnf 10665  df-xr 10666  df-ltxr 10667  df-le 10668  df-sub 10859  df-neg 10860  df-div 11285  df-nn 11626  df-2 11688  df-3 11689  df-n0 11886  df-z 11970  df-uz 12232  df-rp 12378  df-fl 13157  df-mod 13233  df-seq 13365  df-exp 13426  df-cj 14449  df-re 14450  df-im 14451  df-sqrt 14585  df-abs 14586  df-dvds 15599  df-gcd 15833
This theorem is referenced by:  fsumdvdsmul  25771
  Copyright terms: Public domain W3C validator