# Metamath Proof Explorer

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

Ref Expression
Assertion ge0addcl ${⊢}\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 readdcl ${⊢}\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 addge0 ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left(0\le {A}\wedge 0\le {B}\right)\right)\to 0\le {A}+{B}$
6 5 an4s ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge \left({B}\in ℝ\wedge 0\le {B}\right)\right)\to 0\le {A}+{B}$
7 elrege0 ${⊢}{A}+{B}\in \left[0,\mathrm{+\infty }\right)↔\left({A}+{B}\in ℝ\wedge 0\le {A}+{B}\right)$
8 4 6 7 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)$
9 1 2 8 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)$