Proof of Theorem supxrgelem
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | supxrgelem.b | . . . . 5
⊢ (𝜑 → 𝐵 ∈
ℝ*) | 
| 2 |  | pnfge 13173 | . . . . 5
⊢ (𝐵 ∈ ℝ*
→ 𝐵 ≤
+∞) | 
| 3 | 1, 2 | syl 17 | . . . 4
⊢ (𝜑 → 𝐵 ≤ +∞) | 
| 4 | 3 | adantr 480 | . . 3
⊢ ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞)
→ 𝐵 ≤
+∞) | 
| 5 |  | id 22 | . . . . 5
⊢
(sup(𝐴,
ℝ*, < ) = +∞ → sup(𝐴, ℝ*, < ) =
+∞) | 
| 6 | 5 | eqcomd 2742 | . . . 4
⊢
(sup(𝐴,
ℝ*, < ) = +∞ → +∞ = sup(𝐴, ℝ*, <
)) | 
| 7 | 6 | adantl 481 | . . 3
⊢ ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞)
→ +∞ = sup(𝐴,
ℝ*, < )) | 
| 8 | 4, 7 | breqtrd 5168 | . 2
⊢ ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞)
→ 𝐵 ≤ sup(𝐴, ℝ*, <
)) | 
| 9 |  | simpl 482 | . . 3
⊢ ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞)
→ 𝜑) | 
| 10 |  | 1rp 13039 | . . . . . . . 8
⊢ 1 ∈
ℝ+ | 
| 11 |  | nfcv 2904 | . . . . . . . . . 10
⊢
Ⅎ𝑥1 | 
| 12 |  | supxrgelem.xph | . . . . . . . . . . . 12
⊢
Ⅎ𝑥𝜑 | 
| 13 |  | nfv 1913 | . . . . . . . . . . . 12
⊢
Ⅎ𝑥1 ∈
ℝ+ | 
| 14 | 12, 13 | nfan 1898 | . . . . . . . . . . 11
⊢
Ⅎ𝑥(𝜑 ∧ 1 ∈
ℝ+) | 
| 15 |  | nfv 1913 | . . . . . . . . . . 11
⊢
Ⅎ𝑥∃𝑦 ∈ 𝐴 𝐵 < (𝑦 +𝑒 1) | 
| 16 | 14, 15 | nfim 1895 | . . . . . . . . . 10
⊢
Ⅎ𝑥((𝜑 ∧ 1 ∈
ℝ+) → ∃𝑦 ∈ 𝐴 𝐵 < (𝑦 +𝑒 1)) | 
| 17 |  | eleq1 2828 | . . . . . . . . . . . 12
⊢ (𝑥 = 1 → (𝑥 ∈ ℝ+ ↔ 1 ∈
ℝ+)) | 
| 18 | 17 | anbi2d 630 | . . . . . . . . . . 11
⊢ (𝑥 = 1 → ((𝜑 ∧ 𝑥 ∈ ℝ+) ↔ (𝜑 ∧ 1 ∈
ℝ+))) | 
| 19 |  | oveq2 7440 | . . . . . . . . . . . . 13
⊢ (𝑥 = 1 → (𝑦 +𝑒 𝑥) = (𝑦 +𝑒 1)) | 
| 20 | 19 | breq2d 5154 | . . . . . . . . . . . 12
⊢ (𝑥 = 1 → (𝐵 < (𝑦 +𝑒 𝑥) ↔ 𝐵 < (𝑦 +𝑒 1))) | 
| 21 | 20 | rexbidv 3178 | . . . . . . . . . . 11
⊢ (𝑥 = 1 → (∃𝑦 ∈ 𝐴 𝐵 < (𝑦 +𝑒 𝑥) ↔ ∃𝑦 ∈ 𝐴 𝐵 < (𝑦 +𝑒 1))) | 
| 22 | 18, 21 | imbi12d 344 | . . . . . . . . . 10
⊢ (𝑥 = 1 → (((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑦 ∈ 𝐴 𝐵 < (𝑦 +𝑒 𝑥)) ↔ ((𝜑 ∧ 1 ∈ ℝ+) →
∃𝑦 ∈ 𝐴 𝐵 < (𝑦 +𝑒 1)))) | 
| 23 |  | supxrgelem.y | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑦 ∈ 𝐴 𝐵 < (𝑦 +𝑒 𝑥)) | 
| 24 | 11, 16, 22, 23 | vtoclgf 3568 | . . . . . . . . 9
⊢ (1 ∈
ℝ+ → ((𝜑 ∧ 1 ∈ ℝ+) →
∃𝑦 ∈ 𝐴 𝐵 < (𝑦 +𝑒 1))) | 
| 25 | 10, 24 | ax-mp 5 | . . . . . . . 8
⊢ ((𝜑 ∧ 1 ∈
ℝ+) → ∃𝑦 ∈ 𝐴 𝐵 < (𝑦 +𝑒 1)) | 
| 26 | 10, 25 | mpan2 691 | . . . . . . 7
⊢ (𝜑 → ∃𝑦 ∈ 𝐴 𝐵 < (𝑦 +𝑒 1)) | 
| 27 | 26 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞)
→ ∃𝑦 ∈
𝐴 𝐵 < (𝑦 +𝑒 1)) | 
| 28 |  | mnfxr 11319 | . . . . . . . . . . 11
⊢ -∞
∈ ℝ* | 
| 29 | 28 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 < (𝑦 +𝑒 1)) → -∞
∈ ℝ*) | 
| 30 |  | supxrgelem.a | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ⊆
ℝ*) | 
| 31 | 30 | sselda 3982 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ*) | 
| 32 | 31 | 3adant3 1132 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 < (𝑦 +𝑒 1)) → 𝑦 ∈
ℝ*) | 
| 33 |  | supxrcl 13358 | . . . . . . . . . . . 12
⊢ (𝐴 ⊆ ℝ*
→ sup(𝐴,
ℝ*, < ) ∈ ℝ*) | 
| 34 | 30, 33 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → sup(𝐴, ℝ*, < ) ∈
ℝ*) | 
| 35 | 34 | 3ad2ant1 1133 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 < (𝑦 +𝑒 1)) → sup(𝐴, ℝ*, < )
∈ ℝ*) | 
| 36 |  | simpl3 1193 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 < (𝑦 +𝑒 1)) ∧ ¬
-∞ < 𝑦) →
𝐵 < (𝑦 +𝑒 1)) | 
| 37 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ -∞ < 𝑦) → ¬ -∞ <
𝑦) | 
| 38 | 31 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ -∞ < 𝑦) → 𝑦 ∈ ℝ*) | 
| 39 |  | ngtmnft 13209 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℝ*
→ (𝑦 = -∞ ↔
¬ -∞ < 𝑦)) | 
| 40 | 38, 39 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ -∞ < 𝑦) → (𝑦 = -∞ ↔ ¬ -∞ < 𝑦)) | 
| 41 | 37, 40 | mpbird 257 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ -∞ < 𝑦) → 𝑦 = -∞) | 
| 42 | 41 | oveq1d 7447 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ -∞ < 𝑦) → (𝑦 +𝑒 1) = (-∞
+𝑒 1)) | 
| 43 |  | 1xr 11321 | . . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℝ* | 
| 44 | 43 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ -∞ < 𝑦) → 1 ∈
ℝ*) | 
| 45 |  | 1re 11262 | . . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℝ | 
| 46 |  | renepnf 11310 | . . . . . . . . . . . . . . . . 17
⊢ (1 ∈
ℝ → 1 ≠ +∞) | 
| 47 | 45, 46 | ax-mp 5 | . . . . . . . . . . . . . . . 16
⊢ 1 ≠
+∞ | 
| 48 | 47 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ -∞ < 𝑦) → 1 ≠
+∞) | 
| 49 |  | xaddmnf2 13272 | . . . . . . . . . . . . . . 15
⊢ ((1
∈ ℝ* ∧ 1 ≠ +∞) → (-∞
+𝑒 1) = -∞) | 
| 50 | 44, 48, 49 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ -∞ < 𝑦) → (-∞
+𝑒 1) = -∞) | 
| 51 | 42, 50 | eqtrd 2776 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ -∞ < 𝑦) → (𝑦 +𝑒 1) =
-∞) | 
| 52 | 51 | 3adantl3 1168 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 < (𝑦 +𝑒 1)) ∧ ¬
-∞ < 𝑦) →
(𝑦 +𝑒 1)
= -∞) | 
| 53 | 36, 52 | breqtrd 5168 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 < (𝑦 +𝑒 1)) ∧ ¬
-∞ < 𝑦) →
𝐵 <
-∞) | 
| 54 |  | nltmnf 13172 | . . . . . . . . . . . . . 14
⊢ (𝐵 ∈ ℝ*
→ ¬ 𝐵 <
-∞) | 
| 55 | 1, 54 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → ¬ 𝐵 < -∞) | 
| 56 | 55 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ -∞ < 𝑦) → ¬ 𝐵 < -∞) | 
| 57 | 56 | 3ad2antl1 1185 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 < (𝑦 +𝑒 1)) ∧ ¬
-∞ < 𝑦) →
¬ 𝐵 <
-∞) | 
| 58 | 53, 57 | condan 817 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 < (𝑦 +𝑒 1)) → -∞
< 𝑦) | 
| 59 | 30 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐴 ⊆
ℝ*) | 
| 60 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴) | 
| 61 |  | supxrub 13367 | . . . . . . . . . . . 12
⊢ ((𝐴 ⊆ ℝ*
∧ 𝑦 ∈ 𝐴) → 𝑦 ≤ sup(𝐴, ℝ*, <
)) | 
| 62 | 59, 60, 61 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ≤ sup(𝐴, ℝ*, <
)) | 
| 63 | 62 | 3adant3 1132 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 < (𝑦 +𝑒 1)) → 𝑦 ≤ sup(𝐴, ℝ*, <
)) | 
| 64 | 29, 32, 35, 58, 63 | xrltletrd 13204 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 < (𝑦 +𝑒 1)) → -∞
< sup(𝐴,
ℝ*, < )) | 
| 65 | 64 | 3exp 1119 | . . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ 𝐴 → (𝐵 < (𝑦 +𝑒 1) → -∞
< sup(𝐴,
ℝ*, < )))) | 
| 66 | 65 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞)
→ (𝑦 ∈ 𝐴 → (𝐵 < (𝑦 +𝑒 1) → -∞
< sup(𝐴,
ℝ*, < )))) | 
| 67 | 66 | rexlimdv 3152 | . . . . . 6
⊢ ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞)
→ (∃𝑦 ∈
𝐴 𝐵 < (𝑦 +𝑒 1) → -∞
< sup(𝐴,
ℝ*, < ))) | 
| 68 | 27, 67 | mpd 15 | . . . . 5
⊢ ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞)
→ -∞ < sup(𝐴,
ℝ*, < )) | 
| 69 |  | simpr 484 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞)
→ ¬ sup(𝐴,
ℝ*, < ) = +∞) | 
| 70 |  | nltpnft 13207 | . . . . . . . . 9
⊢
(sup(𝐴,
ℝ*, < ) ∈ ℝ* → (sup(𝐴, ℝ*, < ) =
+∞ ↔ ¬ sup(𝐴, ℝ*, < ) <
+∞)) | 
| 71 | 34, 70 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (sup(𝐴, ℝ*, < ) = +∞
↔ ¬ sup(𝐴,
ℝ*, < ) < +∞)) | 
| 72 | 71 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞)
→ (sup(𝐴,
ℝ*, < ) = +∞ ↔ ¬ sup(𝐴, ℝ*, < ) <
+∞)) | 
| 73 | 69, 72 | mtbid 324 | . . . . . 6
⊢ ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞)
→ ¬ ¬ sup(𝐴,
ℝ*, < ) < +∞) | 
| 74 | 73 | notnotrd 133 | . . . . 5
⊢ ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞)
→ sup(𝐴,
ℝ*, < ) < +∞) | 
| 75 | 68, 74 | jca 511 | . . . 4
⊢ ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞)
→ (-∞ < sup(𝐴, ℝ*, < ) ∧
sup(𝐴, ℝ*,
< ) < +∞)) | 
| 76 | 34 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞)
→ sup(𝐴,
ℝ*, < ) ∈ ℝ*) | 
| 77 |  | xrrebnd 13211 | . . . . 5
⊢
(sup(𝐴,
ℝ*, < ) ∈ ℝ* → (sup(𝐴, ℝ*, < )
∈ ℝ ↔ (-∞ < sup(𝐴, ℝ*, < ) ∧
sup(𝐴, ℝ*,
< ) < +∞))) | 
| 78 | 76, 77 | syl 17 | . . . 4
⊢ ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞)
→ (sup(𝐴,
ℝ*, < ) ∈ ℝ ↔ (-∞ < sup(𝐴, ℝ*, < )
∧ sup(𝐴,
ℝ*, < ) < +∞))) | 
| 79 | 75, 78 | mpbird 257 | . . 3
⊢ ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞)
→ sup(𝐴,
ℝ*, < ) ∈ ℝ) | 
| 80 |  | simpl 482 | . . . . 5
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ ¬ 𝐵 ≤
sup(𝐴, ℝ*,
< )) → (𝜑 ∧
sup(𝐴, ℝ*,
< ) ∈ ℝ)) | 
| 81 |  | simpr 484 | . . . . . 6
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ ¬ 𝐵 ≤
sup(𝐴, ℝ*,
< )) → ¬ 𝐵 ≤
sup(𝐴, ℝ*,
< )) | 
| 82 | 34 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) →
sup(𝐴, ℝ*,
< ) ∈ ℝ*) | 
| 83 | 1 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) → 𝐵 ∈
ℝ*) | 
| 84 |  | xrltnle 11329 | . . . . . . . 8
⊢
((sup(𝐴,
ℝ*, < ) ∈ ℝ* ∧ 𝐵 ∈ ℝ*) →
(sup(𝐴,
ℝ*, < ) < 𝐵 ↔ ¬ 𝐵 ≤ sup(𝐴, ℝ*, <
))) | 
| 85 | 82, 83, 84 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐵 ≤ sup(𝐴, ℝ*, < )) →
(sup(𝐴,
ℝ*, < ) < 𝐵 ↔ ¬ 𝐵 ≤ sup(𝐴, ℝ*, <
))) | 
| 86 | 85 | adantlr 715 | . . . . . 6
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ ¬ 𝐵 ≤
sup(𝐴, ℝ*,
< )) → (sup(𝐴,
ℝ*, < ) < 𝐵 ↔ ¬ 𝐵 ≤ sup(𝐴, ℝ*, <
))) | 
| 87 | 81, 86 | mpbird 257 | . . . . 5
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ ¬ 𝐵 ≤
sup(𝐴, ℝ*,
< )) → sup(𝐴,
ℝ*, < ) < 𝐵) | 
| 88 |  | simpll 766 | . . . . . . 7
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → 𝜑) | 
| 89 | 28 | a1i 11 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → -∞ ∈
ℝ*) | 
| 90 | 88, 34 | syl 17 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → sup(𝐴, ℝ*, < ) ∈
ℝ*) | 
| 91 | 88, 1 | syl 17 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → 𝐵 ∈
ℝ*) | 
| 92 |  | mnfle 13178 | . . . . . . . . . . . . . 14
⊢
(sup(𝐴,
ℝ*, < ) ∈ ℝ* → -∞ ≤
sup(𝐴, ℝ*,
< )) | 
| 93 | 34, 92 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → -∞ ≤ sup(𝐴, ℝ*, <
)) | 
| 94 | 93 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → -∞ ≤ sup(𝐴, ℝ*, <
)) | 
| 95 |  | simpr 484 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → sup(𝐴, ℝ*, < ) < 𝐵) | 
| 96 | 89, 90, 91, 94, 95 | xrlelttrd 13203 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → -∞ < 𝐵) | 
| 97 |  | id 22 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝜑) | 
| 98 | 10 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ∈
ℝ+) | 
| 99 | 97, 98, 25 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (𝜑 → ∃𝑦 ∈ 𝐴 𝐵 < (𝑦 +𝑒 1)) | 
| 100 | 99 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → ∃𝑦 ∈ 𝐴 𝐵 < (𝑦 +𝑒 1)) | 
| 101 | 1 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 < (𝑦 +𝑒 1)) → 𝐵 ∈
ℝ*) | 
| 102 | 43 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 < (𝑦 +𝑒 1)) → 1 ∈
ℝ*) | 
| 103 | 32, 102 | jca 511 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 < (𝑦 +𝑒 1)) → (𝑦 ∈ ℝ*
∧ 1 ∈ ℝ*)) | 
| 104 |  | xaddcl 13282 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ*
∧ 1 ∈ ℝ*) → (𝑦 +𝑒 1) ∈
ℝ*) | 
| 105 | 103, 104 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 < (𝑦 +𝑒 1)) → (𝑦 +𝑒 1) ∈
ℝ*) | 
| 106 |  | pnfxr 11316 | . . . . . . . . . . . . . . . . 17
⊢ +∞
∈ ℝ* | 
| 107 | 106 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 < (𝑦 +𝑒 1)) → +∞
∈ ℝ*) | 
| 108 |  | simp3 1138 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 < (𝑦 +𝑒 1)) → 𝐵 < (𝑦 +𝑒 1)) | 
| 109 | 31, 43, 104 | sylancl 586 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑦 +𝑒 1) ∈
ℝ*) | 
| 110 |  | pnfge 13173 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 +𝑒 1) ∈
ℝ* → (𝑦 +𝑒 1) ≤
+∞) | 
| 111 | 109, 110 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑦 +𝑒 1) ≤
+∞) | 
| 112 | 111 | 3adant3 1132 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 < (𝑦 +𝑒 1)) → (𝑦 +𝑒 1) ≤
+∞) | 
| 113 | 101, 105,
107, 108, 112 | xrltletrd 13204 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝐵 < (𝑦 +𝑒 1)) → 𝐵 < +∞) | 
| 114 | 113 | 3exp 1119 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑦 ∈ 𝐴 → (𝐵 < (𝑦 +𝑒 1) → 𝐵 <
+∞))) | 
| 115 | 114 | rexlimdv 3152 | . . . . . . . . . . . . 13
⊢ (𝜑 → (∃𝑦 ∈ 𝐴 𝐵 < (𝑦 +𝑒 1) → 𝐵 <
+∞)) | 
| 116 | 88, 115 | syl 17 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → (∃𝑦 ∈ 𝐴 𝐵 < (𝑦 +𝑒 1) → 𝐵 <
+∞)) | 
| 117 | 100, 116 | mpd 15 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → 𝐵 < +∞) | 
| 118 | 96, 117 | jca 511 | . . . . . . . . . 10
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → (-∞ < 𝐵 ∧ 𝐵 < +∞)) | 
| 119 |  | xrrebnd 13211 | . . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ*
→ (𝐵 ∈ ℝ
↔ (-∞ < 𝐵
∧ 𝐵 <
+∞))) | 
| 120 | 91, 119 | syl 17 | . . . . . . . . . 10
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → (𝐵 ∈ ℝ ↔ (-∞ < 𝐵 ∧ 𝐵 < +∞))) | 
| 121 | 118, 120 | mpbird 257 | . . . . . . . . 9
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → 𝐵 ∈ ℝ) | 
| 122 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) → sup(𝐴,
ℝ*, < ) ∈ ℝ) | 
| 123 | 122 | adantr 480 | . . . . . . . . 9
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → sup(𝐴, ℝ*, < ) ∈
ℝ) | 
| 124 | 121, 123 | resubcld 11692 | . . . . . . . 8
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → (𝐵 − sup(𝐴, ℝ*, < )) ∈
ℝ) | 
| 125 | 26, 115 | mpd 15 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 < +∞) | 
| 126 | 125 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → 𝐵 < +∞) | 
| 127 | 96, 126 | jca 511 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → (-∞ < 𝐵 ∧ 𝐵 < +∞)) | 
| 128 | 127, 120 | mpbird 257 | . . . . . . . . . 10
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → 𝐵 ∈ ℝ) | 
| 129 | 123, 128 | posdifd 11851 | . . . . . . . . 9
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → (sup(𝐴, ℝ*, < ) < 𝐵 ↔ 0 < (𝐵 − sup(𝐴, ℝ*, <
)))) | 
| 130 | 95, 129 | mpbid 232 | . . . . . . . 8
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → 0 < (𝐵 − sup(𝐴, ℝ*, <
))) | 
| 131 | 124, 130 | elrpd 13075 | . . . . . . 7
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → (𝐵 − sup(𝐴, ℝ*, < )) ∈
ℝ+) | 
| 132 |  | ovex 7465 | . . . . . . . 8
⊢ (𝐵 − sup(𝐴, ℝ*, < )) ∈
V | 
| 133 |  | nfcv 2904 | . . . . . . . . 9
⊢
Ⅎ𝑥(𝐵 − sup(𝐴, ℝ*, <
)) | 
| 134 |  | nfv 1913 | . . . . . . . . . . 11
⊢
Ⅎ𝑥(𝐵 − sup(𝐴, ℝ*, < )) ∈
ℝ+ | 
| 135 | 12, 134 | nfan 1898 | . . . . . . . . . 10
⊢
Ⅎ𝑥(𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈
ℝ+) | 
| 136 |  | nfv 1913 | . . . . . . . . . 10
⊢
Ⅎ𝑥∃𝑦 ∈ 𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, <
))) | 
| 137 | 135, 136 | nfim 1895 | . . . . . . . . 9
⊢
Ⅎ𝑥((𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈
ℝ+) → ∃𝑦 ∈ 𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, <
)))) | 
| 138 |  | eleq1 2828 | . . . . . . . . . . 11
⊢ (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (𝑥 ∈ ℝ+
↔ (𝐵 − sup(𝐴, ℝ*, < ))
∈ ℝ+)) | 
| 139 | 138 | anbi2d 630 | . . . . . . . . . 10
⊢ (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) →
((𝜑 ∧ 𝑥 ∈ ℝ+) ↔ (𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈
ℝ+))) | 
| 140 |  | oveq2 7440 | . . . . . . . . . . . 12
⊢ (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (𝑦 +𝑒 𝑥) = (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, <
)))) | 
| 141 | 140 | breq2d 5154 | . . . . . . . . . . 11
⊢ (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (𝐵 < (𝑦 +𝑒 𝑥) ↔ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, <
))))) | 
| 142 | 141 | rexbidv 3178 | . . . . . . . . . 10
⊢ (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) →
(∃𝑦 ∈ 𝐴 𝐵 < (𝑦 +𝑒 𝑥) ↔ ∃𝑦 ∈ 𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, <
))))) | 
| 143 | 139, 142 | imbi12d 344 | . . . . . . . . 9
⊢ (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) →
(((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑦 ∈ 𝐴 𝐵 < (𝑦 +𝑒 𝑥)) ↔ ((𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈
ℝ+) → ∃𝑦 ∈ 𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, <
)))))) | 
| 144 | 133, 137,
143, 23 | vtoclgf 3568 | . . . . . . . 8
⊢ ((𝐵 − sup(𝐴, ℝ*, < )) ∈ V
→ ((𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈
ℝ+) → ∃𝑦 ∈ 𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, <
))))) | 
| 145 | 132, 144 | ax-mp 5 | . . . . . . 7
⊢ ((𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈
ℝ+) → ∃𝑦 ∈ 𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, <
)))) | 
| 146 | 88, 131, 145 | syl2anc 584 | . . . . . 6
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → ∃𝑦 ∈ 𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, <
)))) | 
| 147 |  | ltpnf 13163 | . . . . . . . . . . . . 13
⊢
(sup(𝐴,
ℝ*, < ) ∈ ℝ → sup(𝐴, ℝ*, < ) <
+∞) | 
| 148 | 147 | adantr 480 | . . . . . . . . . . . 12
⊢
((sup(𝐴,
ℝ*, < ) ∈ ℝ ∧ 𝑦 = +∞) → sup(𝐴, ℝ*, < ) <
+∞) | 
| 149 |  | id 22 | . . . . . . . . . . . . . 14
⊢ (𝑦 = +∞ → 𝑦 = +∞) | 
| 150 | 149 | eqcomd 2742 | . . . . . . . . . . . . 13
⊢ (𝑦 = +∞ → +∞ =
𝑦) | 
| 151 | 150 | adantl 481 | . . . . . . . . . . . 12
⊢
((sup(𝐴,
ℝ*, < ) ∈ ℝ ∧ 𝑦 = +∞) → +∞ = 𝑦) | 
| 152 | 148, 151 | breqtrd 5168 | . . . . . . . . . . 11
⊢
((sup(𝐴,
ℝ*, < ) ∈ ℝ ∧ 𝑦 = +∞) → sup(𝐴, ℝ*, < ) < 𝑦) | 
| 153 | 152 | adantll 714 | . . . . . . . . . 10
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ 𝑦 =
+∞) → sup(𝐴,
ℝ*, < ) < 𝑦) | 
| 154 | 153 | ad5ant15 758 | . . . . . . . . 9
⊢
((((((𝜑 ∧
sup(𝐴, ℝ*,
< ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ 𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = +∞) → sup(𝐴, ℝ*, < )
< 𝑦) | 
| 155 |  | simplll 774 | . . . . . . . . . 10
⊢
((((((𝜑 ∧
sup(𝐴, ℝ*,
< ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ 𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬
𝑦 = +∞) →
((𝜑 ∧ sup(𝐴, ℝ*, < )
∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵)) | 
| 156 |  | simpl 482 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
sup(𝐴, ℝ*,
< ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ 𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬
-∞ < 𝑦) →
((((𝜑 ∧ sup(𝐴, ℝ*, < )
∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ 𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, <
))))) | 
| 157 | 88, 41 | sylanl1 680 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ sup(𝐴, ℝ*, < )
∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ 𝐴) ∧ ¬ -∞ < 𝑦) → 𝑦 = -∞) | 
| 158 | 157 | adantlr 715 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
sup(𝐴, ℝ*,
< ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ 𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬
-∞ < 𝑦) →
𝑦 =
-∞) | 
| 159 |  | simplr 768 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
sup(𝐴, ℝ*,
< ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ 𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, <
)))) | 
| 160 |  | oveq1 7439 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = -∞ → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = (-∞
+𝑒 (𝐵
− sup(𝐴,
ℝ*, < )))) | 
| 161 | 160 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
sup(𝐴, ℝ*,
< ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ 𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = (-∞
+𝑒 (𝐵
− sup(𝐴,
ℝ*, < )))) | 
| 162 | 128, 123 | resubcld 11692 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → (𝐵 − sup(𝐴, ℝ*, < )) ∈
ℝ) | 
| 163 | 162 | rexrd 11312 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → (𝐵 − sup(𝐴, ℝ*, < )) ∈
ℝ*) | 
| 164 | 163 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧
sup(𝐴, ℝ*,
< ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ 𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → (𝐵 − sup(𝐴, ℝ*, < )) ∈
ℝ*) | 
| 165 |  | renepnf 11310 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 − sup(𝐴, ℝ*, < )) ∈
ℝ → (𝐵 −
sup(𝐴, ℝ*,
< )) ≠ +∞) | 
| 166 | 124, 165 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → (𝐵 − sup(𝐴, ℝ*, < )) ≠
+∞) | 
| 167 | 166 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧
sup(𝐴, ℝ*,
< ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ 𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → (𝐵 − sup(𝐴, ℝ*, < )) ≠
+∞) | 
| 168 |  | xaddmnf2 13272 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 − sup(𝐴, ℝ*, < )) ∈
ℝ* ∧ (𝐵 − sup(𝐴, ℝ*, < )) ≠
+∞) → (-∞ +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) =
-∞) | 
| 169 | 164, 167,
168 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
sup(𝐴, ℝ*,
< ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ 𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → (-∞
+𝑒 (𝐵
− sup(𝐴,
ℝ*, < ))) = -∞) | 
| 170 | 161, 169 | eqtrd 2776 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
sup(𝐴, ℝ*,
< ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ 𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) =
-∞) | 
| 171 | 159, 170 | breqtrd 5168 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
sup(𝐴, ℝ*,
< ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ 𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ 𝑦 = -∞) → 𝐵 < -∞) | 
| 172 | 156, 158,
171 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
sup(𝐴, ℝ*,
< ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ 𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬
-∞ < 𝑦) →
𝐵 <
-∞) | 
| 173 | 55 | ad5antr 734 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
sup(𝐴, ℝ*,
< ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ 𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬
-∞ < 𝑦) →
¬ 𝐵 <
-∞) | 
| 174 | 172, 173 | condan 817 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ sup(𝐴, ℝ*, < )
∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ 𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) →
-∞ < 𝑦) | 
| 175 | 174 | adantr 480 | . . . . . . . . . . . 12
⊢
((((((𝜑 ∧
sup(𝐴, ℝ*,
< ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ 𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬
𝑦 = +∞) →
-∞ < 𝑦) | 
| 176 |  | simp3 1138 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 = +∞) → ¬ 𝑦 = +∞) | 
| 177 | 31 | 3adant3 1132 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 = +∞) → 𝑦 ∈ ℝ*) | 
| 178 |  | nltpnft 13207 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℝ*
→ (𝑦 = +∞ ↔
¬ 𝑦 <
+∞)) | 
| 179 | 177, 178 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 = +∞) → (𝑦 = +∞ ↔ ¬ 𝑦 < +∞)) | 
| 180 | 176, 179 | mtbid 324 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 = +∞) → ¬ ¬ 𝑦 < +∞) | 
| 181 | 180 | notnotrd 133 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 = +∞) → 𝑦 < +∞) | 
| 182 | 181 | 3adant1r 1177 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ 𝑦 ∈
𝐴 ∧ ¬ 𝑦 = +∞) → 𝑦 < +∞) | 
| 183 | 182 | ad5ant135 1369 | . . . . . . . . . . . 12
⊢
((((((𝜑 ∧
sup(𝐴, ℝ*,
< ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ 𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬
𝑦 = +∞) → 𝑦 < +∞) | 
| 184 | 175, 183 | jca 511 | . . . . . . . . . . 11
⊢
((((((𝜑 ∧
sup(𝐴, ℝ*,
< ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ 𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬
𝑦 = +∞) →
(-∞ < 𝑦 ∧
𝑦 <
+∞)) | 
| 185 | 31 | adantlr 715 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ 𝑦 ∈
𝐴) → 𝑦 ∈
ℝ*) | 
| 186 | 185 | ad5ant13 756 | . . . . . . . . . . . 12
⊢
((((((𝜑 ∧
sup(𝐴, ℝ*,
< ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ 𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬
𝑦 = +∞) → 𝑦 ∈
ℝ*) | 
| 187 |  | xrrebnd 13211 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ*
→ (𝑦 ∈ ℝ
↔ (-∞ < 𝑦
∧ 𝑦 <
+∞))) | 
| 188 | 186, 187 | syl 17 | . . . . . . . . . . 11
⊢
((((((𝜑 ∧
sup(𝐴, ℝ*,
< ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ 𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬
𝑦 = +∞) → (𝑦 ∈ ℝ ↔ (-∞
< 𝑦 ∧ 𝑦 <
+∞))) | 
| 189 | 184, 188 | mpbird 257 | . . . . . . . . . 10
⊢
((((((𝜑 ∧
sup(𝐴, ℝ*,
< ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ 𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬
𝑦 = +∞) → 𝑦 ∈
ℝ) | 
| 190 |  | simplr 768 | . . . . . . . . . 10
⊢
((((((𝜑 ∧
sup(𝐴, ℝ*,
< ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ 𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬
𝑦 = +∞) → 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, <
)))) | 
| 191 | 121 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ sup(𝐴, ℝ*, < )
∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) →
𝐵 ∈
ℝ) | 
| 192 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ) | 
| 193 | 124 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝐵 − sup(𝐴, ℝ*, < )) ∈
ℝ) | 
| 194 |  | rexadd 13275 | . . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℝ ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈
ℝ) → (𝑦
+𝑒 (𝐵
− sup(𝐴,
ℝ*, < ))) = (𝑦 + (𝐵 − sup(𝐴, ℝ*, <
)))) | 
| 195 | 192, 193,
194 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = (𝑦 + (𝐵 − sup(𝐴, ℝ*, <
)))) | 
| 196 | 192, 193 | readdcld 11291 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑦 + (𝐵 − sup(𝐴, ℝ*, < ))) ∈
ℝ) | 
| 197 | 195, 196 | eqeltrd 2840 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) ∈
ℝ) | 
| 198 | 197 | adantr 480 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ sup(𝐴, ℝ*, < )
∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) →
(𝑦 +𝑒
(𝐵 − sup(𝐴, ℝ*, < )))
∈ ℝ) | 
| 199 |  | simpr 484 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ sup(𝐴, ℝ*, < )
∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) →
𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, <
)))) | 
| 200 | 191, 198,
191, 199 | ltsub1dd 11876 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ sup(𝐴, ℝ*, < )
∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) →
(𝐵 − 𝐵) < ((𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) −
𝐵)) | 
| 201 | 121 | recnd 11290 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → 𝐵 ∈ ℂ) | 
| 202 | 201 | subidd 11609 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → (𝐵 − 𝐵) = 0) | 
| 203 | 202 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ sup(𝐴, ℝ*, < )
∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) →
(𝐵 − 𝐵) = 0) | 
| 204 | 201 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → 𝐵 ∈ ℂ) | 
| 205 | 192 | recnd 11290 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ) | 
| 206 | 122 | recnd 11290 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) → sup(𝐴,
ℝ*, < ) ∈ ℂ) | 
| 207 | 206 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → sup(𝐴, ℝ*, < ) ∈
ℂ) | 
| 208 | 205, 207 | subcld 11621 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑦 − sup(𝐴, ℝ*, < )) ∈
ℂ) | 
| 209 | 205, 204,
207 | addsub12d 11644 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑦 + (𝐵 − sup(𝐴, ℝ*, < ))) = (𝐵 + (𝑦 − sup(𝐴, ℝ*, <
)))) | 
| 210 | 195, 209 | eqtrd 2776 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) = (𝐵 + (𝑦 − sup(𝐴, ℝ*, <
)))) | 
| 211 | 204, 208,
210 | mvrladdd 11677 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) → ((𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) −
𝐵) = (𝑦 − sup(𝐴, ℝ*, <
))) | 
| 212 | 211 | adantr 480 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ sup(𝐴, ℝ*, < )
∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) →
((𝑦 +𝑒
(𝐵 − sup(𝐴, ℝ*, < )))
− 𝐵) = (𝑦 − sup(𝐴, ℝ*, <
))) | 
| 213 | 203, 212 | breq12d 5155 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ sup(𝐴, ℝ*, < )
∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) →
((𝐵 − 𝐵) < ((𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) −
𝐵) ↔ 0 < (𝑦 − sup(𝐴, ℝ*, <
)))) | 
| 214 | 200, 213 | mpbid 232 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ sup(𝐴, ℝ*, < )
∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) → 0
< (𝑦 − sup(𝐴, ℝ*, <
))) | 
| 215 | 123 | ad2antrr 726 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ sup(𝐴, ℝ*, < )
∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) →
sup(𝐴, ℝ*,
< ) ∈ ℝ) | 
| 216 |  | simplr 768 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ sup(𝐴, ℝ*, < )
∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) →
𝑦 ∈
ℝ) | 
| 217 | 215, 216 | posdifd 11851 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ sup(𝐴, ℝ*, < )
∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) →
(sup(𝐴,
ℝ*, < ) < 𝑦 ↔ 0 < (𝑦 − sup(𝐴, ℝ*, <
)))) | 
| 218 | 214, 217 | mpbird 257 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ sup(𝐴, ℝ*, < )
∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) →
sup(𝐴, ℝ*,
< ) < 𝑦) | 
| 219 | 155, 189,
190, 218 | syl21anc 837 | . . . . . . . . 9
⊢
((((((𝜑 ∧
sup(𝐴, ℝ*,
< ) ∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ 𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) ∧ ¬
𝑦 = +∞) →
sup(𝐴, ℝ*,
< ) < 𝑦) | 
| 220 | 154, 219 | pm2.61dan 812 | . . . . . . . 8
⊢
(((((𝜑 ∧ sup(𝐴, ℝ*, < )
∈ ℝ) ∧ sup(𝐴, ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ 𝐴) ∧ 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < )))) →
sup(𝐴, ℝ*,
< ) < 𝑦) | 
| 221 | 220 | ex 412 | . . . . . . 7
⊢ ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ 𝐴) → (𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) →
sup(𝐴, ℝ*,
< ) < 𝑦)) | 
| 222 | 221 | reximdva 3167 | . . . . . 6
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → (∃𝑦 ∈ 𝐴 𝐵 < (𝑦 +𝑒 (𝐵 − sup(𝐴, ℝ*, < ))) →
∃𝑦 ∈ 𝐴 sup(𝐴, ℝ*, < ) < 𝑦)) | 
| 223 | 146, 222 | mpd 15 | . . . . 5
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → ∃𝑦 ∈ 𝐴 sup(𝐴, ℝ*, < ) < 𝑦) | 
| 224 | 80, 87, 223 | syl2anc 584 | . . . 4
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ ¬ 𝐵 ≤
sup(𝐴, ℝ*,
< )) → ∃𝑦
∈ 𝐴 sup(𝐴, ℝ*, < )
< 𝑦) | 
| 225 | 59, 33 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → sup(𝐴, ℝ*, < ) ∈
ℝ*) | 
| 226 | 31, 225 | xrlenltd 11328 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑦 ≤ sup(𝐴, ℝ*, < ) ↔ ¬
sup(𝐴, ℝ*,
< ) < 𝑦)) | 
| 227 | 62, 226 | mpbid 232 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ¬ sup(𝐴, ℝ*, < ) < 𝑦) | 
| 228 | 227 | ralrimiva 3145 | . . . . . 6
⊢ (𝜑 → ∀𝑦 ∈ 𝐴 ¬ sup(𝐴, ℝ*, < ) < 𝑦) | 
| 229 |  | ralnex 3071 | . . . . . 6
⊢
(∀𝑦 ∈
𝐴 ¬ sup(𝐴, ℝ*, < )
< 𝑦 ↔ ¬
∃𝑦 ∈ 𝐴 sup(𝐴, ℝ*, < ) < 𝑦) | 
| 230 | 228, 229 | sylib 218 | . . . . 5
⊢ (𝜑 → ¬ ∃𝑦 ∈ 𝐴 sup(𝐴, ℝ*, < ) < 𝑦) | 
| 231 | 230 | ad2antrr 726 | . . . 4
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ ¬ 𝐵 ≤
sup(𝐴, ℝ*,
< )) → ¬ ∃𝑦 ∈ 𝐴 sup(𝐴, ℝ*, < ) < 𝑦) | 
| 232 | 224, 231 | condan 817 | . . 3
⊢ ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) → 𝐵 ≤
sup(𝐴, ℝ*,
< )) | 
| 233 | 9, 79, 232 | syl2anc 584 | . 2
⊢ ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞)
→ 𝐵 ≤ sup(𝐴, ℝ*, <
)) | 
| 234 | 8, 233 | pm2.61dan 812 | 1
⊢ (𝜑 → 𝐵 ≤ sup(𝐴, ℝ*, <
)) |