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 x φ
supxrgere.a φ A *
supxrgere.b φ B
supxrgere.y φ x + y A B x < y
Assertion supxrgere φ B sup A * <

Proof

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