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

Theorem mpodvdsmulf1o 27113
Description: If 𝑀 and 𝑁 are two coprime integers, multiplication forms a bijection from the set of pairs 𝑗, 𝑘 where 𝑗𝑀 and 𝑘𝑁, to the set of divisors of 𝑀 · 𝑁. Version of dvdsmulf1o 27115 using maps-to notation, which does not require ax-mulf 11210. (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.
StepHypRef Expression
1 mpomulf 11225 . . . . . . 7 (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)):(ℂ × ℂ)⟶ℂ
2 ffn 6716 . . . . . . 7 ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)):(ℂ × ℂ)⟶ℂ → (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) Fn (ℂ × ℂ))
31, 2ax-mp 5 . . . . . 6 (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) Fn (ℂ × ℂ)
4 mpodvdsmulf1o.x . . . . . . . . 9 𝑋 = {𝑥 ∈ ℕ ∣ 𝑥𝑀}
54ssrab3 4076 . . . . . . . 8 𝑋 ⊆ ℕ
6 nnsscn 12239 . . . . . . . 8 ℕ ⊆ ℂ
75, 6sstri 3987 . . . . . . 7 𝑋 ⊆ ℂ
8 mpodvdsmulf1o.y . . . . . . . . 9 𝑌 = {𝑥 ∈ ℕ ∣ 𝑥𝑁}
98ssrab3 4076 . . . . . . . 8 𝑌 ⊆ ℕ
109, 6sstri 3987 . . . . . . 7 𝑌 ⊆ ℂ
11 xpss12 5687 . . . . . . 7 ((𝑋 ⊆ ℂ ∧ 𝑌 ⊆ ℂ) → (𝑋 × 𝑌) ⊆ (ℂ × ℂ))
127, 10, 11mp2an 691 . . . . . 6 (𝑋 × 𝑌) ⊆ (ℂ × ℂ)
13 fnssres 6672 . . . . . 6 (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) Fn (ℂ × ℂ) ∧ (𝑋 × 𝑌) ⊆ (ℂ × ℂ)) → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌))
143, 12, 13mp2an 691 . . . . 5 ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌)
1514a1i 11 . . . 4 (𝜑 → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌))
16 ovres 7581 . . . . . . 7 ((𝑖𝑋𝑗𝑌) → (𝑖((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))𝑗) = (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗))
1716adantl 481 . . . . . 6 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (𝑖((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))𝑗) = (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗))
187sseli 3974 . . . . . . . . . 10 (𝑖𝑋𝑖 ∈ ℂ)
1918adantr 480 . . . . . . . . 9 ((𝑖𝑋𝑗𝑌) → 𝑖 ∈ ℂ)
2010sseli 3974 . . . . . . . . . 10 (𝑗𝑌𝑗 ∈ ℂ)
2120adantl 481 . . . . . . . . 9 ((𝑖𝑋𝑗𝑌) → 𝑗 ∈ ℂ)
22 ovmpot 7576 . . . . . . . . . 10 ((𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑖 · 𝑗))
2322eqcomd 2733 . . . . . . . . 9 ((𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (𝑖 · 𝑗) = (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗))
2419, 21, 23syl2anc 583 . . . . . . . 8 ((𝑖𝑋𝑗𝑌) → (𝑖 · 𝑗) = (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗))
2524adantl 481 . . . . . . 7 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (𝑖 · 𝑗) = (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗))
265sseli 3974 . . . . . . . . . 10 (𝑖𝑋𝑖 ∈ ℕ)
2726ad2antrl 727 . . . . . . . . 9 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → 𝑖 ∈ ℕ)
289sseli 3974 . . . . . . . . . 10 (𝑗𝑌𝑗 ∈ ℕ)
2928ad2antll 728 . . . . . . . . 9 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → 𝑗 ∈ ℕ)
3027, 29nnmulcld 12287 . . . . . . . 8 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (𝑖 · 𝑗) ∈ ℕ)
31 breq1 5145 . . . . . . . . . . . 12 (𝑥 = 𝑗 → (𝑥𝑁𝑗𝑁))
3231, 8elrab2 3683 . . . . . . . . . . 11 (𝑗𝑌 ↔ (𝑗 ∈ ℕ ∧ 𝑗𝑁))
3332simprbi 496 . . . . . . . . . 10 (𝑗𝑌𝑗𝑁)
3433ad2antll 728 . . . . . . . . 9 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → 𝑗𝑁)
35 breq1 5145 . . . . . . . . . . . 12 (𝑥 = 𝑖 → (𝑥𝑀𝑖𝑀))
3635, 4elrab2 3683 . . . . . . . . . . 11 (𝑖𝑋 ↔ (𝑖 ∈ ℕ ∧ 𝑖𝑀))
3736simprbi 496 . . . . . . . . . 10 (𝑖𝑋𝑖𝑀)
3837ad2antrl 727 . . . . . . . . 9 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → 𝑖𝑀)
3929nnzd 12607 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → 𝑗 ∈ ℤ)
40 mpodvdsmulf1o.2 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℕ)
4140adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → 𝑁 ∈ ℕ)
4241nnzd 12607 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → 𝑁 ∈ ℤ)
4327nnzd 12607 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → 𝑖 ∈ ℤ)
44 dvdscmul 16251 . . . . . . . . . . 11 ((𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑗𝑁 → (𝑖 · 𝑗) ∥ (𝑖 · 𝑁)))
4539, 42, 43, 44syl3anc 1369 . . . . . . . . . 10 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (𝑗𝑁 → (𝑖 · 𝑗) ∥ (𝑖 · 𝑁)))
46 mpodvdsmulf1o.1 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ ℕ)
4746adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → 𝑀 ∈ ℕ)
4847nnzd 12607 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → 𝑀 ∈ ℤ)
49 dvdsmulc 16252 . . . . . . . . . . 11 ((𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖𝑀 → (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)))
5043, 48, 42, 49syl3anc 1369 . . . . . . . . . 10 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (𝑖𝑀 → (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)))
5130nnzd 12607 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (𝑖 · 𝑗) ∈ ℤ)
5243, 42zmulcld 12694 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (𝑖 · 𝑁) ∈ ℤ)
5348, 42zmulcld 12694 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (𝑀 · 𝑁) ∈ ℤ)
54 dvdstr 16262 . . . . . . . . . . 11 (((𝑖 · 𝑗) ∈ ℤ ∧ (𝑖 · 𝑁) ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) → (((𝑖 · 𝑗) ∥ (𝑖 · 𝑁) ∧ (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
5551, 52, 53, 54syl3anc 1369 . . . . . . . . . 10 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (((𝑖 · 𝑗) ∥ (𝑖 · 𝑁) ∧ (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
5645, 50, 55syl2and 607 . . . . . . . . 9 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → ((𝑗𝑁𝑖𝑀) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
5734, 38, 56mp2and 698 . . . . . . . 8 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁))
58 breq1 5145 . . . . . . . . 9 (𝑥 = (𝑖 · 𝑗) → (𝑥 ∥ (𝑀 · 𝑁) ↔ (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
59 mpodvdsmulf1o.z . . . . . . . . 9 𝑍 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑀 · 𝑁)}
6058, 59elrab2 3683 . . . . . . . 8 ((𝑖 · 𝑗) ∈ 𝑍 ↔ ((𝑖 · 𝑗) ∈ ℕ ∧ (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)))
6130, 57, 60sylanbrc 582 . . . . . . 7 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (𝑖 · 𝑗) ∈ 𝑍)
6225, 61eqeltrrd 2829 . . . . . 6 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) ∈ 𝑍)
6317, 62eqeltrd 2828 . . . . 5 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → (𝑖((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))𝑗) ∈ 𝑍)
6463ralrimivva 3195 . . . 4 (𝜑 → ∀𝑖𝑋𝑗𝑌 (𝑖((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))𝑗) ∈ 𝑍)
65 ffnov 7541 . . . 4 (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍 ↔ (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌) ∧ ∀𝑖𝑋𝑗𝑌 (𝑖((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))𝑗) ∈ 𝑍))
6615, 64, 65sylanbrc 582 . . 3 (𝜑 → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍)
6719ad2antlr 726 . . . . . . . . 9 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ (𝑚𝑋𝑛𝑌)) → 𝑖 ∈ ℂ)
6821ad2antlr 726 . . . . . . . . 9 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ (𝑚𝑋𝑛𝑌)) → 𝑗 ∈ ℂ)
6967, 68, 22syl2anc 583 . . . . . . . 8 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ (𝑚𝑋𝑛𝑌)) → (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑖 · 𝑗))
707sseli 3974 . . . . . . . . . 10 (𝑚𝑋𝑚 ∈ ℂ)
7170ad2antrl 727 . . . . . . . . 9 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ (𝑚𝑋𝑛𝑌)) → 𝑚 ∈ ℂ)
7210sseli 3974 . . . . . . . . . 10 (𝑛𝑌𝑛 ∈ ℂ)
7372ad2antll 728 . . . . . . . . 9 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ (𝑚𝑋𝑛𝑌)) → 𝑛 ∈ ℂ)
74 ovmpot 7576 . . . . . . . . 9 ((𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) = (𝑚 · 𝑛))
7571, 73, 74syl2anc 583 . . . . . . . 8 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ (𝑚𝑋𝑛𝑌)) → (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) = (𝑚 · 𝑛))
7669, 75eqeq12d 2743 . . . . . . 7 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ (𝑚𝑋𝑛𝑌)) → ((𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) ↔ (𝑖 · 𝑗) = (𝑚 · 𝑛)))
7727adantr 480 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℕ)
7877nnnn0d 12554 . . . . . . . . . 10 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℕ0)
79 simprll 778 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚𝑋)
805, 79sselid 3976 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℕ)
8180nnnn0d 12554 . . . . . . . . . 10 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℕ0)
8277nnzd 12607 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℤ)
8329adantr 480 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∈ ℕ)
8483nnzd 12607 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∈ ℤ)
85 dvdsmul1 16246 . . . . . . . . . . . . 13 ((𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ) → 𝑖 ∥ (𝑖 · 𝑗))
8682, 84, 85syl2anc 583 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∥ (𝑖 · 𝑗))
87 simprr 772 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑚 · 𝑛))
887, 79sselid 3976 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℂ)
89 simprlr 779 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛𝑌)
9010, 89sselid 3976 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ ℂ)
9188, 90mulcomd 11257 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 · 𝑛) = (𝑛 · 𝑚))
9287, 91eqtrd 2767 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑛 · 𝑚))
9386, 92breqtrd 5168 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∥ (𝑛 · 𝑚))
949, 89sselid 3976 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ ℕ)
9594nnzd 12607 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ ℤ)
9642adantr 480 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑁 ∈ ℤ)
9782, 96gcdcomd 16480 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 gcd 𝑁) = (𝑁 gcd 𝑖))
9848adantr 480 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑀 ∈ ℤ)
9940nnzd 12607 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ ℤ)
10046nnzd 12607 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ∈ ℤ)
10199, 100gcdcomd 16480 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 gcd 𝑀) = (𝑀 gcd 𝑁))
102 mpodvdsmulf1o.3 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑀 gcd 𝑁) = 1)
103101, 102eqtrd 2767 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 gcd 𝑀) = 1)
104103ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑁 gcd 𝑀) = 1)
10538adantr 480 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖𝑀)
106 rpdvds 16622 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ((𝑁 gcd 𝑀) = 1 ∧ 𝑖𝑀)) → (𝑁 gcd 𝑖) = 1)
10796, 82, 98, 104, 105, 106syl32anc 1376 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑁 gcd 𝑖) = 1)
10897, 107eqtrd 2767 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 gcd 𝑁) = 1)
109 breq1 5145 . . . . . . . . . . . . . . 15 (𝑥 = 𝑛 → (𝑥𝑁𝑛𝑁))
110109, 8elrab2 3683 . . . . . . . . . . . . . 14 (𝑛𝑌 ↔ (𝑛 ∈ ℕ ∧ 𝑛𝑁))
111110simprbi 496 . . . . . . . . . . . . 13 (𝑛𝑌𝑛𝑁)
11289, 111syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛𝑁)
113 rpdvds 16622 . . . . . . . . . . . 12 (((𝑖 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑖 gcd 𝑁) = 1 ∧ 𝑛𝑁)) → (𝑖 gcd 𝑛) = 1)
11482, 95, 96, 108, 112, 113syl32anc 1376 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 gcd 𝑛) = 1)
11580nnzd 12607 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℤ)
116 coprmdvds 16615 . . . . . . . . . . . 12 ((𝑖 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ) → ((𝑖 ∥ (𝑛 · 𝑚) ∧ (𝑖 gcd 𝑛) = 1) → 𝑖𝑚))
11782, 95, 115, 116syl3anc 1369 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → ((𝑖 ∥ (𝑛 · 𝑚) ∧ (𝑖 gcd 𝑛) = 1) → 𝑖𝑚))
11893, 114, 117mp2and 698 . . . . . . . . . 10 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖𝑚)
119 dvdsmul1 16246 . . . . . . . . . . . . 13 ((𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 𝑚 ∥ (𝑚 · 𝑛))
120115, 95, 119syl2anc 583 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∥ (𝑚 · 𝑛))
12177nncnd 12250 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℂ)
12283nncnd 12250 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∈ ℂ)
123121, 122mulcomd 11257 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑗 · 𝑖))
12487, 123eqtr3d 2769 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 · 𝑛) = (𝑗 · 𝑖))
125120, 124breqtrd 5168 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∥ (𝑗 · 𝑖))
126115, 96gcdcomd 16480 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 gcd 𝑁) = (𝑁 gcd 𝑚))
127 breq1 5145 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑚 → (𝑥𝑀𝑚𝑀))
128127, 4elrab2 3683 . . . . . . . . . . . . . . . 16 (𝑚𝑋 ↔ (𝑚 ∈ ℕ ∧ 𝑚𝑀))
129128simprbi 496 . . . . . . . . . . . . . . 15 (𝑚𝑋𝑚𝑀)
13079, 129syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚𝑀)
131 rpdvds 16622 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ((𝑁 gcd 𝑀) = 1 ∧ 𝑚𝑀)) → (𝑁 gcd 𝑚) = 1)
13296, 115, 98, 104, 130, 131syl32anc 1376 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑁 gcd 𝑚) = 1)
133126, 132eqtrd 2767 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 gcd 𝑁) = 1)
13434adantr 480 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗𝑁)
135 rpdvds 16622 . . . . . . . . . . . 12 (((𝑚 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑚 gcd 𝑁) = 1 ∧ 𝑗𝑁)) → (𝑚 gcd 𝑗) = 1)
136115, 84, 96, 133, 134, 135syl32anc 1376 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 gcd 𝑗) = 1)
137 coprmdvds 16615 . . . . . . . . . . . 12 ((𝑚 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑖 ∈ ℤ) → ((𝑚 ∥ (𝑗 · 𝑖) ∧ (𝑚 gcd 𝑗) = 1) → 𝑚𝑖))
138115, 84, 82, 137syl3anc 1369 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → ((𝑚 ∥ (𝑗 · 𝑖) ∧ (𝑚 gcd 𝑗) = 1) → 𝑚𝑖))
139125, 136, 138mp2and 698 . . . . . . . . . 10 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚𝑖)
140 dvdseq 16282 . . . . . . . . . 10 (((𝑖 ∈ ℕ0𝑚 ∈ ℕ0) ∧ (𝑖𝑚𝑚𝑖)) → 𝑖 = 𝑚)
14178, 81, 118, 139, 140syl22anc 838 . . . . . . . . 9 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 = 𝑚)
14277nnne0d 12284 . . . . . . . . . 10 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ≠ 0)
143141oveq1d 7429 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑛) = (𝑚 · 𝑛))
14487, 143eqtr4d 2770 . . . . . . . . . 10 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑖 · 𝑛))
145122, 90, 121, 142, 144mulcanad 11871 . . . . . . . . 9 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 = 𝑛)
146141, 145opeq12d 4877 . . . . . . . 8 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ ((𝑚𝑋𝑛𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩)
147146expr 456 . . . . . . 7 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ (𝑚𝑋𝑛𝑌)) → ((𝑖 · 𝑗) = (𝑚 · 𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
14876, 147sylbid 239 . . . . . 6 (((𝜑 ∧ (𝑖𝑋𝑗𝑌)) ∧ (𝑚𝑋𝑛𝑌)) → ((𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
149148ralrimivva 3195 . . . . 5 ((𝜑 ∧ (𝑖𝑋𝑗𝑌)) → ∀𝑚𝑋𝑛𝑌 ((𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
150149ralrimivva 3195 . . . 4 (𝜑 → ∀𝑖𝑋𝑗𝑌𝑚𝑋𝑛𝑌 ((𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
151 fvres 6910 . . . . . . . . 9 (𝑢 ∈ (𝑋 × 𝑌) → (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢))
152 fvres 6910 . . . . . . . . 9 (𝑣 ∈ (𝑋 × 𝑌) → (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑣) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣))
153151, 152eqeqan12d 2741 . . . . . . . 8 ((𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) → ((((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢) = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑣) ↔ ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣)))
154153imbi1d 341 . . . . . . 7 ((𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) → (((((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢) = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣) → 𝑢 = 𝑣)))
155154ralbidva 3170 . . . . . 6 (𝑢 ∈ (𝑋 × 𝑌) → (∀𝑣 ∈ (𝑋 × 𝑌)((((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢) = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑣 ∈ (𝑋 × 𝑌)(((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣) → 𝑢 = 𝑣)))
156155ralbiia 3086 . . . . 5 (∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢) = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)(((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣) → 𝑢 = 𝑣))
157 fveq2 6891 . . . . . . . . . . 11 (𝑣 = ⟨𝑚, 𝑛⟩ → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘⟨𝑚, 𝑛⟩))
158 df-ov 7417 . . . . . . . . . . 11 (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘⟨𝑚, 𝑛⟩)
159157, 158eqtr4di 2785 . . . . . . . . . 10 (𝑣 = ⟨𝑚, 𝑛⟩ → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛))
160159eqeq2d 2738 . . . . . . . . 9 (𝑣 = ⟨𝑚, 𝑛⟩ → (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣) ↔ ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛)))
161 eqeq2 2739 . . . . . . . . 9 (𝑣 = ⟨𝑚, 𝑛⟩ → (𝑢 = 𝑣𝑢 = ⟨𝑚, 𝑛⟩))
162160, 161imbi12d 344 . . . . . . . 8 (𝑣 = ⟨𝑚, 𝑛⟩ → ((((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣) → 𝑢 = 𝑣) ↔ (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → 𝑢 = ⟨𝑚, 𝑛⟩)))
163162ralxp 5838 . . . . . . 7 (∀𝑣 ∈ (𝑋 × 𝑌)(((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑚𝑋𝑛𝑌 (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → 𝑢 = ⟨𝑚, 𝑛⟩))
164 fveq2 6891 . . . . . . . . . . 11 (𝑢 = ⟨𝑖, 𝑗⟩ → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘⟨𝑖, 𝑗⟩))
165 df-ov 7417 . . . . . . . . . . 11 (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘⟨𝑖, 𝑗⟩)
166164, 165eqtr4di 2785 . . . . . . . . . 10 (𝑢 = ⟨𝑖, 𝑗⟩ → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗))
167166eqeq1d 2729 . . . . . . . . 9 (𝑢 = ⟨𝑖, 𝑗⟩ → (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) ↔ (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛)))
168 eqeq1 2731 . . . . . . . . 9 (𝑢 = ⟨𝑖, 𝑗⟩ → (𝑢 = ⟨𝑚, 𝑛⟩ ↔ ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
169167, 168imbi12d 344 . . . . . . . 8 (𝑢 = ⟨𝑖, 𝑗⟩ → ((((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → 𝑢 = ⟨𝑚, 𝑛⟩) ↔ ((𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩)))
1701692ralbidv 3213 . . . . . . 7 (𝑢 = ⟨𝑖, 𝑗⟩ → (∀𝑚𝑋𝑛𝑌 (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → 𝑢 = ⟨𝑚, 𝑛⟩) ↔ ∀𝑚𝑋𝑛𝑌 ((𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩)))
171163, 170bitrid 283 . . . . . 6 (𝑢 = ⟨𝑖, 𝑗⟩ → (∀𝑣 ∈ (𝑋 × 𝑌)(((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑚𝑋𝑛𝑌 ((𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩)))
172171ralxp 5838 . . . . 5 (∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)(((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑖𝑋𝑗𝑌𝑚𝑋𝑛𝑌 ((𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
173156, 172bitri 275 . . . 4 (∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢) = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑖𝑋𝑗𝑌𝑚𝑋𝑛𝑌 ((𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑛⟩))
174150, 173sylibr 233 . . 3 (𝜑 → ∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢) = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣))
175 dff13 7259 . . 3 (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1𝑍 ↔ (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍 ∧ ∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢) = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣)))
17666, 174, 175sylanbrc 582 . 2 (𝜑 → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1𝑍)
177 breq1 5145 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (𝑥 ∥ (𝑀 · 𝑁) ↔ 𝑤 ∥ (𝑀 · 𝑁)))
178177, 59elrab2 3683 . . . . . . . . . . 11 (𝑤𝑍 ↔ (𝑤 ∈ ℕ ∧ 𝑤 ∥ (𝑀 · 𝑁)))
179178simplbi 497 . . . . . . . . . 10 (𝑤𝑍𝑤 ∈ ℕ)
180179adantl 481 . . . . . . . . 9 ((𝜑𝑤𝑍) → 𝑤 ∈ ℕ)
181180nnzd 12607 . . . . . . . 8 ((𝜑𝑤𝑍) → 𝑤 ∈ ℤ)
18246adantr 480 . . . . . . . . 9 ((𝜑𝑤𝑍) → 𝑀 ∈ ℕ)
183182nnzd 12607 . . . . . . . 8 ((𝜑𝑤𝑍) → 𝑀 ∈ ℤ)
184182nnne0d 12284 . . . . . . . . 9 ((𝜑𝑤𝑍) → 𝑀 ≠ 0)
185 simpr 484 . . . . . . . . . 10 ((𝑤 = 0 ∧ 𝑀 = 0) → 𝑀 = 0)
186185necon3ai 2960 . . . . . . . . 9 (𝑀 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑀 = 0))
187184, 186syl 17 . . . . . . . 8 ((𝜑𝑤𝑍) → ¬ (𝑤 = 0 ∧ 𝑀 = 0))
188 gcdn0cl 16468 . . . . . . . 8 (((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ 𝑀 = 0)) → (𝑤 gcd 𝑀) ∈ ℕ)
189181, 183, 187, 188syl21anc 837 . . . . . . 7 ((𝜑𝑤𝑍) → (𝑤 gcd 𝑀) ∈ ℕ)
190 gcddvds 16469 . . . . . . . . 9 ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
191181, 183, 190syl2anc 583 . . . . . . . 8 ((𝜑𝑤𝑍) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
192191simprd 495 . . . . . . 7 ((𝜑𝑤𝑍) → (𝑤 gcd 𝑀) ∥ 𝑀)
193 breq1 5145 . . . . . . . 8 (𝑥 = (𝑤 gcd 𝑀) → (𝑥𝑀 ↔ (𝑤 gcd 𝑀) ∥ 𝑀))
194193, 4elrab2 3683 . . . . . . 7 ((𝑤 gcd 𝑀) ∈ 𝑋 ↔ ((𝑤 gcd 𝑀) ∈ ℕ ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
195189, 192, 194sylanbrc 582 . . . . . 6 ((𝜑𝑤𝑍) → (𝑤 gcd 𝑀) ∈ 𝑋)
19640adantr 480 . . . . . . . . 9 ((𝜑𝑤𝑍) → 𝑁 ∈ ℕ)
197196nnzd 12607 . . . . . . . 8 ((𝜑𝑤𝑍) → 𝑁 ∈ ℤ)
198196nnne0d 12284 . . . . . . . . 9 ((𝜑𝑤𝑍) → 𝑁 ≠ 0)
199 simpr 484 . . . . . . . . . 10 ((𝑤 = 0 ∧ 𝑁 = 0) → 𝑁 = 0)
200199necon3ai 2960 . . . . . . . . 9 (𝑁 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑁 = 0))
201198, 200syl 17 . . . . . . . 8 ((𝜑𝑤𝑍) → ¬ (𝑤 = 0 ∧ 𝑁 = 0))
202 gcdn0cl 16468 . . . . . . . 8 (((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ 𝑁 = 0)) → (𝑤 gcd 𝑁) ∈ ℕ)
203181, 197, 201, 202syl21anc 837 . . . . . . 7 ((𝜑𝑤𝑍) → (𝑤 gcd 𝑁) ∈ ℕ)
204 gcddvds 16469 . . . . . . . . 9 ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
205181, 197, 204syl2anc 583 . . . . . . . 8 ((𝜑𝑤𝑍) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
206205simprd 495 . . . . . . 7 ((𝜑𝑤𝑍) → (𝑤 gcd 𝑁) ∥ 𝑁)
207 breq1 5145 . . . . . . . 8 (𝑥 = (𝑤 gcd 𝑁) → (𝑥𝑁 ↔ (𝑤 gcd 𝑁) ∥ 𝑁))
208207, 8elrab2 3683 . . . . . . 7 ((𝑤 gcd 𝑁) ∈ 𝑌 ↔ ((𝑤 gcd 𝑁) ∈ ℕ ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
209203, 206, 208sylanbrc 582 . . . . . 6 ((𝜑𝑤𝑍) → (𝑤 gcd 𝑁) ∈ 𝑌)
210195, 209opelxpd 5711 . . . . 5 ((𝜑𝑤𝑍) → ⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩ ∈ (𝑋 × 𝑌))
211210fvresd 6911 . . . . . . 7 ((𝜑𝑤𝑍) → (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
212 df-ov 7417 . . . . . . . 8 ((𝑤 gcd 𝑀)(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))(𝑤 gcd 𝑁)) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩)
213189nncnd 12250 . . . . . . . . 9 ((𝜑𝑤𝑍) → (𝑤 gcd 𝑀) ∈ ℂ)
214203nncnd 12250 . . . . . . . . 9 ((𝜑𝑤𝑍) → (𝑤 gcd 𝑁) ∈ ℂ)
215 ovmpot 7576 . . . . . . . . 9 (((𝑤 gcd 𝑀) ∈ ℂ ∧ (𝑤 gcd 𝑁) ∈ ℂ) → ((𝑤 gcd 𝑀)(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))(𝑤 gcd 𝑁)) = ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)))
216213, 214, 215syl2anc 583 . . . . . . . 8 ((𝜑𝑤𝑍) → ((𝑤 gcd 𝑀)(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))(𝑤 gcd 𝑁)) = ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)))
217212, 216eqtr3id 2781 . . . . . . 7 ((𝜑𝑤𝑍) → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩) = ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)))
218 df-ov 7417 . . . . . . . 8 ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)) = ( · ‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩)
219218a1i 11 . . . . . . 7 ((𝜑𝑤𝑍) → ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)) = ( · ‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
220211, 217, 2193eqtrd 2771 . . . . . 6 ((𝜑𝑤𝑍) → (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩) = ( · ‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
221102adantr 480 . . . . . . . 8 ((𝜑𝑤𝑍) → (𝑀 gcd 𝑁) = 1)
222 rpmulgcd2 16618 . . . . . . . 8 (((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 gcd 𝑁) = 1) → (𝑤 gcd (𝑀 · 𝑁)) = ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)))
223181, 183, 197, 221, 222syl31anc 1371 . . . . . . 7 ((𝜑𝑤𝑍) → (𝑤 gcd (𝑀 · 𝑁)) = ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)))
224223, 218eqtrdi 2783 . . . . . 6 ((𝜑𝑤𝑍) → (𝑤 gcd (𝑀 · 𝑁)) = ( · ‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
225178simprbi 496 . . . . . . . 8 (𝑤𝑍𝑤 ∥ (𝑀 · 𝑁))
226225adantl 481 . . . . . . 7 ((𝜑𝑤𝑍) → 𝑤 ∥ (𝑀 · 𝑁))
22746, 40nnmulcld 12287 . . . . . . . 8 (𝜑 → (𝑀 · 𝑁) ∈ ℕ)
228 gcdeq 16520 . . . . . . . 8 ((𝑤 ∈ ℕ ∧ (𝑀 · 𝑁) ∈ ℕ) → ((𝑤 gcd (𝑀 · 𝑁)) = 𝑤𝑤 ∥ (𝑀 · 𝑁)))
229179, 227, 228syl2anr 596 . . . . . . 7 ((𝜑𝑤𝑍) → ((𝑤 gcd (𝑀 · 𝑁)) = 𝑤𝑤 ∥ (𝑀 · 𝑁)))
230226, 229mpbird 257 . . . . . 6 ((𝜑𝑤𝑍) → (𝑤 gcd (𝑀 · 𝑁)) = 𝑤)
231220, 224, 2303eqtr2rd 2774 . . . . 5 ((𝜑𝑤𝑍) → 𝑤 = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
232 fveq2 6891 . . . . . 6 (𝑢 = ⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩ → (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢) = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩))
233232rspceeqv 3629 . . . . 5 ((⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩ ∈ (𝑋 × 𝑌) ∧ 𝑤 = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘⟨(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)⟩)) → ∃𝑢 ∈ (𝑋 × 𝑌)𝑤 = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢))
234210, 231, 233syl2anc 583 . . . 4 ((𝜑𝑤𝑍) → ∃𝑢 ∈ (𝑋 × 𝑌)𝑤 = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢))
235234ralrimiva 3141 . . 3 (𝜑 → ∀𝑤𝑍𝑢 ∈ (𝑋 × 𝑌)𝑤 = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢))
236 dffo3 7106 . . 3 (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–onto𝑍 ↔ (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍 ∧ ∀𝑤𝑍𝑢 ∈ (𝑋 × 𝑌)𝑤 = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢)))
23766, 235, 236sylanbrc 582 . 2 (𝜑 → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–onto𝑍)
238 df-f1o 6549 . 2 (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1-onto𝑍 ↔ (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1𝑍 ∧ ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–onto𝑍))
239176, 237, 238sylanbrc 582 1 (𝜑 → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1-onto𝑍)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395   = wceq 1534  wcel 2099  wne 2935  wral 3056  wrex 3065  {crab 3427  wss 3944  cop 4630   class class class wbr 5142   × cxp 5670  cres 5674   Fn wfn 6537  wf 6538  1-1wf1 6539  ontowfo 6540  1-1-ontowf1o 6541  cfv 6542  (class class class)co 7414  cmpo 7416  cc 11128  0cc0 11130  1c1 11131   · cmul 11135  cn 12234  0cn0 12494  cz 12580  cdvds 16222   gcd cgcd 16460
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207  ax-pre-sup 11208
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7865  df-1st 7987  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-er 8718  df-en 8956  df-dom 8957  df-sdom 8958  df-sup 9457  df-inf 9458  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-div 11894  df-nn 12235  df-2 12297  df-3 12298  df-n0 12495  df-z 12581  df-uz 12845  df-rp 12999  df-fl 13781  df-mod 13859  df-seq 13991  df-exp 14051  df-cj 15070  df-re 15071  df-im 15072  df-sqrt 15206  df-abs 15207  df-dvds 16223  df-gcd 16461
This theorem is referenced by:  fsumdvdsmul  27114
  Copyright terms: Public domain W3C validator