# Metamath Proof Explorer

## Theorem ge0mulcl

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

Ref Expression
Assertion ge0mulcl ${⊢}\left({A}\in \left[0,\mathrm{+\infty }\right)\wedge {B}\in \left[0,\mathrm{+\infty }\right)\right)\to {A}{B}\in \left[0,\mathrm{+\infty }\right)$

### Proof

Step Hyp Ref Expression
1 elrege0 ${⊢}{A}\in \left[0,\mathrm{+\infty }\right)↔\left({A}\in ℝ\wedge 0\le {A}\right)$
2 elrege0 ${⊢}{B}\in \left[0,\mathrm{+\infty }\right)↔\left({B}\in ℝ\wedge 0\le {B}\right)$
3 remulcl ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}{B}\in ℝ$
4 3 ad2ant2r ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge \left({B}\in ℝ\wedge 0\le {B}\right)\right)\to {A}{B}\in ℝ$
5 mulge0 ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge \left({B}\in ℝ\wedge 0\le {B}\right)\right)\to 0\le {A}{B}$
6 elrege0 ${⊢}{A}{B}\in \left[0,\mathrm{+\infty }\right)↔\left({A}{B}\in ℝ\wedge 0\le {A}{B}\right)$
7 4 5 6 sylanbrc ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge \left({B}\in ℝ\wedge 0\le {B}\right)\right)\to {A}{B}\in \left[0,\mathrm{+\infty }\right)$
8 1 2 7 syl2anb ${⊢}\left({A}\in \left[0,\mathrm{+\infty }\right)\wedge {B}\in \left[0,\mathrm{+\infty }\right)\right)\to {A}{B}\in \left[0,\mathrm{+\infty }\right)$