| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | rlimcld2.1 | . . 3
⊢ (𝜑 → sup(𝐴, ℝ*, < ) =
+∞) | 
| 2 |  | rlimcld2.2 | . . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶) | 
| 3 |  | ssrab2 4079 | . . . 4
⊢ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)} ⊆
ℂ | 
| 4 | 3 | a1i 11 | . . 3
⊢ (𝜑 → {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)} ⊆
ℂ) | 
| 5 |  | eldifi 4130 | . . . . . 6
⊢ (𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) →
𝑦 ∈
ℂ) | 
| 6 | 5 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) →
𝑦 ∈
ℂ) | 
| 7 | 6 | recld 15234 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) →
(ℜ‘𝑦) ∈
ℝ) | 
| 8 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑤 = 𝑦 → (ℜ‘𝑤) = (ℜ‘𝑦)) | 
| 9 | 8 | breq2d 5154 | . . . . . . . . 9
⊢ (𝑤 = 𝑦 → (0 ≤ (ℜ‘𝑤) ↔ 0 ≤
(ℜ‘𝑦))) | 
| 10 | 9 | notbid 318 | . . . . . . . 8
⊢ (𝑤 = 𝑦 → (¬ 0 ≤ (ℜ‘𝑤) ↔ ¬ 0 ≤
(ℜ‘𝑦))) | 
| 11 |  | notrab 4321 | . . . . . . . 8
⊢ (ℂ
∖ {𝑤 ∈ ℂ
∣ 0 ≤ (ℜ‘𝑤)}) = {𝑤 ∈ ℂ ∣ ¬ 0 ≤
(ℜ‘𝑤)} | 
| 12 | 10, 11 | elrab2 3694 | . . . . . . 7
⊢ (𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) ↔
(𝑦 ∈ ℂ ∧
¬ 0 ≤ (ℜ‘𝑦))) | 
| 13 | 12 | simprbi 496 | . . . . . 6
⊢ (𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) →
¬ 0 ≤ (ℜ‘𝑦)) | 
| 14 | 13 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) →
¬ 0 ≤ (ℜ‘𝑦)) | 
| 15 |  | 0re 11264 | . . . . . 6
⊢ 0 ∈
ℝ | 
| 16 |  | ltnle 11341 | . . . . . 6
⊢
(((ℜ‘𝑦)
∈ ℝ ∧ 0 ∈ ℝ) → ((ℜ‘𝑦) < 0 ↔ ¬ 0 ≤
(ℜ‘𝑦))) | 
| 17 | 7, 15, 16 | sylancl 586 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) →
((ℜ‘𝑦) < 0
↔ ¬ 0 ≤ (ℜ‘𝑦))) | 
| 18 | 14, 17 | mpbird 257 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) →
(ℜ‘𝑦) <
0) | 
| 19 | 7, 18 | negelrpd 13070 | . . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) →
-(ℜ‘𝑦) ∈
ℝ+) | 
| 20 | 7 | renegcld 11691 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) →
-(ℜ‘𝑦) ∈
ℝ) | 
| 21 | 20 | adantr 480 | . . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) ∧
𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) →
-(ℜ‘𝑦) ∈
ℝ) | 
| 22 |  | elrabi 3686 | . . . . . . 7
⊢ (𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)} →
𝑧 ∈
ℂ) | 
| 23 | 22 | adantl 481 | . . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) ∧
𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) →
𝑧 ∈
ℂ) | 
| 24 | 6 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) ∧
𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) →
𝑦 ∈
ℂ) | 
| 25 | 23, 24 | subcld 11621 | . . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) ∧
𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) →
(𝑧 − 𝑦) ∈
ℂ) | 
| 26 | 25 | recld 15234 | . . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) ∧
𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) →
(ℜ‘(𝑧 −
𝑦)) ∈
ℝ) | 
| 27 | 25 | abscld 15476 | . . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) ∧
𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) →
(abs‘(𝑧 − 𝑦)) ∈
ℝ) | 
| 28 |  | 0red 11265 | . . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) ∧
𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) → 0
∈ ℝ) | 
| 29 | 23 | recld 15234 | . . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) ∧
𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) →
(ℜ‘𝑧) ∈
ℝ) | 
| 30 | 24 | recld 15234 | . . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) ∧
𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) →
(ℜ‘𝑦) ∈
ℝ) | 
| 31 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑤 = 𝑧 → (ℜ‘𝑤) = (ℜ‘𝑧)) | 
| 32 | 31 | breq2d 5154 | . . . . . . . . 9
⊢ (𝑤 = 𝑧 → (0 ≤ (ℜ‘𝑤) ↔ 0 ≤
(ℜ‘𝑧))) | 
| 33 | 32 | elrab 3691 | . . . . . . . 8
⊢ (𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)} ↔
(𝑧 ∈ ℂ ∧ 0
≤ (ℜ‘𝑧))) | 
| 34 | 33 | simprbi 496 | . . . . . . 7
⊢ (𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)} → 0
≤ (ℜ‘𝑧)) | 
| 35 | 34 | adantl 481 | . . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) ∧
𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) → 0
≤ (ℜ‘𝑧)) | 
| 36 | 28, 29, 30, 35 | lesub1dd 11880 | . . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) ∧
𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) →
(0 − (ℜ‘𝑦)) ≤ ((ℜ‘𝑧) − (ℜ‘𝑦))) | 
| 37 |  | df-neg 11496 | . . . . . 6
⊢
-(ℜ‘𝑦) =
(0 − (ℜ‘𝑦)) | 
| 38 | 37 | a1i 11 | . . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) ∧
𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) →
-(ℜ‘𝑦) = (0
− (ℜ‘𝑦))) | 
| 39 | 23, 24 | resubd 15256 | . . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) ∧
𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) →
(ℜ‘(𝑧 −
𝑦)) = ((ℜ‘𝑧) − (ℜ‘𝑦))) | 
| 40 | 36, 38, 39 | 3brtr4d 5174 | . . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) ∧
𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) →
-(ℜ‘𝑦) ≤
(ℜ‘(𝑧 −
𝑦))) | 
| 41 | 25 | releabsd 15491 | . . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) ∧
𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) →
(ℜ‘(𝑧 −
𝑦)) ≤ (abs‘(𝑧 − 𝑦))) | 
| 42 | 21, 26, 27, 40, 41 | letrd 11419 | . . 3
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)})) ∧
𝑧 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) →
-(ℜ‘𝑦) ≤
(abs‘(𝑧 − 𝑦))) | 
| 43 |  | fveq2 6905 | . . . . 5
⊢ (𝑤 = 𝐵 → (ℜ‘𝑤) = (ℜ‘𝐵)) | 
| 44 | 43 | breq2d 5154 | . . . 4
⊢ (𝑤 = 𝐵 → (0 ≤ (ℜ‘𝑤) ↔ 0 ≤
(ℜ‘𝐵))) | 
| 45 |  | rlimrege0.4 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) | 
| 46 |  | rlimrege0.5 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ (ℜ‘𝐵)) | 
| 47 | 44, 45, 46 | elrabd 3693 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) | 
| 48 | 1, 2, 4, 19, 42, 47 | rlimcld2 15615 | . 2
⊢ (𝜑 → 𝐶 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)}) | 
| 49 |  | fveq2 6905 | . . . . 5
⊢ (𝑤 = 𝐶 → (ℜ‘𝑤) = (ℜ‘𝐶)) | 
| 50 | 49 | breq2d 5154 | . . . 4
⊢ (𝑤 = 𝐶 → (0 ≤ (ℜ‘𝑤) ↔ 0 ≤
(ℜ‘𝐶))) | 
| 51 | 50 | elrab 3691 | . . 3
⊢ (𝐶 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)} ↔
(𝐶 ∈ ℂ ∧ 0
≤ (ℜ‘𝐶))) | 
| 52 | 51 | simprbi 496 | . 2
⊢ (𝐶 ∈ {𝑤 ∈ ℂ ∣ 0 ≤
(ℜ‘𝑤)} → 0
≤ (ℜ‘𝐶)) | 
| 53 | 48, 52 | syl 17 | 1
⊢ (𝜑 → 0 ≤ (ℜ‘𝐶)) |