Metamath Proof Explorer


Theorem pellfundge

Description: Lower bound on the fundamental solution of a Pell equation. (Contributed by Stefan O'Rear, 19-Sep-2014)

Ref Expression
Assertion pellfundge
|- ( D e. ( NN \ []NN ) -> ( ( sqrt ` ( D + 1 ) ) + ( sqrt ` D ) ) <_ ( PellFund ` D ) )

Proof

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 ) )