Theorem possumd

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

	Ref	Expression
Hypotheses	possumd.1	$$⊢\phi \to A\in ℝ$$
	possumd.2	$$⊢\phi \to B\in ℝ$$
Assertion	possumd	$$⊢\phi \to \left(0<A+B\leftrightarrow -B<A\right)$$

Proof

Step	Hyp	Ref	Expression
1		possumd.1	$$⊢\phi \to A\in ℝ$$
2		possumd.2	$$⊢\phi \to B\in ℝ$$
3	2	renegcld	$$⊢\phi \to -B\in ℝ$$
4	3 1	posdifd	$$⊢\phi \to \left(-B<A\leftrightarrow 0<A-\left(-B\right)\right)$$
5	1	recnd	$$⊢\phi \to A\in ℂ$$
6	2	recnd	$$⊢\phi \to B\in ℂ$$
7	5 6	subnegd	$$⊢\phi \to A-\left(-B\right)=A+B$$
8	7	breq2d	$$⊢\phi \to \left(0<A-\left(-B\right)\leftrightarrow 0<A+B\right)$$
9	4 8	bitr2d	$$⊢\phi \to \left(0<A+B\leftrightarrow -B<A\right)$$