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 ≤ 𝐶 ) |
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 ≤ 𝐶 ) |