# Metamath Proof Explorer

## Theorem rmxycomplete

Description: The X and Y sequences taken together enumerate all solutions to the corresponding Pell equation in the right half-plane. This is Metamath 100 proof #39. (Contributed by Stefan O'Rear, 22-Sep-2014)

Ref Expression
Assertion rmxycomplete ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\to \left({{X}}^{2}-\left({{A}}^{2}-1\right){{Y}}^{2}=1↔\exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}\left({X}={A}{X}_{\mathrm{rm}}{n}\wedge {Y}={A}{Y}_{\mathrm{rm}}{n}\right)\right)$

### Proof

Step Hyp Ref Expression
1 rmspecnonsq ${⊢}{A}\in {ℤ}_{\ge 2}\to {{A}}^{2}-1\in \left(ℕ\setminus {◻}_{ℕ}\right)$
2 1 3ad2ant1 ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\to {{A}}^{2}-1\in \left(ℕ\setminus {◻}_{ℕ}\right)$
3 pellfund14b ${⊢}{{A}}^{2}-1\in \left(ℕ\setminus {◻}_{ℕ}\right)\to \left({X}+\sqrt{{{A}}^{2}-1}{Y}\in \mathrm{Pell14QR}\left({{A}}^{2}-1\right)↔\exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}{X}+\sqrt{{{A}}^{2}-1}{Y}={\mathrm{PellFund}\left({{A}}^{2}-1\right)}^{{n}}\right)$
4 2 3 syl ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\to \left({X}+\sqrt{{{A}}^{2}-1}{Y}\in \mathrm{Pell14QR}\left({{A}}^{2}-1\right)↔\exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}{X}+\sqrt{{{A}}^{2}-1}{Y}={\mathrm{PellFund}\left({{A}}^{2}-1\right)}^{{n}}\right)$
5 nn0re ${⊢}{X}\in {ℕ}_{0}\to {X}\in ℝ$
6 5 3ad2ant2 ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\to {X}\in ℝ$
7 rmspecpos ${⊢}{A}\in {ℤ}_{\ge 2}\to {{A}}^{2}-1\in {ℝ}^{+}$
8 7 rpsqrtcld ${⊢}{A}\in {ℤ}_{\ge 2}\to \sqrt{{{A}}^{2}-1}\in {ℝ}^{+}$
9 8 rpred ${⊢}{A}\in {ℤ}_{\ge 2}\to \sqrt{{{A}}^{2}-1}\in ℝ$
10 9 3ad2ant1 ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\to \sqrt{{{A}}^{2}-1}\in ℝ$
11 zre ${⊢}{Y}\in ℤ\to {Y}\in ℝ$
12 11 3ad2ant3 ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\to {Y}\in ℝ$
13 10 12 remulcld ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\to \sqrt{{{A}}^{2}-1}{Y}\in ℝ$
14 6 13 readdcld ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\to {X}+\sqrt{{{A}}^{2}-1}{Y}\in ℝ$
15 14 biantrurd ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\to \left(\exists {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}\left({X}+\sqrt{{{A}}^{2}-1}{Y}={x}+\sqrt{{{A}}^{2}-1}{y}\wedge {{x}}^{2}-\left({{A}}^{2}-1\right){{y}}^{2}=1\right)↔\left({X}+\sqrt{{{A}}^{2}-1}{Y}\in ℝ\wedge \exists {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}\left({X}+\sqrt{{{A}}^{2}-1}{Y}={x}+\sqrt{{{A}}^{2}-1}{y}\wedge {{x}}^{2}-\left({{A}}^{2}-1\right){{y}}^{2}=1\right)\right)\right)$
16 simpl2 ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\wedge {{X}}^{2}-\left({{A}}^{2}-1\right){{Y}}^{2}=1\right)\to {X}\in {ℕ}_{0}$
17 simpl3 ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\wedge {{X}}^{2}-\left({{A}}^{2}-1\right){{Y}}^{2}=1\right)\to {Y}\in ℤ$
18 eqidd ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\wedge {{X}}^{2}-\left({{A}}^{2}-1\right){{Y}}^{2}=1\right)\to {X}+\sqrt{{{A}}^{2}-1}{Y}={X}+\sqrt{{{A}}^{2}-1}{Y}$
19 simpr ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\wedge {{X}}^{2}-\left({{A}}^{2}-1\right){{Y}}^{2}=1\right)\to {{X}}^{2}-\left({{A}}^{2}-1\right){{Y}}^{2}=1$
20 oveq1 ${⊢}{x}={X}\to {x}+\sqrt{{{A}}^{2}-1}{y}={X}+\sqrt{{{A}}^{2}-1}{y}$
21 20 eqeq2d ${⊢}{x}={X}\to \left({X}+\sqrt{{{A}}^{2}-1}{Y}={x}+\sqrt{{{A}}^{2}-1}{y}↔{X}+\sqrt{{{A}}^{2}-1}{Y}={X}+\sqrt{{{A}}^{2}-1}{y}\right)$
22 oveq1 ${⊢}{x}={X}\to {{x}}^{2}={{X}}^{2}$
23 22 oveq1d ${⊢}{x}={X}\to {{x}}^{2}-\left({{A}}^{2}-1\right){{y}}^{2}={{X}}^{2}-\left({{A}}^{2}-1\right){{y}}^{2}$
24 23 eqeq1d ${⊢}{x}={X}\to \left({{x}}^{2}-\left({{A}}^{2}-1\right){{y}}^{2}=1↔{{X}}^{2}-\left({{A}}^{2}-1\right){{y}}^{2}=1\right)$
25 21 24 anbi12d ${⊢}{x}={X}\to \left(\left({X}+\sqrt{{{A}}^{2}-1}{Y}={x}+\sqrt{{{A}}^{2}-1}{y}\wedge {{x}}^{2}-\left({{A}}^{2}-1\right){{y}}^{2}=1\right)↔\left({X}+\sqrt{{{A}}^{2}-1}{Y}={X}+\sqrt{{{A}}^{2}-1}{y}\wedge {{X}}^{2}-\left({{A}}^{2}-1\right){{y}}^{2}=1\right)\right)$
26 oveq2 ${⊢}{y}={Y}\to \sqrt{{{A}}^{2}-1}{y}=\sqrt{{{A}}^{2}-1}{Y}$
27 26 oveq2d ${⊢}{y}={Y}\to {X}+\sqrt{{{A}}^{2}-1}{y}={X}+\sqrt{{{A}}^{2}-1}{Y}$
28 27 eqeq2d ${⊢}{y}={Y}\to \left({X}+\sqrt{{{A}}^{2}-1}{Y}={X}+\sqrt{{{A}}^{2}-1}{y}↔{X}+\sqrt{{{A}}^{2}-1}{Y}={X}+\sqrt{{{A}}^{2}-1}{Y}\right)$
29 oveq1 ${⊢}{y}={Y}\to {{y}}^{2}={{Y}}^{2}$
30 29 oveq2d ${⊢}{y}={Y}\to \left({{A}}^{2}-1\right){{y}}^{2}=\left({{A}}^{2}-1\right){{Y}}^{2}$
31 30 oveq2d ${⊢}{y}={Y}\to {{X}}^{2}-\left({{A}}^{2}-1\right){{y}}^{2}={{X}}^{2}-\left({{A}}^{2}-1\right){{Y}}^{2}$
32 31 eqeq1d ${⊢}{y}={Y}\to \left({{X}}^{2}-\left({{A}}^{2}-1\right){{y}}^{2}=1↔{{X}}^{2}-\left({{A}}^{2}-1\right){{Y}}^{2}=1\right)$
33 28 32 anbi12d ${⊢}{y}={Y}\to \left(\left({X}+\sqrt{{{A}}^{2}-1}{Y}={X}+\sqrt{{{A}}^{2}-1}{y}\wedge {{X}}^{2}-\left({{A}}^{2}-1\right){{y}}^{2}=1\right)↔\left({X}+\sqrt{{{A}}^{2}-1}{Y}={X}+\sqrt{{{A}}^{2}-1}{Y}\wedge {{X}}^{2}-\left({{A}}^{2}-1\right){{Y}}^{2}=1\right)\right)$
34 25 33 rspc2ev ${⊢}\left({X}\in {ℕ}_{0}\wedge {Y}\in ℤ\wedge \left({X}+\sqrt{{{A}}^{2}-1}{Y}={X}+\sqrt{{{A}}^{2}-1}{Y}\wedge {{X}}^{2}-\left({{A}}^{2}-1\right){{Y}}^{2}=1\right)\right)\to \exists {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}\left({X}+\sqrt{{{A}}^{2}-1}{Y}={x}+\sqrt{{{A}}^{2}-1}{y}\wedge {{x}}^{2}-\left({{A}}^{2}-1\right){{y}}^{2}=1\right)$
35 16 17 18 19 34 syl112anc ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\wedge {{X}}^{2}-\left({{A}}^{2}-1\right){{Y}}^{2}=1\right)\to \exists {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}\left({X}+\sqrt{{{A}}^{2}-1}{Y}={x}+\sqrt{{{A}}^{2}-1}{y}\wedge {{x}}^{2}-\left({{A}}^{2}-1\right){{y}}^{2}=1\right)$
36 35 ex ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\to \left({{X}}^{2}-\left({{A}}^{2}-1\right){{Y}}^{2}=1\to \exists {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}\left({X}+\sqrt{{{A}}^{2}-1}{Y}={x}+\sqrt{{{A}}^{2}-1}{y}\wedge {{x}}^{2}-\left({{A}}^{2}-1\right){{y}}^{2}=1\right)\right)$
37 rmspecsqrtnq ${⊢}{A}\in {ℤ}_{\ge 2}\to \sqrt{{{A}}^{2}-1}\in \left(ℂ\setminus ℚ\right)$
38 37 3ad2ant1 ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\to \sqrt{{{A}}^{2}-1}\in \left(ℂ\setminus ℚ\right)$
39 38 adantr ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\wedge \left({x}\in {ℕ}_{0}\wedge {y}\in ℤ\right)\right)\to \sqrt{{{A}}^{2}-1}\in \left(ℂ\setminus ℚ\right)$
40 nn0ssq ${⊢}{ℕ}_{0}\subseteq ℚ$
41 simp2 ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\to {X}\in {ℕ}_{0}$
42 40 41 sseldi ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\to {X}\in ℚ$
43 42 adantr ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\wedge \left({x}\in {ℕ}_{0}\wedge {y}\in ℤ\right)\right)\to {X}\in ℚ$
44 zq ${⊢}{Y}\in ℤ\to {Y}\in ℚ$
45 44 3ad2ant3 ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\to {Y}\in ℚ$
46 45 adantr ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\wedge \left({x}\in {ℕ}_{0}\wedge {y}\in ℤ\right)\right)\to {Y}\in ℚ$
47 40 sseli ${⊢}{x}\in {ℕ}_{0}\to {x}\in ℚ$
48 47 ad2antrl ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\wedge \left({x}\in {ℕ}_{0}\wedge {y}\in ℤ\right)\right)\to {x}\in ℚ$
49 zq ${⊢}{y}\in ℤ\to {y}\in ℚ$
50 49 ad2antll ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\wedge \left({x}\in {ℕ}_{0}\wedge {y}\in ℤ\right)\right)\to {y}\in ℚ$
51 qirropth ${⊢}\left(\sqrt{{{A}}^{2}-1}\in \left(ℂ\setminus ℚ\right)\wedge \left({X}\in ℚ\wedge {Y}\in ℚ\right)\wedge \left({x}\in ℚ\wedge {y}\in ℚ\right)\right)\to \left({X}+\sqrt{{{A}}^{2}-1}{Y}={x}+\sqrt{{{A}}^{2}-1}{y}↔\left({X}={x}\wedge {Y}={y}\right)\right)$
52 39 43 46 48 50 51 syl122anc ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\wedge \left({x}\in {ℕ}_{0}\wedge {y}\in ℤ\right)\right)\to \left({X}+\sqrt{{{A}}^{2}-1}{Y}={x}+\sqrt{{{A}}^{2}-1}{y}↔\left({X}={x}\wedge {Y}={y}\right)\right)$
53 52 biimpd ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\wedge \left({x}\in {ℕ}_{0}\wedge {y}\in ℤ\right)\right)\to \left({X}+\sqrt{{{A}}^{2}-1}{Y}={x}+\sqrt{{{A}}^{2}-1}{y}\to \left({X}={x}\wedge {Y}={y}\right)\right)$
54 53 anim1d ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\wedge \left({x}\in {ℕ}_{0}\wedge {y}\in ℤ\right)\right)\to \left(\left({X}+\sqrt{{{A}}^{2}-1}{Y}={x}+\sqrt{{{A}}^{2}-1}{y}\wedge {{x}}^{2}-\left({{A}}^{2}-1\right){{y}}^{2}=1\right)\to \left(\left({X}={x}\wedge {Y}={y}\right)\wedge {{x}}^{2}-\left({{A}}^{2}-1\right){{y}}^{2}=1\right)\right)$
55 oveq1 ${⊢}{X}={x}\to {{X}}^{2}={{x}}^{2}$
56 oveq1 ${⊢}{Y}={y}\to {{Y}}^{2}={{y}}^{2}$
57 56 oveq2d ${⊢}{Y}={y}\to \left({{A}}^{2}-1\right){{Y}}^{2}=\left({{A}}^{2}-1\right){{y}}^{2}$
58 55 57 oveqan12d ${⊢}\left({X}={x}\wedge {Y}={y}\right)\to {{X}}^{2}-\left({{A}}^{2}-1\right){{Y}}^{2}={{x}}^{2}-\left({{A}}^{2}-1\right){{y}}^{2}$
59 58 eqcomd ${⊢}\left({X}={x}\wedge {Y}={y}\right)\to {{x}}^{2}-\left({{A}}^{2}-1\right){{y}}^{2}={{X}}^{2}-\left({{A}}^{2}-1\right){{Y}}^{2}$
60 59 eqeq1d ${⊢}\left({X}={x}\wedge {Y}={y}\right)\to \left({{x}}^{2}-\left({{A}}^{2}-1\right){{y}}^{2}=1↔{{X}}^{2}-\left({{A}}^{2}-1\right){{Y}}^{2}=1\right)$
61 60 biimpa ${⊢}\left(\left({X}={x}\wedge {Y}={y}\right)\wedge {{x}}^{2}-\left({{A}}^{2}-1\right){{y}}^{2}=1\right)\to {{X}}^{2}-\left({{A}}^{2}-1\right){{Y}}^{2}=1$
62 54 61 syl6 ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\wedge \left({x}\in {ℕ}_{0}\wedge {y}\in ℤ\right)\right)\to \left(\left({X}+\sqrt{{{A}}^{2}-1}{Y}={x}+\sqrt{{{A}}^{2}-1}{y}\wedge {{x}}^{2}-\left({{A}}^{2}-1\right){{y}}^{2}=1\right)\to {{X}}^{2}-\left({{A}}^{2}-1\right){{Y}}^{2}=1\right)$
63 62 rexlimdvva ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\to \left(\exists {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}\left({X}+\sqrt{{{A}}^{2}-1}{Y}={x}+\sqrt{{{A}}^{2}-1}{y}\wedge {{x}}^{2}-\left({{A}}^{2}-1\right){{y}}^{2}=1\right)\to {{X}}^{2}-\left({{A}}^{2}-1\right){{Y}}^{2}=1\right)$
64 36 63 impbid ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\to \left({{X}}^{2}-\left({{A}}^{2}-1\right){{Y}}^{2}=1↔\exists {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}\left({X}+\sqrt{{{A}}^{2}-1}{Y}={x}+\sqrt{{{A}}^{2}-1}{y}\wedge {{x}}^{2}-\left({{A}}^{2}-1\right){{y}}^{2}=1\right)\right)$
65 elpell14qr ${⊢}{{A}}^{2}-1\in \left(ℕ\setminus {◻}_{ℕ}\right)\to \left({X}+\sqrt{{{A}}^{2}-1}{Y}\in \mathrm{Pell14QR}\left({{A}}^{2}-1\right)↔\left({X}+\sqrt{{{A}}^{2}-1}{Y}\in ℝ\wedge \exists {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}\left({X}+\sqrt{{{A}}^{2}-1}{Y}={x}+\sqrt{{{A}}^{2}-1}{y}\wedge {{x}}^{2}-\left({{A}}^{2}-1\right){{y}}^{2}=1\right)\right)\right)$
66 2 65 syl ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\to \left({X}+\sqrt{{{A}}^{2}-1}{Y}\in \mathrm{Pell14QR}\left({{A}}^{2}-1\right)↔\left({X}+\sqrt{{{A}}^{2}-1}{Y}\in ℝ\wedge \exists {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}\left({X}+\sqrt{{{A}}^{2}-1}{Y}={x}+\sqrt{{{A}}^{2}-1}{y}\wedge {{x}}^{2}-\left({{A}}^{2}-1\right){{y}}^{2}=1\right)\right)\right)$
67 15 64 66 3bitr4d ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\to \left({{X}}^{2}-\left({{A}}^{2}-1\right){{Y}}^{2}=1↔{X}+\sqrt{{{A}}^{2}-1}{Y}\in \mathrm{Pell14QR}\left({{A}}^{2}-1\right)\right)$
68 38 adantr ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\wedge {n}\in ℤ\right)\to \sqrt{{{A}}^{2}-1}\in \left(ℂ\setminus ℚ\right)$
69 42 adantr ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\wedge {n}\in ℤ\right)\to {X}\in ℚ$
70 45 adantr ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\wedge {n}\in ℤ\right)\to {Y}\in ℚ$
71 frmx ${⊢}{X}_{\mathrm{rm}}:{ℤ}_{\ge 2}×ℤ⟶{ℕ}_{0}$
72 71 a1i ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\wedge {n}\in ℤ\right)\to {X}_{\mathrm{rm}}:{ℤ}_{\ge 2}×ℤ⟶{ℕ}_{0}$
73 simpl1 ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\wedge {n}\in ℤ\right)\to {A}\in {ℤ}_{\ge 2}$
74 simpr ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\wedge {n}\in ℤ\right)\to {n}\in ℤ$
75 72 73 74 fovrnd ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\wedge {n}\in ℤ\right)\to {A}{X}_{\mathrm{rm}}{n}\in {ℕ}_{0}$
76 40 75 sseldi ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\wedge {n}\in ℤ\right)\to {A}{X}_{\mathrm{rm}}{n}\in ℚ$
77 zssq ${⊢}ℤ\subseteq ℚ$
78 frmy ${⊢}{Y}_{\mathrm{rm}}:{ℤ}_{\ge 2}×ℤ⟶ℤ$
79 78 a1i ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\wedge {n}\in ℤ\right)\to {Y}_{\mathrm{rm}}:{ℤ}_{\ge 2}×ℤ⟶ℤ$
80 79 73 74 fovrnd ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\wedge {n}\in ℤ\right)\to {A}{Y}_{\mathrm{rm}}{n}\in ℤ$
81 77 80 sseldi ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\wedge {n}\in ℤ\right)\to {A}{Y}_{\mathrm{rm}}{n}\in ℚ$
82 qirropth ${⊢}\left(\sqrt{{{A}}^{2}-1}\in \left(ℂ\setminus ℚ\right)\wedge \left({X}\in ℚ\wedge {Y}\in ℚ\right)\wedge \left({A}{X}_{\mathrm{rm}}{n}\in ℚ\wedge {A}{Y}_{\mathrm{rm}}{n}\in ℚ\right)\right)\to \left({X}+\sqrt{{{A}}^{2}-1}{Y}=\left({A}{X}_{\mathrm{rm}}{n}\right)+\sqrt{{{A}}^{2}-1}\left({A}{Y}_{\mathrm{rm}}{n}\right)↔\left({X}={A}{X}_{\mathrm{rm}}{n}\wedge {Y}={A}{Y}_{\mathrm{rm}}{n}\right)\right)$
83 68 69 70 76 81 82 syl122anc ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\wedge {n}\in ℤ\right)\to \left({X}+\sqrt{{{A}}^{2}-1}{Y}=\left({A}{X}_{\mathrm{rm}}{n}\right)+\sqrt{{{A}}^{2}-1}\left({A}{Y}_{\mathrm{rm}}{n}\right)↔\left({X}={A}{X}_{\mathrm{rm}}{n}\wedge {Y}={A}{Y}_{\mathrm{rm}}{n}\right)\right)$
84 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}}$
85 84 3ad2antl1 ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\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}}$
86 rmspecfund ${⊢}{A}\in {ℤ}_{\ge 2}\to \mathrm{PellFund}\left({{A}}^{2}-1\right)={A}+\sqrt{{{A}}^{2}-1}$
87 86 3ad2ant1 ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\to \mathrm{PellFund}\left({{A}}^{2}-1\right)={A}+\sqrt{{{A}}^{2}-1}$
88 87 adantr ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\wedge {n}\in ℤ\right)\to \mathrm{PellFund}\left({{A}}^{2}-1\right)={A}+\sqrt{{{A}}^{2}-1}$
89 88 oveq1d ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\wedge {n}\in ℤ\right)\to {\mathrm{PellFund}\left({{A}}^{2}-1\right)}^{{n}}={\left({A}+\sqrt{{{A}}^{2}-1}\right)}^{{n}}$
90 85 89 eqtr4d ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\wedge {n}\in ℤ\right)\to \left({A}{X}_{\mathrm{rm}}{n}\right)+\sqrt{{{A}}^{2}-1}\left({A}{Y}_{\mathrm{rm}}{n}\right)={\mathrm{PellFund}\left({{A}}^{2}-1\right)}^{{n}}$
91 90 eqeq2d ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\wedge {n}\in ℤ\right)\to \left({X}+\sqrt{{{A}}^{2}-1}{Y}=\left({A}{X}_{\mathrm{rm}}{n}\right)+\sqrt{{{A}}^{2}-1}\left({A}{Y}_{\mathrm{rm}}{n}\right)↔{X}+\sqrt{{{A}}^{2}-1}{Y}={\mathrm{PellFund}\left({{A}}^{2}-1\right)}^{{n}}\right)$
92 83 91 bitr3d ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\wedge {n}\in ℤ\right)\to \left(\left({X}={A}{X}_{\mathrm{rm}}{n}\wedge {Y}={A}{Y}_{\mathrm{rm}}{n}\right)↔{X}+\sqrt{{{A}}^{2}-1}{Y}={\mathrm{PellFund}\left({{A}}^{2}-1\right)}^{{n}}\right)$
93 92 rexbidva ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\to \left(\exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}\left({X}={A}{X}_{\mathrm{rm}}{n}\wedge {Y}={A}{Y}_{\mathrm{rm}}{n}\right)↔\exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}{X}+\sqrt{{{A}}^{2}-1}{Y}={\mathrm{PellFund}\left({{A}}^{2}-1\right)}^{{n}}\right)$
94 4 67 93 3bitr4d ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {X}\in {ℕ}_{0}\wedge {Y}\in ℤ\right)\to \left({{X}}^{2}-\left({{A}}^{2}-1\right){{Y}}^{2}=1↔\exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}\left({X}={A}{X}_{\mathrm{rm}}{n}\wedge {Y}={A}{Y}_{\mathrm{rm}}{n}\right)\right)$