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	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	ltnegd.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	ltadd1d.3	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	lesub3d.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
	lesub3d.g	⊢ ( 𝜑 → ( 𝑋 + 𝐶 ) ≤ 𝐴 )
	lesub3d.l	⊢ ( 𝜑 → 𝐵 ≤ 𝑋 )
Assertion	lesub3d	⊢ ( 𝜑 → 𝐶 ≤ ( 𝐴 − 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		leidd.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		ltnegd.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		ltadd1d.3	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4		lesub3d.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
5		lesub3d.g	⊢ ( 𝜑 → ( 𝑋 + 𝐶 ) ≤ 𝐴 )
6		lesub3d.l	⊢ ( 𝜑 → 𝐵 ≤ 𝑋 )
7	3 2	readdcld	⊢ ( 𝜑 → ( 𝐶 + 𝐵 ) ∈ ℝ )
8	4 3	readdcld	⊢ ( 𝜑 → ( 𝑋 + 𝐶 ) ∈ ℝ )
9	3	recnd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
10	2	recnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
11	9 10	addcomd	⊢ ( 𝜑 → ( 𝐶 + 𝐵 ) = ( 𝐵 + 𝐶 ) )
12	2 4 3 6	leadd1dd	⊢ ( 𝜑 → ( 𝐵 + 𝐶 ) ≤ ( 𝑋 + 𝐶 ) )
13	11 12	eqbrtrd	⊢ ( 𝜑 → ( 𝐶 + 𝐵 ) ≤ ( 𝑋 + 𝐶 ) )
14	7 8 1 13 5	letrd	⊢ ( 𝜑 → ( 𝐶 + 𝐵 ) ≤ 𝐴 )
15		leaddsub	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝐶 + 𝐵 ) ≤ 𝐴 ↔ 𝐶 ≤ ( 𝐴 − 𝐵 ) ) )
16	3 2 1 15	syl3anc	⊢ ( 𝜑 → ( ( 𝐶 + 𝐵 ) ≤ 𝐴 ↔ 𝐶 ≤ ( 𝐴 − 𝐵 ) ) )
17	14 16	mpbid	⊢ ( 𝜑 → 𝐶 ≤ ( 𝐴 − 𝐵 ) )