Metamath Proof Explorer


Theorem addgt0

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

Ref Expression
Assertion addgt0 ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 < 𝐴 ∧ 0 < 𝐵 ) ) → 0 < ( 𝐴 + 𝐵 ) )

Proof

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