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 ≤ ( ℜ ‘ 𝐶 ) )