Metamath Proof Explorer

Theorem pell14qrrp

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

Ref Expression
Assertion pell14qrrp 
|- ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> A e. RR+ )

Proof

Step Hyp Ref Expression
1 pell14qrre 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> A e. RR )
2 pell14qrgt0 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> 0 < A )
3 1 2 elrpd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> A e. RR+ )