Metamath Proof Explorer


Theorem elpell1qr

Description: Membership in a first-quadrant Pell solution set. (Contributed by Stefan O'Rear, 17-Sep-2014)

Ref Expression
Assertion elpell1qr D A Pell1QR D A z 0 w 0 A = z + D w z 2 D w 2 = 1

Proof

Step Hyp Ref Expression
1 pell1qrval D Pell1QR D = a | z 0 w 0 a = z + D w z 2 D w 2 = 1
2 1 eleq2d D A Pell1QR D A a | z 0 w 0 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 0 a = z + D w z 2 D w 2 = 1 z 0 w 0 A = z + D w z 2 D w 2 = 1
6 5 elrab A a | z 0 w 0 a = z + D w z 2 D w 2 = 1 A z 0 w 0 A = z + D w z 2 D w 2 = 1
7 2 6 bitrdi D A Pell1QR D A z 0 w 0 A = z + D w z 2 D w 2 = 1