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 A Pell14QR D A +

Proof

Step Hyp Ref Expression
1 pell14qrre D A Pell14QR D A
2 pell14qrgt0 D A Pell14QR D 0 < A
3 1 2 elrpd D A Pell14QR D A +