| Step | Hyp | Ref
| Expression |
| 1 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐴 → (𝑎↑2) = (𝐴↑2)) |
| 2 | 1 | fvoveq1d 7453 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → (√‘((𝑎↑2) − 1)) = (√‘((𝐴↑2) −
1))) |
| 3 | 2 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → ((√‘((𝑎↑2) − 1)) · (2nd
‘𝑏)) =
((√‘((𝐴↑2)
− 1)) · (2nd ‘𝑏))) |
| 4 | 3 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → ((1st ‘𝑏) + ((√‘((𝑎↑2) − 1)) ·
(2nd ‘𝑏)))
= ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏)))) |
| 5 | 4 | mpteq2dv 5244 |
. . . . . 6
⊢ (𝑎 = 𝐴 → (𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝑎↑2) − 1)) · (2nd
‘𝑏)))) = (𝑏 ∈ (ℕ0
× ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))) |
| 6 | 5 | cnveqd 5886 |
. . . . 5
⊢ (𝑎 = 𝐴 → ◡(𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝑎↑2) − 1)) · (2nd
‘𝑏)))) = ◡(𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))) |
| 7 | 6 | adantr 480 |
. . . 4
⊢ ((𝑎 = 𝐴 ∧ 𝑛 = 𝑁) → ◡(𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝑎↑2) − 1)) · (2nd
‘𝑏)))) = ◡(𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))) |
| 8 | | id 22 |
. . . . . 6
⊢ (𝑎 = 𝐴 → 𝑎 = 𝐴) |
| 9 | 8, 2 | oveq12d 7449 |
. . . . 5
⊢ (𝑎 = 𝐴 → (𝑎 + (√‘((𝑎↑2) − 1))) = (𝐴 + (√‘((𝐴↑2) − 1)))) |
| 10 | | id 22 |
. . . . 5
⊢ (𝑛 = 𝑁 → 𝑛 = 𝑁) |
| 11 | 9, 10 | oveqan12d 7450 |
. . . 4
⊢ ((𝑎 = 𝐴 ∧ 𝑛 = 𝑁) → ((𝑎 + (√‘((𝑎↑2) − 1)))↑𝑛) = ((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁)) |
| 12 | 7, 11 | fveq12d 6913 |
. . 3
⊢ ((𝑎 = 𝐴 ∧ 𝑛 = 𝑁) → (◡(𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝑎↑2) − 1)) · (2nd
‘𝑏))))‘((𝑎 + (√‘((𝑎↑2) − 1)))↑𝑛)) = (◡(𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))‘((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁))) |
| 13 | 12 | fveq2d 6910 |
. 2
⊢ ((𝑎 = 𝐴 ∧ 𝑛 = 𝑁) → (2nd ‘(◡(𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝑎↑2) − 1)) · (2nd
‘𝑏))))‘((𝑎 + (√‘((𝑎↑2) − 1)))↑𝑛))) = (2nd
‘(◡(𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))‘((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁)))) |
| 14 | | df-rmy 42914 |
. 2
⊢
Yrm = (𝑎 ∈
(ℤ≥‘2), 𝑛 ∈ ℤ ↦ (2nd
‘(◡(𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝑎↑2) − 1)) · (2nd
‘𝑏))))‘((𝑎 + (√‘((𝑎↑2) − 1)))↑𝑛)))) |
| 15 | | fvex 6919 |
. 2
⊢
(2nd ‘(◡(𝑏 ∈ (ℕ0
× ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))‘((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁))) ∈ V |
| 16 | 13, 14, 15 | ovmpoa 7588 |
1
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑁) = (2nd ‘(◡(𝑏 ∈ (ℕ0 × ℤ)
↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) ·
(2nd ‘𝑏))))‘((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁)))) |