Theorem pellfundrp

Description: The fundamental Pell solution is a positive real. (Contributed by Stefan O'Rear, 19-Sep-2014)

	Ref	Expression
Assertion	pellfundrp	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \mathrm{PellFund}\left(D\right)\in {ℝ}^{+}$$

Proof

Step	Hyp	Ref	Expression
1		pellfundre	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \mathrm{PellFund}\left(D\right)\in ℝ$$
2		0red	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to 0\in ℝ$$
3		1red	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to 1\in ℝ$$
4		0lt1	$$⊢0<1$$
5	4	a1i	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to 0<1$$
6		pellfundgt1	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to 1<\mathrm{PellFund}\left(D\right)$$
7	2 3 1 5 6	lttrd	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to 0<\mathrm{PellFund}\left(D\right)$$
8	1 7	elrpd	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \mathrm{PellFund}\left(D\right)\in {ℝ}^{+}$$