# Metamath Proof Explorer

## Theorem rmxyelqirr

Description: The solutions used to construct the X and Y sequences are quadratic irrationals. (Contributed by Stefan O'Rear, 21-Sep-2014)

Ref Expression
Assertion 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\}$

### Proof

Step Hyp Ref Expression
1 rmspecnonsq ${⊢}{A}\in {ℤ}_{\ge 2}\to {{A}}^{2}-1\in \left(ℕ\setminus {◻}_{ℕ}\right)$
2 1 adantr ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to {{A}}^{2}-1\in \left(ℕ\setminus {◻}_{ℕ}\right)$
3 pell14qrval ${⊢}{{A}}^{2}-1\in \left(ℕ\setminus {◻}_{ℕ}\right)\to \mathrm{Pell14QR}\left({{A}}^{2}-1\right)=\left\{{a}\in ℝ|\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}\left({a}={c}+\sqrt{{{A}}^{2}-1}{d}\wedge {{c}}^{2}-\left({{A}}^{2}-1\right){{d}}^{2}=1\right)\right\}$
4 2 3 syl ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to \mathrm{Pell14QR}\left({{A}}^{2}-1\right)=\left\{{a}\in ℝ|\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}\left({a}={c}+\sqrt{{{A}}^{2}-1}{d}\wedge {{c}}^{2}-\left({{A}}^{2}-1\right){{d}}^{2}=1\right)\right\}$
5 simpl ${⊢}\left({a}={c}+\sqrt{{{A}}^{2}-1}{d}\wedge {{c}}^{2}-\left({{A}}^{2}-1\right){{d}}^{2}=1\right)\to {a}={c}+\sqrt{{{A}}^{2}-1}{d}$
6 5 reximi ${⊢}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}\left({a}={c}+\sqrt{{{A}}^{2}-1}{d}\wedge {{c}}^{2}-\left({{A}}^{2}-1\right){{d}}^{2}=1\right)\to \exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}{a}={c}+\sqrt{{{A}}^{2}-1}{d}$
7 6 reximi ${⊢}\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}\left({a}={c}+\sqrt{{{A}}^{2}-1}{d}\wedge {{c}}^{2}-\left({{A}}^{2}-1\right){{d}}^{2}=1\right)\to \exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}{a}={c}+\sqrt{{{A}}^{2}-1}{d}$
8 7 rgenw ${⊢}\forall {a}\in ℝ\phantom{\rule{.4em}{0ex}}\left(\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}\left({a}={c}+\sqrt{{{A}}^{2}-1}{d}\wedge {{c}}^{2}-\left({{A}}^{2}-1\right){{d}}^{2}=1\right)\to \exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}{a}={c}+\sqrt{{{A}}^{2}-1}{d}\right)$
9 8 a1i ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to \forall {a}\in ℝ\phantom{\rule{.4em}{0ex}}\left(\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}\left({a}={c}+\sqrt{{{A}}^{2}-1}{d}\wedge {{c}}^{2}-\left({{A}}^{2}-1\right){{d}}^{2}=1\right)\to \exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}{a}={c}+\sqrt{{{A}}^{2}-1}{d}\right)$
10 ss2rab ${⊢}\left\{{a}\in ℝ|\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}\left({a}={c}+\sqrt{{{A}}^{2}-1}{d}\wedge {{c}}^{2}-\left({{A}}^{2}-1\right){{d}}^{2}=1\right)\right\}\subseteq \left\{{a}\in ℝ|\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}{a}={c}+\sqrt{{{A}}^{2}-1}{d}\right\}↔\forall {a}\in ℝ\phantom{\rule{.4em}{0ex}}\left(\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}\left({a}={c}+\sqrt{{{A}}^{2}-1}{d}\wedge {{c}}^{2}-\left({{A}}^{2}-1\right){{d}}^{2}=1\right)\to \exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}{a}={c}+\sqrt{{{A}}^{2}-1}{d}\right)$
11 9 10 sylibr ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to \left\{{a}\in ℝ|\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}\left({a}={c}+\sqrt{{{A}}^{2}-1}{d}\wedge {{c}}^{2}-\left({{A}}^{2}-1\right){{d}}^{2}=1\right)\right\}\subseteq \left\{{a}\in ℝ|\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}{a}={c}+\sqrt{{{A}}^{2}-1}{d}\right\}$
12 ssv ${⊢}ℝ\subseteq \mathrm{V}$
13 rabss2 ${⊢}ℝ\subseteq \mathrm{V}\to \left\{{a}\in ℝ|\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}{a}={c}+\sqrt{{{A}}^{2}-1}{d}\right\}\subseteq \left\{{a}\in \mathrm{V}|\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}{a}={c}+\sqrt{{{A}}^{2}-1}{d}\right\}$
14 12 13 ax-mp ${⊢}\left\{{a}\in ℝ|\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}{a}={c}+\sqrt{{{A}}^{2}-1}{d}\right\}\subseteq \left\{{a}\in \mathrm{V}|\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}{a}={c}+\sqrt{{{A}}^{2}-1}{d}\right\}$
15 11 14 sstrdi ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to \left\{{a}\in ℝ|\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}\left({a}={c}+\sqrt{{{A}}^{2}-1}{d}\wedge {{c}}^{2}-\left({{A}}^{2}-1\right){{d}}^{2}=1\right)\right\}\subseteq \left\{{a}\in \mathrm{V}|\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}{a}={c}+\sqrt{{{A}}^{2}-1}{d}\right\}$
16 rabab ${⊢}\left\{{a}\in \mathrm{V}|\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}{a}={c}+\sqrt{{{A}}^{2}-1}{d}\right\}=\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\}$
17 15 16 sseqtrdi ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to \left\{{a}\in ℝ|\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}\left({a}={c}+\sqrt{{{A}}^{2}-1}{d}\wedge {{c}}^{2}-\left({{A}}^{2}-1\right){{d}}^{2}=1\right)\right\}\subseteq \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\}$
18 4 17 eqsstrd ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to \mathrm{Pell14QR}\left({{A}}^{2}-1\right)\subseteq \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 simpr ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to {N}\in ℤ$
20 rmspecfund ${⊢}{A}\in {ℤ}_{\ge 2}\to \mathrm{PellFund}\left({{A}}^{2}-1\right)={A}+\sqrt{{{A}}^{2}-1}$
21 20 adantr ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to \mathrm{PellFund}\left({{A}}^{2}-1\right)={A}+\sqrt{{{A}}^{2}-1}$
22 21 eqcomd ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to {A}+\sqrt{{{A}}^{2}-1}=\mathrm{PellFund}\left({{A}}^{2}-1\right)$
23 22 oveq1d ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to {\left({A}+\sqrt{{{A}}^{2}-1}\right)}^{{N}}={\mathrm{PellFund}\left({{A}}^{2}-1\right)}^{{N}}$
24 oveq2 ${⊢}{a}={N}\to {\mathrm{PellFund}\left({{A}}^{2}-1\right)}^{{a}}={\mathrm{PellFund}\left({{A}}^{2}-1\right)}^{{N}}$
25 24 rspceeqv ${⊢}\left({N}\in ℤ\wedge {\left({A}+\sqrt{{{A}}^{2}-1}\right)}^{{N}}={\mathrm{PellFund}\left({{A}}^{2}-1\right)}^{{N}}\right)\to \exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}{\left({A}+\sqrt{{{A}}^{2}-1}\right)}^{{N}}={\mathrm{PellFund}\left({{A}}^{2}-1\right)}^{{a}}$
26 19 23 25 syl2anc ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to \exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}{\left({A}+\sqrt{{{A}}^{2}-1}\right)}^{{N}}={\mathrm{PellFund}\left({{A}}^{2}-1\right)}^{{a}}$
27 pellfund14b ${⊢}{{A}}^{2}-1\in \left(ℕ\setminus {◻}_{ℕ}\right)\to \left({\left({A}+\sqrt{{{A}}^{2}-1}\right)}^{{N}}\in \mathrm{Pell14QR}\left({{A}}^{2}-1\right)↔\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}{\left({A}+\sqrt{{{A}}^{2}-1}\right)}^{{N}}={\mathrm{PellFund}\left({{A}}^{2}-1\right)}^{{a}}\right)$
28 2 27 syl ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to \left({\left({A}+\sqrt{{{A}}^{2}-1}\right)}^{{N}}\in \mathrm{Pell14QR}\left({{A}}^{2}-1\right)↔\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}{\left({A}+\sqrt{{{A}}^{2}-1}\right)}^{{N}}={\mathrm{PellFund}\left({{A}}^{2}-1\right)}^{{a}}\right)$
29 26 28 mpbird ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to {\left({A}+\sqrt{{{A}}^{2}-1}\right)}^{{N}}\in \mathrm{Pell14QR}\left({{A}}^{2}-1\right)$
30 18 29 sseldd ${⊢}\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\}$