Step |
Hyp |
Ref |
Expression |
1 |
|
ssrab2 |
|- { a e. ( Pell14QR ` D ) | 1 < a } C_ ( Pell14QR ` D ) |
2 |
|
pell14qrre |
|- ( ( D e. ( NN \ []NN ) /\ a e. ( Pell14QR ` D ) ) -> a e. RR ) |
3 |
2
|
ex |
|- ( D e. ( NN \ []NN ) -> ( a e. ( Pell14QR ` D ) -> a e. RR ) ) |
4 |
3
|
ssrdv |
|- ( D e. ( NN \ []NN ) -> ( Pell14QR ` D ) C_ RR ) |
5 |
1 4
|
sstrid |
|- ( D e. ( NN \ []NN ) -> { a e. ( Pell14QR ` D ) | 1 < a } C_ RR ) |
6 |
|
pell1qrss14 |
|- ( D e. ( NN \ []NN ) -> ( Pell1QR ` D ) C_ ( Pell14QR ` D ) ) |
7 |
|
pellqrex |
|- ( D e. ( NN \ []NN ) -> E. a e. ( Pell1QR ` D ) 1 < a ) |
8 |
|
ssrexv |
|- ( ( Pell1QR ` D ) C_ ( Pell14QR ` D ) -> ( E. a e. ( Pell1QR ` D ) 1 < a -> E. a e. ( Pell14QR ` D ) 1 < a ) ) |
9 |
6 7 8
|
sylc |
|- ( D e. ( NN \ []NN ) -> E. a e. ( Pell14QR ` D ) 1 < a ) |
10 |
|
rabn0 |
|- ( { a e. ( Pell14QR ` D ) | 1 < a } =/= (/) <-> E. a e. ( Pell14QR ` D ) 1 < a ) |
11 |
9 10
|
sylibr |
|- ( D e. ( NN \ []NN ) -> { a e. ( Pell14QR ` D ) | 1 < a } =/= (/) ) |
12 |
|
eldifi |
|- ( D e. ( NN \ []NN ) -> D e. NN ) |
13 |
12
|
peano2nnd |
|- ( D e. ( NN \ []NN ) -> ( D + 1 ) e. NN ) |
14 |
13
|
nnrpd |
|- ( D e. ( NN \ []NN ) -> ( D + 1 ) e. RR+ ) |
15 |
14
|
rpsqrtcld |
|- ( D e. ( NN \ []NN ) -> ( sqrt ` ( D + 1 ) ) e. RR+ ) |
16 |
15
|
rpred |
|- ( D e. ( NN \ []NN ) -> ( sqrt ` ( D + 1 ) ) e. RR ) |
17 |
12
|
nnrpd |
|- ( D e. ( NN \ []NN ) -> D e. RR+ ) |
18 |
17
|
rpsqrtcld |
|- ( D e. ( NN \ []NN ) -> ( sqrt ` D ) e. RR+ ) |
19 |
18
|
rpred |
|- ( D e. ( NN \ []NN ) -> ( sqrt ` D ) e. RR ) |
20 |
16 19
|
readdcld |
|- ( D e. ( NN \ []NN ) -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) e. RR ) |
21 |
|
breq2 |
|- ( a = b -> ( 1 < a <-> 1 < b ) ) |
22 |
21
|
elrab |
|- ( b e. { a e. ( Pell14QR ` D ) | 1 < a } <-> ( b e. ( Pell14QR ` D ) /\ 1 < b ) ) |
23 |
|
pell14qrgap |
|- ( ( D e. ( NN \ []NN ) /\ b e. ( Pell14QR ` D ) /\ 1 < b ) -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ b ) |
24 |
23
|
3expib |
|- ( D e. ( NN \ []NN ) -> ( ( b e. ( Pell14QR ` D ) /\ 1 < b ) -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ b ) ) |
25 |
22 24
|
syl5bi |
|- ( D e. ( NN \ []NN ) -> ( b e. { a e. ( Pell14QR ` D ) | 1 < a } -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ b ) ) |
26 |
25
|
ralrimiv |
|- ( D e. ( NN \ []NN ) -> A. b e. { a e. ( Pell14QR ` D ) | 1 < a } ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ b ) |
27 |
|
infmrgelbi |
|- ( ( ( { a e. ( Pell14QR ` D ) | 1 < a } C_ RR /\ { a e. ( Pell14QR ` D ) | 1 < a } =/= (/) /\ ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) e. RR ) /\ A. b e. { a e. ( Pell14QR ` D ) | 1 < a } ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ b ) -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ inf ( { a e. ( Pell14QR ` D ) | 1 < a } , RR , < ) ) |
28 |
5 11 20 26 27
|
syl31anc |
|- ( D e. ( NN \ []NN ) -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ inf ( { a e. ( Pell14QR ` D ) | 1 < a } , RR , < ) ) |
29 |
|
pellfundval |
|- ( D e. ( NN \ []NN ) -> ( PellFund ` D ) = inf ( { a e. ( Pell14QR ` D ) | 1 < a } , RR , < ) ) |
30 |
28 29
|
breqtrrd |
|- ( D e. ( NN \ []NN ) -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ ( PellFund ` D ) ) |