Theorem addgegt0

Description: The sum of nonnegative and positive numbers is positive. (Contributed by NM, 28-Dec-2005) (Proof shortened by Andrew Salmon, 19-Nov-2011)

	Ref	Expression
Assertion	addgegt0	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 < 𝐵 ) ) → 0 < ( 𝐴 + 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		00id	⊢ ( 0 + 0 ) = 0
2		0re	⊢ 0 ∈ ℝ
3		leltadd	⊢ ( ( ( 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 < ( 𝐴 + 𝐵 ) )