Metamath Proof Explorer

Theorem pellfundglb

Description: If a real is larger than the fundamental solution, there is a nontrivial solution less than it. (Contributed by Stefan O'Rear, 18-Sep-2014)

Ref Expression
Assertion pellfundglb 
|- ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) -> E. x e. ( Pell1QR ` D ) ( ( PellFund ` D ) <_ x /\ x < 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. RR /\ ( PellFund ` D ) < A ) -> ( PellFund ` D ) = inf ( { a e. ( Pell14QR ` D ) | 1 < a } , RR , < ) )
3 simp3 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) -> ( PellFund ` D ) < A )
4 2 3 eqbrtrrd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) -> inf ( { a e. ( Pell14QR ` D ) | 1 < a } , RR , < ) < A )
5 pellfundre 
 |-  ( D e. ( NN \ []NN ) -> ( PellFund ` D ) e. RR )
6 5 3ad2ant1 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) -> ( PellFund ` D ) e. RR )
7 2 6 eqeltrrd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) -> inf ( { a e. ( Pell14QR ` D ) | 1 < a } , RR , < ) e. RR )
8 simp2 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) -> A e. RR )
9 7 8 ltnled 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) -> ( inf ( { a e. ( Pell14QR ` D ) | 1 < a } , RR , < ) < A <-> -. A <_ inf ( { a e. ( Pell14QR ` D ) | 1 < a } , RR , < ) ) )
10 4 9 mpbid 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) -> -. A <_ inf ( { a e. ( Pell14QR ` D ) | 1 < a } , RR , < ) )
11 ssrab2 
 |-  { a e. ( Pell14QR ` D ) | 1 < a } C_ ( Pell14QR ` D )
12 pell14qrre 
 |-  ( ( D e. ( NN \ []NN ) /\ a e. ( Pell14QR ` D ) ) -> a e. RR )
13 12 ex 
 |-  ( D e. ( NN \ []NN ) -> ( a e. ( Pell14QR ` D ) -> a e. RR ) )
14 13 ssrdv 
 |-  ( D e. ( NN \ []NN ) -> ( Pell14QR ` D ) C_ RR )
15 14 3ad2ant1 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) -> ( Pell14QR ` D ) C_ RR )
16 11 15 sstrid 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) -> { a e. ( Pell14QR ` D ) | 1 < a } C_ RR )
17 pell1qrss14 
 |-  ( D e. ( NN \ []NN ) -> ( Pell1QR ` D ) C_ ( Pell14QR ` D ) )
18 17 3ad2ant1 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) -> ( Pell1QR ` D ) C_ ( Pell14QR ` D ) )
19 pellqrex 
 |-  ( D e. ( NN \ []NN ) -> E. a e. ( Pell1QR ` D ) 1 < a )
20 19 3ad2ant1 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) -> E. a e. ( Pell1QR ` D ) 1 < a )
21 ssrexv 
 |-  ( ( Pell1QR ` D ) C_ ( Pell14QR ` D ) -> ( E. a e. ( Pell1QR ` D ) 1 < a -> E. a e. ( Pell14QR ` D ) 1 < a ) )
22 18 20 21 sylc 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) -> E. a e. ( Pell14QR ` D ) 1 < a )
23 rabn0 
 |-  ( { a e. ( Pell14QR ` D ) | 1 < a } =/= (/) <-> E. a e. ( Pell14QR ` D ) 1 < a )
24 22 23 sylibr 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) -> { a e. ( Pell14QR ` D ) | 1 < a } =/= (/) )
25 infmrgelbi 
 |-  ( ( ( { a e. ( Pell14QR ` D ) | 1 < a } C_ RR /\ { a e. ( Pell14QR ` D ) | 1 < a } =/= (/) /\ A e. RR ) /\ A. x e. { a e. ( Pell14QR ` D ) | 1 < a } A <_ x ) -> A <_ inf ( { a e. ( Pell14QR ` D ) | 1 < a } , RR , < ) )
26 25 ex 
 |-  ( ( { a e. ( Pell14QR ` D ) | 1 < a } C_ RR /\ { a e. ( Pell14QR ` D ) | 1 < a } =/= (/) /\ A e. RR ) -> ( A. x e. { a e. ( Pell14QR ` D ) | 1 < a } A <_ x -> A <_ inf ( { a e. ( Pell14QR ` D ) | 1 < a } , RR , < ) ) )
27 16 24 8 26 syl3anc 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) -> ( A. x e. { a e. ( Pell14QR ` D ) | 1 < a } A <_ x -> A <_ inf ( { a e. ( Pell14QR ` D ) | 1 < a } , RR , < ) ) )
28 10 27 mtod 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) -> -. A. x e. { a e. ( Pell14QR ` D ) | 1 < a } A <_ x )
29 rexnal 
 |-  ( E. x e. { a e. ( Pell14QR ` D ) | 1 < a } -. A <_ x <-> -. A. x e. { a e. ( Pell14QR ` D ) | 1 < a } A <_ x )
30 28 29 sylibr 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) -> E. x e. { a e. ( Pell14QR ` D ) | 1 < a } -. A <_ x )
31 breq2 
 |-  ( a = x -> ( 1 < a <-> 1 < x ) )
32 31 elrab 
 |-  ( x e. { a e. ( Pell14QR ` D ) | 1 < a } <-> ( x e. ( Pell14QR ` D ) /\ 1 < x ) )
33 simprl 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) /\ ( x e. ( Pell14QR ` D ) /\ 1 < x ) ) -> x e. ( Pell14QR ` D ) )
34 1red 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) /\ ( x e. ( Pell14QR ` D ) /\ 1 < x ) ) -> 1 e. RR )
35 simpl1 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) /\ ( x e. ( Pell14QR ` D ) /\ 1 < x ) ) -> D e. ( NN \ []NN ) )
36 pell14qrre 
 |-  ( ( D e. ( NN \ []NN ) /\ x e. ( Pell14QR ` D ) ) -> x e. RR )
37 35 33 36 syl2anc 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) /\ ( x e. ( Pell14QR ` D ) /\ 1 < x ) ) -> x e. RR )
38 simprr 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) /\ ( x e. ( Pell14QR ` D ) /\ 1 < x ) ) -> 1 < x )
39 34 37 38 ltled 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) /\ ( x e. ( Pell14QR ` D ) /\ 1 < x ) ) -> 1 <_ x )
40 33 39 jca 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) /\ ( x e. ( Pell14QR ` D ) /\ 1 < x ) ) -> ( x e. ( Pell14QR ` D ) /\ 1 <_ x ) )
41 elpell1qr2 
 |-  ( D e. ( NN \ []NN ) -> ( x e. ( Pell1QR ` D ) <-> ( x e. ( Pell14QR ` D ) /\ 1 <_ x ) ) )
42 35 41 syl 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) /\ ( x e. ( Pell14QR ` D ) /\ 1 < x ) ) -> ( x e. ( Pell1QR ` D ) <-> ( x e. ( Pell14QR ` D ) /\ 1 <_ x ) ) )
43 40 42 mpbird 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) /\ ( x e. ( Pell14QR ` D ) /\ 1 < x ) ) -> x e. ( Pell1QR ` D ) )
44 32 43 sylan2b 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) /\ x e. { a e. ( Pell14QR ` D ) | 1 < a } ) -> x e. ( Pell1QR ` D ) )
45 44 adantrr 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) /\ ( x e. { a e. ( Pell14QR ` D ) | 1 < a } /\ -. A <_ x ) ) -> x e. ( Pell1QR ` D ) )
46 simpl1 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) /\ ( x e. { a e. ( Pell14QR ` D ) | 1 < a } /\ -. A <_ x ) ) -> D e. ( NN \ []NN ) )
47 simprl 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) /\ ( x e. { a e. ( Pell14QR ` D ) | 1 < a } /\ -. A <_ x ) ) -> x e. { a e. ( Pell14QR ` D ) | 1 < a } )
48 11 47 sseldi 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) /\ ( x e. { a e. ( Pell14QR ` D ) | 1 < a } /\ -. A <_ x ) ) -> x e. ( Pell14QR ` D ) )
49 simpr 
 |-  ( ( x e. ( Pell14QR ` D ) /\ 1 < x ) -> 1 < x )
50 49 a1i 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) -> ( ( x e. ( Pell14QR ` D ) /\ 1 < x ) -> 1 < x ) )
51 32 50 syl5bi 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) -> ( x e. { a e. ( Pell14QR ` D ) | 1 < a } -> 1 < x ) )
52 51 imp 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) /\ x e. { a e. ( Pell14QR ` D ) | 1 < a } ) -> 1 < x )
53 52 adantrr 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) /\ ( x e. { a e. ( Pell14QR ` D ) | 1 < a } /\ -. A <_ x ) ) -> 1 < x )
54 pellfundlb 
 |-  ( ( D e. ( NN \ []NN ) /\ x e. ( Pell14QR ` D ) /\ 1 < x ) -> ( PellFund ` D ) <_ x )
55 46 48 53 54 syl3anc 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) /\ ( x e. { a e. ( Pell14QR ` D ) | 1 < a } /\ -. A <_ x ) ) -> ( PellFund ` D ) <_ x )
56 simprr 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) /\ ( x e. { a e. ( Pell14QR ` D ) | 1 < a } /\ -. A <_ x ) ) -> -. A <_ x )
57 15 adantr 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) /\ ( x e. { a e. ( Pell14QR ` D ) | 1 < a } /\ -. A <_ x ) ) -> ( Pell14QR ` D ) C_ RR )
58 57 48 sseldd 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) /\ ( x e. { a e. ( Pell14QR ` D ) | 1 < a } /\ -. A <_ x ) ) -> x e. RR )
59 simpl2 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) /\ ( x e. { a e. ( Pell14QR ` D ) | 1 < a } /\ -. A <_ x ) ) -> A e. RR )
60 58 59 ltnled 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) /\ ( x e. { a e. ( Pell14QR ` D ) | 1 < a } /\ -. A <_ x ) ) -> ( x < A <-> -. A <_ x ) )
61 56 60 mpbird 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) /\ ( x e. { a e. ( Pell14QR ` D ) | 1 < a } /\ -. A <_ x ) ) -> x < A )
62 55 61 jca 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) /\ ( x e. { a e. ( Pell14QR ` D ) | 1 < a } /\ -. A <_ x ) ) -> ( ( PellFund ` D ) <_ x /\ x < A ) )
63 30 45 62 reximssdv 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. RR /\ ( PellFund ` D ) < A ) -> E. x e. ( Pell1QR ` D ) ( ( PellFund ` D ) <_ x /\ x < A ) )