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