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 ( 𝐴 , ℝ* , < ) )