Metamath Proof Explorer


Theorem supxrge

Description: If an extended 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 supxrge.xph 𝑥 𝜑
supxrge.a ( 𝜑𝐴 ⊆ ℝ* )
supxrge.b ( 𝜑𝐵 ∈ ℝ* )
supxrge.y ( ( 𝜑𝑥 ∈ ℝ+ ) → ∃ 𝑦𝐴 𝐵 ≤ ( 𝑦 +𝑒 𝑥 ) )
Assertion supxrge ( 𝜑𝐵 ≤ sup ( 𝐴 , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 supxrge.xph 𝑥 𝜑
2 supxrge.a ( 𝜑𝐴 ⊆ ℝ* )
3 supxrge.b ( 𝜑𝐵 ∈ ℝ* )
4 supxrge.y ( ( 𝜑𝑥 ∈ ℝ+ ) → ∃ 𝑦𝐴 𝐵 ≤ ( 𝑦 +𝑒 𝑥 ) )
5 pnfge ( 𝐵 ∈ ℝ*𝐵 ≤ +∞ )
6 3 5 syl ( 𝜑𝐵 ≤ +∞ )
7 6 adantr ( ( 𝜑 ∧ +∞ ∈ 𝐴 ) → 𝐵 ≤ +∞ )
8 2 adantr ( ( 𝜑 ∧ +∞ ∈ 𝐴 ) → 𝐴 ⊆ ℝ* )
9 simpr ( ( 𝜑 ∧ +∞ ∈ 𝐴 ) → +∞ ∈ 𝐴 )
10 supxrpnf ( ( 𝐴 ⊆ ℝ* ∧ +∞ ∈ 𝐴 ) → sup ( 𝐴 , ℝ* , < ) = +∞ )
11 8 9 10 syl2anc ( ( 𝜑 ∧ +∞ ∈ 𝐴 ) → sup ( 𝐴 , ℝ* , < ) = +∞ )
12 11 eqcomd ( ( 𝜑 ∧ +∞ ∈ 𝐴 ) → +∞ = sup ( 𝐴 , ℝ* , < ) )
13 7 12 breqtrd ( ( 𝜑 ∧ +∞ ∈ 𝐴 ) → 𝐵 ≤ sup ( 𝐴 , ℝ* , < ) )
14 simpr ( ( 𝜑𝐵 = -∞ ) → 𝐵 = -∞ )
15 supxrcl ( 𝐴 ⊆ ℝ* → sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
16 2 15 syl ( 𝜑 → sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
17 mnfle ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ* → -∞ ≤ sup ( 𝐴 , ℝ* , < ) )
18 16 17 syl ( 𝜑 → -∞ ≤ sup ( 𝐴 , ℝ* , < ) )
19 18 adantr ( ( 𝜑𝐵 = -∞ ) → -∞ ≤ sup ( 𝐴 , ℝ* , < ) )
20 14 19 eqbrtrd ( ( 𝜑𝐵 = -∞ ) → 𝐵 ≤ sup ( 𝐴 , ℝ* , < ) )
21 20 adantlr ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 = -∞ ) → 𝐵 ≤ sup ( 𝐴 , ℝ* , < ) )
22 simpl ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ ¬ 𝐵 = -∞ ) → ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) )
23 neqne ( ¬ 𝐵 = -∞ → 𝐵 ≠ -∞ )
24 23 adantl ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ ¬ 𝐵 = -∞ ) → 𝐵 ≠ -∞ )
25 nfv 𝑤 ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ )
26 2 adantr ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) → 𝐴 ⊆ ℝ* )
27 26 adantr ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) → 𝐴 ⊆ ℝ* )
28 3 adantr ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
29 28 adantr ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) → 𝐵 ∈ ℝ* )
30 simpl ( ( 𝜑𝑤 ∈ ℝ+ ) → 𝜑 )
31 rphalfcl ( 𝑤 ∈ ℝ+ → ( 𝑤 / 2 ) ∈ ℝ+ )
32 31 adantl ( ( 𝜑𝑤 ∈ ℝ+ ) → ( 𝑤 / 2 ) ∈ ℝ+ )
33 ovex ( 𝑤 / 2 ) ∈ V
34 nfcv 𝑥 ( 𝑤 / 2 )
35 nfv 𝑥 ( 𝑤 / 2 ) ∈ ℝ+
36 1 35 nfan 𝑥 ( 𝜑 ∧ ( 𝑤 / 2 ) ∈ ℝ+ )
37 nfv 𝑥𝑦𝐴 𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) )
38 36 37 nfim 𝑥 ( ( 𝜑 ∧ ( 𝑤 / 2 ) ∈ ℝ+ ) → ∃ 𝑦𝐴 𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) )
39 eleq1 ( 𝑥 = ( 𝑤 / 2 ) → ( 𝑥 ∈ ℝ+ ↔ ( 𝑤 / 2 ) ∈ ℝ+ ) )
40 39 anbi2d ( 𝑥 = ( 𝑤 / 2 ) → ( ( 𝜑𝑥 ∈ ℝ+ ) ↔ ( 𝜑 ∧ ( 𝑤 / 2 ) ∈ ℝ+ ) ) )
41 oveq2 ( 𝑥 = ( 𝑤 / 2 ) → ( 𝑦 +𝑒 𝑥 ) = ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) )
42 41 breq2d ( 𝑥 = ( 𝑤 / 2 ) → ( 𝐵 ≤ ( 𝑦 +𝑒 𝑥 ) ↔ 𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) )
43 42 rexbidv ( 𝑥 = ( 𝑤 / 2 ) → ( ∃ 𝑦𝐴 𝐵 ≤ ( 𝑦 +𝑒 𝑥 ) ↔ ∃ 𝑦𝐴 𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) )
44 40 43 imbi12d ( 𝑥 = ( 𝑤 / 2 ) → ( ( ( 𝜑𝑥 ∈ ℝ+ ) → ∃ 𝑦𝐴 𝐵 ≤ ( 𝑦 +𝑒 𝑥 ) ) ↔ ( ( 𝜑 ∧ ( 𝑤 / 2 ) ∈ ℝ+ ) → ∃ 𝑦𝐴 𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) ) )
45 34 38 44 4 vtoclgf ( ( 𝑤 / 2 ) ∈ V → ( ( 𝜑 ∧ ( 𝑤 / 2 ) ∈ ℝ+ ) → ∃ 𝑦𝐴 𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) )
46 33 45 ax-mp ( ( 𝜑 ∧ ( 𝑤 / 2 ) ∈ ℝ+ ) → ∃ 𝑦𝐴 𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) )
47 30 32 46 syl2anc ( ( 𝜑𝑤 ∈ ℝ+ ) → ∃ 𝑦𝐴 𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) )
48 47 adantlr ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝑤 ∈ ℝ+ ) → ∃ 𝑦𝐴 𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) )
49 48 adantlr ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) → ∃ 𝑦𝐴 𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) )
50 nfv 𝑦 ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ )
51 neneq ( 𝐵 ≠ -∞ → ¬ 𝐵 = -∞ )
52 51 adantl ( ( 𝜑𝐵 ≠ -∞ ) → ¬ 𝐵 = -∞ )
53 3 adantr ( ( 𝜑𝐵 ≠ -∞ ) → 𝐵 ∈ ℝ* )
54 ngtmnft ( 𝐵 ∈ ℝ* → ( 𝐵 = -∞ ↔ ¬ -∞ < 𝐵 ) )
55 53 54 syl ( ( 𝜑𝐵 ≠ -∞ ) → ( 𝐵 = -∞ ↔ ¬ -∞ < 𝐵 ) )
56 52 55 mtbid ( ( 𝜑𝐵 ≠ -∞ ) → ¬ ¬ -∞ < 𝐵 )
57 56 notnotrd ( ( 𝜑𝐵 ≠ -∞ ) → -∞ < 𝐵 )
58 57 ad4ant13 ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) → -∞ < 𝐵 )
59 58 3ad2ant1 ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) → -∞ < 𝐵 )
60 29 adantr ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) → 𝐵 ∈ ℝ* )
61 60 3ad2ant1 ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) → 𝐵 ∈ ℝ* )
62 61 adantr ( ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) ∧ ¬ -∞ < 𝑦 ) → 𝐵 ∈ ℝ* )
63 mnfxr -∞ ∈ ℝ*
64 63 a1i ( ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) ∧ ¬ -∞ < 𝑦 ) → -∞ ∈ ℝ* )
65 simpl3 ( ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) ∧ ¬ -∞ < 𝑦 ) → 𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) )
66 simpr ( ( ( 𝜑𝑦𝐴 ) ∧ ¬ -∞ < 𝑦 ) → ¬ -∞ < 𝑦 )
67 2 sselda ( ( 𝜑𝑦𝐴 ) → 𝑦 ∈ ℝ* )
68 67 adantr ( ( ( 𝜑𝑦𝐴 ) ∧ ¬ -∞ < 𝑦 ) → 𝑦 ∈ ℝ* )
69 ngtmnft ( 𝑦 ∈ ℝ* → ( 𝑦 = -∞ ↔ ¬ -∞ < 𝑦 ) )
70 68 69 syl ( ( ( 𝜑𝑦𝐴 ) ∧ ¬ -∞ < 𝑦 ) → ( 𝑦 = -∞ ↔ ¬ -∞ < 𝑦 ) )
71 66 70 mpbird ( ( ( 𝜑𝑦𝐴 ) ∧ ¬ -∞ < 𝑦 ) → 𝑦 = -∞ )
72 71 oveq1d ( ( ( 𝜑𝑦𝐴 ) ∧ ¬ -∞ < 𝑦 ) → ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) = ( -∞ +𝑒 ( 𝑤 / 2 ) ) )
73 72 adantllr ( ( ( ( 𝜑𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴 ) ∧ ¬ -∞ < 𝑦 ) → ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) = ( -∞ +𝑒 ( 𝑤 / 2 ) ) )
74 31 rpxrd ( 𝑤 ∈ ℝ+ → ( 𝑤 / 2 ) ∈ ℝ* )
75 31 rpred ( 𝑤 ∈ ℝ+ → ( 𝑤 / 2 ) ∈ ℝ )
76 renepnf ( ( 𝑤 / 2 ) ∈ ℝ → ( 𝑤 / 2 ) ≠ +∞ )
77 75 76 syl ( 𝑤 ∈ ℝ+ → ( 𝑤 / 2 ) ≠ +∞ )
78 xaddmnf2 ( ( ( 𝑤 / 2 ) ∈ ℝ* ∧ ( 𝑤 / 2 ) ≠ +∞ ) → ( -∞ +𝑒 ( 𝑤 / 2 ) ) = -∞ )
79 74 77 78 syl2anc ( 𝑤 ∈ ℝ+ → ( -∞ +𝑒 ( 𝑤 / 2 ) ) = -∞ )
80 79 adantl ( ( 𝜑𝑤 ∈ ℝ+ ) → ( -∞ +𝑒 ( 𝑤 / 2 ) ) = -∞ )
81 80 ad2antrr ( ( ( ( 𝜑𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴 ) ∧ ¬ -∞ < 𝑦 ) → ( -∞ +𝑒 ( 𝑤 / 2 ) ) = -∞ )
82 73 81 eqtrd ( ( ( ( 𝜑𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴 ) ∧ ¬ -∞ < 𝑦 ) → ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) = -∞ )
83 82 adantl3r ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴 ) ∧ ¬ -∞ < 𝑦 ) → ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) = -∞ )
84 83 adantl3r ( ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴 ) ∧ ¬ -∞ < 𝑦 ) → ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) = -∞ )
85 84 3adantl3 ( ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) ∧ ¬ -∞ < 𝑦 ) → ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) = -∞ )
86 65 85 breqtrd ( ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) ∧ ¬ -∞ < 𝑦 ) → 𝐵 ≤ -∞ )
87 mnfle ( 𝐵 ∈ ℝ* → -∞ ≤ 𝐵 )
88 3 87 syl ( 𝜑 → -∞ ≤ 𝐵 )
89 88 adantr ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) → -∞ ≤ 𝐵 )
90 89 ad3antrrr ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ ¬ -∞ < 𝑦 ) → -∞ ≤ 𝐵 )
91 90 3ad2antl1 ( ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) ∧ ¬ -∞ < 𝑦 ) → -∞ ≤ 𝐵 )
92 62 64 86 91 xrletrid ( ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) ∧ ¬ -∞ < 𝑦 ) → 𝐵 = -∞ )
93 simpllr ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ ¬ -∞ < 𝑦 ) → 𝐵 ≠ -∞ )
94 93 3ad2antl1 ( ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) ∧ ¬ -∞ < 𝑦 ) → 𝐵 ≠ -∞ )
95 94 neneqd ( ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) ∧ ¬ -∞ < 𝑦 ) → ¬ 𝐵 = -∞ )
96 92 95 condan ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) → -∞ < 𝑦 )
97 simpr ( ( ( 𝜑𝑦𝐴 ) ∧ ¬ 𝑦 < +∞ ) → ¬ 𝑦 < +∞ )
98 67 adantr ( ( ( 𝜑𝑦𝐴 ) ∧ ¬ 𝑦 < +∞ ) → 𝑦 ∈ ℝ* )
99 nltpnft ( 𝑦 ∈ ℝ* → ( 𝑦 = +∞ ↔ ¬ 𝑦 < +∞ ) )
100 98 99 syl ( ( ( 𝜑𝑦𝐴 ) ∧ ¬ 𝑦 < +∞ ) → ( 𝑦 = +∞ ↔ ¬ 𝑦 < +∞ ) )
101 97 100 mpbird ( ( ( 𝜑𝑦𝐴 ) ∧ ¬ 𝑦 < +∞ ) → 𝑦 = +∞ )
102 101 eqcomd ( ( ( 𝜑𝑦𝐴 ) ∧ ¬ 𝑦 < +∞ ) → +∞ = 𝑦 )
103 simpr ( ( 𝜑𝑦𝐴 ) → 𝑦𝐴 )
104 103 adantr ( ( ( 𝜑𝑦𝐴 ) ∧ ¬ 𝑦 < +∞ ) → 𝑦𝐴 )
105 102 104 eqeltrd ( ( ( 𝜑𝑦𝐴 ) ∧ ¬ 𝑦 < +∞ ) → +∞ ∈ 𝐴 )
106 105 3adantl2 ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴𝑦𝐴 ) ∧ ¬ 𝑦 < +∞ ) → +∞ ∈ 𝐴 )
107 simpl2 ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴𝑦𝐴 ) ∧ ¬ 𝑦 < +∞ ) → ¬ +∞ ∈ 𝐴 )
108 106 107 condan ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴𝑦𝐴 ) → 𝑦 < +∞ )
109 108 ad5ant125 ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴 ) → 𝑦 < +∞ )
110 109 3adant3 ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) → 𝑦 < +∞ )
111 96 110 jca ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) → ( -∞ < 𝑦𝑦 < +∞ ) )
112 67 ad5ant15 ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴 ) → 𝑦 ∈ ℝ* )
113 112 3adant3 ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) → 𝑦 ∈ ℝ* )
114 xrrebnd ( 𝑦 ∈ ℝ* → ( 𝑦 ∈ ℝ ↔ ( -∞ < 𝑦𝑦 < +∞ ) ) )
115 113 114 syl ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) → ( 𝑦 ∈ ℝ ↔ ( -∞ < 𝑦𝑦 < +∞ ) ) )
116 111 115 mpbird ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) → 𝑦 ∈ ℝ )
117 75 adantl ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) → ( 𝑤 / 2 ) ∈ ℝ )
118 117 3ad2ant1 ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) → ( 𝑤 / 2 ) ∈ ℝ )
119 rexadd ( ( 𝑦 ∈ ℝ ∧ ( 𝑤 / 2 ) ∈ ℝ ) → ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) = ( 𝑦 + ( 𝑤 / 2 ) ) )
120 116 118 119 syl2anc ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) → ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) = ( 𝑦 + ( 𝑤 / 2 ) ) )
121 116 118 readdcld ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) → ( 𝑦 + ( 𝑤 / 2 ) ) ∈ ℝ )
122 120 121 eqeltrd ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) → ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ∈ ℝ )
123 122 rexrd ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) → ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ∈ ℝ* )
124 pnfxr +∞ ∈ ℝ*
125 124 a1i ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) → +∞ ∈ ℝ* )
126 simp3 ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) → 𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) )
127 122 ltpnfd ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) → ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) < +∞ )
128 61 123 125 126 127 xrlelttrd ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) → 𝐵 < +∞ )
129 59 128 jca ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) → ( -∞ < 𝐵𝐵 < +∞ ) )
130 xrrebnd ( 𝐵 ∈ ℝ* → ( 𝐵 ∈ ℝ ↔ ( -∞ < 𝐵𝐵 < +∞ ) ) )
131 61 130 syl ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) → ( 𝐵 ∈ ℝ ↔ ( -∞ < 𝐵𝐵 < +∞ ) ) )
132 129 131 mpbird ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) → 𝐵 ∈ ℝ )
133 rpre ( 𝑤 ∈ ℝ+𝑤 ∈ ℝ )
134 133 adantl ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) → 𝑤 ∈ ℝ )
135 134 3ad2ant1 ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) → 𝑤 ∈ ℝ )
136 rexadd ( ( 𝑦 ∈ ℝ ∧ 𝑤 ∈ ℝ ) → ( 𝑦 +𝑒 𝑤 ) = ( 𝑦 + 𝑤 ) )
137 116 135 136 syl2anc ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) → ( 𝑦 +𝑒 𝑤 ) = ( 𝑦 + 𝑤 ) )
138 116 135 readdcld ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) → ( 𝑦 + 𝑤 ) ∈ ℝ )
139 137 138 eqeltrd ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) → ( 𝑦 +𝑒 𝑤 ) ∈ ℝ )
140 rphalflt ( 𝑤 ∈ ℝ+ → ( 𝑤 / 2 ) < 𝑤 )
141 140 adantl ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) → ( 𝑤 / 2 ) < 𝑤 )
142 141 3ad2ant1 ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) → ( 𝑤 / 2 ) < 𝑤 )
143 118 135 116 142 ltadd2dd ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) → ( 𝑦 + ( 𝑤 / 2 ) ) < ( 𝑦 + 𝑤 ) )
144 120 137 breq12d ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) → ( ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) < ( 𝑦 +𝑒 𝑤 ) ↔ ( 𝑦 + ( 𝑤 / 2 ) ) < ( 𝑦 + 𝑤 ) ) )
145 143 144 mpbird ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) → ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) < ( 𝑦 +𝑒 𝑤 ) )
146 132 122 139 126 145 lelttrd ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑦𝐴𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) ) → 𝐵 < ( 𝑦 +𝑒 𝑤 ) )
147 146 3exp ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) → ( 𝑦𝐴 → ( 𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) → 𝐵 < ( 𝑦 +𝑒 𝑤 ) ) ) )
148 50 147 reximdai ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) → ( ∃ 𝑦𝐴 𝐵 ≤ ( 𝑦 +𝑒 ( 𝑤 / 2 ) ) → ∃ 𝑦𝐴 𝐵 < ( 𝑦 +𝑒 𝑤 ) ) )
149 49 148 mpd ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) ∧ 𝑤 ∈ ℝ+ ) → ∃ 𝑦𝐴 𝐵 < ( 𝑦 +𝑒 𝑤 ) )
150 25 27 29 149 supxrgelem ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ 𝐵 ≠ -∞ ) → 𝐵 ≤ sup ( 𝐴 , ℝ* , < ) )
151 22 24 150 syl2anc ( ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) ∧ ¬ 𝐵 = -∞ ) → 𝐵 ≤ sup ( 𝐴 , ℝ* , < ) )
152 21 151 pm2.61dan ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) → 𝐵 ≤ sup ( 𝐴 , ℝ* , < ) )
153 13 152 pm2.61dan ( 𝜑𝐵 ≤ sup ( 𝐴 , ℝ* , < ) )