This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem possumd

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

Ref Expression
Hypotheses possumd.1 ⊢ φ → A ∈ ℝ
possumd.2 ⊢ φ → B ∈ ℝ
Assertion possumd ⊢ φ → 0 < A + B ↔ − B < A

Proof

Step Hyp Ref Expression
1 possumd.1 ⊢ φ → A ∈ ℝ
2 possumd.2 ⊢ φ → B ∈ ℝ
3 2 renegcld ⊢ φ → − B ∈ ℝ
4 3 1 posdifd ⊢ φ → − B < A ↔ 0 < A − − B
5 1 recnd ⊢ φ → A ∈ ℂ
6 2 recnd ⊢ φ → B ∈ ℂ
7 5 6 subnegd ⊢ φ → A − − B = A + B
8 7 breq2d ⊢ φ → 0 < A − − B ↔ 0 < A + B
9 4 8 bitr2d ⊢ φ → 0 < A + B ↔ − B < A