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+∞