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 {\mathbb{Z}}_{\ge 2}\wedge N\in \mathbb{Z}\right)\to A{Y}_{\mathrm{rm}}N=2^{nd}\left({\left(b\in \left({\mathbb{N}}_0\times \mathbb{Z}\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({\mathbb{N}}_0\times \mathbb{Z}\right)⟼1^{st}\left(b\right)+\sqrt{a^2-1}{2}^{nd}\left(b\right)\right)=\left(b\in \left({\mathbb{N}}_0\times \mathbb{Z}\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({\mathbb{N}}_0\times \mathbb{Z}\right)⟼1^{st}\left(b\right)+\sqrt{a^2-1}{2}^{nd}\left(b\right)\right)}^{-1}={\left(b\in \left({\mathbb{N}}_0\times \mathbb{Z}\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({\mathbb{N}}_0\times \mathbb{Z}\right)⟼1^{st}\left(b\right)+\sqrt{a^2-1}{2}^{nd}\left(b\right)\right)}^{-1}={\left(b\in \left({\mathbb{N}}_0\times \mathbb{Z}\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({\mathbb{N}}_0\times \mathbb{Z}\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({\mathbb{N}}_0\times \mathbb{Z}\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({\mathbb{N}}_0\times \mathbb{Z}\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({\mathbb{N}}_0\times \mathbb{Z}\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 {\mathbb{Z}}_{\ge 2},n\in \mathbb{Z}⟼2^{nd}\left({\left(b\in \left({\mathbb{N}}_0\times \mathbb{Z}\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({\mathbb{N}}_0\times \mathbb{Z}\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 {\mathbb{Z}}_{\ge 2}\wedge N\in \mathbb{Z}\right)\to A{Y}_{\mathrm{rm}}N=2^{nd}\left({\left(b\in \left({\mathbb{N}}_0\times \mathbb{Z}\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)$$