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 ( 𝐴 , ℝ* , < ) = +∞ )
rlimcld2.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 )
rlimrege0.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
rlimrege0.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ ( ℜ ‘ 𝐵 ) )
Assertion rlimrege0 ( 𝜑 → 0 ≤ ( ℜ ‘ 𝐶 ) )

Proof

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