Metamath Proof Explorer


Theorem pellfundne1

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

Ref Expression
Assertion pellfundne1 D PellFund D 1

Proof

Step Hyp Ref Expression
1 1red D 1
2 pellfundgt1 D 1 < PellFund D
3 1 2 gtned D PellFund D 1