Theorem pellfundne1

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

	Ref	Expression
Assertion	pellfundne1	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \mathrm{PellFund}\left(D\right)\ne 1$$

Proof

Step	Hyp	Ref	Expression
1		1red	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to 1\in ℝ$$
2		pellfundgt1	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to 1<\mathrm{PellFund}\left(D\right)$$
3	1 2	gtned	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \mathrm{PellFund}\left(D\right)\ne 1$$