Proof of Theorem rmxypairf1o
Step | Hyp | Ref
| Expression |
1 | | ovex 7302 |
. . . 4
⊢
((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))
∈ V |
2 | | eqid 2740 |
. . . 4
⊢ (𝑏 ∈ (ℕ0
× ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))) = (𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))) |
3 | 1, 2 | fnmpti 6573 |
. . 3
⊢ (𝑏 ∈ (ℕ0
× ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))) Fn (ℕ0 ×
ℤ) |
4 | 3 | a1i 11 |
. 2
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))) Fn (ℕ0 ×
ℤ)) |
5 | 2 | rnmpt 5862 |
. . 3
⊢ ran
(𝑏 ∈
(ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))) = {𝑎 ∣ ∃𝑏 ∈ (ℕ0 ×
ℤ)𝑎 =
((1st ‘𝑏)
+ ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))} |
6 | | vex 3435 |
. . . . . . . . . 10
⊢ 𝑐 ∈ V |
7 | | vex 3435 |
. . . . . . . . . 10
⊢ 𝑑 ∈ V |
8 | 6, 7 | op1std 7832 |
. . . . . . . . 9
⊢ (𝑏 = 〈𝑐, 𝑑〉 → (1st ‘𝑏) = 𝑐) |
9 | 6, 7 | op2ndd 7833 |
. . . . . . . . . 10
⊢ (𝑏 = 〈𝑐, 𝑑〉 → (2nd ‘𝑏) = 𝑑) |
10 | 9 | oveq2d 7285 |
. . . . . . . . 9
⊢ (𝑏 = 〈𝑐, 𝑑〉 → ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))
= ((√‘((𝐴↑2) − 1)) · 𝑑)) |
11 | 8, 10 | oveq12d 7287 |
. . . . . . . 8
⊢ (𝑏 = 〈𝑐, 𝑑〉 → ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))
= (𝑐 +
((√‘((𝐴↑2)
− 1)) · 𝑑))) |
12 | 11 | eqeq2d 2751 |
. . . . . . 7
⊢ (𝑏 = 〈𝑐, 𝑑〉 → (𝑎 = ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))
↔ 𝑎 = (𝑐 + ((√‘((𝐴↑2) − 1)) ·
𝑑)))) |
13 | 12 | rexxp 5749 |
. . . . . 6
⊢
(∃𝑏 ∈
(ℕ0 × ℤ)𝑎 = ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))
↔ ∃𝑐 ∈
ℕ0 ∃𝑑 ∈ ℤ 𝑎 = (𝑐 + ((√‘((𝐴↑2) − 1)) · 𝑑))) |
14 | 13 | bicomi 223 |
. . . . 5
⊢
(∃𝑐 ∈
ℕ0 ∃𝑑 ∈ ℤ 𝑎 = (𝑐 + ((√‘((𝐴↑2) − 1)) · 𝑑)) ↔ ∃𝑏 ∈ (ℕ0
× ℤ)𝑎 =
((1st ‘𝑏)
+ ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))) |
15 | 14 | a1i 11 |
. . . 4
⊢ (𝐴 ∈
(ℤ≥‘2) → (∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℤ 𝑎 = (𝑐 + ((√‘((𝐴↑2) − 1)) · 𝑑)) ↔ ∃𝑏 ∈ (ℕ0
× ℤ)𝑎 =
((1st ‘𝑏)
+ ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))) |
16 | 15 | abbidv 2809 |
. . 3
⊢ (𝐴 ∈
(ℤ≥‘2) → {𝑎 ∣ ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℤ 𝑎 = (𝑐 + ((√‘((𝐴↑2) − 1)) · 𝑑))} = {𝑎 ∣ ∃𝑏 ∈ (ℕ0 ×
ℤ)𝑎 =
((1st ‘𝑏)
+ ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))}) |
17 | 5, 16 | eqtr4id 2799 |
. 2
⊢ (𝐴 ∈
(ℤ≥‘2) → ran (𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))) = {𝑎 ∣ ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℤ 𝑎 = (𝑐 + ((√‘((𝐴↑2) − 1)) · 𝑑))}) |
18 | | fveq2 6769 |
. . . . . . . 8
⊢ (𝑏 = 𝑐 → (1st ‘𝑏) = (1st ‘𝑐)) |
19 | | fveq2 6769 |
. . . . . . . . 9
⊢ (𝑏 = 𝑐 → (2nd ‘𝑏) = (2nd ‘𝑐)) |
20 | 19 | oveq2d 7285 |
. . . . . . . 8
⊢ (𝑏 = 𝑐 → ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))
= ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑐))) |
21 | 18, 20 | oveq12d 7287 |
. . . . . . 7
⊢ (𝑏 = 𝑐 → ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))
= ((1st ‘𝑐) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑐)))) |
22 | | ovex 7302 |
. . . . . . 7
⊢
((1st ‘𝑐) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑐)))
∈ V |
23 | 21, 2, 22 | fvmpt 6870 |
. . . . . 6
⊢ (𝑐 ∈ (ℕ0
× ℤ) → ((𝑏
∈ (ℕ0 × ℤ) ↦ ((1st
‘𝑏) +
((√‘((𝐴↑2)
− 1)) · (2nd ‘𝑏))))‘𝑐) = ((1st ‘𝑐) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑐)))) |
24 | 23 | ad2antrl 725 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → ((𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))‘𝑐) = ((1st ‘𝑐) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑐)))) |
25 | | fveq2 6769 |
. . . . . . . 8
⊢ (𝑏 = 𝑑 → (1st ‘𝑏) = (1st ‘𝑑)) |
26 | | fveq2 6769 |
. . . . . . . . 9
⊢ (𝑏 = 𝑑 → (2nd ‘𝑏) = (2nd ‘𝑑)) |
27 | 26 | oveq2d 7285 |
. . . . . . . 8
⊢ (𝑏 = 𝑑 → ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))
= ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑑))) |
28 | 25, 27 | oveq12d 7287 |
. . . . . . 7
⊢ (𝑏 = 𝑑 → ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))
= ((1st ‘𝑑) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑑)))) |
29 | | ovex 7302 |
. . . . . . 7
⊢
((1st ‘𝑑) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑑)))
∈ V |
30 | 28, 2, 29 | fvmpt 6870 |
. . . . . 6
⊢ (𝑑 ∈ (ℕ0
× ℤ) → ((𝑏
∈ (ℕ0 × ℤ) ↦ ((1st
‘𝑏) +
((√‘((𝐴↑2)
− 1)) · (2nd ‘𝑏))))‘𝑑) = ((1st ‘𝑑) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑑)))) |
31 | 30 | ad2antll 726 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → ((𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))‘𝑑) = ((1st ‘𝑑) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑑)))) |
32 | 24, 31 | eqeq12d 2756 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (((𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))‘𝑐) = ((𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))‘𝑑) ↔ ((1st ‘𝑐) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑐)))
= ((1st ‘𝑑) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑑))))) |
33 | | rmspecsqrtnq 40723 |
. . . . . . . 8
⊢ (𝐴 ∈
(ℤ≥‘2) → (√‘((𝐴↑2) − 1)) ∈ (ℂ ∖
ℚ)) |
34 | 33 | adantr 481 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (√‘((𝐴↑2) − 1)) ∈
(ℂ ∖ ℚ)) |
35 | | nn0ssq 12694 |
. . . . . . . 8
⊢
ℕ0 ⊆ ℚ |
36 | | xp1st 7854 |
. . . . . . . . 9
⊢ (𝑐 ∈ (ℕ0
× ℤ) → (1st ‘𝑐) ∈
ℕ0) |
37 | 36 | ad2antrl 725 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (1st ‘𝑐) ∈
ℕ0) |
38 | 35, 37 | sselid 3924 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (1st ‘𝑐) ∈
ℚ) |
39 | | xp2nd 7855 |
. . . . . . . . 9
⊢ (𝑐 ∈ (ℕ0
× ℤ) → (2nd ‘𝑐) ∈ ℤ) |
40 | 39 | ad2antrl 725 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (2nd ‘𝑐) ∈
ℤ) |
41 | | zq 12691 |
. . . . . . . 8
⊢
((2nd ‘𝑐) ∈ ℤ → (2nd
‘𝑐) ∈
ℚ) |
42 | 40, 41 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (2nd ‘𝑐) ∈
ℚ) |
43 | | xp1st 7854 |
. . . . . . . . 9
⊢ (𝑑 ∈ (ℕ0
× ℤ) → (1st ‘𝑑) ∈
ℕ0) |
44 | 43 | ad2antll 726 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (1st ‘𝑑) ∈
ℕ0) |
45 | 35, 44 | sselid 3924 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (1st ‘𝑑) ∈
ℚ) |
46 | | xp2nd 7855 |
. . . . . . . . 9
⊢ (𝑑 ∈ (ℕ0
× ℤ) → (2nd ‘𝑑) ∈ ℤ) |
47 | 46 | ad2antll 726 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (2nd ‘𝑑) ∈
ℤ) |
48 | | zq 12691 |
. . . . . . . 8
⊢
((2nd ‘𝑑) ∈ ℤ → (2nd
‘𝑑) ∈
ℚ) |
49 | 47, 48 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (2nd ‘𝑑) ∈
ℚ) |
50 | | qirropth 40725 |
. . . . . . 7
⊢
(((√‘((𝐴↑2) − 1)) ∈ (ℂ ∖
ℚ) ∧ ((1st ‘𝑐) ∈ ℚ ∧ (2nd
‘𝑐) ∈ ℚ)
∧ ((1st ‘𝑑) ∈ ℚ ∧ (2nd
‘𝑑) ∈ ℚ))
→ (((1st ‘𝑐) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑐)))
= ((1st ‘𝑑) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑑)))
↔ ((1st ‘𝑐) = (1st ‘𝑑) ∧ (2nd ‘𝑐) = (2nd ‘𝑑)))) |
51 | 34, 38, 42, 45, 49, 50 | syl122anc 1378 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (((1st ‘𝑐) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑐)))
= ((1st ‘𝑑) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑑)))
↔ ((1st ‘𝑐) = (1st ‘𝑑) ∧ (2nd ‘𝑐) = (2nd ‘𝑑)))) |
52 | 51 | biimpd 228 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (((1st ‘𝑐) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑐)))
= ((1st ‘𝑑) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑑)))
→ ((1st ‘𝑐) = (1st ‘𝑑) ∧ (2nd ‘𝑐) = (2nd ‘𝑑)))) |
53 | | xpopth 7863 |
. . . . . 6
⊢ ((𝑐 ∈ (ℕ0
× ℤ) ∧ 𝑑
∈ (ℕ0 × ℤ)) → (((1st
‘𝑐) = (1st
‘𝑑) ∧
(2nd ‘𝑐) =
(2nd ‘𝑑))
↔ 𝑐 = 𝑑)) |
54 | 53 | adantl 482 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (((1st ‘𝑐) = (1st ‘𝑑) ∧ (2nd
‘𝑐) = (2nd
‘𝑑)) ↔ 𝑐 = 𝑑)) |
55 | 52, 54 | sylibd 238 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (((1st ‘𝑐) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑐)))
= ((1st ‘𝑑) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑑)))
→ 𝑐 = 𝑑)) |
56 | 32, 55 | sylbid 239 |
. . 3
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (((𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))‘𝑐) = ((𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))‘𝑑) → 𝑐 = 𝑑)) |
57 | 56 | ralrimivva 3117 |
. 2
⊢ (𝐴 ∈
(ℤ≥‘2) → ∀𝑐 ∈ (ℕ0 ×
ℤ)∀𝑑 ∈
(ℕ0 × ℤ)(((𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))‘𝑐) = ((𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))‘𝑑) → 𝑐 = 𝑑)) |
58 | | dff1o6 7142 |
. 2
⊢ ((𝑏 ∈ (ℕ0
× ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))):(ℕ0 ×
ℤ)–1-1-onto→{𝑎 ∣ ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℤ 𝑎 = (𝑐 + ((√‘((𝐴↑2) − 1)) · 𝑑))} ↔ ((𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))) Fn (ℕ0 × ℤ)
∧ ran (𝑏 ∈
(ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))) = {𝑎 ∣ ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℤ 𝑎 = (𝑐 + ((√‘((𝐴↑2) − 1)) · 𝑑))} ∧ ∀𝑐 ∈ (ℕ0
× ℤ)∀𝑑
∈ (ℕ0 × ℤ)(((𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))‘𝑐) = ((𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))‘𝑑) → 𝑐 = 𝑑))) |
59 | 4, 17, 57, 58 | syl3anbrc 1342 |
1
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))):(ℕ0 ×
ℤ)–1-1-onto→{𝑎 ∣ ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℤ 𝑎 = (𝑐 + ((√‘((𝐴↑2) − 1)) · 𝑑))}) |