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 ≤ ( 𝐴 + 𝐵 ) )