# Metamath Proof Explorer

## Theorem pell14qrval

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

Ref Expression
Assertion pell14qrval
`|- ( D e. ( NN \ []NN ) -> ( Pell14QR ` D ) = { y e. RR | E. z e. NN0 E. w e. ZZ ( 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. ZZ ( y = ( z + ( ( sqrt ` a ) x. w ) ) /\ ( ( z ^ 2 ) - ( a x. ( w ^ 2 ) ) ) = 1 ) <-> E. z e. NN0 E. w e. ZZ ( 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. ZZ ( y = ( z + ( ( sqrt ` a ) x. w ) ) /\ ( ( z ^ 2 ) - ( a x. ( w ^ 2 ) ) ) = 1 ) } = { y e. RR | E. z e. NN0 E. w e. ZZ ( y = ( z + ( ( sqrt ` D ) x. w ) ) /\ ( ( z ^ 2 ) - ( D x. ( w ^ 2 ) ) ) = 1 ) } )`
11 df-pell14qr
` |-  Pell14QR = ( a e. ( NN \ []NN ) |-> { y e. RR | E. z e. NN0 E. w e. ZZ ( 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. ZZ ( y = ( z + ( ( sqrt ` D ) x. w ) ) /\ ( ( z ^ 2 ) - ( D x. ( w ^ 2 ) ) ) = 1 ) } e. _V`
14 10 11 13 fvmpt
` |-  ( D e. ( NN \ []NN ) -> ( Pell14QR ` D ) = { y e. RR | E. z e. NN0 E. w e. ZZ ( y = ( z + ( ( sqrt ` D ) x. w ) ) /\ ( ( z ^ 2 ) - ( D x. ( w ^ 2 ) ) ) = 1 ) } )`