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 e. ( NN \ []NN ) -> ( PellFund ` D ) =/= 1 )

Proof

Step Hyp Ref Expression
1 1red 
 |-  ( D e. ( NN \ []NN ) -> 1 e. RR )
2 pellfundgt1 
 |-  ( D e. ( NN \ []NN ) -> 1 < ( PellFund ` D ) )
3 1 2 gtned 
 |-  ( D e. ( NN \ []NN ) -> ( PellFund ` D ) =/= 1 )