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	$$⊢\phi \to A\in ℝ$$
	ltnegd.2	$$⊢\phi \to B\in ℝ$$
	ltadd1d.3	$$⊢\phi \to C\in ℝ$$
	lesub3d.x	$$⊢\phi \to X\in ℝ$$
	lesub3d.g	$$⊢\phi \to X+C\le A$$
	lesub3d.l	$$⊢\phi \to B\le X$$
Assertion	lesub3d	$$⊢\phi \to C\le A-B$$

Proof

Step	Hyp	Ref	Expression
1		leidd.1	$$⊢\phi \to A\in ℝ$$
2		ltnegd.2	$$⊢\phi \to B\in ℝ$$
3		ltadd1d.3	$$⊢\phi \to C\in ℝ$$
4		lesub3d.x	$$⊢\phi \to X\in ℝ$$
5		lesub3d.g	$$⊢\phi \to X+C\le A$$
6		lesub3d.l	$$⊢\phi \to B\le X$$
7	3 2	readdcld	$$⊢\phi \to C+B\in ℝ$$
8	4 3	readdcld	$$⊢\phi \to X+C\in ℝ$$
9	3	recnd	$$⊢\phi \to C\in ℂ$$
10	2	recnd	$$⊢\phi \to B\in ℂ$$
11	9 10	addcomd	$$⊢\phi \to C+B=B+C$$
12	2 4 3 6	leadd1dd	$$⊢\phi \to B+C\le X+C$$
13	11 12	eqbrtrd	$$⊢\phi \to C+B\le X+C$$
14	7 8 1 13 5	letrd	$$⊢\phi \to C+B\le A$$
15		leaddsub	$$⊢\left(C\in ℝ\wedge B\in ℝ\wedge A\in ℝ\right)\to \left(C+B\le A\leftrightarrow C\le A-B\right)$$
16	3 2 1 15	syl3anc	$$⊢\phi \to \left(C+B\le A\leftrightarrow C\le A-B\right)$$
17	14 16	mpbid	$$⊢\phi \to C\le A-B$$