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