Theorem pellfundge

Description: Lower bound on the fundamental solution of a Pell equation. (Contributed by Stefan O'Rear, 19-Sep-2014)

	Ref	Expression
Assertion	pellfundge	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \sqrt{D+1}+\sqrt{D}\le \mathrm{PellFund}\left(D\right)$$

Proof

Step	Hyp	Ref	Expression
1		ssrab2	$$⊢\left\{a\in \mathrm{Pell14QR}\left(D\right)|1<a\right\}\subseteq \mathrm{Pell14QR}\left(D\right)$$
2		pell14qrre	$$⊢\left(D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\wedge a\in \mathrm{Pell14QR}\left(D\right)\right)\to a\in ℝ$$
3	2	ex	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \left(a\in \mathrm{Pell14QR}\left(D\right)\to a\in ℝ\right)$$
4	3	ssrdv	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \mathrm{Pell14QR}\left(D\right)\subseteq ℝ$$
5	1 4	sstrid	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \left\{a\in \mathrm{Pell14QR}\left(D\right)|1<a\right\}\subseteq ℝ$$
6		pell1qrss14	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \mathrm{Pell1QR}\left(D\right)\subseteq \mathrm{Pell14QR}\left(D\right)$$
7		pellqrex	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \exists a\in \mathrm{Pell1QR}\left(D\right)1<a$$
8		ssrexv	$$⊢\mathrm{Pell1QR}\left(D\right)\subseteq \mathrm{Pell14QR}\left(D\right)\to \left(\exists a\in \mathrm{Pell1QR}\left(D\right)1<a\to \exists a\in \mathrm{Pell14QR}\left(D\right)1<a\right)$$
9	6 7 8	sylc	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \exists a\in \mathrm{Pell14QR}\left(D\right)1<a$$
10		rabn0	$$⊢\left\{a\in \mathrm{Pell14QR}\left(D\right)|1<a\right\}\ne \varnothing \leftrightarrow \exists a\in \mathrm{Pell14QR}\left(D\right)1<a$$
11	9 10	sylibr	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \left\{a\in \mathrm{Pell14QR}\left(D\right)|1<a\right\}\ne \varnothing$$
12		eldifi	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to D\in \mathbb{N}$$
13	12	peano2nnd	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to D+1\in \mathbb{N}$$
14	13	nnrpd	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to D+1\in {ℝ}^{+}$$
15	14	rpsqrtcld	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \sqrt{D+1}\in {ℝ}^{+}$$
16	15	rpred	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \sqrt{D+1}\in ℝ$$
17	12	nnrpd	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to D\in {ℝ}^{+}$$
18	17	rpsqrtcld	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \sqrt{D}\in {ℝ}^{+}$$
19	18	rpred	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \sqrt{D}\in ℝ$$
20	16 19	readdcld	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \sqrt{D+1}+\sqrt{D}\in ℝ$$
21		breq2	$$⊢a=b\to \left(1<a\leftrightarrow 1<b\right)$$
22	21	elrab	$$⊢b\in \left\{a\in \mathrm{Pell14QR}\left(D\right)|1<a\right\}\leftrightarrow \left(b\in \mathrm{Pell14QR}\left(D\right)\wedge 1<b\right)$$
23		pell14qrgap	$$⊢\left(D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\wedge b\in \mathrm{Pell14QR}\left(D\right)\wedge 1<b\right)\to \sqrt{D+1}+\sqrt{D}\le b$$
24	23	3expib	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \left(\left(b\in \mathrm{Pell14QR}\left(D\right)\wedge 1<b\right)\to \sqrt{D+1}+\sqrt{D}\le b\right)$$
25	22 24	biimtrid	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \left(b\in \left\{a\in \mathrm{Pell14QR}\left(D\right)|1<a\right\}\to \sqrt{D+1}+\sqrt{D}\le b\right)$$
26	25	ralrimiv	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \forall b\in \left\{a\in \mathrm{Pell14QR}\left(D\right)|1<a\right\}\sqrt{D+1}+\sqrt{D}\le b$$
27		infmrgelbi	$$⊢\left(\left(\left\{a\in \mathrm{Pell14QR}\left(D\right)|1<a\right\}\subseteq ℝ\wedge \left\{a\in \mathrm{Pell14QR}\left(D\right)|1<a\right\}\ne \varnothing \wedge \sqrt{D+1}+\sqrt{D}\in ℝ\right)\wedge \forall b\in \left\{a\in \mathrm{Pell14QR}\left(D\right)|1<a\right\}\sqrt{D+1}+\sqrt{D}\le b\right)\to \sqrt{D+1}+\sqrt{D}\le inf\left(\left\{a\in \mathrm{Pell14QR}\left(D\right)|1<a\right\},ℝ,<\right)$$
28	5 11 20 26 27	syl31anc	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \sqrt{D+1}+\sqrt{D}\le inf\left(\left\{a\in \mathrm{Pell14QR}\left(D\right)|1<a\right\},ℝ,<\right)$$
29		pellfundval	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \mathrm{PellFund}\left(D\right)=inf\left(\left\{a\in \mathrm{Pell14QR}\left(D\right)|1<a\right\},ℝ,<\right)$$
30	28 29	breqtrrd	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \sqrt{D+1}+\sqrt{D}\le \mathrm{PellFund}\left(D\right)$$