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