Theorem pellfundne1

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

	Ref	Expression
Assertion	pellfundne1	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( PellFund ‘ 𝐷 ) ≠ 1 )

Proof

Step	Hyp	Ref	Expression
1		1red	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 1 ∈ ℝ )
2		pellfundgt1	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 1 < ( PellFund ‘ 𝐷 ) )
3	1 2	gtned	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( PellFund ‘ 𝐷 ) ≠ 1 )