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