Metamath Proof Explorer

Theorem pell14qrre

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

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

Proof

Step Hyp Ref Expression
1 pell14qrss1234 
 |-  ( D e. ( NN \ []NN ) -> ( Pell14QR ` D ) C_ ( Pell1234QR ` D ) )
2 1 sselda 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> A e. ( Pell1234QR ` D ) )
3 pell1234qrre 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) -> A e. RR )
4 2 3 syldan 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> A e. RR )