Metamath Proof Explorer


Theorem infrpge

Description: The infimum of a nonempty, bounded subset of extended reals can be approximated from above by an element of the set. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses infrpge.xph
|- F/ x ph
infrpge.a
|- ( ph -> A C_ RR* )
infrpge.an0
|- ( ph -> A =/= (/) )
infrpge.bnd
|- ( ph -> E. x e. RR A. y e. A x <_ y )
infrpge.b
|- ( ph -> B e. RR+ )
Assertion infrpge
|- ( ph -> E. z e. A z <_ ( inf ( A , RR* , < ) +e B ) )

Proof

Step Hyp Ref Expression
1 infrpge.xph
 |-  F/ x ph
2 infrpge.a
 |-  ( ph -> A C_ RR* )
3 infrpge.an0
 |-  ( ph -> A =/= (/) )
4 infrpge.bnd
 |-  ( ph -> E. x e. RR A. y e. A x <_ y )
5 infrpge.b
 |-  ( ph -> B e. RR+ )
6 n0
 |-  ( A =/= (/) <-> E. z z e. A )
7 6 biimpi
 |-  ( A =/= (/) -> E. z z e. A )
8 3 7 syl
 |-  ( ph -> E. z z e. A )
9 8 adantr
 |-  ( ( ph /\ inf ( A , RR* , < ) = +oo ) -> E. z z e. A )
10 nfv
 |-  F/ z ( ph /\ inf ( A , RR* , < ) = +oo )
11 simpr
 |-  ( ( ( ph /\ inf ( A , RR* , < ) = +oo ) /\ z e. A ) -> z e. A )
12 2 adantr
 |-  ( ( ph /\ z e. A ) -> A C_ RR* )
13 simpr
 |-  ( ( ph /\ z e. A ) -> z e. A )
14 12 13 sseldd
 |-  ( ( ph /\ z e. A ) -> z e. RR* )
15 pnfge
 |-  ( z e. RR* -> z <_ +oo )
16 14 15 syl
 |-  ( ( ph /\ z e. A ) -> z <_ +oo )
17 16 adantlr
 |-  ( ( ( ph /\ inf ( A , RR* , < ) = +oo ) /\ z e. A ) -> z <_ +oo )
18 oveq1
 |-  ( inf ( A , RR* , < ) = +oo -> ( inf ( A , RR* , < ) +e B ) = ( +oo +e B ) )
19 18 adantl
 |-  ( ( ph /\ inf ( A , RR* , < ) = +oo ) -> ( inf ( A , RR* , < ) +e B ) = ( +oo +e B ) )
20 5 rpxrd
 |-  ( ph -> B e. RR* )
21 5 rpred
 |-  ( ph -> B e. RR )
22 renemnf
 |-  ( B e. RR -> B =/= -oo )
23 21 22 syl
 |-  ( ph -> B =/= -oo )
24 xaddpnf2
 |-  ( ( B e. RR* /\ B =/= -oo ) -> ( +oo +e B ) = +oo )
25 20 23 24 syl2anc
 |-  ( ph -> ( +oo +e B ) = +oo )
26 25 adantr
 |-  ( ( ph /\ inf ( A , RR* , < ) = +oo ) -> ( +oo +e B ) = +oo )
27 19 26 eqtr2d
 |-  ( ( ph /\ inf ( A , RR* , < ) = +oo ) -> +oo = ( inf ( A , RR* , < ) +e B ) )
28 27 adantr
 |-  ( ( ( ph /\ inf ( A , RR* , < ) = +oo ) /\ z e. A ) -> +oo = ( inf ( A , RR* , < ) +e B ) )
29 17 28 breqtrd
 |-  ( ( ( ph /\ inf ( A , RR* , < ) = +oo ) /\ z e. A ) -> z <_ ( inf ( A , RR* , < ) +e B ) )
30 11 29 jca
 |-  ( ( ( ph /\ inf ( A , RR* , < ) = +oo ) /\ z e. A ) -> ( z e. A /\ z <_ ( inf ( A , RR* , < ) +e B ) ) )
31 30 ex
 |-  ( ( ph /\ inf ( A , RR* , < ) = +oo ) -> ( z e. A -> ( z e. A /\ z <_ ( inf ( A , RR* , < ) +e B ) ) ) )
32 10 31 eximd
 |-  ( ( ph /\ inf ( A , RR* , < ) = +oo ) -> ( E. z z e. A -> E. z ( z e. A /\ z <_ ( inf ( A , RR* , < ) +e B ) ) ) )
33 9 32 mpd
 |-  ( ( ph /\ inf ( A , RR* , < ) = +oo ) -> E. z ( z e. A /\ z <_ ( inf ( A , RR* , < ) +e B ) ) )
34 df-rex
 |-  ( E. z e. A z <_ ( inf ( A , RR* , < ) +e B ) <-> E. z ( z e. A /\ z <_ ( inf ( A , RR* , < ) +e B ) ) )
35 33 34 sylibr
 |-  ( ( ph /\ inf ( A , RR* , < ) = +oo ) -> E. z e. A z <_ ( inf ( A , RR* , < ) +e B ) )
36 simpl
 |-  ( ( ph /\ -. inf ( A , RR* , < ) = +oo ) -> ph )
37 nfv
 |-  F/ x -oo < inf ( A , RR* , < )
38 mnfxr
 |-  -oo e. RR*
39 38 a1i
 |-  ( ( ph /\ x e. RR /\ A. y e. A x <_ y ) -> -oo e. RR* )
40 rexr
 |-  ( x e. RR -> x e. RR* )
41 40 3ad2ant2
 |-  ( ( ph /\ x e. RR /\ A. y e. A x <_ y ) -> x e. RR* )
42 infxrcl
 |-  ( A C_ RR* -> inf ( A , RR* , < ) e. RR* )
43 2 42 syl
 |-  ( ph -> inf ( A , RR* , < ) e. RR* )
44 43 3ad2ant1
 |-  ( ( ph /\ x e. RR /\ A. y e. A x <_ y ) -> inf ( A , RR* , < ) e. RR* )
45 mnflt
 |-  ( x e. RR -> -oo < x )
46 45 3ad2ant2
 |-  ( ( ph /\ x e. RR /\ A. y e. A x <_ y ) -> -oo < x )
47 simp3
 |-  ( ( ph /\ x e. RR /\ A. y e. A x <_ y ) -> A. y e. A x <_ y )
48 2 adantr
 |-  ( ( ph /\ x e. RR ) -> A C_ RR* )
49 40 adantl
 |-  ( ( ph /\ x e. RR ) -> x e. RR* )
50 infxrgelb
 |-  ( ( A C_ RR* /\ x e. RR* ) -> ( x <_ inf ( A , RR* , < ) <-> A. y e. A x <_ y ) )
51 48 49 50 syl2anc
 |-  ( ( ph /\ x e. RR ) -> ( x <_ inf ( A , RR* , < ) <-> A. y e. A x <_ y ) )
52 51 3adant3
 |-  ( ( ph /\ x e. RR /\ A. y e. A x <_ y ) -> ( x <_ inf ( A , RR* , < ) <-> A. y e. A x <_ y ) )
53 47 52 mpbird
 |-  ( ( ph /\ x e. RR /\ A. y e. A x <_ y ) -> x <_ inf ( A , RR* , < ) )
54 39 41 44 46 53 xrltletrd
 |-  ( ( ph /\ x e. RR /\ A. y e. A x <_ y ) -> -oo < inf ( A , RR* , < ) )
55 54 3exp
 |-  ( ph -> ( x e. RR -> ( A. y e. A x <_ y -> -oo < inf ( A , RR* , < ) ) ) )
56 1 37 55 rexlimd
 |-  ( ph -> ( E. x e. RR A. y e. A x <_ y -> -oo < inf ( A , RR* , < ) ) )
57 4 56 mpd
 |-  ( ph -> -oo < inf ( A , RR* , < ) )
58 57 adantr
 |-  ( ( ph /\ -. inf ( A , RR* , < ) = +oo ) -> -oo < inf ( A , RR* , < ) )
59 neqne
 |-  ( -. inf ( A , RR* , < ) = +oo -> inf ( A , RR* , < ) =/= +oo )
60 59 adantl
 |-  ( ( ph /\ -. inf ( A , RR* , < ) = +oo ) -> inf ( A , RR* , < ) =/= +oo )
61 43 adantr
 |-  ( ( ph /\ -. inf ( A , RR* , < ) = +oo ) -> inf ( A , RR* , < ) e. RR* )
62 60 61 nepnfltpnf
 |-  ( ( ph /\ -. inf ( A , RR* , < ) = +oo ) -> inf ( A , RR* , < ) < +oo )
63 58 62 jca
 |-  ( ( ph /\ -. inf ( A , RR* , < ) = +oo ) -> ( -oo < inf ( A , RR* , < ) /\ inf ( A , RR* , < ) < +oo ) )
64 xrrebnd
 |-  ( inf ( A , RR* , < ) e. RR* -> ( inf ( A , RR* , < ) e. RR <-> ( -oo < inf ( A , RR* , < ) /\ inf ( A , RR* , < ) < +oo ) ) )
65 43 64 syl
 |-  ( ph -> ( inf ( A , RR* , < ) e. RR <-> ( -oo < inf ( A , RR* , < ) /\ inf ( A , RR* , < ) < +oo ) ) )
66 65 adantr
 |-  ( ( ph /\ -. inf ( A , RR* , < ) = +oo ) -> ( inf ( A , RR* , < ) e. RR <-> ( -oo < inf ( A , RR* , < ) /\ inf ( A , RR* , < ) < +oo ) ) )
67 63 66 mpbird
 |-  ( ( ph /\ -. inf ( A , RR* , < ) = +oo ) -> inf ( A , RR* , < ) e. RR )
68 simpr
 |-  ( ( ph /\ inf ( A , RR* , < ) e. RR ) -> inf ( A , RR* , < ) e. RR )
69 5 adantr
 |-  ( ( ph /\ inf ( A , RR* , < ) e. RR ) -> B e. RR+ )
70 68 69 ltaddrpd
 |-  ( ( ph /\ inf ( A , RR* , < ) e. RR ) -> inf ( A , RR* , < ) < ( inf ( A , RR* , < ) + B ) )
71 21 adantr
 |-  ( ( ph /\ inf ( A , RR* , < ) e. RR ) -> B e. RR )
72 rexadd
 |-  ( ( inf ( A , RR* , < ) e. RR /\ B e. RR ) -> ( inf ( A , RR* , < ) +e B ) = ( inf ( A , RR* , < ) + B ) )
73 68 71 72 syl2anc
 |-  ( ( ph /\ inf ( A , RR* , < ) e. RR ) -> ( inf ( A , RR* , < ) +e B ) = ( inf ( A , RR* , < ) + B ) )
74 73 eqcomd
 |-  ( ( ph /\ inf ( A , RR* , < ) e. RR ) -> ( inf ( A , RR* , < ) + B ) = ( inf ( A , RR* , < ) +e B ) )
75 70 74 breqtrd
 |-  ( ( ph /\ inf ( A , RR* , < ) e. RR ) -> inf ( A , RR* , < ) < ( inf ( A , RR* , < ) +e B ) )
76 43 adantr
 |-  ( ( ph /\ inf ( A , RR* , < ) e. RR ) -> inf ( A , RR* , < ) e. RR* )
77 43 20 xaddcld
 |-  ( ph -> ( inf ( A , RR* , < ) +e B ) e. RR* )
78 77 adantr
 |-  ( ( ph /\ inf ( A , RR* , < ) e. RR ) -> ( inf ( A , RR* , < ) +e B ) e. RR* )
79 xrltnle
 |-  ( ( inf ( A , RR* , < ) e. RR* /\ ( inf ( A , RR* , < ) +e B ) e. RR* ) -> ( inf ( A , RR* , < ) < ( inf ( A , RR* , < ) +e B ) <-> -. ( inf ( A , RR* , < ) +e B ) <_ inf ( A , RR* , < ) ) )
80 76 78 79 syl2anc
 |-  ( ( ph /\ inf ( A , RR* , < ) e. RR ) -> ( inf ( A , RR* , < ) < ( inf ( A , RR* , < ) +e B ) <-> -. ( inf ( A , RR* , < ) +e B ) <_ inf ( A , RR* , < ) ) )
81 75 80 mpbid
 |-  ( ( ph /\ inf ( A , RR* , < ) e. RR ) -> -. ( inf ( A , RR* , < ) +e B ) <_ inf ( A , RR* , < ) )
82 36 67 81 syl2anc
 |-  ( ( ph /\ -. inf ( A , RR* , < ) = +oo ) -> -. ( inf ( A , RR* , < ) +e B ) <_ inf ( A , RR* , < ) )
83 simpr
 |-  ( ( ph /\ -. ( inf ( A , RR* , < ) +e B ) <_ inf ( A , RR* , < ) ) -> -. ( inf ( A , RR* , < ) +e B ) <_ inf ( A , RR* , < ) )
84 simpl
 |-  ( ( ph /\ -. ( inf ( A , RR* , < ) +e B ) <_ inf ( A , RR* , < ) ) -> ph )
85 infxrgelb
 |-  ( ( A C_ RR* /\ ( inf ( A , RR* , < ) +e B ) e. RR* ) -> ( ( inf ( A , RR* , < ) +e B ) <_ inf ( A , RR* , < ) <-> A. z e. A ( inf ( A , RR* , < ) +e B ) <_ z ) )
86 2 77 85 syl2anc
 |-  ( ph -> ( ( inf ( A , RR* , < ) +e B ) <_ inf ( A , RR* , < ) <-> A. z e. A ( inf ( A , RR* , < ) +e B ) <_ z ) )
87 84 86 syl
 |-  ( ( ph /\ -. ( inf ( A , RR* , < ) +e B ) <_ inf ( A , RR* , < ) ) -> ( ( inf ( A , RR* , < ) +e B ) <_ inf ( A , RR* , < ) <-> A. z e. A ( inf ( A , RR* , < ) +e B ) <_ z ) )
88 83 87 mtbid
 |-  ( ( ph /\ -. ( inf ( A , RR* , < ) +e B ) <_ inf ( A , RR* , < ) ) -> -. A. z e. A ( inf ( A , RR* , < ) +e B ) <_ z )
89 rexnal
 |-  ( E. z e. A -. ( inf ( A , RR* , < ) +e B ) <_ z <-> -. A. z e. A ( inf ( A , RR* , < ) +e B ) <_ z )
90 88 89 sylibr
 |-  ( ( ph /\ -. ( inf ( A , RR* , < ) +e B ) <_ inf ( A , RR* , < ) ) -> E. z e. A -. ( inf ( A , RR* , < ) +e B ) <_ z )
91 36 82 90 syl2anc
 |-  ( ( ph /\ -. inf ( A , RR* , < ) = +oo ) -> E. z e. A -. ( inf ( A , RR* , < ) +e B ) <_ z )
92 14 adantr
 |-  ( ( ( ph /\ z e. A ) /\ -. ( inf ( A , RR* , < ) +e B ) <_ z ) -> z e. RR* )
93 77 ad2antrr
 |-  ( ( ( ph /\ z e. A ) /\ -. ( inf ( A , RR* , < ) +e B ) <_ z ) -> ( inf ( A , RR* , < ) +e B ) e. RR* )
94 simpr
 |-  ( ( ( ph /\ z e. A ) /\ -. ( inf ( A , RR* , < ) +e B ) <_ z ) -> -. ( inf ( A , RR* , < ) +e B ) <_ z )
95 xrltnle
 |-  ( ( z e. RR* /\ ( inf ( A , RR* , < ) +e B ) e. RR* ) -> ( z < ( inf ( A , RR* , < ) +e B ) <-> -. ( inf ( A , RR* , < ) +e B ) <_ z ) )
96 92 93 95 syl2anc
 |-  ( ( ( ph /\ z e. A ) /\ -. ( inf ( A , RR* , < ) +e B ) <_ z ) -> ( z < ( inf ( A , RR* , < ) +e B ) <-> -. ( inf ( A , RR* , < ) +e B ) <_ z ) )
97 94 96 mpbird
 |-  ( ( ( ph /\ z e. A ) /\ -. ( inf ( A , RR* , < ) +e B ) <_ z ) -> z < ( inf ( A , RR* , < ) +e B ) )
98 92 93 97 xrltled
 |-  ( ( ( ph /\ z e. A ) /\ -. ( inf ( A , RR* , < ) +e B ) <_ z ) -> z <_ ( inf ( A , RR* , < ) +e B ) )
99 98 ex
 |-  ( ( ph /\ z e. A ) -> ( -. ( inf ( A , RR* , < ) +e B ) <_ z -> z <_ ( inf ( A , RR* , < ) +e B ) ) )
100 99 adantlr
 |-  ( ( ( ph /\ -. inf ( A , RR* , < ) = +oo ) /\ z e. A ) -> ( -. ( inf ( A , RR* , < ) +e B ) <_ z -> z <_ ( inf ( A , RR* , < ) +e B ) ) )
101 100 reximdva
 |-  ( ( ph /\ -. inf ( A , RR* , < ) = +oo ) -> ( E. z e. A -. ( inf ( A , RR* , < ) +e B ) <_ z -> E. z e. A z <_ ( inf ( A , RR* , < ) +e B ) ) )
102 91 101 mpd
 |-  ( ( ph /\ -. inf ( A , RR* , < ) = +oo ) -> E. z e. A z <_ ( inf ( A , RR* , < ) +e B ) )
103 35 102 pm2.61dan
 |-  ( ph -> E. z e. A z <_ ( inf ( A , RR* , < ) +e B ) )