# Metamath Proof Explorer

## Theorem rmyfval

Description: Value of the Y sequence. Not used after rmxyval is proved. (Contributed by Stefan O'Rear, 21-Sep-2014)

Ref Expression
Assertion rmyfval ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to {A}{Y}_{\mathrm{rm}}{N}={2}^{nd}\left({\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)}^{-1}\left({\left({A}+\sqrt{{{A}}^{2}-1}\right)}^{{N}}\right)\right)$

### Proof

Step Hyp Ref Expression
1 oveq1 ${⊢}{a}={A}\to {{a}}^{2}={{A}}^{2}$
2 1 fvoveq1d ${⊢}{a}={A}\to \sqrt{{{a}}^{2}-1}=\sqrt{{{A}}^{2}-1}$
3 2 oveq1d ${⊢}{a}={A}\to \sqrt{{{a}}^{2}-1}{2}^{nd}\left({b}\right)=\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)$
4 3 oveq2d ${⊢}{a}={A}\to {1}^{st}\left({b}\right)+\sqrt{{{a}}^{2}-1}{2}^{nd}\left({b}\right)={1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)$
5 4 mpteq2dv ${⊢}{a}={A}\to \left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{a}}^{2}-1}{2}^{nd}\left({b}\right)\right)=\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)$
6 5 cnveqd ${⊢}{a}={A}\to {\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{a}}^{2}-1}{2}^{nd}\left({b}\right)\right)}^{-1}={\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)}^{-1}$
7 6 adantr ${⊢}\left({a}={A}\wedge {n}={N}\right)\to {\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{a}}^{2}-1}{2}^{nd}\left({b}\right)\right)}^{-1}={\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)}^{-1}$
8 id ${⊢}{a}={A}\to {a}={A}$
9 8 2 oveq12d ${⊢}{a}={A}\to {a}+\sqrt{{{a}}^{2}-1}={A}+\sqrt{{{A}}^{2}-1}$
10 id ${⊢}{n}={N}\to {n}={N}$
11 9 10 oveqan12d ${⊢}\left({a}={A}\wedge {n}={N}\right)\to {\left({a}+\sqrt{{{a}}^{2}-1}\right)}^{{n}}={\left({A}+\sqrt{{{A}}^{2}-1}\right)}^{{N}}$
12 7 11 fveq12d ${⊢}\left({a}={A}\wedge {n}={N}\right)\to {\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{a}}^{2}-1}{2}^{nd}\left({b}\right)\right)}^{-1}\left({\left({a}+\sqrt{{{a}}^{2}-1}\right)}^{{n}}\right)={\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)}^{-1}\left({\left({A}+\sqrt{{{A}}^{2}-1}\right)}^{{N}}\right)$
13 12 fveq2d ${⊢}\left({a}={A}\wedge {n}={N}\right)\to {2}^{nd}\left({\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{a}}^{2}-1}{2}^{nd}\left({b}\right)\right)}^{-1}\left({\left({a}+\sqrt{{{a}}^{2}-1}\right)}^{{n}}\right)\right)={2}^{nd}\left({\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)}^{-1}\left({\left({A}+\sqrt{{{A}}^{2}-1}\right)}^{{N}}\right)\right)$
14 df-rmy ${⊢}{Y}_{\mathrm{rm}}=\left({a}\in {ℤ}_{\ge 2},{n}\in ℤ⟼{2}^{nd}\left({\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{a}}^{2}-1}{2}^{nd}\left({b}\right)\right)}^{-1}\left({\left({a}+\sqrt{{{a}}^{2}-1}\right)}^{{n}}\right)\right)\right)$
15 fvex ${⊢}{2}^{nd}\left({\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)}^{-1}\left({\left({A}+\sqrt{{{A}}^{2}-1}\right)}^{{N}}\right)\right)\in \mathrm{V}$
16 13 14 15 ovmpoa ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to {A}{Y}_{\mathrm{rm}}{N}={2}^{nd}\left({\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)}^{-1}\left({\left({A}+\sqrt{{{A}}^{2}-1}\right)}^{{N}}\right)\right)$