# Metamath Proof Explorer

## Theorem rmxy0

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

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

### Proof

Step Hyp Ref Expression
1 0z ${⊢}0\in ℤ$
2 rmxyval ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge 0\in ℤ\right)\to \left({A}{X}_{\mathrm{rm}}0\right)+\sqrt{{{A}}^{2}-1}\left({A}{Y}_{\mathrm{rm}}0\right)={\left({A}+\sqrt{{{A}}^{2}-1}\right)}^{0}$
3 1 2 mpan2 ${⊢}{A}\in {ℤ}_{\ge 2}\to \left({A}{X}_{\mathrm{rm}}0\right)+\sqrt{{{A}}^{2}-1}\left({A}{Y}_{\mathrm{rm}}0\right)={\left({A}+\sqrt{{{A}}^{2}-1}\right)}^{0}$
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 exp0d ${⊢}{A}\in {ℤ}_{\ge 2}\to {\left({A}+\sqrt{{{A}}^{2}-1}\right)}^{0}=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 mul01d ${⊢}{A}\in {ℤ}_{\ge 2}\to \sqrt{{{A}}^{2}-1}\cdot 0=0$
11 10 oveq2d ${⊢}{A}\in {ℤ}_{\ge 2}\to 1+\sqrt{{{A}}^{2}-1}\cdot 0=1+0$
12 1p0e1 ${⊢}1+0=1$
13 11 12 syl6req ${⊢}{A}\in {ℤ}_{\ge 2}\to 1=1+\sqrt{{{A}}^{2}-1}\cdot 0$
14 3 6 13 3eqtrd ${⊢}{A}\in {ℤ}_{\ge 2}\to \left({A}{X}_{\mathrm{rm}}0\right)+\sqrt{{{A}}^{2}-1}\left({A}{Y}_{\mathrm{rm}}0\right)=1+\sqrt{{{A}}^{2}-1}\cdot 0$
15 rmspecsqrtnq ${⊢}{A}\in {ℤ}_{\ge 2}\to \sqrt{{{A}}^{2}-1}\in \left(ℂ\setminus ℚ\right)$
16 nn0ssq ${⊢}{ℕ}_{0}\subseteq ℚ$
17 frmx ${⊢}{X}_{\mathrm{rm}}:{ℤ}_{\ge 2}×ℤ⟶{ℕ}_{0}$
18 17 fovcl ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge 0\in ℤ\right)\to {A}{X}_{\mathrm{rm}}0\in {ℕ}_{0}$
19 1 18 mpan2 ${⊢}{A}\in {ℤ}_{\ge 2}\to {A}{X}_{\mathrm{rm}}0\in {ℕ}_{0}$
20 16 19 sseldi ${⊢}{A}\in {ℤ}_{\ge 2}\to {A}{X}_{\mathrm{rm}}0\in ℚ$
21 zssq ${⊢}ℤ\subseteq ℚ$
22 frmy ${⊢}{Y}_{\mathrm{rm}}:{ℤ}_{\ge 2}×ℤ⟶ℤ$
23 22 fovcl ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge 0\in ℤ\right)\to {A}{Y}_{\mathrm{rm}}0\in ℤ$
24 1 23 mpan2 ${⊢}{A}\in {ℤ}_{\ge 2}\to {A}{Y}_{\mathrm{rm}}0\in ℤ$
25 21 24 sseldi ${⊢}{A}\in {ℤ}_{\ge 2}\to {A}{Y}_{\mathrm{rm}}0\in ℚ$
26 1z ${⊢}1\in ℤ$
27 21 26 sselii ${⊢}1\in ℚ$
28 27 a1i ${⊢}{A}\in {ℤ}_{\ge 2}\to 1\in ℚ$
29 21 1 sselii ${⊢}0\in ℚ$
30 29 a1i ${⊢}{A}\in {ℤ}_{\ge 2}\to 0\in ℚ$
31 qirropth ${⊢}\left(\sqrt{{{A}}^{2}-1}\in \left(ℂ\setminus ℚ\right)\wedge \left({A}{X}_{\mathrm{rm}}0\in ℚ\wedge {A}{Y}_{\mathrm{rm}}0\in ℚ\right)\wedge \left(1\in ℚ\wedge 0\in ℚ\right)\right)\to \left(\left({A}{X}_{\mathrm{rm}}0\right)+\sqrt{{{A}}^{2}-1}\left({A}{Y}_{\mathrm{rm}}0\right)=1+\sqrt{{{A}}^{2}-1}\cdot 0↔\left({A}{X}_{\mathrm{rm}}0=1\wedge {A}{Y}_{\mathrm{rm}}0=0\right)\right)$
32 15 20 25 28 30 31 syl122anc ${⊢}{A}\in {ℤ}_{\ge 2}\to \left(\left({A}{X}_{\mathrm{rm}}0\right)+\sqrt{{{A}}^{2}-1}\left({A}{Y}_{\mathrm{rm}}0\right)=1+\sqrt{{{A}}^{2}-1}\cdot 0↔\left({A}{X}_{\mathrm{rm}}0=1\wedge {A}{Y}_{\mathrm{rm}}0=0\right)\right)$
33 14 32 mpbid ${⊢}{A}\in {ℤ}_{\ge 2}\to \left({A}{X}_{\mathrm{rm}}0=1\wedge {A}{Y}_{\mathrm{rm}}0=0\right)$