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
|- ( 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 ) )

Proof

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 ) )