Proof of Theorem supxrgere
| Step | Hyp | Ref
| Expression |
| 1 | | supxrgere.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 2 | | rexr 11307 |
. . . . . 6
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℝ*) |
| 3 | | pnfxr 11315 |
. . . . . . 7
⊢ +∞
∈ ℝ* |
| 4 | 3 | a1i 11 |
. . . . . 6
⊢ (𝐵 ∈ ℝ → +∞
∈ ℝ*) |
| 5 | | ltpnf 13162 |
. . . . . 6
⊢ (𝐵 ∈ ℝ → 𝐵 < +∞) |
| 6 | 2, 4, 5 | xrltled 13192 |
. . . . 5
⊢ (𝐵 ∈ ℝ → 𝐵 ≤ +∞) |
| 7 | 1, 6 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐵 ≤ +∞) |
| 8 | 7 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞)
→ 𝐵 ≤
+∞) |
| 9 | | id 22 |
. . . . 5
⊢
(sup(𝐴,
ℝ*, < ) = +∞ → sup(𝐴, ℝ*, < ) =
+∞) |
| 10 | 9 | eqcomd 2743 |
. . . 4
⊢
(sup(𝐴,
ℝ*, < ) = +∞ → +∞ = sup(𝐴, ℝ*, <
)) |
| 11 | 10 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞)
→ +∞ = sup(𝐴,
ℝ*, < )) |
| 12 | 8, 11 | breqtrd 5169 |
. 2
⊢ ((𝜑 ∧ sup(𝐴, ℝ*, < ) = +∞)
→ 𝐵 ≤ sup(𝐴, ℝ*, <
)) |
| 13 | | simpl 482 |
. . 3
⊢ ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞)
→ 𝜑) |
| 14 | | 1rp 13038 |
. . . . . . . 8
⊢ 1 ∈
ℝ+ |
| 15 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑥1 |
| 16 | | supxrgere.xph |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥𝜑 |
| 17 | | nfv 1914 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥1 ∈
ℝ+ |
| 18 | 16, 17 | nfan 1899 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(𝜑 ∧ 1 ∈
ℝ+) |
| 19 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥∃𝑦 ∈ 𝐴 (𝐵 − 1) < 𝑦 |
| 20 | 18, 19 | nfim 1896 |
. . . . . . . . . 10
⊢
Ⅎ𝑥((𝜑 ∧ 1 ∈
ℝ+) → ∃𝑦 ∈ 𝐴 (𝐵 − 1) < 𝑦) |
| 21 | | eleq1 2829 |
. . . . . . . . . . . 12
⊢ (𝑥 = 1 → (𝑥 ∈ ℝ+ ↔ 1 ∈
ℝ+)) |
| 22 | 21 | anbi2d 630 |
. . . . . . . . . . 11
⊢ (𝑥 = 1 → ((𝜑 ∧ 𝑥 ∈ ℝ+) ↔ (𝜑 ∧ 1 ∈
ℝ+))) |
| 23 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 1 → (𝐵 − 𝑥) = (𝐵 − 1)) |
| 24 | 23 | breq1d 5153 |
. . . . . . . . . . . 12
⊢ (𝑥 = 1 → ((𝐵 − 𝑥) < 𝑦 ↔ (𝐵 − 1) < 𝑦)) |
| 25 | 24 | rexbidv 3179 |
. . . . . . . . . . 11
⊢ (𝑥 = 1 → (∃𝑦 ∈ 𝐴 (𝐵 − 𝑥) < 𝑦 ↔ ∃𝑦 ∈ 𝐴 (𝐵 − 1) < 𝑦)) |
| 26 | 22, 25 | imbi12d 344 |
. . . . . . . . . 10
⊢ (𝑥 = 1 → (((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑦 ∈ 𝐴 (𝐵 − 𝑥) < 𝑦) ↔ ((𝜑 ∧ 1 ∈ ℝ+) →
∃𝑦 ∈ 𝐴 (𝐵 − 1) < 𝑦))) |
| 27 | | supxrgere.y |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑦 ∈ 𝐴 (𝐵 − 𝑥) < 𝑦) |
| 28 | 15, 20, 26, 27 | vtoclgf 3569 |
. . . . . . . . 9
⊢ (1 ∈
ℝ+ → ((𝜑 ∧ 1 ∈ ℝ+) →
∃𝑦 ∈ 𝐴 (𝐵 − 1) < 𝑦)) |
| 29 | 14, 28 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝜑 ∧ 1 ∈
ℝ+) → ∃𝑦 ∈ 𝐴 (𝐵 − 1) < 𝑦) |
| 30 | 14, 29 | mpan2 691 |
. . . . . . 7
⊢ (𝜑 → ∃𝑦 ∈ 𝐴 (𝐵 − 1) < 𝑦) |
| 31 | 30 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞)
→ ∃𝑦 ∈
𝐴 (𝐵 − 1) < 𝑦) |
| 32 | | mnfxr 11318 |
. . . . . . . . . . 11
⊢ -∞
∈ ℝ* |
| 33 | 32 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ (𝐵 − 1) < 𝑦) → -∞ ∈
ℝ*) |
| 34 | | supxrgere.a |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ⊆
ℝ*) |
| 35 | 34 | sselda 3983 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ*) |
| 36 | 35 | 3adant3 1133 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ (𝐵 − 1) < 𝑦) → 𝑦 ∈ ℝ*) |
| 37 | | supxrcl 13357 |
. . . . . . . . . . . 12
⊢ (𝐴 ⊆ ℝ*
→ sup(𝐴,
ℝ*, < ) ∈ ℝ*) |
| 38 | 34, 37 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → sup(𝐴, ℝ*, < ) ∈
ℝ*) |
| 39 | 38 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ (𝐵 − 1) < 𝑦) → sup(𝐴, ℝ*, < ) ∈
ℝ*) |
| 40 | | peano2rem 11576 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ ℝ → (𝐵 − 1) ∈
ℝ) |
| 41 | 1, 40 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐵 − 1) ∈ ℝ) |
| 42 | 41 | rexrd 11311 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵 − 1) ∈
ℝ*) |
| 43 | 42 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ -∞ < 𝑦) → (𝐵 − 1) ∈
ℝ*) |
| 44 | 43 | 3ad2antl1 1186 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ (𝐵 − 1) < 𝑦) ∧ ¬ -∞ < 𝑦) → (𝐵 − 1) ∈
ℝ*) |
| 45 | 36 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ (𝐵 − 1) < 𝑦) ∧ ¬ -∞ < 𝑦) → 𝑦 ∈ ℝ*) |
| 46 | 32 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ (𝐵 − 1) < 𝑦) ∧ ¬ -∞ < 𝑦) → -∞ ∈
ℝ*) |
| 47 | | simpl3 1194 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ (𝐵 − 1) < 𝑦) ∧ ¬ -∞ < 𝑦) → (𝐵 − 1) < 𝑦) |
| 48 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ -∞ < 𝑦) → ¬ -∞ <
𝑦) |
| 49 | 35 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ -∞ < 𝑦) → 𝑦 ∈ ℝ*) |
| 50 | 32 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ -∞ < 𝑦) → -∞ ∈
ℝ*) |
| 51 | | xrlenlt 11326 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℝ*
∧ -∞ ∈ ℝ*) → (𝑦 ≤ -∞ ↔ ¬ -∞ <
𝑦)) |
| 52 | 49, 50, 51 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ -∞ < 𝑦) → (𝑦 ≤ -∞ ↔ ¬ -∞ <
𝑦)) |
| 53 | 48, 52 | mpbird 257 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ ¬ -∞ < 𝑦) → 𝑦 ≤ -∞) |
| 54 | 53 | 3adantl3 1169 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ (𝐵 − 1) < 𝑦) ∧ ¬ -∞ < 𝑦) → 𝑦 ≤ -∞) |
| 55 | 44, 45, 46, 47, 54 | xrltletrd 13203 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ (𝐵 − 1) < 𝑦) ∧ ¬ -∞ < 𝑦) → (𝐵 − 1) < -∞) |
| 56 | | nltmnf 13171 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 − 1) ∈
ℝ* → ¬ (𝐵 − 1) < -∞) |
| 57 | 42, 56 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ¬ (𝐵 − 1) < -∞) |
| 58 | 57 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ -∞ < 𝑦) → ¬ (𝐵 − 1) <
-∞) |
| 59 | 58 | 3ad2antl1 1186 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ (𝐵 − 1) < 𝑦) ∧ ¬ -∞ < 𝑦) → ¬ (𝐵 − 1) <
-∞) |
| 60 | 55, 59 | condan 818 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ (𝐵 − 1) < 𝑦) → -∞ < 𝑦) |
| 61 | 34 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐴 ⊆
ℝ*) |
| 62 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴) |
| 63 | | supxrub 13366 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ ℝ*
∧ 𝑦 ∈ 𝐴) → 𝑦 ≤ sup(𝐴, ℝ*, <
)) |
| 64 | 61, 62, 63 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ≤ sup(𝐴, ℝ*, <
)) |
| 65 | 64 | 3adant3 1133 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ (𝐵 − 1) < 𝑦) → 𝑦 ≤ sup(𝐴, ℝ*, <
)) |
| 66 | 33, 36, 39, 60, 65 | xrltletrd 13203 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ (𝐵 − 1) < 𝑦) → -∞ < sup(𝐴, ℝ*, <
)) |
| 67 | 66 | 3exp 1120 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ 𝐴 → ((𝐵 − 1) < 𝑦 → -∞ < sup(𝐴, ℝ*, <
)))) |
| 68 | 67 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞)
→ (𝑦 ∈ 𝐴 → ((𝐵 − 1) < 𝑦 → -∞ < sup(𝐴, ℝ*, <
)))) |
| 69 | 68 | rexlimdv 3153 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞)
→ (∃𝑦 ∈
𝐴 (𝐵 − 1) < 𝑦 → -∞ < sup(𝐴, ℝ*, <
))) |
| 70 | 31, 69 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞)
→ -∞ < sup(𝐴,
ℝ*, < )) |
| 71 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞)
→ ¬ sup(𝐴,
ℝ*, < ) = +∞) |
| 72 | | nltpnft 13206 |
. . . . . . . . 9
⊢
(sup(𝐴,
ℝ*, < ) ∈ ℝ* → (sup(𝐴, ℝ*, < ) =
+∞ ↔ ¬ sup(𝐴, ℝ*, < ) <
+∞)) |
| 73 | 38, 72 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (sup(𝐴, ℝ*, < ) = +∞
↔ ¬ sup(𝐴,
ℝ*, < ) < +∞)) |
| 74 | 73 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞)
→ (sup(𝐴,
ℝ*, < ) = +∞ ↔ ¬ sup(𝐴, ℝ*, < ) <
+∞)) |
| 75 | 71, 74 | mtbid 324 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞)
→ ¬ ¬ sup(𝐴,
ℝ*, < ) < +∞) |
| 76 | 75 | notnotrd 133 |
. . . . 5
⊢ ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞)
→ sup(𝐴,
ℝ*, < ) < +∞) |
| 77 | 70, 76 | jca 511 |
. . . 4
⊢ ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞)
→ (-∞ < sup(𝐴, ℝ*, < ) ∧
sup(𝐴, ℝ*,
< ) < +∞)) |
| 78 | 38 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞)
→ sup(𝐴,
ℝ*, < ) ∈ ℝ*) |
| 79 | | xrrebnd 13210 |
. . . . 5
⊢
(sup(𝐴,
ℝ*, < ) ∈ ℝ* → (sup(𝐴, ℝ*, < )
∈ ℝ ↔ (-∞ < sup(𝐴, ℝ*, < ) ∧
sup(𝐴, ℝ*,
< ) < +∞))) |
| 80 | 78, 79 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞)
→ (sup(𝐴,
ℝ*, < ) ∈ ℝ ↔ (-∞ < sup(𝐴, ℝ*, < )
∧ sup(𝐴,
ℝ*, < ) < +∞))) |
| 81 | 77, 80 | mpbird 257 |
. . 3
⊢ ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞)
→ sup(𝐴,
ℝ*, < ) ∈ ℝ) |
| 82 | | simpl 482 |
. . . . 5
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ ¬ 𝐵 ≤
sup(𝐴, ℝ*,
< )) → (𝜑 ∧
sup(𝐴, ℝ*,
< ) ∈ ℝ)) |
| 83 | | simpr 484 |
. . . . . 6
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ ¬ 𝐵 ≤
sup(𝐴, ℝ*,
< )) → ¬ 𝐵 ≤
sup(𝐴, ℝ*,
< )) |
| 84 | 82 | simprd 495 |
. . . . . . 7
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ ¬ 𝐵 ≤
sup(𝐴, ℝ*,
< )) → sup(𝐴,
ℝ*, < ) ∈ ℝ) |
| 85 | 1 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ ¬ 𝐵 ≤
sup(𝐴, ℝ*,
< )) → 𝐵 ∈
ℝ) |
| 86 | 84, 85 | ltnled 11408 |
. . . . . 6
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ ¬ 𝐵 ≤
sup(𝐴, ℝ*,
< )) → (sup(𝐴,
ℝ*, < ) < 𝐵 ↔ ¬ 𝐵 ≤ sup(𝐴, ℝ*, <
))) |
| 87 | 83, 86 | mpbird 257 |
. . . . 5
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ ¬ 𝐵 ≤
sup(𝐴, ℝ*,
< )) → sup(𝐴,
ℝ*, < ) < 𝐵) |
| 88 | | simpll 767 |
. . . . . . 7
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → 𝜑) |
| 89 | 1 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) → 𝐵 ∈
ℝ) |
| 90 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) → sup(𝐴,
ℝ*, < ) ∈ ℝ) |
| 91 | 89, 90 | resubcld 11691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) → (𝐵 −
sup(𝐴, ℝ*,
< )) ∈ ℝ) |
| 92 | 91 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → (𝐵 − sup(𝐴, ℝ*, < )) ∈
ℝ) |
| 93 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → sup(𝐴, ℝ*, < ) < 𝐵) |
| 94 | 90 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → sup(𝐴, ℝ*, < ) ∈
ℝ) |
| 95 | 88, 1 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → 𝐵 ∈ ℝ) |
| 96 | 94, 95 | posdifd 11850 |
. . . . . . . . 9
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → (sup(𝐴, ℝ*, < ) < 𝐵 ↔ 0 < (𝐵 − sup(𝐴, ℝ*, <
)))) |
| 97 | 93, 96 | mpbid 232 |
. . . . . . . 8
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → 0 < (𝐵 − sup(𝐴, ℝ*, <
))) |
| 98 | 92, 97 | elrpd 13074 |
. . . . . . 7
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → (𝐵 − sup(𝐴, ℝ*, < )) ∈
ℝ+) |
| 99 | | ovex 7464 |
. . . . . . . 8
⊢ (𝐵 − sup(𝐴, ℝ*, < )) ∈
V |
| 100 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝐵 − sup(𝐴, ℝ*, <
)) |
| 101 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(𝐵 − sup(𝐴, ℝ*, < )) ∈
ℝ+ |
| 102 | 16, 101 | nfan 1899 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈
ℝ+) |
| 103 | | nfv 1914 |
. . . . . . . . . 10
⊢
Ⅎ𝑥∃𝑦 ∈ 𝐴 (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦 |
| 104 | 102, 103 | nfim 1896 |
. . . . . . . . 9
⊢
Ⅎ𝑥((𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈
ℝ+) → ∃𝑦 ∈ 𝐴 (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦) |
| 105 | | eleq1 2829 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (𝑥 ∈ ℝ+
↔ (𝐵 − sup(𝐴, ℝ*, < ))
∈ ℝ+)) |
| 106 | 105 | anbi2d 630 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) →
((𝜑 ∧ 𝑥 ∈ ℝ+) ↔ (𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈
ℝ+))) |
| 107 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) → (𝐵 − 𝑥) = (𝐵 − (𝐵 − sup(𝐴, ℝ*, <
)))) |
| 108 | 107 | breq1d 5153 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) →
((𝐵 − 𝑥) < 𝑦 ↔ (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦)) |
| 109 | 108 | rexbidv 3179 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) →
(∃𝑦 ∈ 𝐴 (𝐵 − 𝑥) < 𝑦 ↔ ∃𝑦 ∈ 𝐴 (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦)) |
| 110 | 106, 109 | imbi12d 344 |
. . . . . . . . 9
⊢ (𝑥 = (𝐵 − sup(𝐴, ℝ*, < )) →
(((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑦 ∈ 𝐴 (𝐵 − 𝑥) < 𝑦) ↔ ((𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈
ℝ+) → ∃𝑦 ∈ 𝐴 (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦))) |
| 111 | 100, 104,
110, 27 | vtoclgf 3569 |
. . . . . . . 8
⊢ ((𝐵 − sup(𝐴, ℝ*, < )) ∈ V
→ ((𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈
ℝ+) → ∃𝑦 ∈ 𝐴 (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦)) |
| 112 | 99, 111 | ax-mp 5 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 − sup(𝐴, ℝ*, < )) ∈
ℝ+) → ∃𝑦 ∈ 𝐴 (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦) |
| 113 | 88, 98, 112 | syl2anc 584 |
. . . . . 6
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → ∃𝑦 ∈ 𝐴 (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦) |
| 114 | 1 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ ℂ) |
| 115 | 114 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) ∧ (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦) → 𝐵 ∈ ℂ) |
| 116 | 90 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) → sup(𝐴,
ℝ*, < ) ∈ ℂ) |
| 117 | 116 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) ∧ (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦) → sup(𝐴, ℝ*, < ) ∈
ℂ) |
| 118 | 115, 117 | nncand 11625 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) ∧ (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦) → (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) = sup(𝐴, ℝ*, <
)) |
| 119 | 118 | eqcomd 2743 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) ∧ (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦) → sup(𝐴, ℝ*, < ) = (𝐵 − (𝐵 − sup(𝐴, ℝ*, <
)))) |
| 120 | | simpr 484 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) ∧ (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦) → (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦) |
| 121 | 119, 120 | eqbrtrd 5165 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) ∧ (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦) → sup(𝐴, ℝ*, < ) < 𝑦) |
| 122 | 121 | ex 412 |
. . . . . . . 8
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → ((𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦 → sup(𝐴, ℝ*, < ) < 𝑦)) |
| 123 | 122 | adantr 480 |
. . . . . . 7
⊢ ((((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) ∧ 𝑦 ∈ 𝐴) → ((𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦 → sup(𝐴, ℝ*, < ) < 𝑦)) |
| 124 | 123 | reximdva 3168 |
. . . . . 6
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → (∃𝑦 ∈ 𝐴 (𝐵 − (𝐵 − sup(𝐴, ℝ*, < ))) < 𝑦 → ∃𝑦 ∈ 𝐴 sup(𝐴, ℝ*, < ) < 𝑦)) |
| 125 | 113, 124 | mpd 15 |
. . . . 5
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ sup(𝐴,
ℝ*, < ) < 𝐵) → ∃𝑦 ∈ 𝐴 sup(𝐴, ℝ*, < ) < 𝑦) |
| 126 | 82, 87, 125 | syl2anc 584 |
. . . 4
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ ¬ 𝐵 ≤
sup(𝐴, ℝ*,
< )) → ∃𝑦
∈ 𝐴 sup(𝐴, ℝ*, < )
< 𝑦) |
| 127 | 61, 37 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → sup(𝐴, ℝ*, < ) ∈
ℝ*) |
| 128 | 35, 127 | xrlenltd 11327 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑦 ≤ sup(𝐴, ℝ*, < ) ↔ ¬
sup(𝐴, ℝ*,
< ) < 𝑦)) |
| 129 | 64, 128 | mpbid 232 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ¬ sup(𝐴, ℝ*, < ) < 𝑦) |
| 130 | 129 | ralrimiva 3146 |
. . . . . 6
⊢ (𝜑 → ∀𝑦 ∈ 𝐴 ¬ sup(𝐴, ℝ*, < ) < 𝑦) |
| 131 | | ralnex 3072 |
. . . . . 6
⊢
(∀𝑦 ∈
𝐴 ¬ sup(𝐴, ℝ*, < )
< 𝑦 ↔ ¬
∃𝑦 ∈ 𝐴 sup(𝐴, ℝ*, < ) < 𝑦) |
| 132 | 130, 131 | sylib 218 |
. . . . 5
⊢ (𝜑 → ¬ ∃𝑦 ∈ 𝐴 sup(𝐴, ℝ*, < ) < 𝑦) |
| 133 | 132 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) ∧ ¬ 𝐵 ≤
sup(𝐴, ℝ*,
< )) → ¬ ∃𝑦 ∈ 𝐴 sup(𝐴, ℝ*, < ) < 𝑦) |
| 134 | 126, 133 | condan 818 |
. . 3
⊢ ((𝜑 ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) → 𝐵 ≤
sup(𝐴, ℝ*,
< )) |
| 135 | 13, 81, 134 | syl2anc 584 |
. 2
⊢ ((𝜑 ∧ ¬ sup(𝐴, ℝ*, < ) = +∞)
→ 𝐵 ≤ sup(𝐴, ℝ*, <
)) |
| 136 | 12, 135 | pm2.61dan 813 |
1
⊢ (𝜑 → 𝐵 ≤ sup(𝐴, ℝ*, <
)) |