Step |
Hyp |
Ref |
Expression |
1 |
|
1red |
|- ( D e. ( NN \ []NN ) -> 1 e. RR ) |
2 |
|
1nn0 |
|- 1 e. NN0 |
3 |
2
|
a1i |
|- ( D e. ( NN \ []NN ) -> 1 e. NN0 ) |
4 |
|
0nn0 |
|- 0 e. NN0 |
5 |
4
|
a1i |
|- ( D e. ( NN \ []NN ) -> 0 e. NN0 ) |
6 |
|
eldifi |
|- ( D e. ( NN \ []NN ) -> D e. NN ) |
7 |
6
|
nncnd |
|- ( D e. ( NN \ []NN ) -> D e. CC ) |
8 |
7
|
sqrtcld |
|- ( D e. ( NN \ []NN ) -> ( sqrt ` D ) e. CC ) |
9 |
8
|
mul01d |
|- ( D e. ( NN \ []NN ) -> ( ( sqrt ` D ) x. 0 ) = 0 ) |
10 |
9
|
oveq2d |
|- ( D e. ( NN \ []NN ) -> ( 1 + ( ( sqrt ` D ) x. 0 ) ) = ( 1 + 0 ) ) |
11 |
|
1p0e1 |
|- ( 1 + 0 ) = 1 |
12 |
10 11
|
eqtr2di |
|- ( D e. ( NN \ []NN ) -> 1 = ( 1 + ( ( sqrt ` D ) x. 0 ) ) ) |
13 |
|
sq1 |
|- ( 1 ^ 2 ) = 1 |
14 |
13
|
a1i |
|- ( D e. ( NN \ []NN ) -> ( 1 ^ 2 ) = 1 ) |
15 |
|
sq0 |
|- ( 0 ^ 2 ) = 0 |
16 |
15
|
oveq2i |
|- ( D x. ( 0 ^ 2 ) ) = ( D x. 0 ) |
17 |
7
|
mul01d |
|- ( D e. ( NN \ []NN ) -> ( D x. 0 ) = 0 ) |
18 |
16 17
|
syl5eq |
|- ( D e. ( NN \ []NN ) -> ( D x. ( 0 ^ 2 ) ) = 0 ) |
19 |
14 18
|
oveq12d |
|- ( D e. ( NN \ []NN ) -> ( ( 1 ^ 2 ) - ( D x. ( 0 ^ 2 ) ) ) = ( 1 - 0 ) ) |
20 |
|
1m0e1 |
|- ( 1 - 0 ) = 1 |
21 |
19 20
|
eqtrdi |
|- ( D e. ( NN \ []NN ) -> ( ( 1 ^ 2 ) - ( D x. ( 0 ^ 2 ) ) ) = 1 ) |
22 |
|
oveq1 |
|- ( a = 1 -> ( a + ( ( sqrt ` D ) x. b ) ) = ( 1 + ( ( sqrt ` D ) x. b ) ) ) |
23 |
22
|
eqeq2d |
|- ( a = 1 -> ( 1 = ( a + ( ( sqrt ` D ) x. b ) ) <-> 1 = ( 1 + ( ( sqrt ` D ) x. b ) ) ) ) |
24 |
|
oveq1 |
|- ( a = 1 -> ( a ^ 2 ) = ( 1 ^ 2 ) ) |
25 |
24
|
oveq1d |
|- ( a = 1 -> ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = ( ( 1 ^ 2 ) - ( D x. ( b ^ 2 ) ) ) ) |
26 |
25
|
eqeq1d |
|- ( a = 1 -> ( ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 <-> ( ( 1 ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) |
27 |
23 26
|
anbi12d |
|- ( a = 1 -> ( ( 1 = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) <-> ( 1 = ( 1 + ( ( sqrt ` D ) x. b ) ) /\ ( ( 1 ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) ) |
28 |
|
oveq2 |
|- ( b = 0 -> ( ( sqrt ` D ) x. b ) = ( ( sqrt ` D ) x. 0 ) ) |
29 |
28
|
oveq2d |
|- ( b = 0 -> ( 1 + ( ( sqrt ` D ) x. b ) ) = ( 1 + ( ( sqrt ` D ) x. 0 ) ) ) |
30 |
29
|
eqeq2d |
|- ( b = 0 -> ( 1 = ( 1 + ( ( sqrt ` D ) x. b ) ) <-> 1 = ( 1 + ( ( sqrt ` D ) x. 0 ) ) ) ) |
31 |
|
oveq1 |
|- ( b = 0 -> ( b ^ 2 ) = ( 0 ^ 2 ) ) |
32 |
31
|
oveq2d |
|- ( b = 0 -> ( D x. ( b ^ 2 ) ) = ( D x. ( 0 ^ 2 ) ) ) |
33 |
32
|
oveq2d |
|- ( b = 0 -> ( ( 1 ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = ( ( 1 ^ 2 ) - ( D x. ( 0 ^ 2 ) ) ) ) |
34 |
33
|
eqeq1d |
|- ( b = 0 -> ( ( ( 1 ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 <-> ( ( 1 ^ 2 ) - ( D x. ( 0 ^ 2 ) ) ) = 1 ) ) |
35 |
30 34
|
anbi12d |
|- ( b = 0 -> ( ( 1 = ( 1 + ( ( sqrt ` D ) x. b ) ) /\ ( ( 1 ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) <-> ( 1 = ( 1 + ( ( sqrt ` D ) x. 0 ) ) /\ ( ( 1 ^ 2 ) - ( D x. ( 0 ^ 2 ) ) ) = 1 ) ) ) |
36 |
27 35
|
rspc2ev |
|- ( ( 1 e. NN0 /\ 0 e. NN0 /\ ( 1 = ( 1 + ( ( sqrt ` D ) x. 0 ) ) /\ ( ( 1 ^ 2 ) - ( D x. ( 0 ^ 2 ) ) ) = 1 ) ) -> E. a e. NN0 E. b e. NN0 ( 1 = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) |
37 |
3 5 12 21 36
|
syl112anc |
|- ( D e. ( NN \ []NN ) -> E. a e. NN0 E. b e. NN0 ( 1 = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) |
38 |
|
elpell1qr |
|- ( D e. ( NN \ []NN ) -> ( 1 e. ( Pell1QR ` D ) <-> ( 1 e. RR /\ E. a e. NN0 E. b e. NN0 ( 1 = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) ) ) |
39 |
1 37 38
|
mpbir2and |
|- ( D e. ( NN \ []NN ) -> 1 e. ( Pell1QR ` D ) ) |