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 ⊢φ→supAℝ*<=+∞
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 ⊢φ→supAℝ*<=+∞
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