Metamath Proof Explorer

Theorem rlimrege0

Description: The limit of a sequence of complex numbers with nonnegative real part has nonnegative real part. (Contributed by Mario Carneiro, 10-May-2016)

Ref Expression
Hypotheses rlimcld2.1 ⊢ φ → sup A ℝ * < = +∞
rlimcld2.2 ⊢ φ → x ∈ A ⟼ B ⇝ℝ C
rlimrege0.4 ⊢ φ ∧ x ∈ A → B ∈ ℂ
rlimrege0.5 ⊢ φ ∧ x ∈ A → 0 ≤ ℜ ⁡ B
Assertion rlimrege0 ⊢ φ → 0 ≤ ℜ ⁡ C

Proof

Step Hyp Ref Expression
1 rlimcld2.1 ⊢ φ → sup A ℝ * < = +∞
2 rlimcld2.2 ⊢ φ → x ∈ A ⟼ B ⇝ℝ C
3 rlimrege0.4 ⊢ φ ∧ x ∈ A → B ∈ ℂ
4 rlimrege0.5 ⊢ φ ∧ x ∈ A → 0 ≤ ℜ ⁡ B
5 ssrab2 ⊢ w ∈ ℂ | 0 ≤ ℜ ⁡ w ⊆ ℂ
6 5 a1i ⊢ φ → w ∈ ℂ | 0 ≤ ℜ ⁡ w ⊆ ℂ
7 eldifi ⊢ y ∈ ℂ ∖ w ∈ ℂ | 0 ≤ ℜ ⁡ w → y ∈ ℂ
8 7 adantl ⊢ φ ∧ y ∈ ℂ ∖ w ∈ ℂ | 0 ≤ ℜ ⁡ w → y ∈ ℂ
9 8 recld ⊢ φ ∧ y ∈ ℂ ∖ w ∈ ℂ | 0 ≤ ℜ ⁡ w → ℜ ⁡ y ∈ ℝ
10 fveq2 ⊢ w = y → ℜ ⁡ w = ℜ ⁡ y
11 10 breq2d ⊢ w = y → 0 ≤ ℜ ⁡ w ↔ 0 ≤ ℜ ⁡ y
12 11 notbid ⊢ w = y → ¬ 0 ≤ ℜ ⁡ w ↔ ¬ 0 ≤ ℜ ⁡ y
13 notrab ⊢ ℂ ∖ w ∈ ℂ | 0 ≤ ℜ ⁡ w = w ∈ ℂ | ¬ 0 ≤ ℜ ⁡ w
14 12 13 elrab2 ⊢ y ∈ ℂ ∖ w ∈ ℂ | 0 ≤ ℜ ⁡ w ↔ y ∈ ℂ ∧ ¬ 0 ≤ ℜ ⁡ y
15 14 simprbi ⊢ y ∈ ℂ ∖ w ∈ ℂ | 0 ≤ ℜ ⁡ w → ¬ 0 ≤ ℜ ⁡ y
16 15 adantl ⊢ φ ∧ y ∈ ℂ ∖ w ∈ ℂ | 0 ≤ ℜ ⁡ w → ¬ 0 ≤ ℜ ⁡ y
17 0re ⊢ 0 ∈ ℝ
18 ltnle ⊢ ℜ ⁡ y ∈ ℝ ∧ 0 ∈ ℝ → ℜ ⁡ y < 0 ↔ ¬ 0 ≤ ℜ ⁡ y
19 9 17 18 sylancl ⊢ φ ∧ y ∈ ℂ ∖ w ∈ ℂ | 0 ≤ ℜ ⁡ w → ℜ ⁡ y < 0 ↔ ¬ 0 ≤ ℜ ⁡ y
20 16 19 mpbird ⊢ φ ∧ y ∈ ℂ ∖ w ∈ ℂ | 0 ≤ ℜ ⁡ w → ℜ ⁡ y < 0
21 9 20 negelrpd ⊢ φ ∧ y ∈ ℂ ∖ w ∈ ℂ | 0 ≤ ℜ ⁡ w → − ℜ ⁡ y ∈ ℝ +
22 9 renegcld ⊢ φ ∧ y ∈ ℂ ∖ w ∈ ℂ | 0 ≤ ℜ ⁡ w → − ℜ ⁡ y ∈ ℝ
23 22 adantr ⊢ φ ∧ y ∈ ℂ ∖ w ∈ ℂ | 0 ≤ ℜ ⁡ w ∧ z ∈ w ∈ ℂ | 0 ≤ ℜ ⁡ w → − ℜ ⁡ y ∈ ℝ
24 elrabi ⊢ z ∈ w ∈ ℂ | 0 ≤ ℜ ⁡ w → z ∈ ℂ
25 24 adantl ⊢ φ ∧ y ∈ ℂ ∖ w ∈ ℂ | 0 ≤ ℜ ⁡ w ∧ z ∈ w ∈ ℂ | 0 ≤ ℜ ⁡ w → z ∈ ℂ
26 8 adantr ⊢ φ ∧ y ∈ ℂ ∖ w ∈ ℂ | 0 ≤ ℜ ⁡ w ∧ z ∈ w ∈ ℂ | 0 ≤ ℜ ⁡ w → y ∈ ℂ
27 25 26 subcld ⊢ φ ∧ y ∈ ℂ ∖ w ∈ ℂ | 0 ≤ ℜ ⁡ w ∧ z ∈ w ∈ ℂ | 0 ≤ ℜ ⁡ w → z − y ∈ ℂ
28 27 recld ⊢ φ ∧ y ∈ ℂ ∖ w ∈ ℂ | 0 ≤ ℜ ⁡ w ∧ z ∈ w ∈ ℂ | 0 ≤ ℜ ⁡ w → ℜ ⁡ z − y ∈ ℝ
29 27 abscld ⊢ φ ∧ y ∈ ℂ ∖ w ∈ ℂ | 0 ≤ ℜ ⁡ w ∧ z ∈ w ∈ ℂ | 0 ≤ ℜ ⁡ w → z − y ∈ ℝ
30 0red ⊢ φ ∧ y ∈ ℂ ∖ w ∈ ℂ | 0 ≤ ℜ ⁡ w ∧ z ∈ w ∈ ℂ | 0 ≤ ℜ ⁡ w → 0 ∈ ℝ
31 25 recld ⊢ φ ∧ y ∈ ℂ ∖ w ∈ ℂ | 0 ≤ ℜ ⁡ w ∧ z ∈ w ∈ ℂ | 0 ≤ ℜ ⁡ w → ℜ ⁡ z ∈ ℝ
32 26 recld ⊢ φ ∧ y ∈ ℂ ∖ w ∈ ℂ | 0 ≤ ℜ ⁡ w ∧ z ∈ w ∈ ℂ | 0 ≤ ℜ ⁡ w → ℜ ⁡ y ∈ ℝ
33 fveq2 ⊢ w = z → ℜ ⁡ w = ℜ ⁡ z
34 33 breq2d ⊢ w = z → 0 ≤ ℜ ⁡ w ↔ 0 ≤ ℜ ⁡ z
35 34 elrab ⊢ z ∈ w ∈ ℂ | 0 ≤ ℜ ⁡ w ↔ z ∈ ℂ ∧ 0 ≤ ℜ ⁡ z
36 35 simprbi ⊢ z ∈ w ∈ ℂ | 0 ≤ ℜ ⁡ w → 0 ≤ ℜ ⁡ z
37 36 adantl ⊢ φ ∧ y ∈ ℂ ∖ w ∈ ℂ | 0 ≤ ℜ ⁡ w ∧ z ∈ w ∈ ℂ | 0 ≤ ℜ ⁡ w → 0 ≤ ℜ ⁡ z
38 30 31 32 37 lesub1dd ⊢ φ ∧ y ∈ ℂ ∖ w ∈ ℂ | 0 ≤ ℜ ⁡ w ∧ z ∈ w ∈ ℂ | 0 ≤ ℜ ⁡ w → 0 − ℜ ⁡ y ≤ ℜ ⁡ z − ℜ ⁡ y
39 df-neg ⊢ − ℜ ⁡ y = 0 − ℜ ⁡ y
40 39 a1i ⊢ φ ∧ y ∈ ℂ ∖ w ∈ ℂ | 0 ≤ ℜ ⁡ w ∧ z ∈ w ∈ ℂ | 0 ≤ ℜ ⁡ w → − ℜ ⁡ y = 0 − ℜ ⁡ y
41 25 26 resubd ⊢ φ ∧ y ∈ ℂ ∖ w ∈ ℂ | 0 ≤ ℜ ⁡ w ∧ z ∈ w ∈ ℂ | 0 ≤ ℜ ⁡ w → ℜ ⁡ z − y = ℜ ⁡ z − ℜ ⁡ y
42 38 40 41 3brtr4d ⊢ φ ∧ y ∈ ℂ ∖ w ∈ ℂ | 0 ≤ ℜ ⁡ w ∧ z ∈ w ∈ ℂ | 0 ≤ ℜ ⁡ w → − ℜ ⁡ y ≤ ℜ ⁡ z − y
43 27 releabsd ⊢ φ ∧ y ∈ ℂ ∖ w ∈ ℂ | 0 ≤ ℜ ⁡ w ∧ z ∈ w ∈ ℂ | 0 ≤ ℜ ⁡ w → ℜ ⁡ z − y ≤ z − y
44 23 28 29 42 43 letrd ⊢ φ ∧ y ∈ ℂ ∖ w ∈ ℂ | 0 ≤ ℜ ⁡ w ∧ z ∈ w ∈ ℂ | 0 ≤ ℜ ⁡ w → − ℜ ⁡ y ≤ z − y
45 fveq2 ⊢ w = B → ℜ ⁡ w = ℜ ⁡ B
46 45 breq2d ⊢ w = B → 0 ≤ ℜ ⁡ w ↔ 0 ≤ ℜ ⁡ B
47 46 3 4 elrabd ⊢ φ ∧ x ∈ A → B ∈ w ∈ ℂ | 0 ≤ ℜ ⁡ w
48 1 2 6 21 44 47 rlimcld2 ⊢ φ → C ∈ w ∈ ℂ | 0 ≤ ℜ ⁡ w
49 fveq2 ⊢ w = C → ℜ ⁡ w = ℜ ⁡ C
50 49 breq2d ⊢ w = C → 0 ≤ ℜ ⁡ w ↔ 0 ≤ ℜ ⁡ C
51 50 elrab ⊢ C ∈ w ∈ ℂ | 0 ≤ ℜ ⁡ w ↔ C ∈ ℂ ∧ 0 ≤ ℜ ⁡ C
52 51 simprbi ⊢ C ∈ w ∈ ℂ | 0 ≤ ℜ ⁡ w → 0 ≤ ℜ ⁡ C
53 48 52 syl ⊢ φ → 0 ≤ ℜ ⁡ C