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