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 e. ( NN \ []NN ) -> ( A e. ( Pell1QR ` D ) <-> ( A e. RR /\ E. z e. NN0 E. w e. NN0 ( A = ( z + ( ( sqrt ` D ) x. w ) ) /\ ( ( z ^ 2 ) - ( D x. ( w ^ 2 ) ) ) = 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 pell1qrval 
 |-  ( D e. ( NN \ []NN ) -> ( Pell1QR ` D ) = { a e. RR | E. z e. NN0 E. w e. NN0 ( a = ( z + ( ( sqrt ` D ) x. w ) ) /\ ( ( z ^ 2 ) - ( D x. ( w ^ 2 ) ) ) = 1 ) } )
2 1 eleq2d 
 |-  ( D e. ( NN \ []NN ) -> ( A e. ( Pell1QR ` D ) <-> A e. { a e. RR | E. z e. NN0 E. w e. NN0 ( a = ( z + ( ( sqrt ` D ) x. w ) ) /\ ( ( z ^ 2 ) - ( D x. ( w ^ 2 ) ) ) = 1 ) } ) )
3 eqeq1 
 |-  ( a = A -> ( a = ( z + ( ( sqrt ` D ) x. w ) ) <-> A = ( z + ( ( sqrt ` D ) x. w ) ) ) )
4 3 anbi1d 
 |-  ( a = A -> ( ( a = ( z + ( ( sqrt ` D ) x. w ) ) /\ ( ( z ^ 2 ) - ( D x. ( w ^ 2 ) ) ) = 1 ) <-> ( A = ( z + ( ( sqrt ` D ) x. w ) ) /\ ( ( z ^ 2 ) - ( D x. ( w ^ 2 ) ) ) = 1 ) ) )
5 4 2rexbidv 
 |-  ( a = A -> ( E. z e. NN0 E. w e. NN0 ( a = ( z + ( ( sqrt ` D ) x. w ) ) /\ ( ( z ^ 2 ) - ( D x. ( w ^ 2 ) ) ) = 1 ) <-> E. z e. NN0 E. w e. NN0 ( A = ( z + ( ( sqrt ` D ) x. w ) ) /\ ( ( z ^ 2 ) - ( D x. ( w ^ 2 ) ) ) = 1 ) ) )
6 5 elrab 
 |-  ( A e. { a e. RR | E. z e. NN0 E. w e. NN0 ( a = ( z + ( ( sqrt ` D ) x. w ) ) /\ ( ( z ^ 2 ) - ( D x. ( w ^ 2 ) ) ) = 1 ) } <-> ( A e. RR /\ E. z e. NN0 E. w e. NN0 ( A = ( z + ( ( sqrt ` D ) x. w ) ) /\ ( ( z ^ 2 ) - ( D x. ( w ^ 2 ) ) ) = 1 ) ) )
7 2 6 bitrdi 
 |-  ( D e. ( NN \ []NN ) -> ( A e. ( Pell1QR ` D ) <-> ( A e. RR /\ E. z e. NN0 E. w e. NN0 ( A = ( z + ( ( sqrt ` D ) x. w ) ) /\ ( ( z ^ 2 ) - ( D x. ( w ^ 2 ) ) ) = 1 ) ) ) )