# Metamath Proof Explorer

## Theorem rmxyval

Description: Main definition of the X and Y sequences. Compare definition 2.3 of JonesMatijasevic p. 694. (Contributed by Stefan O'Rear, 19-Oct-2014)

Ref Expression
Assertion rmxyval ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to \left({A}{X}_{\mathrm{rm}}{N}\right)+\sqrt{{{A}}^{2}-1}\left({A}{Y}_{\mathrm{rm}}{N}\right)={\left({A}+\sqrt{{{A}}^{2}-1}\right)}^{{N}}$

### Proof

Step Hyp Ref Expression
1 rmxfval ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to {A}{X}_{\mathrm{rm}}{N}={1}^{st}\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 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)$
3 2 oveq2d ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to \sqrt{{{A}}^{2}-1}\left({A}{Y}_{\mathrm{rm}}{N}\right)=\sqrt{{{A}}^{2}-1}{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)$
4 1 3 oveq12d ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to \left({A}{X}_{\mathrm{rm}}{N}\right)+\sqrt{{{A}}^{2}-1}\left({A}{Y}_{\mathrm{rm}}{N}\right)={1}^{st}\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)+\sqrt{{{A}}^{2}-1}{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)$
5 rmxyelxp ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\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)\in \left({ℕ}_{0}×ℤ\right)$
6 fveq2 ${⊢}{a}={\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)\to {1}^{st}\left({a}\right)={1}^{st}\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)$
7 fveq2 ${⊢}{a}={\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)\to {2}^{nd}\left({a}\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)$
8 7 oveq2d ${⊢}{a}={\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)\to \sqrt{{{A}}^{2}-1}{2}^{nd}\left({a}\right)=\sqrt{{{A}}^{2}-1}{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)$
9 6 8 oveq12d ${⊢}{a}={\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)\to {1}^{st}\left({a}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({a}\right)={1}^{st}\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)+\sqrt{{{A}}^{2}-1}{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)$
10 fveq2 ${⊢}{b}={a}\to {1}^{st}\left({b}\right)={1}^{st}\left({a}\right)$
11 fveq2 ${⊢}{b}={a}\to {2}^{nd}\left({b}\right)={2}^{nd}\left({a}\right)$
12 11 oveq2d ${⊢}{b}={a}\to \sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)=\sqrt{{{A}}^{2}-1}{2}^{nd}\left({a}\right)$
13 10 12 oveq12d ${⊢}{b}={a}\to {1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)={1}^{st}\left({a}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({a}\right)$
14 13 cbvmptv ${⊢}\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)=\left({a}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({a}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({a}\right)\right)$
15 ovex ${⊢}{1}^{st}\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)+\sqrt{{{A}}^{2}-1}{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 9 14 15 fvmpt ${⊢}{\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)\in \left({ℕ}_{0}×ℤ\right)\to \left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)\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)={1}^{st}\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)+\sqrt{{{A}}^{2}-1}{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)$
17 5 16 syl ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to \left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)\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)={1}^{st}\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)+\sqrt{{{A}}^{2}-1}{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)$
18 rmxypairf1o ${⊢}{A}\in {ℤ}_{\ge 2}\to \left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right):{ℕ}_{0}×ℤ\underset{1-1 onto}{⟶}\left\{{a}|\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}{a}={c}+\sqrt{{{A}}^{2}-1}{d}\right\}$
19 18 adantr ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to \left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right):{ℕ}_{0}×ℤ\underset{1-1 onto}{⟶}\left\{{a}|\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}{a}={c}+\sqrt{{{A}}^{2}-1}{d}\right\}$
20 rmxyelqirr ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to {\left({A}+\sqrt{{{A}}^{2}-1}\right)}^{{N}}\in \left\{{a}|\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}{a}={c}+\sqrt{{{A}}^{2}-1}{d}\right\}$
21 f1ocnvfv2 ${⊢}\left(\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right):{ℕ}_{0}×ℤ\underset{1-1 onto}{⟶}\left\{{a}|\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}{a}={c}+\sqrt{{{A}}^{2}-1}{d}\right\}\wedge {\left({A}+\sqrt{{{A}}^{2}-1}\right)}^{{N}}\in \left\{{a}|\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}{a}={c}+\sqrt{{{A}}^{2}-1}{d}\right\}\right)\to \left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)\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)={\left({A}+\sqrt{{{A}}^{2}-1}\right)}^{{N}}$
22 19 20 21 syl2anc ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to \left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)\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)={\left({A}+\sqrt{{{A}}^{2}-1}\right)}^{{N}}$
23 4 17 22 3eqtr2d ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to \left({A}{X}_{\mathrm{rm}}{N}\right)+\sqrt{{{A}}^{2}-1}\left({A}{Y}_{\mathrm{rm}}{N}\right)={\left({A}+\sqrt{{{A}}^{2}-1}\right)}^{{N}}$