Theorem possumd

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

	Ref	Expression
Hypotheses	possumd.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	possumd.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
Assertion	possumd	⊢ ( 𝜑 → ( 0 < ( 𝐴 + 𝐵 ) ↔ - 𝐵 < 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		possumd.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		possumd.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3	2	renegcld	⊢ ( 𝜑 → - 𝐵 ∈ ℝ )
4	3 1	posdifd	⊢ ( 𝜑 → ( - 𝐵 < 𝐴 ↔ 0 < ( 𝐴 − - 𝐵 ) ) )
5	1	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
6	2	recnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
7	5 6	subnegd	⊢ ( 𝜑 → ( 𝐴 − - 𝐵 ) = ( 𝐴 + 𝐵 ) )
8	7	breq2d	⊢ ( 𝜑 → ( 0 < ( 𝐴 − - 𝐵 ) ↔ 0 < ( 𝐴 + 𝐵 ) ) )
9	4 8	bitr2d	⊢ ( 𝜑 → ( 0 < ( 𝐴 + 𝐵 ) ↔ - 𝐵 < 𝐴 ) )