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 | ||
sn-addgt0d.b | |||
sn-addgt0d.1 | |||
sn-addgt0d.2 | |||
Assertion | sn-addgt0d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sn-addgt0d.a | ||
2 | sn-addgt0d.b | ||
3 | sn-addgt0d.1 | ||
4 | sn-addgt0d.2 | ||
5 | 0red | ||
6 | 1 2 | readdcld | |
7 | sn-ltaddpos | ||
8 | 2 1 7 | syl2anc | |
9 | 4 8 | mpbid | |
10 | 5 1 6 3 9 | lttrd |