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 | |- ( ph -> A e. RR ) |
|
sn-addgt0d.b | |- ( ph -> B e. RR ) |
||
sn-addgt0d.1 | |- ( ph -> 0 < A ) |
||
sn-addgt0d.2 | |- ( ph -> 0 < B ) |
||
Assertion | sn-addgt0d | |- ( ph -> 0 < ( A + B ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sn-addgt0d.a | |- ( ph -> A e. RR ) |
|
2 | sn-addgt0d.b | |- ( ph -> B e. RR ) |
|
3 | sn-addgt0d.1 | |- ( ph -> 0 < A ) |
|
4 | sn-addgt0d.2 | |- ( ph -> 0 < B ) |
|
5 | 0red | |- ( ph -> 0 e. RR ) |
|
6 | 1 2 | readdcld | |- ( ph -> ( A + B ) e. RR ) |
7 | sn-ltaddpos | |- ( ( B e. RR /\ A e. RR ) -> ( 0 < B <-> A < ( A + B ) ) ) |
|
8 | 2 1 7 | syl2anc | |- ( ph -> ( 0 < B <-> A < ( A + B ) ) ) |
9 | 4 8 | mpbid | |- ( ph -> A < ( A + B ) ) |
10 | 5 1 6 3 9 | lttrd | |- ( ph -> 0 < ( A + B ) ) |