# Metamath Proof Explorer

## Theorem rmspecfund

Description: The base of exponent used to define the X and Y sequences is the fundamental solution of the corresponding Pell equation. (Contributed by Stefan O'Rear, 21-Sep-2014)

Ref Expression
Assertion rmspecfund ${⊢}{A}\in {ℤ}_{\ge 2}\to \mathrm{PellFund}\left({{A}}^{2}-1\right)={A}+\sqrt{{{A}}^{2}-1}$

### Proof

Step Hyp Ref Expression
1 rmspecnonsq ${⊢}{A}\in {ℤ}_{\ge 2}\to {{A}}^{2}-1\in \left(ℕ\setminus {◻}_{ℕ}\right)$
2 eluzelz ${⊢}{A}\in {ℤ}_{\ge 2}\to {A}\in ℤ$
3 zsqcl ${⊢}{A}\in ℤ\to {{A}}^{2}\in ℤ$
4 2 3 syl ${⊢}{A}\in {ℤ}_{\ge 2}\to {{A}}^{2}\in ℤ$
5 4 zred ${⊢}{A}\in {ℤ}_{\ge 2}\to {{A}}^{2}\in ℝ$
6 1red ${⊢}{A}\in {ℤ}_{\ge 2}\to 1\in ℝ$
7 5 6 resubcld ${⊢}{A}\in {ℤ}_{\ge 2}\to {{A}}^{2}-1\in ℝ$
8 sq1 ${⊢}{1}^{2}=1$
9 8 a1i ${⊢}{A}\in {ℤ}_{\ge 2}\to {1}^{2}=1$
10 eluz2b2 ${⊢}{A}\in {ℤ}_{\ge 2}↔\left({A}\in ℕ\wedge 1<{A}\right)$
11 10 simprbi ${⊢}{A}\in {ℤ}_{\ge 2}\to 1<{A}$
12 eluzelre ${⊢}{A}\in {ℤ}_{\ge 2}\to {A}\in ℝ$
13 0le1 ${⊢}0\le 1$
14 13 a1i ${⊢}{A}\in {ℤ}_{\ge 2}\to 0\le 1$
15 eluzge2nn0 ${⊢}{A}\in {ℤ}_{\ge 2}\to {A}\in {ℕ}_{0}$
16 15 nn0ge0d ${⊢}{A}\in {ℤ}_{\ge 2}\to 0\le {A}$
17 6 12 14 16 lt2sqd ${⊢}{A}\in {ℤ}_{\ge 2}\to \left(1<{A}↔{1}^{2}<{{A}}^{2}\right)$
18 11 17 mpbid ${⊢}{A}\in {ℤ}_{\ge 2}\to {1}^{2}<{{A}}^{2}$
19 9 18 eqbrtrrd ${⊢}{A}\in {ℤ}_{\ge 2}\to 1<{{A}}^{2}$
20 6 5 posdifd ${⊢}{A}\in {ℤ}_{\ge 2}\to \left(1<{{A}}^{2}↔0<{{A}}^{2}-1\right)$
21 19 20 mpbid ${⊢}{A}\in {ℤ}_{\ge 2}\to 0<{{A}}^{2}-1$
22 7 21 elrpd ${⊢}{A}\in {ℤ}_{\ge 2}\to {{A}}^{2}-1\in {ℝ}^{+}$
23 22 rpsqrtcld ${⊢}{A}\in {ℤ}_{\ge 2}\to \sqrt{{{A}}^{2}-1}\in {ℝ}^{+}$
24 23 rpred ${⊢}{A}\in {ℤ}_{\ge 2}\to \sqrt{{{A}}^{2}-1}\in ℝ$
25 24 recnd ${⊢}{A}\in {ℤ}_{\ge 2}\to \sqrt{{{A}}^{2}-1}\in ℂ$
26 25 mulid1d ${⊢}{A}\in {ℤ}_{\ge 2}\to \sqrt{{{A}}^{2}-1}\cdot 1=\sqrt{{{A}}^{2}-1}$
27 26 oveq2d ${⊢}{A}\in {ℤ}_{\ge 2}\to {A}+\sqrt{{{A}}^{2}-1}\cdot 1={A}+\sqrt{{{A}}^{2}-1}$
28 pell1qrss14 ${⊢}{{A}}^{2}-1\in \left(ℕ\setminus {◻}_{ℕ}\right)\to \mathrm{Pell1QR}\left({{A}}^{2}-1\right)\subseteq \mathrm{Pell14QR}\left({{A}}^{2}-1\right)$
29 1 28 syl ${⊢}{A}\in {ℤ}_{\ge 2}\to \mathrm{Pell1QR}\left({{A}}^{2}-1\right)\subseteq \mathrm{Pell14QR}\left({{A}}^{2}-1\right)$
30 1nn0 ${⊢}1\in {ℕ}_{0}$
31 30 a1i ${⊢}{A}\in {ℤ}_{\ge 2}\to 1\in {ℕ}_{0}$
32 8 oveq2i ${⊢}\left({{A}}^{2}-1\right){1}^{2}=\left({{A}}^{2}-1\right)\cdot 1$
33 7 recnd ${⊢}{A}\in {ℤ}_{\ge 2}\to {{A}}^{2}-1\in ℂ$
34 33 mulid1d ${⊢}{A}\in {ℤ}_{\ge 2}\to \left({{A}}^{2}-1\right)\cdot 1={{A}}^{2}-1$
35 32 34 syl5eq ${⊢}{A}\in {ℤ}_{\ge 2}\to \left({{A}}^{2}-1\right){1}^{2}={{A}}^{2}-1$
36 35 oveq2d ${⊢}{A}\in {ℤ}_{\ge 2}\to {{A}}^{2}-\left({{A}}^{2}-1\right){1}^{2}={{A}}^{2}-\left({{A}}^{2}-1\right)$
37 5 recnd ${⊢}{A}\in {ℤ}_{\ge 2}\to {{A}}^{2}\in ℂ$
38 1cnd ${⊢}{A}\in {ℤ}_{\ge 2}\to 1\in ℂ$
39 37 38 nncand ${⊢}{A}\in {ℤ}_{\ge 2}\to {{A}}^{2}-\left({{A}}^{2}-1\right)=1$
40 36 39 eqtrd ${⊢}{A}\in {ℤ}_{\ge 2}\to {{A}}^{2}-\left({{A}}^{2}-1\right){1}^{2}=1$
41 pellqrexplicit ${⊢}\left(\left({{A}}^{2}-1\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in {ℕ}_{0}\wedge 1\in {ℕ}_{0}\right)\wedge {{A}}^{2}-\left({{A}}^{2}-1\right){1}^{2}=1\right)\to {A}+\sqrt{{{A}}^{2}-1}\cdot 1\in \mathrm{Pell1QR}\left({{A}}^{2}-1\right)$
42 1 15 31 40 41 syl31anc ${⊢}{A}\in {ℤ}_{\ge 2}\to {A}+\sqrt{{{A}}^{2}-1}\cdot 1\in \mathrm{Pell1QR}\left({{A}}^{2}-1\right)$
43 29 42 sseldd ${⊢}{A}\in {ℤ}_{\ge 2}\to {A}+\sqrt{{{A}}^{2}-1}\cdot 1\in \mathrm{Pell14QR}\left({{A}}^{2}-1\right)$
44 27 43 eqeltrrd ${⊢}{A}\in {ℤ}_{\ge 2}\to {A}+\sqrt{{{A}}^{2}-1}\in \mathrm{Pell14QR}\left({{A}}^{2}-1\right)$
45 6 24 readdcld ${⊢}{A}\in {ℤ}_{\ge 2}\to 1+\sqrt{{{A}}^{2}-1}\in ℝ$
46 12 24 readdcld ${⊢}{A}\in {ℤ}_{\ge 2}\to {A}+\sqrt{{{A}}^{2}-1}\in ℝ$
47 6 23 ltaddrpd ${⊢}{A}\in {ℤ}_{\ge 2}\to 1<1+\sqrt{{{A}}^{2}-1}$
48 6 12 24 11 ltadd1dd ${⊢}{A}\in {ℤ}_{\ge 2}\to 1+\sqrt{{{A}}^{2}-1}<{A}+\sqrt{{{A}}^{2}-1}$
49 6 45 46 47 48 lttrd ${⊢}{A}\in {ℤ}_{\ge 2}\to 1<{A}+\sqrt{{{A}}^{2}-1}$
50 pellfundlb ${⊢}\left({{A}}^{2}-1\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}+\sqrt{{{A}}^{2}-1}\in \mathrm{Pell14QR}\left({{A}}^{2}-1\right)\wedge 1<{A}+\sqrt{{{A}}^{2}-1}\right)\to \mathrm{PellFund}\left({{A}}^{2}-1\right)\le {A}+\sqrt{{{A}}^{2}-1}$
51 1 44 49 50 syl3anc ${⊢}{A}\in {ℤ}_{\ge 2}\to \mathrm{PellFund}\left({{A}}^{2}-1\right)\le {A}+\sqrt{{{A}}^{2}-1}$
52 37 38 npcand ${⊢}{A}\in {ℤ}_{\ge 2}\to {{A}}^{2}-1+1={{A}}^{2}$
53 52 fveq2d ${⊢}{A}\in {ℤ}_{\ge 2}\to \sqrt{{{A}}^{2}-1+1}=\sqrt{{{A}}^{2}}$
54 12 16 sqrtsqd ${⊢}{A}\in {ℤ}_{\ge 2}\to \sqrt{{{A}}^{2}}={A}$
55 53 54 eqtrd ${⊢}{A}\in {ℤ}_{\ge 2}\to \sqrt{{{A}}^{2}-1+1}={A}$
56 55 oveq1d ${⊢}{A}\in {ℤ}_{\ge 2}\to \sqrt{{{A}}^{2}-1+1}+\sqrt{{{A}}^{2}-1}={A}+\sqrt{{{A}}^{2}-1}$
57 pellfundge ${⊢}{{A}}^{2}-1\in \left(ℕ\setminus {◻}_{ℕ}\right)\to \sqrt{{{A}}^{2}-1+1}+\sqrt{{{A}}^{2}-1}\le \mathrm{PellFund}\left({{A}}^{2}-1\right)$
58 1 57 syl ${⊢}{A}\in {ℤ}_{\ge 2}\to \sqrt{{{A}}^{2}-1+1}+\sqrt{{{A}}^{2}-1}\le \mathrm{PellFund}\left({{A}}^{2}-1\right)$
59 56 58 eqbrtrrd ${⊢}{A}\in {ℤ}_{\ge 2}\to {A}+\sqrt{{{A}}^{2}-1}\le \mathrm{PellFund}\left({{A}}^{2}-1\right)$
60 pellfundre ${⊢}{{A}}^{2}-1\in \left(ℕ\setminus {◻}_{ℕ}\right)\to \mathrm{PellFund}\left({{A}}^{2}-1\right)\in ℝ$
61 1 60 syl ${⊢}{A}\in {ℤ}_{\ge 2}\to \mathrm{PellFund}\left({{A}}^{2}-1\right)\in ℝ$
62 61 46 letri3d ${⊢}{A}\in {ℤ}_{\ge 2}\to \left(\mathrm{PellFund}\left({{A}}^{2}-1\right)={A}+\sqrt{{{A}}^{2}-1}↔\left(\mathrm{PellFund}\left({{A}}^{2}-1\right)\le {A}+\sqrt{{{A}}^{2}-1}\wedge {A}+\sqrt{{{A}}^{2}-1}\le \mathrm{PellFund}\left({{A}}^{2}-1\right)\right)\right)$
63 51 59 62 mpbir2and ${⊢}{A}\in {ℤ}_{\ge 2}\to \mathrm{PellFund}\left({{A}}^{2}-1\right)={A}+\sqrt{{{A}}^{2}-1}$