Proof of Theorem rmxypairf1o
Step | Hyp | Ref
| Expression |
1 | | ovex 7191 |
. . . 4
⊢
((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))
∈ V |
2 | | eqid 2823 |
. . . 4
⊢ (𝑏 ∈ (ℕ0
× ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))) = (𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))) |
3 | 1, 2 | fnmpti 6493 |
. . 3
⊢ (𝑏 ∈ (ℕ0
× ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))) Fn (ℕ0 ×
ℤ) |
4 | 3 | a1i 11 |
. 2
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))) Fn (ℕ0 ×
ℤ)) |
5 | | vex 3499 |
. . . . . . . . . 10
⊢ 𝑐 ∈ V |
6 | | vex 3499 |
. . . . . . . . . 10
⊢ 𝑑 ∈ V |
7 | 5, 6 | op1std 7701 |
. . . . . . . . 9
⊢ (𝑏 = 〈𝑐, 𝑑〉 → (1st ‘𝑏) = 𝑐) |
8 | 5, 6 | op2ndd 7702 |
. . . . . . . . . 10
⊢ (𝑏 = 〈𝑐, 𝑑〉 → (2nd ‘𝑏) = 𝑑) |
9 | 8 | oveq2d 7174 |
. . . . . . . . 9
⊢ (𝑏 = 〈𝑐, 𝑑〉 → ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))
= ((√‘((𝐴↑2) − 1)) · 𝑑)) |
10 | 7, 9 | oveq12d 7176 |
. . . . . . . 8
⊢ (𝑏 = 〈𝑐, 𝑑〉 → ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))
= (𝑐 +
((√‘((𝐴↑2)
− 1)) · 𝑑))) |
11 | 10 | eqeq2d 2834 |
. . . . . . 7
⊢ (𝑏 = 〈𝑐, 𝑑〉 → (𝑎 = ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))
↔ 𝑎 = (𝑐 + ((√‘((𝐴↑2) − 1)) ·
𝑑)))) |
12 | 11 | rexxp 5715 |
. . . . . 6
⊢
(∃𝑏 ∈
(ℕ0 × ℤ)𝑎 = ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))
↔ ∃𝑐 ∈
ℕ0 ∃𝑑 ∈ ℤ 𝑎 = (𝑐 + ((√‘((𝐴↑2) − 1)) · 𝑑))) |
13 | 12 | bicomi 226 |
. . . . 5
⊢
(∃𝑐 ∈
ℕ0 ∃𝑑 ∈ ℤ 𝑎 = (𝑐 + ((√‘((𝐴↑2) − 1)) · 𝑑)) ↔ ∃𝑏 ∈ (ℕ0
× ℤ)𝑎 =
((1st ‘𝑏)
+ ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))) |
14 | 13 | a1i 11 |
. . . 4
⊢ (𝐴 ∈
(ℤ≥‘2) → (∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℤ 𝑎 = (𝑐 + ((√‘((𝐴↑2) − 1)) · 𝑑)) ↔ ∃𝑏 ∈ (ℕ0
× ℤ)𝑎 =
((1st ‘𝑏)
+ ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))) |
15 | 14 | abbidv 2887 |
. . 3
⊢ (𝐴 ∈
(ℤ≥‘2) → {𝑎 ∣ ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℤ 𝑎 = (𝑐 + ((√‘((𝐴↑2) − 1)) · 𝑑))} = {𝑎 ∣ ∃𝑏 ∈ (ℕ0 ×
ℤ)𝑎 =
((1st ‘𝑏)
+ ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))}) |
16 | 2 | rnmpt 5829 |
. . 3
⊢ ran
(𝑏 ∈
(ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))) = {𝑎 ∣ ∃𝑏 ∈ (ℕ0 ×
ℤ)𝑎 =
((1st ‘𝑏)
+ ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))} |
17 | 15, 16 | syl6reqr 2877 |
. 2
⊢ (𝐴 ∈
(ℤ≥‘2) → ran (𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))) = {𝑎 ∣ ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℤ 𝑎 = (𝑐 + ((√‘((𝐴↑2) − 1)) · 𝑑))}) |
18 | | fveq2 6672 |
. . . . . . . 8
⊢ (𝑏 = 𝑐 → (1st ‘𝑏) = (1st ‘𝑐)) |
19 | | fveq2 6672 |
. . . . . . . . 9
⊢ (𝑏 = 𝑐 → (2nd ‘𝑏) = (2nd ‘𝑐)) |
20 | 19 | oveq2d 7174 |
. . . . . . . 8
⊢ (𝑏 = 𝑐 → ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))
= ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑐))) |
21 | 18, 20 | oveq12d 7176 |
. . . . . . 7
⊢ (𝑏 = 𝑐 → ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))
= ((1st ‘𝑐) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑐)))) |
22 | | ovex 7191 |
. . . . . . 7
⊢
((1st ‘𝑐) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑐)))
∈ V |
23 | 21, 2, 22 | fvmpt 6770 |
. . . . . 6
⊢ (𝑐 ∈ (ℕ0
× ℤ) → ((𝑏
∈ (ℕ0 × ℤ) ↦ ((1st
‘𝑏) +
((√‘((𝐴↑2)
− 1)) · (2nd ‘𝑏))))‘𝑐) = ((1st ‘𝑐) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑐)))) |
24 | 23 | ad2antrl 726 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → ((𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))‘𝑐) = ((1st ‘𝑐) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑐)))) |
25 | | fveq2 6672 |
. . . . . . . 8
⊢ (𝑏 = 𝑑 → (1st ‘𝑏) = (1st ‘𝑑)) |
26 | | fveq2 6672 |
. . . . . . . . 9
⊢ (𝑏 = 𝑑 → (2nd ‘𝑏) = (2nd ‘𝑑)) |
27 | 26 | oveq2d 7174 |
. . . . . . . 8
⊢ (𝑏 = 𝑑 → ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))
= ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑑))) |
28 | 25, 27 | oveq12d 7176 |
. . . . . . 7
⊢ (𝑏 = 𝑑 → ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))
= ((1st ‘𝑑) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑑)))) |
29 | | ovex 7191 |
. . . . . . 7
⊢
((1st ‘𝑑) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑑)))
∈ V |
30 | 28, 2, 29 | fvmpt 6770 |
. . . . . 6
⊢ (𝑑 ∈ (ℕ0
× ℤ) → ((𝑏
∈ (ℕ0 × ℤ) ↦ ((1st
‘𝑏) +
((√‘((𝐴↑2)
− 1)) · (2nd ‘𝑏))))‘𝑑) = ((1st ‘𝑑) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑑)))) |
31 | 30 | ad2antll 727 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → ((𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))‘𝑑) = ((1st ‘𝑑) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑑)))) |
32 | 24, 31 | eqeq12d 2839 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (((𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))‘𝑐) = ((𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))‘𝑑) ↔ ((1st ‘𝑐) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑐)))
= ((1st ‘𝑑) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑑))))) |
33 | | rmspecsqrtnq 39510 |
. . . . . . . 8
⊢ (𝐴 ∈
(ℤ≥‘2) → (√‘((𝐴↑2) − 1)) ∈ (ℂ ∖
ℚ)) |
34 | 33 | adantr 483 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (√‘((𝐴↑2) − 1)) ∈
(ℂ ∖ ℚ)) |
35 | | nn0ssq 12359 |
. . . . . . . 8
⊢
ℕ0 ⊆ ℚ |
36 | | xp1st 7723 |
. . . . . . . . 9
⊢ (𝑐 ∈ (ℕ0
× ℤ) → (1st ‘𝑐) ∈
ℕ0) |
37 | 36 | ad2antrl 726 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (1st ‘𝑐) ∈
ℕ0) |
38 | 35, 37 | sseldi 3967 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (1st ‘𝑐) ∈
ℚ) |
39 | | xp2nd 7724 |
. . . . . . . . 9
⊢ (𝑐 ∈ (ℕ0
× ℤ) → (2nd ‘𝑐) ∈ ℤ) |
40 | 39 | ad2antrl 726 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (2nd ‘𝑐) ∈
ℤ) |
41 | | zq 12357 |
. . . . . . . 8
⊢
((2nd ‘𝑐) ∈ ℤ → (2nd
‘𝑐) ∈
ℚ) |
42 | 40, 41 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (2nd ‘𝑐) ∈
ℚ) |
43 | | xp1st 7723 |
. . . . . . . . 9
⊢ (𝑑 ∈ (ℕ0
× ℤ) → (1st ‘𝑑) ∈
ℕ0) |
44 | 43 | ad2antll 727 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (1st ‘𝑑) ∈
ℕ0) |
45 | 35, 44 | sseldi 3967 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (1st ‘𝑑) ∈
ℚ) |
46 | | xp2nd 7724 |
. . . . . . . . 9
⊢ (𝑑 ∈ (ℕ0
× ℤ) → (2nd ‘𝑑) ∈ ℤ) |
47 | 46 | ad2antll 727 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (2nd ‘𝑑) ∈
ℤ) |
48 | | zq 12357 |
. . . . . . . 8
⊢
((2nd ‘𝑑) ∈ ℤ → (2nd
‘𝑑) ∈
ℚ) |
49 | 47, 48 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (2nd ‘𝑑) ∈
ℚ) |
50 | | qirropth 39512 |
. . . . . . 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 1375 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (((1st ‘𝑐) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑐)))
= ((1st ‘𝑑) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑑)))
↔ ((1st ‘𝑐) = (1st ‘𝑑) ∧ (2nd ‘𝑐) = (2nd ‘𝑑)))) |
52 | 51 | biimpd 231 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (((1st ‘𝑐) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑐)))
= ((1st ‘𝑑) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑑)))
→ ((1st ‘𝑐) = (1st ‘𝑑) ∧ (2nd ‘𝑐) = (2nd ‘𝑑)))) |
53 | | xpopth 7732 |
. . . . . 6
⊢ ((𝑐 ∈ (ℕ0
× ℤ) ∧ 𝑑
∈ (ℕ0 × ℤ)) → (((1st
‘𝑐) = (1st
‘𝑑) ∧
(2nd ‘𝑐) =
(2nd ‘𝑑))
↔ 𝑐 = 𝑑)) |
54 | 53 | adantl 484 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (((1st ‘𝑐) = (1st ‘𝑑) ∧ (2nd
‘𝑐) = (2nd
‘𝑑)) ↔ 𝑐 = 𝑑)) |
55 | 52, 54 | sylibd 241 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (((1st ‘𝑐) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑐)))
= ((1st ‘𝑑) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑑)))
→ 𝑐 = 𝑑)) |
56 | 32, 55 | sylbid 242 |
. . 3
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑐 ∈ (ℕ0 × ℤ)
∧ 𝑑 ∈
(ℕ0 × ℤ))) → (((𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))‘𝑐) = ((𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))‘𝑑) → 𝑐 = 𝑑)) |
57 | 56 | ralrimivva 3193 |
. 2
⊢ (𝐴 ∈
(ℤ≥‘2) → ∀𝑐 ∈ (ℕ0 ×
ℤ)∀𝑑 ∈
(ℕ0 × ℤ)(((𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))‘𝑐) = ((𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))‘𝑑) → 𝑐 = 𝑑)) |
58 | | dff1o6 7034 |
. 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 1339 |
1
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))):(ℕ0 ×
ℤ)–1-1-onto→{𝑎 ∣ ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℤ 𝑎 = (𝑐 + ((√‘((𝐴↑2) − 1)) · 𝑑))}) |