Step | Hyp | Ref
| Expression |
1 | | rlimcld2.1 |
. . 3
⊢ (𝜑 → sup(𝐴, ℝ*, < ) =
+∞) |
2 | | rlimcld2.2 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶) |
3 | | ssrab2 3687 |
. . . 4
⊢ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)} ⊆
ℂ |
4 | 3 | a1i 11 |
. . 3
⊢ (𝜑 → {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)} ⊆
ℂ) |
5 | | eldifi 3732 |
. . . . . . 7
⊢ (𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) →
𝑦 ∈
ℂ) |
6 | 5 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) →
𝑦 ∈
ℂ) |
7 | 6 | recld 13934 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) →
(ℜ‘𝑦) ∈
ℝ) |
8 | 7 | renegcld 10457 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) →
-(ℜ‘𝑦) ∈
ℝ) |
9 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑦 → (ℜ‘𝑤) = (ℜ‘𝑦)) |
10 | 9 | breq2d 4665 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑦 → (0 ≤ (ℜ‘𝑤) ↔ 0 ≤
(ℜ‘𝑦))) |
11 | 10 | notbid 308 |
. . . . . . . . 9
⊢ (𝑤 = 𝑦 → (¬ 0 ≤ (ℜ‘𝑤) ↔ ¬ 0 ≤
(ℜ‘𝑦))) |
12 | | notrab 3904 |
. . . . . . . . 9
⊢ (ℂ
∖ {𝑤 ∈ ℂ
∣ 0 ≤ (ℜ‘𝑤)}) = {𝑤 ∈ ℂ ∣ ¬ 0 ≤
(ℜ‘𝑤)} |
13 | 11, 12 | elrab2 3366 |
. . . . . . . 8
⊢ (𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) ↔
(𝑦 ∈ ℂ ∧
¬ 0 ≤ (ℜ‘𝑦))) |
14 | 13 | simprbi 480 |
. . . . . . 7
⊢ (𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) →
¬ 0 ≤ (ℜ‘𝑦)) |
15 | 14 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) →
¬ 0 ≤ (ℜ‘𝑦)) |
16 | | 0re 10040 |
. . . . . . 7
⊢ 0 ∈
ℝ |
17 | | ltnle 10117 |
. . . . . . 7
⊢
(((ℜ‘𝑦)
∈ ℝ ∧ 0 ∈ ℝ) → ((ℜ‘𝑦) < 0 ↔ ¬ 0 ≤
(ℜ‘𝑦))) |
18 | 7, 16, 17 | sylancl 694 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) →
((ℜ‘𝑦) < 0
↔ ¬ 0 ≤ (ℜ‘𝑦))) |
19 | 15, 18 | mpbird 247 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) →
(ℜ‘𝑦) <
0) |
20 | 7 | lt0neg1d 10597 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) →
((ℜ‘𝑦) < 0
↔ 0 < -(ℜ‘𝑦))) |
21 | 19, 20 | mpbid 222 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) →
0 < -(ℜ‘𝑦)) |
22 | 8, 21 | elrpd 11869 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) →
-(ℜ‘𝑦) ∈
ℝ+) |
23 | 8 | adantr 481 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) ∧
𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) →
-(ℜ‘𝑦) ∈
ℝ) |
24 | | elrabi 3359 |
. . . . . . 7
⊢ (𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)} →
𝑧 ∈
ℂ) |
25 | 24 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) ∧
𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) →
𝑧 ∈
ℂ) |
26 | 6 | adantr 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) ∧
𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) →
𝑦 ∈
ℂ) |
27 | 25, 26 | subcld 10392 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) ∧
𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) →
(𝑧 − 𝑦) ∈
ℂ) |
28 | 27 | recld 13934 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) ∧
𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) →
(ℜ‘(𝑧 −
𝑦)) ∈
ℝ) |
29 | 27 | abscld 14175 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) ∧
𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) →
(abs‘(𝑧 − 𝑦)) ∈
ℝ) |
30 | | 0red 10041 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) ∧
𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) → 0
∈ ℝ) |
31 | 25 | recld 13934 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) ∧
𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) →
(ℜ‘𝑧) ∈
ℝ) |
32 | 26 | recld 13934 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) ∧
𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) →
(ℜ‘𝑦) ∈
ℝ) |
33 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑧 → (ℜ‘𝑤) = (ℜ‘𝑧)) |
34 | 33 | breq2d 4665 |
. . . . . . . . 9
⊢ (𝑤 = 𝑧 → (0 ≤ (ℜ‘𝑤) ↔ 0 ≤
(ℜ‘𝑧))) |
35 | 34 | elrab 3363 |
. . . . . . . 8
⊢ (𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)} ↔
(𝑧 ∈ ℂ ∧ 0
≤ (ℜ‘𝑧))) |
36 | 35 | simprbi 480 |
. . . . . . 7
⊢ (𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)} → 0
≤ (ℜ‘𝑧)) |
37 | 36 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) ∧
𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) → 0
≤ (ℜ‘𝑧)) |
38 | 30, 31, 32, 37 | lesub1dd 10643 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) ∧
𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) →
(0 − (ℜ‘𝑦)) ≤ ((ℜ‘𝑧) − (ℜ‘𝑦))) |
39 | | df-neg 10269 |
. . . . . 6
⊢
-(ℜ‘𝑦) =
(0 − (ℜ‘𝑦)) |
40 | 39 | a1i 11 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) ∧
𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) →
-(ℜ‘𝑦) = (0
− (ℜ‘𝑦))) |
41 | 25, 26 | resubd 13956 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) ∧
𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) →
(ℜ‘(𝑧 −
𝑦)) = ((ℜ‘𝑧) − (ℜ‘𝑦))) |
42 | 38, 40, 41 | 3brtr4d 4685 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) ∧
𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) →
-(ℜ‘𝑦) ≤
(ℜ‘(𝑧 −
𝑦))) |
43 | 27 | releabsd 14190 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) ∧
𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) →
(ℜ‘(𝑧 −
𝑦)) ≤ (abs‘(𝑧 − 𝑦))) |
44 | 23, 28, 29, 42, 43 | letrd 10194 |
. . 3
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) ∧
𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) →
-(ℜ‘𝑦) ≤
(abs‘(𝑧 − 𝑦))) |
45 | | rlimrege0.4 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
46 | | rlimrege0.5 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ (ℜ‘𝐵)) |
47 | | fveq2 6191 |
. . . . . 6
⊢ (𝑤 = 𝐵 → (ℜ‘𝑤) = (ℜ‘𝐵)) |
48 | 47 | breq2d 4665 |
. . . . 5
⊢ (𝑤 = 𝐵 → (0 ≤ (ℜ‘𝑤) ↔ 0 ≤
(ℜ‘𝐵))) |
49 | 48 | elrab 3363 |
. . . 4
⊢ (𝐵 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)} ↔
(𝐵 ∈ ℂ ∧ 0
≤ (ℜ‘𝐵))) |
50 | 45, 46, 49 | sylanbrc 698 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) |
51 | 1, 2, 4, 22, 44, 50 | rlimcld2 14309 |
. 2
⊢ (𝜑 → 𝐶 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) |
52 | | fveq2 6191 |
. . . . 5
⊢ (𝑤 = 𝐶 → (ℜ‘𝑤) = (ℜ‘𝐶)) |
53 | 52 | breq2d 4665 |
. . . 4
⊢ (𝑤 = 𝐶 → (0 ≤ (ℜ‘𝑤) ↔ 0 ≤
(ℜ‘𝐶))) |
54 | 53 | elrab 3363 |
. . 3
⊢ (𝐶 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)} ↔
(𝐶 ∈ ℂ ∧ 0
≤ (ℜ‘𝐶))) |
55 | 54 | simprbi 480 |
. 2
⊢ (𝐶 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)} → 0
≤ (ℜ‘𝐶)) |
56 | 51, 55 | syl 17 |
1
⊢ (𝜑 → 0 ≤ (ℜ‘𝐶)) |