Step |
Hyp |
Ref |
Expression |
1 |
|
elpell1qr |
|- ( D e. ( NN \ []NN ) -> ( A e. ( Pell1QR ` D ) <-> ( A e. RR /\ E. a e. NN0 E. b e. NN0 ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) ) ) |
2 |
1
|
adantr |
|- ( ( D e. ( NN \ []NN ) /\ 1 < A ) -> ( A e. ( Pell1QR ` D ) <-> ( A e. RR /\ E. a e. NN0 E. b e. NN0 ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) ) ) |
3 |
|
eldifi |
|- ( D e. ( NN \ []NN ) -> D e. NN ) |
4 |
3
|
ad4antr |
|- ( ( ( ( ( D e. ( NN \ []NN ) /\ 1 < A ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> D e. NN ) |
5 |
|
simplr |
|- ( ( ( ( ( D e. ( NN \ []NN ) /\ 1 < A ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( a e. NN0 /\ b e. NN0 ) ) |
6 |
|
simp-4r |
|- ( ( ( ( ( D e. ( NN \ []NN ) /\ 1 < A ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> 1 < A ) |
7 |
|
simprl |
|- ( ( ( ( ( D e. ( NN \ []NN ) /\ 1 < A ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> A = ( a + ( ( sqrt ` D ) x. b ) ) ) |
8 |
6 7
|
breqtrd |
|- ( ( ( ( ( D e. ( NN \ []NN ) /\ 1 < A ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> 1 < ( a + ( ( sqrt ` D ) x. b ) ) ) |
9 |
|
simprr |
|- ( ( ( ( ( D e. ( NN \ []NN ) /\ 1 < A ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) |
10 |
|
pell1qrgaplem |
|- ( ( ( D e. NN /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( 1 < ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ ( a + ( ( sqrt ` D ) x. b ) ) ) |
11 |
4 5 8 9 10
|
syl22anc |
|- ( ( ( ( ( D e. ( NN \ []NN ) /\ 1 < A ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ ( a + ( ( sqrt ` D ) x. b ) ) ) |
12 |
11 7
|
breqtrrd |
|- ( ( ( ( ( D e. ( NN \ []NN ) /\ 1 < A ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ A ) |
13 |
12
|
ex |
|- ( ( ( ( D e. ( NN \ []NN ) /\ 1 < A ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. NN0 ) ) -> ( ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ A ) ) |
14 |
13
|
rexlimdvva |
|- ( ( ( D e. ( NN \ []NN ) /\ 1 < A ) /\ A e. RR ) -> ( E. a e. NN0 E. b e. NN0 ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ A ) ) |
15 |
14
|
expimpd |
|- ( ( D e. ( NN \ []NN ) /\ 1 < A ) -> ( ( A e. RR /\ E. a e. NN0 E. b e. NN0 ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ A ) ) |
16 |
2 15
|
sylbid |
|- ( ( D e. ( NN \ []NN ) /\ 1 < A ) -> ( A e. ( Pell1QR ` D ) -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ A ) ) |
17 |
16
|
ex |
|- ( D e. ( NN \ []NN ) -> ( 1 < A -> ( A e. ( Pell1QR ` D ) -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ A ) ) ) |
18 |
17
|
com23 |
|- ( D e. ( NN \ []NN ) -> ( A e. ( Pell1QR ` D ) -> ( 1 < A -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ A ) ) ) |
19 |
18
|
3imp |
|- ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1QR ` D ) /\ 1 < A ) -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ A ) |