Metamath Proof Explorer

Theorem pellfundre

Description: The fundamental solution of a Pell equation exists as a real number. (Contributed by Stefan O'Rear, 18-Sep-2014)

Ref Expression
Assertion pellfundre 
|- ( D e. ( NN \ []NN ) -> ( PellFund ` D ) e. RR )

Proof

Step Hyp Ref Expression
1 pellfundval 
 |-  ( D e. ( NN \ []NN ) -> ( PellFund ` D ) = inf ( { a e. ( Pell14QR ` D ) | 1 < a } , RR , < ) )
2 ssrab2 
 |-  { a e. ( Pell14QR ` D ) | 1 < a } C_ ( Pell14QR ` D )
3 pell14qrre 
 |-  ( ( D e. ( NN \ []NN ) /\ a e. ( Pell14QR ` D ) ) -> a e. RR )
4 3 ex 
 |-  ( D e. ( NN \ []NN ) -> ( a e. ( Pell14QR ` D ) -> a e. RR ) )
5 4 ssrdv 
 |-  ( D e. ( NN \ []NN ) -> ( Pell14QR ` D ) C_ RR )
6 2 5 sstrid 
 |-  ( D e. ( NN \ []NN ) -> { a e. ( Pell14QR ` D ) | 1 < a } C_ RR )
7 pell1qrss14 
 |-  ( D e. ( NN \ []NN ) -> ( Pell1QR ` D ) C_ ( Pell14QR ` D ) )
8 pellqrex 
 |-  ( D e. ( NN \ []NN ) -> E. a e. ( Pell1QR ` D ) 1 < a )
9 ssrexv 
 |-  ( ( Pell1QR ` D ) C_ ( Pell14QR ` D ) -> ( E. a e. ( Pell1QR ` D ) 1 < a -> E. a e. ( Pell14QR ` D ) 1 < a ) )
10 7 8 9 sylc 
 |-  ( D e. ( NN \ []NN ) -> E. a e. ( Pell14QR ` D ) 1 < a )
11 rabn0 
 |-  ( { a e. ( Pell14QR ` D ) | 1 < a } =/= (/) <-> E. a e. ( Pell14QR ` D ) 1 < a )
12 10 11 sylibr 
 |-  ( D e. ( NN \ []NN ) -> { a e. ( Pell14QR ` D ) | 1 < a } =/= (/) )
13 1re 
 |-  1 e. RR
14 breq2 
 |-  ( a = c -> ( 1 < a <-> 1 < c ) )
15 14 elrab 
 |-  ( c e. { a e. ( Pell14QR ` D ) | 1 < a } <-> ( c e. ( Pell14QR ` D ) /\ 1 < c ) )
16 pell14qrre 
 |-  ( ( D e. ( NN \ []NN ) /\ c e. ( Pell14QR ` D ) ) -> c e. RR )
17 ltle 
 |-  ( ( 1 e. RR /\ c e. RR ) -> ( 1 < c -> 1 <_ c ) )
18 13 16 17 sylancr 
 |-  ( ( D e. ( NN \ []NN ) /\ c e. ( Pell14QR ` D ) ) -> ( 1 < c -> 1 <_ c ) )
19 18 expimpd 
 |-  ( D e. ( NN \ []NN ) -> ( ( c e. ( Pell14QR ` D ) /\ 1 < c ) -> 1 <_ c ) )
20 15 19 syl5bi 
 |-  ( D e. ( NN \ []NN ) -> ( c e. { a e. ( Pell14QR ` D ) | 1 < a } -> 1 <_ c ) )
21 20 ralrimiv 
 |-  ( D e. ( NN \ []NN ) -> A. c e. { a e. ( Pell14QR ` D ) | 1 < a } 1 <_ c )
22 breq1 
 |-  ( b = 1 -> ( b <_ c <-> 1 <_ c ) )
23 22 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 ) )
24 23 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 )
25 13 21 24 sylancr 
 |-  ( D e. ( NN \ []NN ) -> E. b e. RR A. c e. { a e. ( Pell14QR ` D ) | 1 < a } b <_ c )
26 infrecl 
 |-  ( ( { a e. ( Pell14QR ` D ) | 1 < a } C_ RR /\ { a e. ( Pell14QR ` D ) | 1 < a } =/= (/) /\ E. b e. RR A. c e. { a e. ( Pell14QR ` D ) | 1 < a } b <_ c ) -> inf ( { a e. ( Pell14QR ` D ) | 1 < a } , RR , < ) e. RR )
27 6 12 25 26 syl3anc 
 |-  ( D e. ( NN \ []NN ) -> inf ( { a e. ( Pell14QR ` D ) | 1 < a } , RR , < ) e. RR )
28 1 27 eqeltrd 
 |-  ( D e. ( NN \ []NN ) -> ( PellFund ` D ) e. RR )