Step | Hyp | Ref
| Expression |
1 | | mpomulf 11225 |
. . . . . . 7
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)):(ℂ ×
ℂ)⟶ℂ |
2 | | ffn 6716 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)):(ℂ × ℂ)⟶ℂ
→ (𝑥 ∈ ℂ,
𝑦 ∈ ℂ ↦
(𝑥 · 𝑦)) Fn (ℂ ×
ℂ)) |
3 | 1, 2 | ax-mp 5 |
. . . . . 6
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) Fn (ℂ ×
ℂ) |
4 | | mpodvdsmulf1o.x |
. . . . . . . . 9
⊢ 𝑋 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀} |
5 | 4 | ssrab3 4076 |
. . . . . . . 8
⊢ 𝑋 ⊆
ℕ |
6 | | nnsscn 12239 |
. . . . . . . 8
⊢ ℕ
⊆ ℂ |
7 | 5, 6 | sstri 3987 |
. . . . . . 7
⊢ 𝑋 ⊆
ℂ |
8 | | mpodvdsmulf1o.y |
. . . . . . . . 9
⊢ 𝑌 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} |
9 | 8 | ssrab3 4076 |
. . . . . . . 8
⊢ 𝑌 ⊆
ℕ |
10 | 9, 6 | sstri 3987 |
. . . . . . 7
⊢ 𝑌 ⊆
ℂ |
11 | | xpss12 5687 |
. . . . . . 7
⊢ ((𝑋 ⊆ ℂ ∧ 𝑌 ⊆ ℂ) → (𝑋 × 𝑌) ⊆ (ℂ ×
ℂ)) |
12 | 7, 10, 11 | mp2an 691 |
. . . . . 6
⊢ (𝑋 × 𝑌) ⊆ (ℂ ×
ℂ) |
13 | | fnssres 6672 |
. . . . . 6
⊢ (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) Fn (ℂ × ℂ) ∧ (𝑋 × 𝑌) ⊆ (ℂ × ℂ)) →
((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌)) |
14 | 3, 12, 13 | mp2an 691 |
. . . . 5
⊢ ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌) |
15 | 14 | a1i 11 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌)) |
16 | | ovres 7581 |
. . . . . . 7
⊢ ((𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌) → (𝑖((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))𝑗) = (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗)) |
17 | 16 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))𝑗) = (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗)) |
18 | 7 | sseli 3974 |
. . . . . . . . . 10
⊢ (𝑖 ∈ 𝑋 → 𝑖 ∈ ℂ) |
19 | 18 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌) → 𝑖 ∈ ℂ) |
20 | 10 | sseli 3974 |
. . . . . . . . . 10
⊢ (𝑗 ∈ 𝑌 → 𝑗 ∈ ℂ) |
21 | 20 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌) → 𝑗 ∈ ℂ) |
22 | | ovmpot 7576 |
. . . . . . . . . 10
⊢ ((𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑖 · 𝑗)) |
23 | 22 | eqcomd 2733 |
. . . . . . . . 9
⊢ ((𝑖 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (𝑖 · 𝑗) = (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗)) |
24 | 19, 21, 23 | syl2anc 583 |
. . . . . . . 8
⊢ ((𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌) → (𝑖 · 𝑗) = (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗)) |
25 | 24 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 · 𝑗) = (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗)) |
26 | 5 | sseli 3974 |
. . . . . . . . . 10
⊢ (𝑖 ∈ 𝑋 → 𝑖 ∈ ℕ) |
27 | 26 | ad2antrl 727 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑖 ∈ ℕ) |
28 | 9 | sseli 3974 |
. . . . . . . . . 10
⊢ (𝑗 ∈ 𝑌 → 𝑗 ∈ ℕ) |
29 | 28 | ad2antll 728 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑗 ∈ ℕ) |
30 | 27, 29 | nnmulcld 12287 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 · 𝑗) ∈ ℕ) |
31 | | breq1 5145 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑗 → (𝑥 ∥ 𝑁 ↔ 𝑗 ∥ 𝑁)) |
32 | 31, 8 | elrab2 3683 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ 𝑌 ↔ (𝑗 ∈ ℕ ∧ 𝑗 ∥ 𝑁)) |
33 | 32 | simprbi 496 |
. . . . . . . . . 10
⊢ (𝑗 ∈ 𝑌 → 𝑗 ∥ 𝑁) |
34 | 33 | ad2antll 728 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑗 ∥ 𝑁) |
35 | | breq1 5145 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑖 → (𝑥 ∥ 𝑀 ↔ 𝑖 ∥ 𝑀)) |
36 | 35, 4 | elrab2 3683 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ 𝑋 ↔ (𝑖 ∈ ℕ ∧ 𝑖 ∥ 𝑀)) |
37 | 36 | simprbi 496 |
. . . . . . . . . 10
⊢ (𝑖 ∈ 𝑋 → 𝑖 ∥ 𝑀) |
38 | 37 | ad2antrl 727 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑖 ∥ 𝑀) |
39 | 29 | nnzd 12607 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑗 ∈ ℤ) |
40 | | mpodvdsmulf1o.2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℕ) |
41 | 40 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑁 ∈ ℕ) |
42 | 41 | nnzd 12607 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑁 ∈ ℤ) |
43 | 27 | nnzd 12607 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑖 ∈ ℤ) |
44 | | dvdscmul 16251 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑗 ∥ 𝑁 → (𝑖 · 𝑗) ∥ (𝑖 · 𝑁))) |
45 | 39, 42, 43, 44 | syl3anc 1369 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑗 ∥ 𝑁 → (𝑖 · 𝑗) ∥ (𝑖 · 𝑁))) |
46 | | mpodvdsmulf1o.1 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ ℕ) |
47 | 46 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑀 ∈ ℕ) |
48 | 47 | nnzd 12607 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → 𝑀 ∈ ℤ) |
49 | | dvdsmulc 16252 |
. . . . . . . . . . 11
⊢ ((𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∥ 𝑀 → (𝑖 · 𝑁) ∥ (𝑀 · 𝑁))) |
50 | 43, 48, 42, 49 | syl3anc 1369 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 ∥ 𝑀 → (𝑖 · 𝑁) ∥ (𝑀 · 𝑁))) |
51 | 30 | nnzd 12607 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 · 𝑗) ∈ ℤ) |
52 | 43, 42 | zmulcld 12694 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 · 𝑁) ∈ ℤ) |
53 | 48, 42 | zmulcld 12694 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑀 · 𝑁) ∈ ℤ) |
54 | | dvdstr 16262 |
. . . . . . . . . . 11
⊢ (((𝑖 · 𝑗) ∈ ℤ ∧ (𝑖 · 𝑁) ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) → (((𝑖 · 𝑗) ∥ (𝑖 · 𝑁) ∧ (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁))) |
55 | 51, 52, 53, 54 | syl3anc 1369 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (((𝑖 · 𝑗) ∥ (𝑖 · 𝑁) ∧ (𝑖 · 𝑁) ∥ (𝑀 · 𝑁)) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁))) |
56 | 45, 50, 55 | syl2and 607 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → ((𝑗 ∥ 𝑁 ∧ 𝑖 ∥ 𝑀) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁))) |
57 | 34, 38, 56 | mp2and 698 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 · 𝑗) ∥ (𝑀 · 𝑁)) |
58 | | breq1 5145 |
. . . . . . . . 9
⊢ (𝑥 = (𝑖 · 𝑗) → (𝑥 ∥ (𝑀 · 𝑁) ↔ (𝑖 · 𝑗) ∥ (𝑀 · 𝑁))) |
59 | | mpodvdsmulf1o.z |
. . . . . . . . 9
⊢ 𝑍 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑀 · 𝑁)} |
60 | 58, 59 | elrab2 3683 |
. . . . . . . 8
⊢ ((𝑖 · 𝑗) ∈ 𝑍 ↔ ((𝑖 · 𝑗) ∈ ℕ ∧ (𝑖 · 𝑗) ∥ (𝑀 · 𝑁))) |
61 | 30, 57, 60 | sylanbrc 582 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖 · 𝑗) ∈ 𝑍) |
62 | 25, 61 | eqeltrrd 2829 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) ∈ 𝑍) |
63 | 17, 62 | eqeltrd 2828 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → (𝑖((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))𝑗) ∈ 𝑍) |
64 | 63 | ralrimivva 3195 |
. . . 4
⊢ (𝜑 → ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑌 (𝑖((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))𝑗) ∈ 𝑍) |
65 | | ffnov 7541 |
. . . 4
⊢ (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍 ↔ (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑌 (𝑖((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))𝑗) ∈ 𝑍)) |
66 | 15, 64, 65 | sylanbrc 582 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍) |
67 | 19 | ad2antlr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌)) → 𝑖 ∈ ℂ) |
68 | 21 | ad2antlr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌)) → 𝑗 ∈ ℂ) |
69 | 67, 68, 22 | syl2anc 583 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌)) → (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑖 · 𝑗)) |
70 | 7 | sseli 3974 |
. . . . . . . . . 10
⊢ (𝑚 ∈ 𝑋 → 𝑚 ∈ ℂ) |
71 | 70 | ad2antrl 727 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌)) → 𝑚 ∈ ℂ) |
72 | 10 | sseli 3974 |
. . . . . . . . . 10
⊢ (𝑛 ∈ 𝑌 → 𝑛 ∈ ℂ) |
73 | 72 | ad2antll 728 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌)) → 𝑛 ∈ ℂ) |
74 | | ovmpot 7576 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) = (𝑚 · 𝑛)) |
75 | 71, 73, 74 | syl2anc 583 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌)) → (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) = (𝑚 · 𝑛)) |
76 | 69, 75 | eqeq12d 2743 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌)) → ((𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) ↔ (𝑖 · 𝑗) = (𝑚 · 𝑛))) |
77 | 27 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℕ) |
78 | 77 | nnnn0d 12554 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℕ0) |
79 | | simprll 778 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ 𝑋) |
80 | 5, 79 | sselid 3976 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℕ) |
81 | 80 | nnnn0d 12554 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℕ0) |
82 | 77 | nnzd 12607 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℤ) |
83 | 29 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∈ ℕ) |
84 | 83 | nnzd 12607 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∈ ℤ) |
85 | | dvdsmul1 16246 |
. . . . . . . . . . . . 13
⊢ ((𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ) → 𝑖 ∥ (𝑖 · 𝑗)) |
86 | 82, 84, 85 | syl2anc 583 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∥ (𝑖 · 𝑗)) |
87 | | simprr 772 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑚 · 𝑛)) |
88 | 7, 79 | sselid 3976 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℂ) |
89 | | simprlr 779 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ 𝑌) |
90 | 10, 89 | sselid 3976 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ ℂ) |
91 | 88, 90 | mulcomd 11257 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 · 𝑛) = (𝑛 · 𝑚)) |
92 | 87, 91 | eqtrd 2767 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑛 · 𝑚)) |
93 | 86, 92 | breqtrd 5168 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∥ (𝑛 · 𝑚)) |
94 | 9, 89 | sselid 3976 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ ℕ) |
95 | 94 | nnzd 12607 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∈ ℤ) |
96 | 42 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑁 ∈ ℤ) |
97 | 82, 96 | gcdcomd 16480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 gcd 𝑁) = (𝑁 gcd 𝑖)) |
98 | 48 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑀 ∈ ℤ) |
99 | 40 | nnzd 12607 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ ℤ) |
100 | 46 | nnzd 12607 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑀 ∈ ℤ) |
101 | 99, 100 | gcdcomd 16480 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁 gcd 𝑀) = (𝑀 gcd 𝑁)) |
102 | | mpodvdsmulf1o.3 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑀 gcd 𝑁) = 1) |
103 | 101, 102 | eqtrd 2767 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 gcd 𝑀) = 1) |
104 | 103 | ad2antrr 725 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑁 gcd 𝑀) = 1) |
105 | 38 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∥ 𝑀) |
106 | | rpdvds 16622 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ((𝑁 gcd 𝑀) = 1 ∧ 𝑖 ∥ 𝑀)) → (𝑁 gcd 𝑖) = 1) |
107 | 96, 82, 98, 104, 105, 106 | syl32anc 1376 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑁 gcd 𝑖) = 1) |
108 | 97, 107 | eqtrd 2767 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 gcd 𝑁) = 1) |
109 | | breq1 5145 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑛 → (𝑥 ∥ 𝑁 ↔ 𝑛 ∥ 𝑁)) |
110 | 109, 8 | elrab2 3683 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝑌 ↔ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝑁)) |
111 | 110 | simprbi 496 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ 𝑌 → 𝑛 ∥ 𝑁) |
112 | 89, 111 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑛 ∥ 𝑁) |
113 | | rpdvds 16622 |
. . . . . . . . . . . 12
⊢ (((𝑖 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑖 gcd 𝑁) = 1 ∧ 𝑛 ∥ 𝑁)) → (𝑖 gcd 𝑛) = 1) |
114 | 82, 95, 96, 108, 112, 113 | syl32anc 1376 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 gcd 𝑛) = 1) |
115 | 80 | nnzd 12607 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∈ ℤ) |
116 | | coprmdvds 16615 |
. . . . . . . . . . . 12
⊢ ((𝑖 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ) → ((𝑖 ∥ (𝑛 · 𝑚) ∧ (𝑖 gcd 𝑛) = 1) → 𝑖 ∥ 𝑚)) |
117 | 82, 95, 115, 116 | syl3anc 1369 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → ((𝑖 ∥ (𝑛 · 𝑚) ∧ (𝑖 gcd 𝑛) = 1) → 𝑖 ∥ 𝑚)) |
118 | 93, 114, 117 | mp2and 698 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∥ 𝑚) |
119 | | dvdsmul1 16246 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 𝑚 ∥ (𝑚 · 𝑛)) |
120 | 115, 95, 119 | syl2anc 583 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∥ (𝑚 · 𝑛)) |
121 | 77 | nncnd 12250 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ∈ ℂ) |
122 | 83 | nncnd 12250 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∈ ℂ) |
123 | 121, 122 | mulcomd 11257 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑗 · 𝑖)) |
124 | 87, 123 | eqtr3d 2769 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 · 𝑛) = (𝑗 · 𝑖)) |
125 | 120, 124 | breqtrd 5168 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∥ (𝑗 · 𝑖)) |
126 | 115, 96 | gcdcomd 16480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 gcd 𝑁) = (𝑁 gcd 𝑚)) |
127 | | breq1 5145 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑚 → (𝑥 ∥ 𝑀 ↔ 𝑚 ∥ 𝑀)) |
128 | 127, 4 | elrab2 3683 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ 𝑋 ↔ (𝑚 ∈ ℕ ∧ 𝑚 ∥ 𝑀)) |
129 | 128 | simprbi 496 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ 𝑋 → 𝑚 ∥ 𝑀) |
130 | 79, 129 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∥ 𝑀) |
131 | | rpdvds 16622 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ((𝑁 gcd 𝑀) = 1 ∧ 𝑚 ∥ 𝑀)) → (𝑁 gcd 𝑚) = 1) |
132 | 96, 115, 98, 104, 130, 131 | syl32anc 1376 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑁 gcd 𝑚) = 1) |
133 | 126, 132 | eqtrd 2767 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 gcd 𝑁) = 1) |
134 | 34 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 ∥ 𝑁) |
135 | | rpdvds 16622 |
. . . . . . . . . . . 12
⊢ (((𝑚 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑚 gcd 𝑁) = 1 ∧ 𝑗 ∥ 𝑁)) → (𝑚 gcd 𝑗) = 1) |
136 | 115, 84, 96, 133, 134, 135 | syl32anc 1376 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑚 gcd 𝑗) = 1) |
137 | | coprmdvds 16615 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑖 ∈ ℤ) → ((𝑚 ∥ (𝑗 · 𝑖) ∧ (𝑚 gcd 𝑗) = 1) → 𝑚 ∥ 𝑖)) |
138 | 115, 84, 82, 137 | syl3anc 1369 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → ((𝑚 ∥ (𝑗 · 𝑖) ∧ (𝑚 gcd 𝑗) = 1) → 𝑚 ∥ 𝑖)) |
139 | 125, 136,
138 | mp2and 698 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑚 ∥ 𝑖) |
140 | | dvdseq 16282 |
. . . . . . . . . 10
⊢ (((𝑖 ∈ ℕ0
∧ 𝑚 ∈
ℕ0) ∧ (𝑖 ∥ 𝑚 ∧ 𝑚 ∥ 𝑖)) → 𝑖 = 𝑚) |
141 | 78, 81, 118, 139, 140 | syl22anc 838 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 = 𝑚) |
142 | 77 | nnne0d 12284 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑖 ≠ 0) |
143 | 141 | oveq1d 7429 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑛) = (𝑚 · 𝑛)) |
144 | 87, 143 | eqtr4d 2770 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → (𝑖 · 𝑗) = (𝑖 · 𝑛)) |
145 | 122, 90, 121, 142, 144 | mulcanad 11871 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 𝑗 = 𝑛) |
146 | 141, 145 | opeq12d 4877 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌) ∧ (𝑖 · 𝑗) = (𝑚 · 𝑛))) → 〈𝑖, 𝑗〉 = 〈𝑚, 𝑛〉) |
147 | 146 | expr 456 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌)) → ((𝑖 · 𝑗) = (𝑚 · 𝑛) → 〈𝑖, 𝑗〉 = 〈𝑚, 𝑛〉)) |
148 | 76, 147 | sylbid 239 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑌)) → ((𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → 〈𝑖, 𝑗〉 = 〈𝑚, 𝑛〉)) |
149 | 148 | ralrimivva 3195 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑌)) → ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → 〈𝑖, 𝑗〉 = 〈𝑚, 𝑛〉)) |
150 | 149 | ralrimivva 3195 |
. . . 4
⊢ (𝜑 → ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑌 ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → 〈𝑖, 𝑗〉 = 〈𝑚, 𝑛〉)) |
151 | | fvres 6910 |
. . . . . . . . 9
⊢ (𝑢 ∈ (𝑋 × 𝑌) → (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢)) |
152 | | fvres 6910 |
. . . . . . . . 9
⊢ (𝑣 ∈ (𝑋 × 𝑌) → (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑣) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣)) |
153 | 151, 152 | eqeqan12d 2741 |
. . . . . . . 8
⊢ ((𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) → ((((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢) = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑣) ↔ ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣))) |
154 | 153 | imbi1d 341 |
. . . . . . 7
⊢ ((𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) → (((((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢) = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣) → 𝑢 = 𝑣))) |
155 | 154 | ralbidva 3170 |
. . . . . 6
⊢ (𝑢 ∈ (𝑋 × 𝑌) → (∀𝑣 ∈ (𝑋 × 𝑌)((((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢) = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑣 ∈ (𝑋 × 𝑌)(((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣) → 𝑢 = 𝑣))) |
156 | 155 | ralbiia 3086 |
. . . . 5
⊢
(∀𝑢 ∈
(𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢) = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)(((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣) → 𝑢 = 𝑣)) |
157 | | fveq2 6891 |
. . . . . . . . . . 11
⊢ (𝑣 = 〈𝑚, 𝑛〉 → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘〈𝑚, 𝑛〉)) |
158 | | df-ov 7417 |
. . . . . . . . . . 11
⊢ (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘〈𝑚, 𝑛〉) |
159 | 157, 158 | eqtr4di 2785 |
. . . . . . . . . 10
⊢ (𝑣 = 〈𝑚, 𝑛〉 → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛)) |
160 | 159 | eqeq2d 2738 |
. . . . . . . . 9
⊢ (𝑣 = 〈𝑚, 𝑛〉 → (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣) ↔ ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛))) |
161 | | eqeq2 2739 |
. . . . . . . . 9
⊢ (𝑣 = 〈𝑚, 𝑛〉 → (𝑢 = 𝑣 ↔ 𝑢 = 〈𝑚, 𝑛〉)) |
162 | 160, 161 | imbi12d 344 |
. . . . . . . 8
⊢ (𝑣 = 〈𝑚, 𝑛〉 → ((((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣) → 𝑢 = 𝑣) ↔ (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → 𝑢 = 〈𝑚, 𝑛〉))) |
163 | 162 | ralxp 5838 |
. . . . . . 7
⊢
(∀𝑣 ∈
(𝑋 × 𝑌)(((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → 𝑢 = 〈𝑚, 𝑛〉)) |
164 | | fveq2 6891 |
. . . . . . . . . . 11
⊢ (𝑢 = 〈𝑖, 𝑗〉 → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘〈𝑖, 𝑗〉)) |
165 | | df-ov 7417 |
. . . . . . . . . . 11
⊢ (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘〈𝑖, 𝑗〉) |
166 | 164, 165 | eqtr4di 2785 |
. . . . . . . . . 10
⊢ (𝑢 = 〈𝑖, 𝑗〉 → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗)) |
167 | 166 | eqeq1d 2729 |
. . . . . . . . 9
⊢ (𝑢 = 〈𝑖, 𝑗〉 → (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) ↔ (𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛))) |
168 | | eqeq1 2731 |
. . . . . . . . 9
⊢ (𝑢 = 〈𝑖, 𝑗〉 → (𝑢 = 〈𝑚, 𝑛〉 ↔ 〈𝑖, 𝑗〉 = 〈𝑚, 𝑛〉)) |
169 | 167, 168 | imbi12d 344 |
. . . . . . . 8
⊢ (𝑢 = 〈𝑖, 𝑗〉 → ((((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → 𝑢 = 〈𝑚, 𝑛〉) ↔ ((𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → 〈𝑖, 𝑗〉 = 〈𝑚, 𝑛〉))) |
170 | 169 | 2ralbidv 3213 |
. . . . . . 7
⊢ (𝑢 = 〈𝑖, 𝑗〉 → (∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → 𝑢 = 〈𝑚, 𝑛〉) ↔ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → 〈𝑖, 𝑗〉 = 〈𝑚, 𝑛〉))) |
171 | 163, 170 | bitrid 283 |
. . . . . 6
⊢ (𝑢 = 〈𝑖, 𝑗〉 → (∀𝑣 ∈ (𝑋 × 𝑌)(((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → 〈𝑖, 𝑗〉 = 〈𝑚, 𝑛〉))) |
172 | 171 | ralxp 5838 |
. . . . 5
⊢
(∀𝑢 ∈
(𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)(((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑢) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑌 ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → 〈𝑖, 𝑗〉 = 〈𝑚, 𝑛〉)) |
173 | 156, 172 | bitri 275 |
. . . 4
⊢
(∀𝑢 ∈
(𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢) = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣) ↔ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑌 ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑌 ((𝑖(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑗) = (𝑚(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑛) → 〈𝑖, 𝑗〉 = 〈𝑚, 𝑛〉)) |
174 | 150, 173 | sylibr 233 |
. . 3
⊢ (𝜑 → ∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢) = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣)) |
175 | | dff13 7259 |
. . 3
⊢ (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1→𝑍 ↔ (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍 ∧ ∀𝑢 ∈ (𝑋 × 𝑌)∀𝑣 ∈ (𝑋 × 𝑌)((((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢) = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑣) → 𝑢 = 𝑣))) |
176 | 66, 174, 175 | sylanbrc 582 |
. 2
⊢ (𝜑 → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1→𝑍) |
177 | | breq1 5145 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑤 → (𝑥 ∥ (𝑀 · 𝑁) ↔ 𝑤 ∥ (𝑀 · 𝑁))) |
178 | 177, 59 | elrab2 3683 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ 𝑍 ↔ (𝑤 ∈ ℕ ∧ 𝑤 ∥ (𝑀 · 𝑁))) |
179 | 178 | simplbi 497 |
. . . . . . . . . 10
⊢ (𝑤 ∈ 𝑍 → 𝑤 ∈ ℕ) |
180 | 179 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∈ ℕ) |
181 | 180 | nnzd 12607 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∈ ℤ) |
182 | 46 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑀 ∈ ℕ) |
183 | 182 | nnzd 12607 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑀 ∈ ℤ) |
184 | 182 | nnne0d 12284 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑀 ≠ 0) |
185 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝑤 = 0 ∧ 𝑀 = 0) → 𝑀 = 0) |
186 | 185 | necon3ai 2960 |
. . . . . . . . 9
⊢ (𝑀 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑀 = 0)) |
187 | 184, 186 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ¬ (𝑤 = 0 ∧ 𝑀 = 0)) |
188 | | gcdn0cl 16468 |
. . . . . . . 8
⊢ (((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ¬
(𝑤 = 0 ∧ 𝑀 = 0)) → (𝑤 gcd 𝑀) ∈ ℕ) |
189 | 181, 183,
187, 188 | syl21anc 837 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑀) ∈ ℕ) |
190 | | gcddvds 16469 |
. . . . . . . . 9
⊢ ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀)) |
191 | 181, 183,
190 | syl2anc 583 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀)) |
192 | 191 | simprd 495 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑀) ∥ 𝑀) |
193 | | breq1 5145 |
. . . . . . . 8
⊢ (𝑥 = (𝑤 gcd 𝑀) → (𝑥 ∥ 𝑀 ↔ (𝑤 gcd 𝑀) ∥ 𝑀)) |
194 | 193, 4 | elrab2 3683 |
. . . . . . 7
⊢ ((𝑤 gcd 𝑀) ∈ 𝑋 ↔ ((𝑤 gcd 𝑀) ∈ ℕ ∧ (𝑤 gcd 𝑀) ∥ 𝑀)) |
195 | 189, 192,
194 | sylanbrc 582 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑀) ∈ 𝑋) |
196 | 40 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑁 ∈ ℕ) |
197 | 196 | nnzd 12607 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑁 ∈ ℤ) |
198 | 196 | nnne0d 12284 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑁 ≠ 0) |
199 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝑤 = 0 ∧ 𝑁 = 0) → 𝑁 = 0) |
200 | 199 | necon3ai 2960 |
. . . . . . . . 9
⊢ (𝑁 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑁 = 0)) |
201 | 198, 200 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ¬ (𝑤 = 0 ∧ 𝑁 = 0)) |
202 | | gcdn0cl 16468 |
. . . . . . . 8
⊢ (((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑤 = 0 ∧ 𝑁 = 0)) → (𝑤 gcd 𝑁) ∈ ℕ) |
203 | 181, 197,
201, 202 | syl21anc 837 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑁) ∈ ℕ) |
204 | | gcddvds 16469 |
. . . . . . . . 9
⊢ ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁)) |
205 | 181, 197,
204 | syl2anc 583 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁)) |
206 | 205 | simprd 495 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑁) ∥ 𝑁) |
207 | | breq1 5145 |
. . . . . . . 8
⊢ (𝑥 = (𝑤 gcd 𝑁) → (𝑥 ∥ 𝑁 ↔ (𝑤 gcd 𝑁) ∥ 𝑁)) |
208 | 207, 8 | elrab2 3683 |
. . . . . . 7
⊢ ((𝑤 gcd 𝑁) ∈ 𝑌 ↔ ((𝑤 gcd 𝑁) ∈ ℕ ∧ (𝑤 gcd 𝑁) ∥ 𝑁)) |
209 | 203, 206,
208 | sylanbrc 582 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑁) ∈ 𝑌) |
210 | 195, 209 | opelxpd 5711 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 〈(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)〉 ∈ (𝑋 × 𝑌)) |
211 | 210 | fvresd 6911 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘〈(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)〉) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘〈(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)〉)) |
212 | | df-ov 7417 |
. . . . . . . 8
⊢ ((𝑤 gcd 𝑀)(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))(𝑤 gcd 𝑁)) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘〈(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)〉) |
213 | 189 | nncnd 12250 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑀) ∈ ℂ) |
214 | 203 | nncnd 12250 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd 𝑁) ∈ ℂ) |
215 | | ovmpot 7576 |
. . . . . . . . 9
⊢ (((𝑤 gcd 𝑀) ∈ ℂ ∧ (𝑤 gcd 𝑁) ∈ ℂ) → ((𝑤 gcd 𝑀)(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))(𝑤 gcd 𝑁)) = ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁))) |
216 | 213, 214,
215 | syl2anc 583 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ((𝑤 gcd 𝑀)(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))(𝑤 gcd 𝑁)) = ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁))) |
217 | 212, 216 | eqtr3id 2781 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘〈(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)〉) = ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁))) |
218 | | df-ov 7417 |
. . . . . . . 8
⊢ ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)) = ( · ‘〈(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)〉) |
219 | 218 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁)) = ( · ‘〈(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)〉)) |
220 | 211, 217,
219 | 3eqtrd 2771 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘〈(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)〉) = ( · ‘〈(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)〉)) |
221 | 102 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑀 gcd 𝑁) = 1) |
222 | | rpmulgcd2 16618 |
. . . . . . . 8
⊢ (((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 gcd 𝑁) = 1) → (𝑤 gcd (𝑀 · 𝑁)) = ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁))) |
223 | 181, 183,
197, 221, 222 | syl31anc 1371 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd (𝑀 · 𝑁)) = ((𝑤 gcd 𝑀) · (𝑤 gcd 𝑁))) |
224 | 223, 218 | eqtrdi 2783 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd (𝑀 · 𝑁)) = ( · ‘〈(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)〉)) |
225 | 178 | simprbi 496 |
. . . . . . . 8
⊢ (𝑤 ∈ 𝑍 → 𝑤 ∥ (𝑀 · 𝑁)) |
226 | 225 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∥ (𝑀 · 𝑁)) |
227 | 46, 40 | nnmulcld 12287 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 · 𝑁) ∈ ℕ) |
228 | | gcdeq 16520 |
. . . . . . . 8
⊢ ((𝑤 ∈ ℕ ∧ (𝑀 · 𝑁) ∈ ℕ) → ((𝑤 gcd (𝑀 · 𝑁)) = 𝑤 ↔ 𝑤 ∥ (𝑀 · 𝑁))) |
229 | 179, 227,
228 | syl2anr 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ((𝑤 gcd (𝑀 · 𝑁)) = 𝑤 ↔ 𝑤 ∥ (𝑀 · 𝑁))) |
230 | 226, 229 | mpbird 257 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤 gcd (𝑀 · 𝑁)) = 𝑤) |
231 | 220, 224,
230 | 3eqtr2rd 2774 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘〈(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)〉)) |
232 | | fveq2 6891 |
. . . . . 6
⊢ (𝑢 = 〈(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)〉 → (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢) = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘〈(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)〉)) |
233 | 232 | rspceeqv 3629 |
. . . . 5
⊢
((〈(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)〉 ∈ (𝑋 × 𝑌) ∧ 𝑤 = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘〈(𝑤 gcd 𝑀), (𝑤 gcd 𝑁)〉)) → ∃𝑢 ∈ (𝑋 × 𝑌)𝑤 = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢)) |
234 | 210, 231,
233 | syl2anc 583 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ∃𝑢 ∈ (𝑋 × 𝑌)𝑤 = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢)) |
235 | 234 | ralrimiva 3141 |
. . 3
⊢ (𝜑 → ∀𝑤 ∈ 𝑍 ∃𝑢 ∈ (𝑋 × 𝑌)𝑤 = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢)) |
236 | | dffo3 7106 |
. . 3
⊢ (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–onto→𝑍 ↔ (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)⟶𝑍 ∧ ∀𝑤 ∈ 𝑍 ∃𝑢 ∈ (𝑋 × 𝑌)𝑤 = (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌))‘𝑢))) |
237 | 66, 235, 236 | sylanbrc 582 |
. 2
⊢ (𝜑 → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–onto→𝑍) |
238 | | df-f1o 6549 |
. 2
⊢ (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1-onto→𝑍 ↔ (((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1→𝑍 ∧ ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–onto→𝑍)) |
239 | 176, 237,
238 | sylanbrc 582 |
1
⊢ (𝜑 → ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ↾ (𝑋 × 𝑌)):(𝑋 × 𝑌)–1-1-onto→𝑍) |