Metamath Proof Explorer


Theorem possumd

Description: Condition for a positive sum. (Contributed by Scott Fenton, 16-Dec-2017)

Ref Expression
Hypotheses possumd.1
|- ( ph -> A e. RR )
possumd.2
|- ( ph -> B e. RR )
Assertion possumd
|- ( ph -> ( 0 < ( A + B ) <-> -u B < A ) )

Proof

Step Hyp Ref Expression
1 possumd.1
 |-  ( ph -> A e. RR )
2 possumd.2
 |-  ( ph -> B e. RR )
3 2 renegcld
 |-  ( ph -> -u B e. RR )
4 3 1 posdifd
 |-  ( ph -> ( -u B < A <-> 0 < ( A - -u B ) ) )
5 1 recnd
 |-  ( ph -> A e. CC )
6 2 recnd
 |-  ( ph -> B e. CC )
7 5 6 subnegd
 |-  ( ph -> ( A - -u B ) = ( A + B ) )
8 7 breq2d
 |-  ( ph -> ( 0 < ( A - -u B ) <-> 0 < ( A + B ) ) )
9 4 8 bitr2d
 |-  ( ph -> ( 0 < ( A + B ) <-> -u B < A ) )