Metamath Proof Explorer


Theorem ltaddpos2

Description: Adding a positive number to another number increases it. (Contributed by NM, 8-Apr-2005)

Ref Expression
Assertion ltaddpos2
|- ( ( A e. RR /\ B e. RR ) -> ( 0 < A <-> B < ( A + B ) ) )

Proof

Step Hyp Ref Expression
1 ltaddpos
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 < A <-> B < ( B + A ) ) )
2 recn
 |-  ( A e. RR -> A e. CC )
3 recn
 |-  ( B e. RR -> B e. CC )
4 addcom
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
5 2 3 4 syl2an
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + B ) = ( B + A ) )
6 5 breq2d
 |-  ( ( A e. RR /\ B e. RR ) -> ( B < ( A + B ) <-> B < ( B + A ) ) )
7 1 6 bitr4d
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 < A <-> B < ( A + B ) ) )