Metamath Proof Explorer


Theorem rlimge0

Description: The limit of a sequence of nonnegative reals is nonnegative. (Contributed by Mario Carneiro, 10-May-2016)

Ref Expression
Hypotheses rlimcld2.1 ( 𝜑 → sup ( 𝐴 , ℝ* , < ) = +∞ )
rlimcld2.2 ( 𝜑 → ( 𝑥𝐴𝐵 ) ⇝𝑟 𝐶 )
rlimrecl.3 ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℝ )
rlimge0.4 ( ( 𝜑𝑥𝐴 ) → 0 ≤ 𝐵 )
Assertion rlimge0 ( 𝜑 → 0 ≤ 𝐶 )

Proof

Step Hyp Ref Expression
1 rlimcld2.1 ( 𝜑 → sup ( 𝐴 , ℝ* , < ) = +∞ )
2 rlimcld2.2 ( 𝜑 → ( 𝑥𝐴𝐵 ) ⇝𝑟 𝐶 )
3 rlimrecl.3 ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℝ )
4 rlimge0.4 ( ( 𝜑𝑥𝐴 ) → 0 ≤ 𝐵 )
5 3 recnd ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℂ )
6 3 rered ( ( 𝜑𝑥𝐴 ) → ( ℜ ‘ 𝐵 ) = 𝐵 )
7 4 6 breqtrrd ( ( 𝜑𝑥𝐴 ) → 0 ≤ ( ℜ ‘ 𝐵 ) )
8 1 2 5 7 rlimrege0 ( 𝜑 → 0 ≤ ( ℜ ‘ 𝐶 ) )
9 1 2 3 rlimrecl ( 𝜑𝐶 ∈ ℝ )
10 9 rered ( 𝜑 → ( ℜ ‘ 𝐶 ) = 𝐶 )
11 8 10 breqtrd ( 𝜑 → 0 ≤ 𝐶 )