Metamath Proof Explorer


Theorem sn-addgt0d

Description: The sum of positive numbers is positive. Proof of addgt0d without ax-mulcom . (Contributed by SN, 25-Jan-2025)

Ref Expression
Hypotheses sn-addgt0d.a φ A
sn-addgt0d.b φ B
sn-addgt0d.1 φ 0 < A
sn-addgt0d.2 φ 0 < B
Assertion sn-addgt0d φ 0 < A + B

Proof

Step Hyp Ref Expression
1 sn-addgt0d.a φ A
2 sn-addgt0d.b φ B
3 sn-addgt0d.1 φ 0 < A
4 sn-addgt0d.2 φ 0 < B
5 0red φ 0
6 1 2 readdcld φ A + B
7 sn-ltaddpos B A 0 < B A < A + B
8 2 1 7 syl2anc φ 0 < B A < A + B
9 4 8 mpbid φ A < A + B
10 5 1 6 3 9 lttrd φ 0 < A + B