This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem addgt0d

Description: Addition of 2 positive numbers is positive. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypotheses leidd.1 ⊢ φ → A ∈ ℝ
ltnegd.2 ⊢ φ → B ∈ ℝ
addgt0d.3 ⊢ φ → 0 < A
addgt0d.4 ⊢ φ → 0 < B
Assertion addgt0d ⊢ φ → 0 < A + B

Proof

Step Hyp Ref Expression
1 leidd.1 ⊢ φ → A ∈ ℝ
2 ltnegd.2 ⊢ φ → B ∈ ℝ
3 addgt0d.3 ⊢ φ → 0 < A
4 addgt0d.4 ⊢ φ → 0 < B
5 0red ⊢ φ → 0 ∈ ℝ
6 5 1 3 ltled ⊢ φ → 0 ≤ A
7 1 2 6 4 addgegt0d ⊢ φ → 0 < A + B