Metamath Proof Explorer


Theorem addge0

Description: The sum of 2 nonnegative numbers is nonnegative. (Contributed by NM, 17-Mar-2005) (Proof shortened by Andrew Salmon, 19-Nov-2011)

Ref Expression
Assertion addge0 ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) ) → 0 ≤ ( 𝐴 + 𝐵 ) )

Proof

Step Hyp Ref Expression
1 00id ( 0 + 0 ) = 0
2 0re 0 ∈ ℝ
3 le2add ( ( ( 0 ∈ ℝ ∧ 0 ∈ ℝ ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) → ( ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) → ( 0 + 0 ) ≤ ( 𝐴 + 𝐵 ) ) )
4 2 2 3 mpanl12 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) → ( 0 + 0 ) ≤ ( 𝐴 + 𝐵 ) ) )
5 4 imp ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) ) → ( 0 + 0 ) ≤ ( 𝐴 + 𝐵 ) )
6 1 5 eqbrtrrid ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) ) → 0 ≤ ( 𝐴 + 𝐵 ) )