Theorem ltsubrp

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

	Ref	Expression
Assertion	ltsubrp	|- ( ( A e. RR /\ B e. RR+ ) -> ( A - B ) < A )

Proof

Step	Hyp	Ref	Expression
1		elrp	|- ( B e. RR+ <-> ( B e. RR /\ 0 < B ) )
2		ltsubpos	|- ( ( B e. RR /\ A e. RR ) -> ( 0 < B <-> ( A - B ) < A ) )
3	2	biimpd	|- ( ( B e. RR /\ A e. RR ) -> ( 0 < B -> ( A - B ) < A ) )
4	3	expcom	|- ( A e. RR -> ( B e. RR -> ( 0 < B -> ( A - B ) < A ) ) )
5	4	imp32	|- ( ( A e. RR /\ ( B e. RR /\ 0 < B ) ) -> ( A - B ) < A )
6	1 5	sylan2b	|- ( ( A e. RR /\ B e. RR+ ) -> ( A - B ) < A )