# Metamath Proof Explorer

## 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 {ℤ}_{\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 ℤ$
2 rmxyval ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge 1\in ℤ\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 {ℤ}_{\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 {ℤ}_{\ge 2}\to {A}+\sqrt{{{A}}^{2}-1}\in {ℝ}^{+}$
5 4 rpcnd ${⊢}{A}\in {ℤ}_{\ge 2}\to {A}+\sqrt{{{A}}^{2}-1}\in ℂ$
6 5 exp1d ${⊢}{A}\in {ℤ}_{\ge 2}\to {\left({A}+\sqrt{{{A}}^{2}-1}\right)}^{1}={A}+\sqrt{{{A}}^{2}-1}$
7 rmspecpos ${⊢}{A}\in {ℤ}_{\ge 2}\to {{A}}^{2}-1\in {ℝ}^{+}$
8 7 rpcnd ${⊢}{A}\in {ℤ}_{\ge 2}\to {{A}}^{2}-1\in ℂ$
9 8 sqrtcld ${⊢}{A}\in {ℤ}_{\ge 2}\to \sqrt{{{A}}^{2}-1}\in ℂ$
10 9 mulid1d ${⊢}{A}\in {ℤ}_{\ge 2}\to \sqrt{{{A}}^{2}-1}\cdot 1=\sqrt{{{A}}^{2}-1}$
11 10 eqcomd ${⊢}{A}\in {ℤ}_{\ge 2}\to \sqrt{{{A}}^{2}-1}=\sqrt{{{A}}^{2}-1}\cdot 1$
12 11 oveq2d ${⊢}{A}\in {ℤ}_{\ge 2}\to {A}+\sqrt{{{A}}^{2}-1}={A}+\sqrt{{{A}}^{2}-1}\cdot 1$
13 3 6 12 3eqtrd ${⊢}{A}\in {ℤ}_{\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 {ℤ}_{\ge 2}\to \sqrt{{{A}}^{2}-1}\in \left(ℂ\setminus ℚ\right)$
15 nn0ssq ${⊢}{ℕ}_{0}\subseteq ℚ$
16 frmx ${⊢}{X}_{\mathrm{rm}}:{ℤ}_{\ge 2}×ℤ⟶{ℕ}_{0}$
17 16 fovcl ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge 1\in ℤ\right)\to {A}{X}_{\mathrm{rm}}1\in {ℕ}_{0}$
18 1 17 mpan2 ${⊢}{A}\in {ℤ}_{\ge 2}\to {A}{X}_{\mathrm{rm}}1\in {ℕ}_{0}$
19 15 18 sseldi ${⊢}{A}\in {ℤ}_{\ge 2}\to {A}{X}_{\mathrm{rm}}1\in ℚ$
20 zssq ${⊢}ℤ\subseteq ℚ$
21 frmy ${⊢}{Y}_{\mathrm{rm}}:{ℤ}_{\ge 2}×ℤ⟶ℤ$
22 21 fovcl ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge 1\in ℤ\right)\to {A}{Y}_{\mathrm{rm}}1\in ℤ$
23 1 22 mpan2 ${⊢}{A}\in {ℤ}_{\ge 2}\to {A}{Y}_{\mathrm{rm}}1\in ℤ$
24 20 23 sseldi ${⊢}{A}\in {ℤ}_{\ge 2}\to {A}{Y}_{\mathrm{rm}}1\in ℚ$
25 eluzelz ${⊢}{A}\in {ℤ}_{\ge 2}\to {A}\in ℤ$
26 zq ${⊢}{A}\in ℤ\to {A}\in ℚ$
27 25 26 syl ${⊢}{A}\in {ℤ}_{\ge 2}\to {A}\in ℚ$
28 20 1 sselii ${⊢}1\in ℚ$
29 28 a1i ${⊢}{A}\in {ℤ}_{\ge 2}\to 1\in ℚ$
30 qirropth ${⊢}\left(\sqrt{{{A}}^{2}-1}\in \left(ℂ\setminus ℚ\right)\wedge \left({A}{X}_{\mathrm{rm}}1\in ℚ\wedge {A}{Y}_{\mathrm{rm}}1\in ℚ\right)\wedge \left({A}\in ℚ\wedge 1\in ℚ\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↔\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 {ℤ}_{\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↔\left({A}{X}_{\mathrm{rm}}1={A}\wedge {A}{Y}_{\mathrm{rm}}1=1\right)\right)$
32 13 31 mpbid ${⊢}{A}\in {ℤ}_{\ge 2}\to \left({A}{X}_{\mathrm{rm}}1={A}\wedge {A}{Y}_{\mathrm{rm}}1=1\right)$