| Step | Hyp | Ref
| Expression |
| 1 | | supxrge.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
| 2 | | pnfge 13172 |
. . . . 5
⊢ (𝐵 ∈ ℝ*
→ 𝐵 ≤
+∞) |
| 3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐵 ≤ +∞) |
| 4 | 3 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ +∞ ∈ 𝐴) → 𝐵 ≤ +∞) |
| 5 | | supxrge.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆
ℝ*) |
| 6 | 5 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ +∞ ∈ 𝐴) → 𝐴 ⊆
ℝ*) |
| 7 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ +∞ ∈ 𝐴) → +∞ ∈ 𝐴) |
| 8 | | supxrpnf 13360 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ*
∧ +∞ ∈ 𝐴)
→ sup(𝐴,
ℝ*, < ) = +∞) |
| 9 | 6, 7, 8 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ +∞ ∈ 𝐴) → sup(𝐴, ℝ*, < ) =
+∞) |
| 10 | 9 | eqcomd 2743 |
. . 3
⊢ ((𝜑 ∧ +∞ ∈ 𝐴) → +∞ = sup(𝐴, ℝ*, <
)) |
| 11 | 4, 10 | breqtrd 5169 |
. 2
⊢ ((𝜑 ∧ +∞ ∈ 𝐴) → 𝐵 ≤ sup(𝐴, ℝ*, <
)) |
| 12 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 = -∞) → 𝐵 = -∞) |
| 13 | | supxrcl 13357 |
. . . . . . . 8
⊢ (𝐴 ⊆ ℝ*
→ sup(𝐴,
ℝ*, < ) ∈ ℝ*) |
| 14 | 5, 13 | syl 17 |
. . . . . . 7
⊢ (𝜑 → sup(𝐴, ℝ*, < ) ∈
ℝ*) |
| 15 | | mnfle 13177 |
. . . . . . 7
⊢
(sup(𝐴,
ℝ*, < ) ∈ ℝ* → -∞ ≤
sup(𝐴, ℝ*,
< )) |
| 16 | 14, 15 | syl 17 |
. . . . . 6
⊢ (𝜑 → -∞ ≤ sup(𝐴, ℝ*, <
)) |
| 17 | 16 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 = -∞) → -∞ ≤ sup(𝐴, ℝ*, <
)) |
| 18 | 12, 17 | eqbrtrd 5165 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 = -∞) → 𝐵 ≤ sup(𝐴, ℝ*, <
)) |
| 19 | 18 | adantlr 715 |
. . 3
⊢ (((𝜑 ∧ ¬ +∞ ∈ 𝐴) ∧ 𝐵 = -∞) → 𝐵 ≤ sup(𝐴, ℝ*, <
)) |
| 20 | | simpl 482 |
. . . 4
⊢ (((𝜑 ∧ ¬ +∞ ∈ 𝐴) ∧ ¬ 𝐵 = -∞) → (𝜑 ∧ ¬ +∞ ∈ 𝐴)) |
| 21 | | neqne 2948 |
. . . . 5
⊢ (¬
𝐵 = -∞ → 𝐵 ≠ -∞) |
| 22 | 21 | adantl 481 |
. . . 4
⊢ (((𝜑 ∧ ¬ +∞ ∈ 𝐴) ∧ ¬ 𝐵 = -∞) → 𝐵 ≠ -∞) |
| 23 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑤((𝜑 ∧ ¬ +∞ ∈ 𝐴) ∧ 𝐵 ≠ -∞) |
| 24 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ +∞ ∈ 𝐴) → 𝐴 ⊆
ℝ*) |
| 25 | 24 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ ¬ +∞ ∈ 𝐴) ∧ 𝐵 ≠ -∞) → 𝐴 ⊆
ℝ*) |
| 26 | 1 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ +∞ ∈ 𝐴) → 𝐵 ∈
ℝ*) |
| 27 | 26 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ ¬ +∞ ∈ 𝐴) ∧ 𝐵 ≠ -∞) → 𝐵 ∈
ℝ*) |
| 28 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → 𝜑) |
| 29 | | rphalfcl 13062 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ℝ+
→ (𝑤 / 2) ∈
ℝ+) |
| 30 | 29 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → (𝑤 / 2) ∈
ℝ+) |
| 31 | | ovex 7464 |
. . . . . . . . . 10
⊢ (𝑤 / 2) ∈ V |
| 32 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(𝑤 / 2) |
| 33 | | supxrge.xph |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥𝜑 |
| 34 | | nfv 1914 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝑤 / 2) ∈
ℝ+ |
| 35 | 33, 34 | nfan 1899 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(𝜑 ∧ (𝑤 / 2) ∈
ℝ+) |
| 36 | | nfv 1914 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥∃𝑦 ∈ 𝐴 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2)) |
| 37 | 35, 36 | nfim 1896 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥((𝜑 ∧ (𝑤 / 2) ∈ ℝ+) →
∃𝑦 ∈ 𝐴 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) |
| 38 | | eleq1 2829 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑤 / 2) → (𝑥 ∈ ℝ+ ↔ (𝑤 / 2) ∈
ℝ+)) |
| 39 | 38 | anbi2d 630 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑤 / 2) → ((𝜑 ∧ 𝑥 ∈ ℝ+) ↔ (𝜑 ∧ (𝑤 / 2) ∈
ℝ+))) |
| 40 | | oveq2 7439 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑤 / 2) → (𝑦 +𝑒 𝑥) = (𝑦 +𝑒 (𝑤 / 2))) |
| 41 | 40 | breq2d 5155 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑤 / 2) → (𝐵 ≤ (𝑦 +𝑒 𝑥) ↔ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2)))) |
| 42 | 41 | rexbidv 3179 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑤 / 2) → (∃𝑦 ∈ 𝐴 𝐵 ≤ (𝑦 +𝑒 𝑥) ↔ ∃𝑦 ∈ 𝐴 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2)))) |
| 43 | 39, 42 | imbi12d 344 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑤 / 2) → (((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑦 ∈ 𝐴 𝐵 ≤ (𝑦 +𝑒 𝑥)) ↔ ((𝜑 ∧ (𝑤 / 2) ∈ ℝ+) →
∃𝑦 ∈ 𝐴 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))))) |
| 44 | | supxrge.y |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑦 ∈ 𝐴 𝐵 ≤ (𝑦 +𝑒 𝑥)) |
| 45 | 32, 37, 43, 44 | vtoclgf 3569 |
. . . . . . . . . 10
⊢ ((𝑤 / 2) ∈ V → ((𝜑 ∧ (𝑤 / 2) ∈ ℝ+) →
∃𝑦 ∈ 𝐴 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2)))) |
| 46 | 31, 45 | ax-mp 5 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑤 / 2) ∈ ℝ+) →
∃𝑦 ∈ 𝐴 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) |
| 47 | 28, 30, 46 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
∃𝑦 ∈ 𝐴 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) |
| 48 | 47 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ +∞ ∈ 𝐴) ∧ 𝑤 ∈ ℝ+) →
∃𝑦 ∈ 𝐴 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) |
| 49 | 48 | adantlr 715 |
. . . . . 6
⊢ ((((𝜑 ∧ ¬ +∞ ∈ 𝐴) ∧ 𝐵 ≠ -∞) ∧ 𝑤 ∈ ℝ+) →
∃𝑦 ∈ 𝐴 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) |
| 50 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑦(((𝜑 ∧ ¬ +∞ ∈ 𝐴) ∧ 𝐵 ≠ -∞) ∧ 𝑤 ∈ ℝ+) |
| 51 | | neneq 2946 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ≠ -∞ → ¬
𝐵 =
-∞) |
| 52 | 51 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐵 ≠ -∞) → ¬ 𝐵 = -∞) |
| 53 | 1 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐵 ≠ -∞) → 𝐵 ∈
ℝ*) |
| 54 | | ngtmnft 13208 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ ℝ*
→ (𝐵 = -∞ ↔
¬ -∞ < 𝐵)) |
| 55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐵 ≠ -∞) → (𝐵 = -∞ ↔ ¬ -∞ < 𝐵)) |
| 56 | 52, 55 | mtbid 324 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐵 ≠ -∞) → ¬ ¬ -∞
< 𝐵) |
| 57 | 56 | notnotrd 133 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐵 ≠ -∞) → -∞ < 𝐵) |
| 58 | 57 | ad4ant13 751 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ 𝐴) ∧ 𝐵 ≠ -∞) ∧ 𝑤 ∈ ℝ+) → -∞
< 𝐵) |
| 59 | 58 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) → -∞ < 𝐵) |
| 60 | 27 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ¬ +∞ ∈ 𝐴) ∧ 𝐵 ≠ -∞) ∧ 𝑤 ∈ ℝ+) → 𝐵 ∈
ℝ*) |
| 61 | 60 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) → 𝐵 ∈
ℝ*) |
| 62 | 61 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) ∧ ¬ -∞ < 𝑦) → 𝐵 ∈
ℝ*) |
| 63 | | mnfxr 11318 |
. . . . . . . . . . . . . . . . . . . 20
⊢ -∞
∈ ℝ* |
| 64 | 63 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) ∧ ¬ -∞ < 𝑦) → -∞ ∈
ℝ*) |
| 65 | | simpl3 1194 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) ∧ ¬ -∞ < 𝑦) → 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) |
| 66 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ -∞ < 𝑦) → ¬ -∞ <
𝑦) |
| 67 | 5 | sselda 3983 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ*) |
| 68 | 67 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ -∞ < 𝑦) → 𝑦 ∈ ℝ*) |
| 69 | | ngtmnft 13208 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 ∈ ℝ*
→ (𝑦 = -∞ ↔
¬ -∞ < 𝑦)) |
| 70 | 68, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ -∞ < 𝑦) → (𝑦 = -∞ ↔ ¬ -∞ < 𝑦)) |
| 71 | 66, 70 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ -∞ < 𝑦) → 𝑦 = -∞) |
| 72 | 71 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ -∞ < 𝑦) → (𝑦 +𝑒 (𝑤 / 2)) = (-∞ +𝑒
(𝑤 / 2))) |
| 73 | 72 | adantllr 719 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑦 ∈ 𝐴) ∧ ¬ -∞ < 𝑦) → (𝑦 +𝑒 (𝑤 / 2)) = (-∞ +𝑒
(𝑤 / 2))) |
| 74 | 29 | rpxrd 13078 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 ∈ ℝ+
→ (𝑤 / 2) ∈
ℝ*) |
| 75 | 29 | rpred 13077 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑤 ∈ ℝ+
→ (𝑤 / 2) ∈
ℝ) |
| 76 | | renepnf 11309 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑤 / 2) ∈ ℝ →
(𝑤 / 2) ≠
+∞) |
| 77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 ∈ ℝ+
→ (𝑤 / 2) ≠
+∞) |
| 78 | | xaddmnf2 13271 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑤 / 2) ∈ ℝ*
∧ (𝑤 / 2) ≠
+∞) → (-∞ +𝑒 (𝑤 / 2)) = -∞) |
| 79 | 74, 77, 78 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑤 ∈ ℝ+
→ (-∞ +𝑒 (𝑤 / 2)) = -∞) |
| 80 | 79 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → (-∞
+𝑒 (𝑤 /
2)) = -∞) |
| 81 | 80 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑦 ∈ 𝐴) ∧ ¬ -∞ < 𝑦) → (-∞
+𝑒 (𝑤 /
2)) = -∞) |
| 82 | 73, 81 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑦 ∈ 𝐴) ∧ ¬ -∞ < 𝑦) → (𝑦 +𝑒 (𝑤 / 2)) = -∞) |
| 83 | 82 | adantl3r 750 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴) ∧ ¬ -∞ < 𝑦) → (𝑦 +𝑒 (𝑤 / 2)) = -∞) |
| 84 | 83 | adantl3r 750 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴) ∧ ¬ -∞ < 𝑦) → (𝑦 +𝑒 (𝑤 / 2)) = -∞) |
| 85 | 84 | 3adantl3 1169 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) ∧ ¬ -∞ < 𝑦) → (𝑦 +𝑒 (𝑤 / 2)) = -∞) |
| 86 | 65, 85 | breqtrd 5169 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) ∧ ¬ -∞ < 𝑦) → 𝐵 ≤ -∞) |
| 87 | | mnfle 13177 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐵 ∈ ℝ*
→ -∞ ≤ 𝐵) |
| 88 | 1, 87 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → -∞ ≤ 𝐵) |
| 89 | 88 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ ¬ +∞ ∈ 𝐴) → -∞ ≤ 𝐵) |
| 90 | 89 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ ¬ -∞ < 𝑦) → -∞ ≤ 𝐵) |
| 91 | 90 | 3ad2antl1 1186 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) ∧ ¬ -∞ < 𝑦) → -∞ ≤ 𝐵) |
| 92 | 62, 64, 86, 91 | xrletrid 13197 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) ∧ ¬ -∞ < 𝑦) → 𝐵 = -∞) |
| 93 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ ¬ -∞ < 𝑦) → 𝐵 ≠ -∞) |
| 94 | 93 | 3ad2antl1 1186 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) ∧ ¬ -∞ < 𝑦) → 𝐵 ≠ -∞) |
| 95 | 94 | neneqd 2945 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) ∧ ¬ -∞ < 𝑦) → ¬ 𝐵 = -∞) |
| 96 | 92, 95 | condan 818 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) → -∞ < 𝑦) |
| 97 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 < +∞) → ¬ 𝑦 < +∞) |
| 98 | 67 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 < +∞) → 𝑦 ∈ ℝ*) |
| 99 | | nltpnft 13206 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ ℝ*
→ (𝑦 = +∞ ↔
¬ 𝑦 <
+∞)) |
| 100 | 98, 99 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 < +∞) → (𝑦 = +∞ ↔ ¬ 𝑦 < +∞)) |
| 101 | 97, 100 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 < +∞) → 𝑦 = +∞) |
| 102 | 101 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 < +∞) → +∞ = 𝑦) |
| 103 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴) |
| 104 | 103 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 < +∞) → 𝑦 ∈ 𝐴) |
| 105 | 102, 104 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 < +∞) → +∞ ∈ 𝐴) |
| 106 | 105 | 3adantl2 1168 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ ¬ +∞ ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 < +∞) → +∞ ∈ 𝐴) |
| 107 | | simpl2 1193 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ ¬ +∞ ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 < +∞) → ¬ +∞ ∈
𝐴) |
| 108 | 106, 107 | condan 818 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ ¬ +∞ ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝑦 < +∞) |
| 109 | 108 | ad5ant125 1368 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴) → 𝑦 < +∞) |
| 110 | 109 | 3adant3 1133 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) → 𝑦 < +∞) |
| 111 | 96, 110 | jca 511 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) → (-∞ < 𝑦 ∧ 𝑦 < +∞)) |
| 112 | 67 | ad5ant15 759 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ*) |
| 113 | 112 | 3adant3 1133 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) → 𝑦 ∈ ℝ*) |
| 114 | | xrrebnd 13210 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℝ*
→ (𝑦 ∈ ℝ
↔ (-∞ < 𝑦
∧ 𝑦 <
+∞))) |
| 115 | 113, 114 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) → (𝑦 ∈ ℝ ↔ (-∞ < 𝑦 ∧ 𝑦 < +∞))) |
| 116 | 111, 115 | mpbird 257 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) → 𝑦 ∈ ℝ) |
| 117 | 75 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ ¬ +∞ ∈ 𝐴) ∧ 𝐵 ≠ -∞) ∧ 𝑤 ∈ ℝ+) → (𝑤 / 2) ∈
ℝ) |
| 118 | 117 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) → (𝑤 / 2) ∈ ℝ) |
| 119 | | rexadd 13274 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℝ ∧ (𝑤 / 2) ∈ ℝ) →
(𝑦 +𝑒
(𝑤 / 2)) = (𝑦 + (𝑤 / 2))) |
| 120 | 116, 118,
119 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) → (𝑦 +𝑒 (𝑤 / 2)) = (𝑦 + (𝑤 / 2))) |
| 121 | 116, 118 | readdcld 11290 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) → (𝑦 + (𝑤 / 2)) ∈ ℝ) |
| 122 | 120, 121 | eqeltrd 2841 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) → (𝑦 +𝑒 (𝑤 / 2)) ∈ ℝ) |
| 123 | 122 | rexrd 11311 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) → (𝑦 +𝑒 (𝑤 / 2)) ∈
ℝ*) |
| 124 | | pnfxr 11315 |
. . . . . . . . . . . . 13
⊢ +∞
∈ ℝ* |
| 125 | 124 | a1i 11 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) → +∞ ∈
ℝ*) |
| 126 | | simp3 1139 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) → 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) |
| 127 | 122 | ltpnfd 13163 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) → (𝑦 +𝑒 (𝑤 / 2)) < +∞) |
| 128 | 61, 123, 125, 126, 127 | xrlelttrd 13202 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) → 𝐵 < +∞) |
| 129 | 59, 128 | jca 511 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) → (-∞ < 𝐵 ∧ 𝐵 < +∞)) |
| 130 | | xrrebnd 13210 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ*
→ (𝐵 ∈ ℝ
↔ (-∞ < 𝐵
∧ 𝐵 <
+∞))) |
| 131 | 61, 130 | syl 17 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) → (𝐵 ∈ ℝ ↔ (-∞ < 𝐵 ∧ 𝐵 < +∞))) |
| 132 | 129, 131 | mpbird 257 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) → 𝐵 ∈ ℝ) |
| 133 | | rpre 13043 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ ℝ+
→ 𝑤 ∈
ℝ) |
| 134 | 133 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ 𝐴) ∧ 𝐵 ≠ -∞) ∧ 𝑤 ∈ ℝ+) → 𝑤 ∈
ℝ) |
| 135 | 134 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) → 𝑤 ∈ ℝ) |
| 136 | | rexadd 13274 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℝ ∧ 𝑤 ∈ ℝ) → (𝑦 +𝑒 𝑤) = (𝑦 + 𝑤)) |
| 137 | 116, 135,
136 | syl2anc 584 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) → (𝑦 +𝑒 𝑤) = (𝑦 + 𝑤)) |
| 138 | 116, 135 | readdcld 11290 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) → (𝑦 + 𝑤) ∈ ℝ) |
| 139 | 137, 138 | eqeltrd 2841 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) → (𝑦 +𝑒 𝑤) ∈ ℝ) |
| 140 | | rphalflt 13064 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ ℝ+
→ (𝑤 / 2) < 𝑤) |
| 141 | 140 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ 𝐴) ∧ 𝐵 ≠ -∞) ∧ 𝑤 ∈ ℝ+) → (𝑤 / 2) < 𝑤) |
| 142 | 141 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) → (𝑤 / 2) < 𝑤) |
| 143 | 118, 135,
116, 142 | ltadd2dd 11420 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) → (𝑦 + (𝑤 / 2)) < (𝑦 + 𝑤)) |
| 144 | 120, 137 | breq12d 5156 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) → ((𝑦 +𝑒 (𝑤 / 2)) < (𝑦 +𝑒 𝑤) ↔ (𝑦 + (𝑤 / 2)) < (𝑦 + 𝑤))) |
| 145 | 143, 144 | mpbird 257 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) → (𝑦 +𝑒 (𝑤 / 2)) < (𝑦 +𝑒 𝑤)) |
| 146 | 132, 122,
139, 126, 145 | lelttrd 11419 |
. . . . . . . 8
⊢
(((((𝜑 ∧ ¬
+∞ ∈ 𝐴) ∧
𝐵 ≠ -∞) ∧
𝑤 ∈
ℝ+) ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2))) → 𝐵 < (𝑦 +𝑒 𝑤)) |
| 147 | 146 | 3exp 1120 |
. . . . . . 7
⊢ ((((𝜑 ∧ ¬ +∞ ∈ 𝐴) ∧ 𝐵 ≠ -∞) ∧ 𝑤 ∈ ℝ+) → (𝑦 ∈ 𝐴 → (𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2)) → 𝐵 < (𝑦 +𝑒 𝑤)))) |
| 148 | 50, 147 | reximdai 3261 |
. . . . . 6
⊢ ((((𝜑 ∧ ¬ +∞ ∈ 𝐴) ∧ 𝐵 ≠ -∞) ∧ 𝑤 ∈ ℝ+) →
(∃𝑦 ∈ 𝐴 𝐵 ≤ (𝑦 +𝑒 (𝑤 / 2)) → ∃𝑦 ∈ 𝐴 𝐵 < (𝑦 +𝑒 𝑤))) |
| 149 | 49, 148 | mpd 15 |
. . . . 5
⊢ ((((𝜑 ∧ ¬ +∞ ∈ 𝐴) ∧ 𝐵 ≠ -∞) ∧ 𝑤 ∈ ℝ+) →
∃𝑦 ∈ 𝐴 𝐵 < (𝑦 +𝑒 𝑤)) |
| 150 | 23, 25, 27, 149 | supxrgelem 45348 |
. . . 4
⊢ (((𝜑 ∧ ¬ +∞ ∈ 𝐴) ∧ 𝐵 ≠ -∞) → 𝐵 ≤ sup(𝐴, ℝ*, <
)) |
| 151 | 20, 22, 150 | syl2anc 584 |
. . 3
⊢ (((𝜑 ∧ ¬ +∞ ∈ 𝐴) ∧ ¬ 𝐵 = -∞) → 𝐵 ≤ sup(𝐴, ℝ*, <
)) |
| 152 | 19, 151 | pm2.61dan 813 |
. 2
⊢ ((𝜑 ∧ ¬ +∞ ∈ 𝐴) → 𝐵 ≤ sup(𝐴, ℝ*, <
)) |
| 153 | 11, 152 | pm2.61dan 813 |
1
⊢ (𝜑 → 𝐵 ≤ sup(𝐴, ℝ*, <
)) |