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