Metamath Proof Explorer


Theorem supxrgere

Description: If a real number can be approximated from below by members of a set, then it is less than or equal to the supremum of the set. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses supxrgere.xph
|- F/ x ph
supxrgere.a
|- ( ph -> A C_ RR* )
supxrgere.b
|- ( ph -> B e. RR )
supxrgere.y
|- ( ( ph /\ x e. RR+ ) -> E. y e. A ( B - x ) < y )
Assertion supxrgere
|- ( ph -> B <_ sup ( A , RR* , < ) )

Proof

Step Hyp Ref Expression
1 supxrgere.xph
 |-  F/ x ph
2 supxrgere.a
 |-  ( ph -> A C_ RR* )
3 supxrgere.b
 |-  ( ph -> B e. RR )
4 supxrgere.y
 |-  ( ( ph /\ x e. RR+ ) -> E. y e. A ( B - x ) < y )
5 rexr
 |-  ( B e. RR -> B e. RR* )
6 pnfxr
 |-  +oo e. RR*
7 6 a1i
 |-  ( B e. RR -> +oo e. RR* )
8 ltpnf
 |-  ( B e. RR -> B < +oo )
9 5 7 8 xrltled
 |-  ( B e. RR -> B <_ +oo )
10 3 9 syl
 |-  ( ph -> B <_ +oo )
11 10 adantr
 |-  ( ( ph /\ sup ( A , RR* , < ) = +oo ) -> B <_ +oo )
12 id
 |-  ( sup ( A , RR* , < ) = +oo -> sup ( A , RR* , < ) = +oo )
13 12 eqcomd
 |-  ( sup ( A , RR* , < ) = +oo -> +oo = sup ( A , RR* , < ) )
14 13 adantl
 |-  ( ( ph /\ sup ( A , RR* , < ) = +oo ) -> +oo = sup ( A , RR* , < ) )
15 11 14 breqtrd
 |-  ( ( ph /\ sup ( A , RR* , < ) = +oo ) -> B <_ sup ( A , RR* , < ) )
16 simpl
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> ph )
17 1rp
 |-  1 e. RR+
18 nfcv
 |-  F/_ x 1
19 nfv
 |-  F/ x 1 e. RR+
20 1 19 nfan
 |-  F/ x ( ph /\ 1 e. RR+ )
21 nfv
 |-  F/ x E. y e. A ( B - 1 ) < y
22 20 21 nfim
 |-  F/ x ( ( ph /\ 1 e. RR+ ) -> E. y e. A ( B - 1 ) < y )
23 eleq1
 |-  ( x = 1 -> ( x e. RR+ <-> 1 e. RR+ ) )
24 23 anbi2d
 |-  ( x = 1 -> ( ( ph /\ x e. RR+ ) <-> ( ph /\ 1 e. RR+ ) ) )
25 oveq2
 |-  ( x = 1 -> ( B - x ) = ( B - 1 ) )
26 25 breq1d
 |-  ( x = 1 -> ( ( B - x ) < y <-> ( B - 1 ) < y ) )
27 26 rexbidv
 |-  ( x = 1 -> ( E. y e. A ( B - x ) < y <-> E. y e. A ( B - 1 ) < y ) )
28 24 27 imbi12d
 |-  ( x = 1 -> ( ( ( ph /\ x e. RR+ ) -> E. y e. A ( B - x ) < y ) <-> ( ( ph /\ 1 e. RR+ ) -> E. y e. A ( B - 1 ) < y ) ) )
29 18 22 28 4 vtoclgf
 |-  ( 1 e. RR+ -> ( ( ph /\ 1 e. RR+ ) -> E. y e. A ( B - 1 ) < y ) )
30 17 29 ax-mp
 |-  ( ( ph /\ 1 e. RR+ ) -> E. y e. A ( B - 1 ) < y )
31 17 30 mpan2
 |-  ( ph -> E. y e. A ( B - 1 ) < y )
32 31 adantr
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> E. y e. A ( B - 1 ) < y )
33 mnfxr
 |-  -oo e. RR*
34 33 a1i
 |-  ( ( ph /\ y e. A /\ ( B - 1 ) < y ) -> -oo e. RR* )
35 2 sselda
 |-  ( ( ph /\ y e. A ) -> y e. RR* )
36 35 3adant3
 |-  ( ( ph /\ y e. A /\ ( B - 1 ) < y ) -> y e. RR* )
37 supxrcl
 |-  ( A C_ RR* -> sup ( A , RR* , < ) e. RR* )
38 2 37 syl
 |-  ( ph -> sup ( A , RR* , < ) e. RR* )
39 38 3ad2ant1
 |-  ( ( ph /\ y e. A /\ ( B - 1 ) < y ) -> sup ( A , RR* , < ) e. RR* )
40 peano2rem
 |-  ( B e. RR -> ( B - 1 ) e. RR )
41 3 40 syl
 |-  ( ph -> ( B - 1 ) e. RR )
42 41 rexrd
 |-  ( ph -> ( B - 1 ) e. RR* )
43 42 adantr
 |-  ( ( ph /\ -. -oo < y ) -> ( B - 1 ) e. RR* )
44 43 3ad2antl1
 |-  ( ( ( ph /\ y e. A /\ ( B - 1 ) < y ) /\ -. -oo < y ) -> ( B - 1 ) e. RR* )
45 36 adantr
 |-  ( ( ( ph /\ y e. A /\ ( B - 1 ) < y ) /\ -. -oo < y ) -> y e. RR* )
46 33 a1i
 |-  ( ( ( ph /\ y e. A /\ ( B - 1 ) < y ) /\ -. -oo < y ) -> -oo e. RR* )
47 simpl3
 |-  ( ( ( ph /\ y e. A /\ ( B - 1 ) < y ) /\ -. -oo < y ) -> ( B - 1 ) < y )
48 simpr
 |-  ( ( ( ph /\ y e. A ) /\ -. -oo < y ) -> -. -oo < y )
49 35 adantr
 |-  ( ( ( ph /\ y e. A ) /\ -. -oo < y ) -> y e. RR* )
50 33 a1i
 |-  ( ( ( ph /\ y e. A ) /\ -. -oo < y ) -> -oo e. RR* )
51 xrlenlt
 |-  ( ( y e. RR* /\ -oo e. RR* ) -> ( y <_ -oo <-> -. -oo < y ) )
52 49 50 51 syl2anc
 |-  ( ( ( ph /\ y e. A ) /\ -. -oo < y ) -> ( y <_ -oo <-> -. -oo < y ) )
53 48 52 mpbird
 |-  ( ( ( ph /\ y e. A ) /\ -. -oo < y ) -> y <_ -oo )
54 53 3adantl3
 |-  ( ( ( ph /\ y e. A /\ ( B - 1 ) < y ) /\ -. -oo < y ) -> y <_ -oo )
55 44 45 46 47 54 xrltletrd
 |-  ( ( ( ph /\ y e. A /\ ( B - 1 ) < y ) /\ -. -oo < y ) -> ( B - 1 ) < -oo )
56 nltmnf
 |-  ( ( B - 1 ) e. RR* -> -. ( B - 1 ) < -oo )
57 42 56 syl
 |-  ( ph -> -. ( B - 1 ) < -oo )
58 57 adantr
 |-  ( ( ph /\ -. -oo < y ) -> -. ( B - 1 ) < -oo )
59 58 3ad2antl1
 |-  ( ( ( ph /\ y e. A /\ ( B - 1 ) < y ) /\ -. -oo < y ) -> -. ( B - 1 ) < -oo )
60 55 59 condan
 |-  ( ( ph /\ y e. A /\ ( B - 1 ) < y ) -> -oo < y )
61 2 adantr
 |-  ( ( ph /\ y e. A ) -> A C_ RR* )
62 simpr
 |-  ( ( ph /\ y e. A ) -> y e. A )
63 supxrub
 |-  ( ( A C_ RR* /\ y e. A ) -> y <_ sup ( A , RR* , < ) )
64 61 62 63 syl2anc
 |-  ( ( ph /\ y e. A ) -> y <_ sup ( A , RR* , < ) )
65 64 3adant3
 |-  ( ( ph /\ y e. A /\ ( B - 1 ) < y ) -> y <_ sup ( A , RR* , < ) )
66 34 36 39 60 65 xrltletrd
 |-  ( ( ph /\ y e. A /\ ( B - 1 ) < y ) -> -oo < sup ( A , RR* , < ) )
67 66 3exp
 |-  ( ph -> ( y e. A -> ( ( B - 1 ) < y -> -oo < sup ( A , RR* , < ) ) ) )
68 67 adantr
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> ( y e. A -> ( ( B - 1 ) < y -> -oo < sup ( A , RR* , < ) ) ) )
69 68 rexlimdv
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> ( E. y e. A ( B - 1 ) < y -> -oo < sup ( A , RR* , < ) ) )
70 32 69 mpd
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> -oo < sup ( A , RR* , < ) )
71 simpr
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> -. sup ( A , RR* , < ) = +oo )
72 nltpnft
 |-  ( sup ( A , RR* , < ) e. RR* -> ( sup ( A , RR* , < ) = +oo <-> -. sup ( A , RR* , < ) < +oo ) )
73 38 72 syl
 |-  ( ph -> ( sup ( A , RR* , < ) = +oo <-> -. sup ( A , RR* , < ) < +oo ) )
74 73 adantr
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> ( sup ( A , RR* , < ) = +oo <-> -. sup ( A , RR* , < ) < +oo ) )
75 71 74 mtbid
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> -. -. sup ( A , RR* , < ) < +oo )
76 75 notnotrd
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> sup ( A , RR* , < ) < +oo )
77 70 76 jca
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> ( -oo < sup ( A , RR* , < ) /\ sup ( A , RR* , < ) < +oo ) )
78 38 adantr
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> sup ( A , RR* , < ) e. RR* )
79 xrrebnd
 |-  ( sup ( A , RR* , < ) e. RR* -> ( sup ( A , RR* , < ) e. RR <-> ( -oo < sup ( A , RR* , < ) /\ sup ( A , RR* , < ) < +oo ) ) )
80 78 79 syl
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> ( sup ( A , RR* , < ) e. RR <-> ( -oo < sup ( A , RR* , < ) /\ sup ( A , RR* , < ) < +oo ) ) )
81 77 80 mpbird
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> sup ( A , RR* , < ) e. RR )
82 simpl
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ -. B <_ sup ( A , RR* , < ) ) -> ( ph /\ sup ( A , RR* , < ) e. RR ) )
83 simpr
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ -. B <_ sup ( A , RR* , < ) ) -> -. B <_ sup ( A , RR* , < ) )
84 82 simprd
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ -. B <_ sup ( A , RR* , < ) ) -> sup ( A , RR* , < ) e. RR )
85 3 ad2antrr
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ -. B <_ sup ( A , RR* , < ) ) -> B e. RR )
86 84 85 ltnled
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ -. B <_ sup ( A , RR* , < ) ) -> ( sup ( A , RR* , < ) < B <-> -. B <_ sup ( A , RR* , < ) ) )
87 83 86 mpbird
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ -. B <_ sup ( A , RR* , < ) ) -> sup ( A , RR* , < ) < B )
88 simpll
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> ph )
89 3 adantr
 |-  ( ( ph /\ sup ( A , RR* , < ) e. RR ) -> B e. RR )
90 simpr
 |-  ( ( ph /\ sup ( A , RR* , < ) e. RR ) -> sup ( A , RR* , < ) e. RR )
91 89 90 resubcld
 |-  ( ( ph /\ sup ( A , RR* , < ) e. RR ) -> ( B - sup ( A , RR* , < ) ) e. RR )
92 91 adantr
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> ( B - sup ( A , RR* , < ) ) e. RR )
93 simpr
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> sup ( A , RR* , < ) < B )
94 90 adantr
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> sup ( A , RR* , < ) e. RR )
95 88 3 syl
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> B e. RR )
96 94 95 posdifd
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> ( sup ( A , RR* , < ) < B <-> 0 < ( B - sup ( A , RR* , < ) ) ) )
97 93 96 mpbid
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> 0 < ( B - sup ( A , RR* , < ) ) )
98 92 97 elrpd
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> ( B - sup ( A , RR* , < ) ) e. RR+ )
99 ovex
 |-  ( B - sup ( A , RR* , < ) ) e. _V
100 nfcv
 |-  F/_ x ( B - sup ( A , RR* , < ) )
101 nfv
 |-  F/ x ( B - sup ( A , RR* , < ) ) e. RR+
102 1 101 nfan
 |-  F/ x ( ph /\ ( B - sup ( A , RR* , < ) ) e. RR+ )
103 nfv
 |-  F/ x E. y e. A ( B - ( B - sup ( A , RR* , < ) ) ) < y
104 102 103 nfim
 |-  F/ x ( ( ph /\ ( B - sup ( A , RR* , < ) ) e. RR+ ) -> E. y e. A ( B - ( B - sup ( A , RR* , < ) ) ) < y )
105 eleq1
 |-  ( x = ( B - sup ( A , RR* , < ) ) -> ( x e. RR+ <-> ( B - sup ( A , RR* , < ) ) e. RR+ ) )
106 105 anbi2d
 |-  ( x = ( B - sup ( A , RR* , < ) ) -> ( ( ph /\ x e. RR+ ) <-> ( ph /\ ( B - sup ( A , RR* , < ) ) e. RR+ ) ) )
107 oveq2
 |-  ( x = ( B - sup ( A , RR* , < ) ) -> ( B - x ) = ( B - ( B - sup ( A , RR* , < ) ) ) )
108 107 breq1d
 |-  ( x = ( B - sup ( A , RR* , < ) ) -> ( ( B - x ) < y <-> ( B - ( B - sup ( A , RR* , < ) ) ) < y ) )
109 108 rexbidv
 |-  ( x = ( B - sup ( A , RR* , < ) ) -> ( E. y e. A ( B - x ) < y <-> E. y e. A ( B - ( B - sup ( A , RR* , < ) ) ) < y ) )
110 106 109 imbi12d
 |-  ( x = ( B - sup ( A , RR* , < ) ) -> ( ( ( ph /\ x e. RR+ ) -> E. y e. A ( B - x ) < y ) <-> ( ( ph /\ ( B - sup ( A , RR* , < ) ) e. RR+ ) -> E. y e. A ( B - ( B - sup ( A , RR* , < ) ) ) < y ) ) )
111 100 104 110 4 vtoclgf
 |-  ( ( B - sup ( A , RR* , < ) ) e. _V -> ( ( ph /\ ( B - sup ( A , RR* , < ) ) e. RR+ ) -> E. y e. A ( B - ( B - sup ( A , RR* , < ) ) ) < y ) )
112 99 111 ax-mp
 |-  ( ( ph /\ ( B - sup ( A , RR* , < ) ) e. RR+ ) -> E. y e. A ( B - ( B - sup ( A , RR* , < ) ) ) < y )
113 88 98 112 syl2anc
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> E. y e. A ( B - ( B - sup ( A , RR* , < ) ) ) < y )
114 3 recnd
 |-  ( ph -> B e. CC )
115 114 ad3antrrr
 |-  ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ ( B - ( B - sup ( A , RR* , < ) ) ) < y ) -> B e. CC )
116 90 recnd
 |-  ( ( ph /\ sup ( A , RR* , < ) e. RR ) -> sup ( A , RR* , < ) e. CC )
117 116 ad2antrr
 |-  ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ ( B - ( B - sup ( A , RR* , < ) ) ) < y ) -> sup ( A , RR* , < ) e. CC )
118 115 117 nncand
 |-  ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ ( B - ( B - sup ( A , RR* , < ) ) ) < y ) -> ( B - ( B - sup ( A , RR* , < ) ) ) = sup ( A , RR* , < ) )
119 118 eqcomd
 |-  ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ ( B - ( B - sup ( A , RR* , < ) ) ) < y ) -> sup ( A , RR* , < ) = ( B - ( B - sup ( A , RR* , < ) ) ) )
120 simpr
 |-  ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ ( B - ( B - sup ( A , RR* , < ) ) ) < y ) -> ( B - ( B - sup ( A , RR* , < ) ) ) < y )
121 119 120 eqbrtrd
 |-  ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ ( B - ( B - sup ( A , RR* , < ) ) ) < y ) -> sup ( A , RR* , < ) < y )
122 121 ex
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> ( ( B - ( B - sup ( A , RR* , < ) ) ) < y -> sup ( A , RR* , < ) < y ) )
123 122 adantr
 |-  ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. A ) -> ( ( B - ( B - sup ( A , RR* , < ) ) ) < y -> sup ( A , RR* , < ) < y ) )
124 123 reximdva
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> ( E. y e. A ( B - ( B - sup ( A , RR* , < ) ) ) < y -> E. y e. A sup ( A , RR* , < ) < y ) )
125 113 124 mpd
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> E. y e. A sup ( A , RR* , < ) < y )
126 82 87 125 syl2anc
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ -. B <_ sup ( A , RR* , < ) ) -> E. y e. A sup ( A , RR* , < ) < y )
127 61 37 syl
 |-  ( ( ph /\ y e. A ) -> sup ( A , RR* , < ) e. RR* )
128 35 127 xrlenltd
 |-  ( ( ph /\ y e. A ) -> ( y <_ sup ( A , RR* , < ) <-> -. sup ( A , RR* , < ) < y ) )
129 64 128 mpbid
 |-  ( ( ph /\ y e. A ) -> -. sup ( A , RR* , < ) < y )
130 129 ralrimiva
 |-  ( ph -> A. y e. A -. sup ( A , RR* , < ) < y )
131 ralnex
 |-  ( A. y e. A -. sup ( A , RR* , < ) < y <-> -. E. y e. A sup ( A , RR* , < ) < y )
132 130 131 sylib
 |-  ( ph -> -. E. y e. A sup ( A , RR* , < ) < y )
133 132 ad2antrr
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ -. B <_ sup ( A , RR* , < ) ) -> -. E. y e. A sup ( A , RR* , < ) < y )
134 126 133 condan
 |-  ( ( ph /\ sup ( A , RR* , < ) e. RR ) -> B <_ sup ( A , RR* , < ) )
135 16 81 134 syl2anc
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> B <_ sup ( A , RR* , < ) )
136 15 135 pm2.61dan
 |-  ( ph -> B <_ sup ( A , RR* , < ) )