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 {\mathbb{Z}}_{\ge 2}\to \mathrm{PellFund}\left(A^2-1\right)=A+\sqrt{A^2-1}$$

Proof

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