Theorem lesub1

Description: Subtraction from both sides of 'less than or equal to'. (Contributed by NM, 13-May-2004) (Proof shortened by Mario Carneiro, 27-May-2016)

	Ref	Expression
Assertion	lesub1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 − 𝐶 ) ≤ ( 𝐵 − 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℝ )
2		simp3	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ )
3		simp2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℝ )
4	3 2	resubcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 − 𝐶 ) ∈ ℝ )
5		lesubadd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ ( 𝐵 − 𝐶 ) ∈ ℝ ) → ( ( 𝐴 − 𝐶 ) ≤ ( 𝐵 − 𝐶 ) ↔ 𝐴 ≤ ( ( 𝐵 − 𝐶 ) + 𝐶 ) ) )
6	1 2 4 5	syl3anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 − 𝐶 ) ≤ ( 𝐵 − 𝐶 ) ↔ 𝐴 ≤ ( ( 𝐵 − 𝐶 ) + 𝐶 ) ) )
7	3	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℂ )
8	2	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℂ )
9	7 8	npcand	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐵 − 𝐶 ) + 𝐶 ) = 𝐵 )
10	9	breq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ≤ ( ( 𝐵 − 𝐶 ) + 𝐶 ) ↔ 𝐴 ≤ 𝐵 ) )
11	6 10	bitr2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 − 𝐶 ) ≤ ( 𝐵 − 𝐶 ) ) )