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