Theorem ltsubrp

Description: Subtracting a positive real from another number decreases it. (Contributed by FL, 27-Dec-2007)

	Ref	Expression
Assertion	ltsubrp	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to A-B<A$$

Proof

Step	Hyp	Ref	Expression
1		elrp	$$⊢B\in {ℝ}^{+}\leftrightarrow \left(B\in ℝ\wedge 0<B\right)$$
2		ltsubpos	$$⊢\left(B\in ℝ\wedge A\in ℝ\right)\to \left(0<B\leftrightarrow A-B<A\right)$$
3	2	biimpd	$$⊢\left(B\in ℝ\wedge A\in ℝ\right)\to \left(0<B\to A-B<A\right)$$
4	3	expcom	$$⊢A\in ℝ\to \left(B\in ℝ\to \left(0<B\to A-B<A\right)\right)$$
5	4	imp32	$$⊢\left(A\in ℝ\wedge \left(B\in ℝ\wedge 0<B\right)\right)\to A-B<A$$
6	1 5	sylan2b	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to A-B<A$$