Theorem lesub3d

Description: The result of subtracting a number less than or equal to an intermediate number from a number greater than or equal to a third number increased by the intermediate number is greater than or equal to the third number. (Contributed by AV, 13-Aug-2020)

	Ref	Expression
Hypotheses	leidd.1	|- ( ph -> A e. RR )
	ltnegd.2	|- ( ph -> B e. RR )
	ltadd1d.3	|- ( ph -> C e. RR )
	lesub3d.x	|- ( ph -> X e. RR )
	lesub3d.g	|- ( ph -> ( X + C ) <_ A )
	lesub3d.l	|- ( ph -> B <_ X )
Assertion	lesub3d	|- ( ph -> C <_ ( A - B ) )

Proof

Step	Hyp	Ref	Expression
1		leidd.1	|- ( ph -> A e. RR )
2		ltnegd.2	|- ( ph -> B e. RR )
3		ltadd1d.3	|- ( ph -> C e. RR )
4		lesub3d.x	|- ( ph -> X e. RR )
5		lesub3d.g	|- ( ph -> ( X + C ) <_ A )
6		lesub3d.l	|- ( ph -> B <_ X )
7	3 2	readdcld	|- ( ph -> ( C + B ) e. RR )
8	4 3	readdcld	|- ( ph -> ( X + C ) e. RR )
9	3	recnd	|- ( ph -> C e. CC )
10	2	recnd	|- ( ph -> B e. CC )
11	9 10	addcomd	|- ( ph -> ( C + B ) = ( B + C ) )
12	2 4 3 6	leadd1dd	|- ( ph -> ( B + C ) <_ ( X + C ) )
13	11 12	eqbrtrd	|- ( ph -> ( C + B ) <_ ( X + C ) )
14	7 8 1 13 5	letrd	|- ( ph -> ( C + B ) <_ A )
15		leaddsub	|- ( ( C e. RR /\ B e. RR /\ A e. RR ) -> ( ( C + B ) <_ A <-> C <_ ( A - B ) ) )
16	3 2 1 15	syl3anc	|- ( ph -> ( ( C + B ) <_ A <-> C <_ ( A - B ) ) )
17	14 16	mpbid	|- ( ph -> C <_ ( A - B ) )