Metamath Proof Explorer


Theorem pell1234qrre

Description: General Pell solutions are (coded as) real numbers. (Contributed by Stefan O'Rear, 17-Sep-2014)

Ref Expression
Assertion pell1234qrre D A Pell1234QR D A

Proof

Step Hyp Ref Expression
1 elpell1234qr D A Pell1234QR D A a b A = a + D b a 2 D b 2 = 1
2 1 simprbda D A Pell1234QR D A