Metamath Proof Explorer


Theorem elpell14qr

Description: Membership in the set of positive Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014)

Ref Expression
Assertion elpell14qr D A Pell14QR D A z 0 w A = z + D w z 2 D w 2 = 1

Proof

Step Hyp Ref Expression
1 pell14qrval D Pell14QR D = a | z 0 w a = z + D w z 2 D w 2 = 1
2 1 eleq2d D A Pell14QR D A a | z 0 w a = z + D w z 2 D w 2 = 1
3 eqeq1 a = A a = z + D w A = z + D w
4 3 anbi1d a = A a = z + D w z 2 D w 2 = 1 A = z + D w z 2 D w 2 = 1
5 4 2rexbidv a = A z 0 w a = z + D w z 2 D w 2 = 1 z 0 w A = z + D w z 2 D w 2 = 1
6 5 elrab A a | z 0 w a = z + D w z 2 D w 2 = 1 A z 0 w A = z + D w z 2 D w 2 = 1
7 2 6 bitrdi D A Pell14QR D A z 0 w A = z + D w z 2 D w 2 = 1