Metamath Proof Explorer

Theorem pellfundlb

Description: A nontrivial first quadrant solution is at least as large as the fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014) (Proof shortened by AV, 15-Sep-2020)

Ref Expression
Assertion pellfundlb 
|- ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> ( PellFund ` D ) <_ A )

Proof

Step Hyp Ref Expression
1 pellfundval 
 |-  ( D e. ( NN \ []NN ) -> ( PellFund ` D ) = inf ( { a e. ( Pell14QR ` D ) | 1 < a } , RR , < ) )
2 1 3ad2ant1 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> ( PellFund ` D ) = inf ( { a e. ( Pell14QR ` D ) | 1 < a } , RR , < ) )
3 ssrab2 
 |-  { a e. ( Pell14QR ` D ) | 1 < a } C_ ( Pell14QR ` D )
4 pell14qrre 
 |-  ( ( D e. ( NN \ []NN ) /\ d e. ( Pell14QR ` D ) ) -> d e. RR )
5 4 ex 
 |-  ( D e. ( NN \ []NN ) -> ( d e. ( Pell14QR ` D ) -> d e. RR ) )
6 5 ssrdv 
 |-  ( D e. ( NN \ []NN ) -> ( Pell14QR ` D ) C_ RR )
7 3 6 sstrid 
 |-  ( D e. ( NN \ []NN ) -> { a e. ( Pell14QR ` D ) | 1 < a } C_ RR )
8 7 3ad2ant1 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> { a e. ( Pell14QR ` D ) | 1 < a } C_ RR )
9 1re 
 |-  1 e. RR
10 breq2 
 |-  ( a = c -> ( 1 < a <-> 1 < c ) )
11 10 elrab 
 |-  ( c e. { a e. ( Pell14QR ` D ) | 1 < a } <-> ( c e. ( Pell14QR ` D ) /\ 1 < c ) )
12 pell14qrre 
 |-  ( ( D e. ( NN \ []NN ) /\ c e. ( Pell14QR ` D ) ) -> c e. RR )
13 ltle 
 |-  ( ( 1 e. RR /\ c e. RR ) -> ( 1 < c -> 1 <_ c ) )
14 9 12 13 sylancr 
 |-  ( ( D e. ( NN \ []NN ) /\ c e. ( Pell14QR ` D ) ) -> ( 1 < c -> 1 <_ c ) )
15 14 expimpd 
 |-  ( D e. ( NN \ []NN ) -> ( ( c e. ( Pell14QR ` D ) /\ 1 < c ) -> 1 <_ c ) )
16 11 15 biimtrid 
 |-  ( D e. ( NN \ []NN ) -> ( c e. { a e. ( Pell14QR ` D ) | 1 < a } -> 1 <_ c ) )
17 16 ralrimiv 
 |-  ( D e. ( NN \ []NN ) -> A. c e. { a e. ( Pell14QR ` D ) | 1 < a } 1 <_ c )
18 17 3ad2ant1 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> A. c e. { a e. ( Pell14QR ` D ) | 1 < a } 1 <_ c )
19 breq1 
 |-  ( b = 1 -> ( b <_ c <-> 1 <_ c ) )
20 19 ralbidv 
 |-  ( b = 1 -> ( A. c e. { a e. ( Pell14QR ` D ) | 1 < a } b <_ c <-> A. c e. { a e. ( Pell14QR ` D ) | 1 < a } 1 <_ c ) )
21 20 rspcev 
 |-  ( ( 1 e. RR /\ A. c e. { a e. ( Pell14QR ` D ) | 1 < a } 1 <_ c ) -> E. b e. RR A. c e. { a e. ( Pell14QR ` D ) | 1 < a } b <_ c )
22 9 18 21 sylancr 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> E. b e. RR A. c e. { a e. ( Pell14QR ` D ) | 1 < a } b <_ c )
23 simp2 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> A e. ( Pell14QR ` D ) )
24 simp3 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> 1 < A )
25 breq2 
 |-  ( a = A -> ( 1 < a <-> 1 < A ) )
26 25 elrab 
 |-  ( A e. { a e. ( Pell14QR ` D ) | 1 < a } <-> ( A e. ( Pell14QR ` D ) /\ 1 < A ) )
27 23 24 26 sylanbrc 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> A e. { a e. ( Pell14QR ` D ) | 1 < a } )
28 infrelb 
 |-  ( ( { a e. ( Pell14QR ` D ) | 1 < a } C_ RR /\ E. b e. RR A. c e. { a e. ( Pell14QR ` D ) | 1 < a } b <_ c /\ A e. { a e. ( Pell14QR ` D ) | 1 < a } ) -> inf ( { a e. ( Pell14QR ` D ) | 1 < a } , RR , < ) <_ A )
29 8 22 27 28 syl3anc 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> inf ( { a e. ( Pell14QR ` D ) | 1 < a } , RR , < ) <_ A )
30 2 29 eqbrtrd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ 1 < A ) -> ( PellFund ` D ) <_ A )