Metamath Proof Explorer

Theorem pell1qrval

Description: Value of the set of first-quadrant Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014)

Ref Expression
Assertion pell1qrval 
|- ( D e. ( NN \ []NN ) -> ( Pell1QR ` D ) = { y e. RR | E. z e. NN0 E. w e. NN0 ( y = ( z + ( ( sqrt ` D ) x. w ) ) /\ ( ( z ^ 2 ) - ( D x. ( w ^ 2 ) ) ) = 1 ) } )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( a = D -> ( sqrt ` a ) = ( sqrt ` D ) )
2 1 oveq1d 
 |-  ( a = D -> ( ( sqrt ` a ) x. w ) = ( ( sqrt ` D ) x. w ) )
3 2 oveq2d 
 |-  ( a = D -> ( z + ( ( sqrt ` a ) x. w ) ) = ( z + ( ( sqrt ` D ) x. w ) ) )
4 3 eqeq2d 
 |-  ( a = D -> ( y = ( z + ( ( sqrt ` a ) x. w ) ) <-> y = ( z + ( ( sqrt ` D ) x. w ) ) ) )
5 oveq1 
 |-  ( a = D -> ( a x. ( w ^ 2 ) ) = ( D x. ( w ^ 2 ) ) )
6 5 oveq2d 
 |-  ( a = D -> ( ( z ^ 2 ) - ( a x. ( w ^ 2 ) ) ) = ( ( z ^ 2 ) - ( D x. ( w ^ 2 ) ) ) )
7 6 eqeq1d 
 |-  ( a = D -> ( ( ( z ^ 2 ) - ( a x. ( w ^ 2 ) ) ) = 1 <-> ( ( z ^ 2 ) - ( D x. ( w ^ 2 ) ) ) = 1 ) )
8 4 7 anbi12d 
 |-  ( a = D -> ( ( y = ( z + ( ( sqrt ` a ) x. w ) ) /\ ( ( z ^ 2 ) - ( a x. ( w ^ 2 ) ) ) = 1 ) <-> ( y = ( z + ( ( sqrt ` D ) x. w ) ) /\ ( ( z ^ 2 ) - ( D x. ( w ^ 2 ) ) ) = 1 ) ) )
9 8 2rexbidv 
 |-  ( a = D -> ( E. z e. NN0 E. w e. NN0 ( y = ( z + ( ( sqrt ` a ) x. w ) ) /\ ( ( z ^ 2 ) - ( a x. ( w ^ 2 ) ) ) = 1 ) <-> E. z e. NN0 E. w e. NN0 ( y = ( z + ( ( sqrt ` D ) x. w ) ) /\ ( ( z ^ 2 ) - ( D x. ( w ^ 2 ) ) ) = 1 ) ) )
10 9 rabbidv 
 |-  ( a = D -> { y e. RR | E. z e. NN0 E. w e. NN0 ( y = ( z + ( ( sqrt ` a ) x. w ) ) /\ ( ( z ^ 2 ) - ( a x. ( w ^ 2 ) ) ) = 1 ) } = { y e. RR | E. z e. NN0 E. w e. NN0 ( y = ( z + ( ( sqrt ` D ) x. w ) ) /\ ( ( z ^ 2 ) - ( D x. ( w ^ 2 ) ) ) = 1 ) } )
11 df-pell1qr 
 |-  Pell1QR = ( a e. ( NN \ []NN ) |-> { y e. RR | E. z e. NN0 E. w e. NN0 ( y = ( z + ( ( sqrt ` a ) x. w ) ) /\ ( ( z ^ 2 ) - ( a x. ( w ^ 2 ) ) ) = 1 ) } )
12 reex 
 |-  RR e. _V
13 12 rabex 
 |-  { y e. RR | E. z e. NN0 E. w e. NN0 ( y = ( z + ( ( sqrt ` D ) x. w ) ) /\ ( ( z ^ 2 ) - ( D x. ( w ^ 2 ) ) ) = 1 ) } e. _V
14 10 11 13 fvmpt 
 |-  ( D e. ( NN \ []NN ) -> ( Pell1QR ` D ) = { y e. RR | E. z e. NN0 E. w e. NN0 ( y = ( z + ( ( sqrt ` D ) x. w ) ) /\ ( ( z ^ 2 ) - ( D x. ( w ^ 2 ) ) ) = 1 ) } )