Proof of Theorem rmxypairf1o
| Step | Hyp | Ref
| Expression |
| 1 | | ovex 7464 |
. . . 4
⊢
((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))
∈ V |
| 2 | | eqid 2737 |
. . . 4
⊢ (𝑏 ∈ (ℕ0
× ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))) = (𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))) |
| 3 | 1, 2 | fnmpti 6711 |
. . 3
⊢ (𝑏 ∈ (ℕ0
× ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))) Fn (ℕ0 ×
ℤ) |
| 4 | 3 | a1i 11 |
. 2
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))) Fn (ℕ0 ×
ℤ)) |
| 5 | 2 | rnmpt 5968 |
. . 3
⊢ ran
(𝑏 ∈
(ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))) = {𝑎 ∣ ∃𝑏 ∈ (ℕ0 ×
ℤ)𝑎 =
((1st ‘𝑏)
+ ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))} |
| 6 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑐 ∈ V |
| 7 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑑 ∈ V |
| 8 | 6, 7 | op1std 8024 |
. . . . . . . . 9
⊢ (𝑏 = 〈𝑐, 𝑑〉 → (1st ‘𝑏) = 𝑐) |
| 9 | 6, 7 | op2ndd 8025 |
. . . . . . . . . 10
⊢ (𝑏 = 〈𝑐, 𝑑〉 → (2nd ‘𝑏) = 𝑑) |
| 10 | 9 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑏 = 〈𝑐, 𝑑〉 → ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))
= ((√‘((𝐴↑2) − 1)) · 𝑑)) |
| 11 | 8, 10 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝑏 = 〈𝑐, 𝑑〉 → ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))
= (𝑐 +
((√‘((𝐴↑2)
− 1)) · 𝑑))) |
| 12 | 11 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝑏 = 〈𝑐, 𝑑〉 → (𝑎 = ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))
↔ 𝑎 = (𝑐 + ((√‘((𝐴↑2) − 1)) ·
𝑑)))) |
| 13 | 12 | rexxp 5853 |
. . . . . 6
⊢
(∃𝑏 ∈
(ℕ0 × ℤ)𝑎 = ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))
↔ ∃𝑐 ∈
ℕ0 ∃𝑑 ∈ ℤ 𝑎 = (𝑐 + ((√‘((𝐴↑2) − 1)) · 𝑑))) |
| 14 | 13 | bicomi 224 |
. . . . 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 2808 |
. . 3
⊢ (𝐴 ∈
(ℤ≥‘2) → {𝑎 ∣ ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℤ 𝑎 = (𝑐 + ((√‘((𝐴↑2) − 1)) · 𝑑))} = {𝑎 ∣ ∃𝑏 ∈ (ℕ0 ×
ℤ)𝑎 =
((1st ‘𝑏)
+ ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))}) |
| 17 | 5, 16 | eqtr4id 2796 |
. 2
⊢ (𝐴 ∈
(ℤ≥‘2) → ran (𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))) = {𝑎 ∣ ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℤ 𝑎 = (𝑐 + ((√‘((𝐴↑2) − 1)) · 𝑑))}) |
| 18 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑏 = 𝑐 → (1st ‘𝑏) = (1st ‘𝑐)) |
| 19 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑏 = 𝑐 → (2nd ‘𝑏) = (2nd ‘𝑐)) |
| 20 | 19 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑏 = 𝑐 → ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))
= ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑐))) |
| 21 | 18, 20 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑏 = 𝑐 → ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))
= ((1st ‘𝑐) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑐)))) |
| 22 | | ovex 7464 |
. . . . . . 7
⊢
((1st ‘𝑐) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑐)))
∈ V |
| 23 | 21, 2, 22 | fvmpt 7016 |
. . . . . 6
⊢ (𝑐 ∈ (ℕ0
× ℤ) → ((𝑏
∈ (ℕ0 × ℤ) ↦ ((1st
‘𝑏) +
((√‘((𝐴↑2)
− 1)) · (2nd ‘𝑏))))‘𝑐) = ((1st ‘𝑐) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑐)))) |
| 24 | 23 | ad2antrl 728 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → ((𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))‘𝑐) = ((1st ‘𝑐) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑐)))) |
| 25 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑏 = 𝑑 → (1st ‘𝑏) = (1st ‘𝑑)) |
| 26 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑏 = 𝑑 → (2nd ‘𝑏) = (2nd ‘𝑑)) |
| 27 | 26 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑏 = 𝑑 → ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))
= ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑑))) |
| 28 | 25, 27 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑏 = 𝑑 → ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))
= ((1st ‘𝑑) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑑)))) |
| 29 | | ovex 7464 |
. . . . . . 7
⊢
((1st ‘𝑑) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑑)))
∈ V |
| 30 | 28, 2, 29 | fvmpt 7016 |
. . . . . 6
⊢ (𝑑 ∈ (ℕ0
× ℤ) → ((𝑏
∈ (ℕ0 × ℤ) ↦ ((1st
‘𝑏) +
((√‘((𝐴↑2)
− 1)) · (2nd ‘𝑏))))‘𝑑) = ((1st ‘𝑑) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑑)))) |
| 31 | 30 | ad2antll 729 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → ((𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))‘𝑑) = ((1st ‘𝑑) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑑)))) |
| 32 | 24, 31 | eqeq12d 2753 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (((𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))‘𝑐) = ((𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))‘𝑑) ↔ ((1st ‘𝑐) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑐)))
= ((1st ‘𝑑) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑑))))) |
| 33 | | rmspecsqrtnq 42917 |
. . . . . . . 8
⊢ (𝐴 ∈
(ℤ≥‘2) → (√‘((𝐴↑2) − 1)) ∈ (ℂ ∖
ℚ)) |
| 34 | 33 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (√‘((𝐴↑2) − 1)) ∈
(ℂ ∖ ℚ)) |
| 35 | | nn0ssq 12999 |
. . . . . . . 8
⊢
ℕ0 ⊆ ℚ |
| 36 | | xp1st 8046 |
. . . . . . . . 9
⊢ (𝑐 ∈ (ℕ0
× ℤ) → (1st ‘𝑐) ∈
ℕ0) |
| 37 | 36 | ad2antrl 728 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (1st ‘𝑐) ∈
ℕ0) |
| 38 | 35, 37 | sselid 3981 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (1st ‘𝑐) ∈
ℚ) |
| 39 | | xp2nd 8047 |
. . . . . . . . 9
⊢ (𝑐 ∈ (ℕ0
× ℤ) → (2nd ‘𝑐) ∈ ℤ) |
| 40 | 39 | ad2antrl 728 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (2nd ‘𝑐) ∈
ℤ) |
| 41 | | zq 12996 |
. . . . . . . 8
⊢
((2nd ‘𝑐) ∈ ℤ → (2nd
‘𝑐) ∈
ℚ) |
| 42 | 40, 41 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (2nd ‘𝑐) ∈
ℚ) |
| 43 | | xp1st 8046 |
. . . . . . . . 9
⊢ (𝑑 ∈ (ℕ0
× ℤ) → (1st ‘𝑑) ∈
ℕ0) |
| 44 | 43 | ad2antll 729 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (1st ‘𝑑) ∈
ℕ0) |
| 45 | 35, 44 | sselid 3981 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (1st ‘𝑑) ∈
ℚ) |
| 46 | | xp2nd 8047 |
. . . . . . . . 9
⊢ (𝑑 ∈ (ℕ0
× ℤ) → (2nd ‘𝑑) ∈ ℤ) |
| 47 | 46 | ad2antll 729 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (2nd ‘𝑑) ∈
ℤ) |
| 48 | | zq 12996 |
. . . . . . . 8
⊢
((2nd ‘𝑑) ∈ ℤ → (2nd
‘𝑑) ∈
ℚ) |
| 49 | 47, 48 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (2nd ‘𝑑) ∈
ℚ) |
| 50 | | qirropth 42919 |
. . . . . . 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 1381 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (((1st ‘𝑐) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑐)))
= ((1st ‘𝑑) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑑)))
↔ ((1st ‘𝑐) = (1st ‘𝑑) ∧ (2nd ‘𝑐) = (2nd ‘𝑑)))) |
| 52 | 51 | biimpd 229 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (((1st ‘𝑐) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑐)))
= ((1st ‘𝑑) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑑)))
→ ((1st ‘𝑐) = (1st ‘𝑑) ∧ (2nd ‘𝑐) = (2nd ‘𝑑)))) |
| 53 | | xpopth 8055 |
. . . . . 6
⊢ ((𝑐 ∈ (ℕ0
× ℤ) ∧ 𝑑
∈ (ℕ0 × ℤ)) → (((1st
‘𝑐) = (1st
‘𝑑) ∧
(2nd ‘𝑐) =
(2nd ‘𝑑))
↔ 𝑐 = 𝑑)) |
| 54 | 53 | adantl 481 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (((1st ‘𝑐) = (1st ‘𝑑) ∧ (2nd
‘𝑐) = (2nd
‘𝑑)) ↔ 𝑐 = 𝑑)) |
| 55 | 52, 54 | sylibd 239 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (((1st ‘𝑐) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑐)))
= ((1st ‘𝑑) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑑)))
→ 𝑐 = 𝑑)) |
| 56 | 32, 55 | sylbid 240 |
. . 3
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (((𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))‘𝑐) = ((𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))‘𝑑) → 𝑐 = 𝑑)) |
| 57 | 56 | ralrimivva 3202 |
. 2
⊢ (𝐴 ∈
(ℤ≥‘2) → ∀𝑐 ∈ (ℕ0 ×
ℤ)∀𝑑 ∈
(ℕ0 × ℤ)(((𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))‘𝑐) = ((𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))‘𝑑) → 𝑐 = 𝑑)) |
| 58 | | dff1o6 7295 |
. 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 1344 |
1
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))):(ℕ0 ×
ℤ)–1-1-onto→{𝑎 ∣ ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℤ 𝑎 = (𝑐 + ((√‘((𝐴↑2) − 1)) · 𝑑))}) |