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 DAPell1QRDAz0w0A=z+Dwz2Dw2=1

Proof

Step Hyp Ref Expression
1 pell1qrval DPell1QRD=a|z0w0a=z+Dwz2Dw2=1
2 1 eleq2d DAPell1QRDAa|z0w0a=z+Dwz2Dw2=1
3 eqeq1 a=Aa=z+DwA=z+Dw
4 3 anbi1d a=Aa=z+Dwz2Dw2=1A=z+Dwz2Dw2=1
5 4 2rexbidv a=Az0w0a=z+Dwz2Dw2=1z0w0A=z+Dwz2Dw2=1
6 5 elrab Aa|z0w0a=z+Dwz2Dw2=1Az0w0A=z+Dwz2Dw2=1
7 2 6 bitrdi DAPell1QRDAz0w0A=z+Dwz2Dw2=1