Description: Subtracting a positive number from another number decreases it. (Contributed by NM, 17-Nov-2004) (Proof shortened by Andrew Salmon, 19-Nov-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ltsubpos | |- ( ( A e. RR /\ B e. RR ) -> ( 0 < A <-> ( B - A ) < B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ltaddpos | |- ( ( A e. RR /\ B e. RR ) -> ( 0 < A <-> B < ( B + A ) ) ) |
|
| 2 | ltsubadd | |- ( ( B e. RR /\ A e. RR /\ B e. RR ) -> ( ( B - A ) < B <-> B < ( B + A ) ) ) |
|
| 3 | 2 | 3anidm13 | |- ( ( B e. RR /\ A e. RR ) -> ( ( B - A ) < B <-> B < ( B + A ) ) ) |
| 4 | 3 | ancoms | |- ( ( A e. RR /\ B e. RR ) -> ( ( B - A ) < B <-> B < ( B + A ) ) ) |
| 5 | 1 4 | bitr4d | |- ( ( A e. RR /\ B e. RR ) -> ( 0 < A <-> ( B - A ) < B ) ) |