Metamath Proof Explorer

Theorem pellfundrp

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

Ref Expression
Assertion pellfundrp 
|- ( D e. ( NN \ []NN ) -> ( PellFund ` D ) e. RR+ )

Proof

Step Hyp Ref Expression
1 pellfundre 
 |-  ( D e. ( NN \ []NN ) -> ( PellFund ` D ) e. RR )
2 0red 
 |-  ( D e. ( NN \ []NN ) -> 0 e. RR )
3 1red 
 |-  ( D e. ( NN \ []NN ) -> 1 e. RR )
4 0lt1 
 |-  0 < 1
5 4 a1i 
 |-  ( D e. ( NN \ []NN ) -> 0 < 1 )
6 pellfundgt1 
 |-  ( D e. ( NN \ []NN ) -> 1 < ( PellFund ` D ) )
7 2 3 1 5 6 lttrd 
 |-  ( D e. ( NN \ []NN ) -> 0 < ( PellFund ` D ) )
8 1 7 elrpd 
 |-  ( D e. ( NN \ []NN ) -> ( PellFund ` D ) e. RR+ )