Metamath Proof Explorer

Theorem ge0mulcl

Description: The nonnegative reals are closed under multiplication. (Contributed by Mario Carneiro, 19-Jun-2014)

Ref Expression
Assertion ge0mulcl ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ → A ⁢ B ∈ 0 +∞

Proof

Step Hyp Ref Expression
1 elrege0 ⊢ A ∈ 0 +∞ ↔ A ∈ ℝ ∧ 0 ≤ A
2 elrege0 ⊢ B ∈ 0 +∞ ↔ B ∈ ℝ ∧ 0 ≤ B
3 remulcl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ⁢ B ∈ ℝ
4 3 ad2ant2r ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A ⁢ B ∈ ℝ
5 mulge0 ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → 0 ≤ A ⁢ B
6 elrege0 ⊢ A ⁢ B ∈ 0 +∞ ↔ A ⁢ B ∈ ℝ ∧ 0 ≤ A ⁢ B
7 4 5 6 sylanbrc ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A ⁢ B ∈ 0 +∞
8 1 2 7 syl2anb ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ → A ⁢ B ∈ 0 +∞