Metamath Proof Explorer


Theorem suplesup

Description: If any element of A can be approximated from below by members of B , then the supremum of A is less than or equal to the supremum of B . (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses suplesup.a φ A
suplesup.b φ B *
suplesup.c φ x A y + z B x y < z
Assertion suplesup φ sup A * < sup B * <

Proof

Step Hyp Ref Expression
1 suplesup.a φ A
2 suplesup.b φ B *
3 suplesup.c φ x A y + z B x y < z
4 ressxr *
5 1 4 sstrdi φ A *
6 supxrcl A * sup A * < *
7 5 6 syl φ sup A * < *
8 7 adantr φ sup A * < = +∞ sup A * < *
9 eqidd φ sup A * < = +∞ +∞ = +∞
10 simpr φ sup A * < = +∞ sup A * < = +∞
11 peano2re w w + 1
12 11 adantl φ sup A * < = +∞ w w + 1
13 5 adantr φ sup A * < = +∞ A *
14 supxrunb2 A * r x A r < x sup A * < = +∞
15 13 14 syl φ sup A * < = +∞ r x A r < x sup A * < = +∞
16 10 15 mpbird φ sup A * < = +∞ r x A r < x
17 16 adantr φ sup A * < = +∞ w r x A r < x
18 breq1 r = w + 1 r < x w + 1 < x
19 18 rexbidv r = w + 1 x A r < x x A w + 1 < x
20 19 rspcva w + 1 r x A r < x x A w + 1 < x
21 12 17 20 syl2anc φ sup A * < = +∞ w x A w + 1 < x
22 1rp 1 +
23 22 a1i φ x A 1 +
24 3 r19.21bi φ x A y + z B x y < z
25 oveq2 y = 1 x y = x 1
26 25 breq1d y = 1 x y < z x 1 < z
27 26 rexbidv y = 1 z B x y < z z B x 1 < z
28 27 rspcva 1 + y + z B x y < z z B x 1 < z
29 23 24 28 syl2anc φ x A z B x 1 < z
30 29 adantlr φ w x A z B x 1 < z
31 30 3adant3 φ w x A w + 1 < x z B x 1 < z
32 nfv z φ w x A w + 1 < x
33 simp11r φ w x A w + 1 < x z B x 1 < z w
34 4 33 sseldi φ w x A w + 1 < x z B x 1 < z w *
35 1 sselda φ x A x
36 1red φ x A 1
37 35 36 resubcld φ x A x 1
38 37 adantlr φ w x A x 1
39 38 3adant3 φ w x A w + 1 < x x 1
40 39 3ad2ant1 φ w x A w + 1 < x z B x 1 < z x 1
41 4 40 sseldi φ w x A w + 1 < x z B x 1 < z x 1 *
42 2 sselda φ z B z *
43 42 adantlr φ w z B z *
44 43 3ad2antl1 φ w x A w + 1 < x z B z *
45 44 3adant3 φ w x A w + 1 < x z B x 1 < z z *
46 simp3 φ w x A w + 1 < x w + 1 < x
47 simp1r φ w x A w + 1 < x w
48 1red φ w x A w + 1 < x 1
49 35 adantlr φ w x A x
50 49 3adant3 φ w x A w + 1 < x x
51 47 48 50 ltaddsubd φ w x A w + 1 < x w + 1 < x w < x 1
52 46 51 mpbid φ w x A w + 1 < x w < x 1
53 52 3ad2ant1 φ w x A w + 1 < x z B x 1 < z w < x 1
54 simp3 φ w x A w + 1 < x z B x 1 < z x 1 < z
55 34 41 45 53 54 xrlttrd φ w x A w + 1 < x z B x 1 < z w < z
56 55 3exp φ w x A w + 1 < x z B x 1 < z w < z
57 32 56 reximdai φ w x A w + 1 < x z B x 1 < z z B w < z
58 31 57 mpd φ w x A w + 1 < x z B w < z
59 58 3exp φ w x A w + 1 < x z B w < z
60 59 adantlr φ sup A * < = +∞ w x A w + 1 < x z B w < z
61 60 rexlimdv φ sup A * < = +∞ w x A w + 1 < x z B w < z
62 21 61 mpd φ sup A * < = +∞ w z B w < z
63 4 a1i φ *
64 63 sselda φ w w *
65 64 ad2antrr φ w z B w < z w *
66 43 adantr φ w z B w < z z *
67 simpr φ w z B w < z w < z
68 65 66 67 xrltled φ w z B w < z w z
69 68 ex φ w z B w < z w z
70 69 adantllr φ sup A * < = +∞ w z B w < z w z
71 70 reximdva φ sup A * < = +∞ w z B w < z z B w z
72 62 71 mpd φ sup A * < = +∞ w z B w z
73 72 ralrimiva φ sup A * < = +∞ w z B w z
74 supxrunb1 B * w z B w z sup B * < = +∞
75 2 74 syl φ w z B w z sup B * < = +∞
76 75 adantr φ sup A * < = +∞ w z B w z sup B * < = +∞
77 73 76 mpbid φ sup A * < = +∞ sup B * < = +∞
78 9 10 77 3eqtr4d φ sup A * < = +∞ sup A * < = sup B * <
79 8 78 xreqled φ sup A * < = +∞ sup A * < sup B * <
80 supeq1 A = sup A * < = sup * <
81 xrsup0 sup * < = −∞
82 81 a1i A = sup * < = −∞
83 80 82 eqtrd A = sup A * < = −∞
84 83 adantl φ A = sup A * < = −∞
85 supxrcl B * sup B * < *
86 2 85 syl φ sup B * < *
87 mnfle sup B * < * −∞ sup B * <
88 86 87 syl φ −∞ sup B * <
89 88 adantr φ A = −∞ sup B * <
90 84 89 eqbrtrd φ A = sup A * < sup B * <
91 90 adantlr φ ¬ sup A * < = +∞ A = sup A * < sup B * <
92 simpll φ ¬ sup A * < = +∞ ¬ A = φ
93 1 adantr φ ¬ A = A
94 neqne ¬ A = A
95 94 adantl φ ¬ A = A
96 supxrgtmnf A A −∞ < sup A * <
97 93 95 96 syl2anc φ ¬ A = −∞ < sup A * <
98 97 adantlr φ ¬ sup A * < = +∞ ¬ A = −∞ < sup A * <
99 simpr φ ¬ sup A * < = +∞ ¬ sup A * < = +∞
100 simpl φ ¬ sup A * < = +∞ φ
101 nltpnft sup A * < * sup A * < = +∞ ¬ sup A * < < +∞
102 100 7 101 3syl φ ¬ sup A * < = +∞ sup A * < = +∞ ¬ sup A * < < +∞
103 99 102 mtbid φ ¬ sup A * < = +∞ ¬ ¬ sup A * < < +∞
104 notnotr ¬ ¬ sup A * < < +∞ sup A * < < +∞
105 103 104 syl φ ¬ sup A * < = +∞ sup A * < < +∞
106 105 adantr φ ¬ sup A * < = +∞ ¬ A = sup A * < < +∞
107 98 106 jca φ ¬ sup A * < = +∞ ¬ A = −∞ < sup A * < sup A * < < +∞
108 92 7 syl φ ¬ sup A * < = +∞ ¬ A = sup A * < *
109 xrrebnd sup A * < * sup A * < −∞ < sup A * < sup A * < < +∞
110 108 109 syl φ ¬ sup A * < = +∞ ¬ A = sup A * < −∞ < sup A * < sup A * < < +∞
111 107 110 mpbird φ ¬ sup A * < = +∞ ¬ A = sup A * <
112 nfv w φ sup A * <
113 2 adantr φ sup A * < B *
114 simpr φ sup A * < sup A * <
115 114 adantr φ sup A * < w + sup A * <
116 simpr φ sup A * < w + w +
117 116 rphalfcld φ sup A * < w + w 2 +
118 115 117 ltsubrpd φ sup A * < w + sup A * < w 2 < sup A * <
119 5 ad2antrr φ sup A * < w + A *
120 rpre w + w
121 2re 2
122 121 a1i w + 2
123 2ne0 2 0
124 123 a1i w + 2 0
125 120 122 124 redivcld w + w 2
126 125 adantl φ sup A * < w + w 2
127 115 126 resubcld φ sup A * < w + sup A * < w 2
128 4 127 sseldi φ sup A * < w + sup A * < w 2 *
129 supxrlub A * sup A * < w 2 * sup A * < w 2 < sup A * < x A sup A * < w 2 < x
130 119 128 129 syl2anc φ sup A * < w + sup A * < w 2 < sup A * < x A sup A * < w 2 < x
131 118 130 mpbid φ sup A * < w + x A sup A * < w 2 < x
132 rphalfcl w + w 2 +
133 132 3ad2ant2 φ w + x A w 2 +
134 24 3adant2 φ w + x A y + z B x y < z
135 oveq2 y = w 2 x y = x w 2
136 135 breq1d y = w 2 x y < z x w 2 < z
137 136 rexbidv y = w 2 z B x y < z z B x w 2 < z
138 137 rspcva w 2 + y + z B x y < z z B x w 2 < z
139 133 134 138 syl2anc φ w + x A z B x w 2 < z
140 139 ad5ant134 φ sup A * < w + x A sup A * < w 2 < x z B x w 2 < z
141 recn sup A * < sup A * <
142 141 adantr sup A * < w + sup A * <
143 120 recnd w + w
144 143 adantl sup A * < w + w
145 144 halfcld sup A * < w + w 2
146 142 145 145 subsub4d sup A * < w + sup A * < - w 2 - w 2 = sup A * < w 2 + w 2
147 143 2halvesd w + w 2 + w 2 = w
148 147 oveq2d w + sup A * < w 2 + w 2 = sup A * < w
149 148 adantl sup A * < w + sup A * < w 2 + w 2 = sup A * < w
150 146 149 eqtr2d sup A * < w + sup A * < w = sup A * < - w 2 - w 2
151 150 adantll φ sup A * < w + sup A * < w = sup A * < - w 2 - w 2
152 151 adantr φ sup A * < w + x A sup A * < w = sup A * < - w 2 - w 2
153 152 ad3antrrr φ sup A * < w + x A sup A * < w 2 < x z B x w 2 < z sup A * < w = sup A * < - w 2 - w 2
154 127 126 resubcld φ sup A * < w + sup A * < - w 2 - w 2
155 154 adantr φ sup A * < w + x A sup A * < - w 2 - w 2
156 155 ad3antrrr φ sup A * < w + x A sup A * < w 2 < x z B x w 2 < z sup A * < - w 2 - w 2
157 4 156 sseldi φ sup A * < w + x A sup A * < w 2 < x z B x w 2 < z sup A * < - w 2 - w 2 *
158 120 49 sylanl2 φ w + x A x
159 125 ad2antlr φ w + x A w 2
160 158 159 resubcld φ w + x A x w 2
161 160 adantllr φ sup A * < w + x A x w 2
162 161 ad3antrrr φ sup A * < w + x A sup A * < w 2 < x z B x w 2 < z x w 2
163 4 162 sseldi φ sup A * < w + x A sup A * < w 2 < x z B x w 2 < z x w 2 *
164 simp-6l φ sup A * < w + x A sup A * < w 2 < x z B x w 2 < z φ
165 simplr φ sup A * < w + x A sup A * < w 2 < x z B x w 2 < z z B
166 164 165 42 syl2anc φ sup A * < w + x A sup A * < w 2 < x z B x w 2 < z z *
167 simp-6r φ sup A * < w + x A sup A * < w 2 < x z B x w 2 < z sup A * <
168 120 ad5antlr φ sup A * < w + x A sup A * < w 2 < x z B x w 2 < z w
169 168 rehalfcld φ sup A * < w + x A sup A * < w 2 < x z B x w 2 < z w 2
170 167 169 resubcld φ sup A * < w + x A sup A * < w 2 < x z B x w 2 < z sup A * < w 2
171 simp-4r φ sup A * < w + x A sup A * < w 2 < x z B x w 2 < z x A
172 164 171 35 syl2anc φ sup A * < w + x A sup A * < w 2 < x z B x w 2 < z x
173 simpllr φ sup A * < w + x A sup A * < w 2 < x z B x w 2 < z sup A * < w 2 < x
174 170 172 169 173 ltsub1dd φ sup A * < w + x A sup A * < w 2 < x z B x w 2 < z sup A * < - w 2 - w 2 < x w 2
175 simpr φ sup A * < w + x A sup A * < w 2 < x z B x w 2 < z x w 2 < z
176 157 163 166 174 175 xrlttrd φ sup A * < w + x A sup A * < w 2 < x z B x w 2 < z sup A * < - w 2 - w 2 < z
177 153 176 eqbrtrd φ sup A * < w + x A sup A * < w 2 < x z B x w 2 < z sup A * < w < z
178 177 ex φ sup A * < w + x A sup A * < w 2 < x z B x w 2 < z sup A * < w < z
179 178 reximdva φ sup A * < w + x A sup A * < w 2 < x z B x w 2 < z z B sup A * < w < z
180 140 179 mpd φ sup A * < w + x A sup A * < w 2 < x z B sup A * < w < z
181 180 rexlimdva2 φ sup A * < w + x A sup A * < w 2 < x z B sup A * < w < z
182 131 181 mpd φ sup A * < w + z B sup A * < w < z
183 112 113 114 182 supxrgere φ sup A * < sup A * < sup B * <
184 92 111 183 syl2anc φ ¬ sup A * < = +∞ ¬ A = sup A * < sup B * <
185 91 184 pm2.61dan φ ¬ sup A * < = +∞ sup A * < sup B * <
186 79 185 pm2.61dan φ sup A * < sup B * <