Theorem rmxy1

Description: Value of the X and Y sequences at 1. (Contributed by Stefan O'Rear, 22-Sep-2014)

	Ref	Expression
Assertion	rmxy1	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to \left(A{X}_{\mathrm{rm}}1=A\wedge A{Y}_{\mathrm{rm}}1=1\right)$$

Proof

Step	Hyp	Ref	Expression
1		1z	$$⊢1\in \mathbb{Z}$$
2		rmxyval	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge 1\in \mathbb{Z}\right)\to \left(A{X}_{\mathrm{rm}}1\right)+\sqrt{A^2-1}\left(A{Y}_{\mathrm{rm}}1\right)={\left(A+\sqrt{A^2-1}\right)}^1$$
3	1 2	mpan2	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to \left(A{X}_{\mathrm{rm}}1\right)+\sqrt{A^2-1}\left(A{Y}_{\mathrm{rm}}1\right)={\left(A+\sqrt{A^2-1}\right)}^1$$
4		rmbaserp	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A+\sqrt{A^2-1}\in {ℝ}^{+}$$
5	4	rpcnd	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A+\sqrt{A^2-1}\in ℂ$$
6	5	exp1d	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to {\left(A+\sqrt{A^2-1}\right)}^1=A+\sqrt{A^2-1}$$
7		rmspecpos	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A^2-1\in {ℝ}^{+}$$
8	7	rpcnd	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A^2-1\in ℂ$$
9	8	sqrtcld	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to \sqrt{A^2-1}\in ℂ$$
10	9	mulid1d	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to \sqrt{A^2-1}\cdot 1=\sqrt{A^2-1}$$
11	10	eqcomd	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to \sqrt{A^2-1}=\sqrt{A^2-1}\cdot 1$$
12	11	oveq2d	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A+\sqrt{A^2-1}=A+\sqrt{A^2-1}\cdot 1$$
13	3 6 12	3eqtrd	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to \left(A{X}_{\mathrm{rm}}1\right)+\sqrt{A^2-1}\left(A{Y}_{\mathrm{rm}}1\right)=A+\sqrt{A^2-1}\cdot 1$$
14		rmspecsqrtnq	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to \sqrt{A^2-1}\in \left(ℂ\setminus \mathbb{Q}\right)$$
15		nn0ssq	$$⊢{\mathbb{N}}_0\subseteq \mathbb{Q}$$
16		frmx	$$⊢X_{\mathrm{rm}}:{\mathbb{Z}}_{\ge 2}\times \mathbb{Z}⟶{\mathbb{N}}_0$$
17	16	fovcl	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge 1\in \mathbb{Z}\right)\to A{X}_{\mathrm{rm}}1\in {\mathbb{N}}_0$$
18	1 17	mpan2	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A{X}_{\mathrm{rm}}1\in {\mathbb{N}}_0$$
19	15 18	sseldi	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A{X}_{\mathrm{rm}}1\in \mathbb{Q}$$
20		zssq	$$⊢\mathbb{Z}\subseteq \mathbb{Q}$$
21		frmy	$$⊢Y_{\mathrm{rm}}:{\mathbb{Z}}_{\ge 2}\times \mathbb{Z}⟶\mathbb{Z}$$
22	21	fovcl	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge 1\in \mathbb{Z}\right)\to A{Y}_{\mathrm{rm}}1\in \mathbb{Z}$$
23	1 22	mpan2	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A{Y}_{\mathrm{rm}}1\in \mathbb{Z}$$
24	20 23	sseldi	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A{Y}_{\mathrm{rm}}1\in \mathbb{Q}$$
25		eluzelz	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A\in \mathbb{Z}$$
26		zq	$$⊢A\in \mathbb{Z}\to A\in \mathbb{Q}$$
27	25 26	syl	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A\in \mathbb{Q}$$
28	20 1	sselii	$$⊢1\in \mathbb{Q}$$
29	28	a1i	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 1\in \mathbb{Q}$$
30		qirropth	$$⊢\left(\sqrt{A^2-1}\in \left(ℂ\setminus \mathbb{Q}\right)\wedge \left(A{X}_{\mathrm{rm}}1\in \mathbb{Q}\wedge A{Y}_{\mathrm{rm}}1\in \mathbb{Q}\right)\wedge \left(A\in \mathbb{Q}\wedge 1\in \mathbb{Q}\right)\right)\to \left(\left(A{X}_{\mathrm{rm}}1\right)+\sqrt{A^2-1}\left(A{Y}_{\mathrm{rm}}1\right)=A+\sqrt{A^2-1}\cdot 1\leftrightarrow \left(A{X}_{\mathrm{rm}}1=A\wedge A{Y}_{\mathrm{rm}}1=1\right)\right)$$
31	14 19 24 27 29 30	syl122anc	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to \left(\left(A{X}_{\mathrm{rm}}1\right)+\sqrt{A^2-1}\left(A{Y}_{\mathrm{rm}}1\right)=A+\sqrt{A^2-1}\cdot 1\leftrightarrow \left(A{X}_{\mathrm{rm}}1=A\wedge A{Y}_{\mathrm{rm}}1=1\right)\right)$$
32	13 31	mpbid	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to \left(A{X}_{\mathrm{rm}}1=A\wedge A{Y}_{\mathrm{rm}}1=1\right)$$