Theorem lesub2

Description: Subtraction of both sides of 'less than or equal to'. (Contributed by NM, 29-Sep-2005) (Revised by Mario Carneiro, 27-May-2016)

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

Proof

Step	Hyp	Ref	Expression
1		leadd2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐶 + 𝐴 ) ≤ ( 𝐶 + 𝐵 ) ) )
2		simp3	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ )
3		simp1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℝ )
4	2 3	readdcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 + 𝐴 ) ∈ ℝ )
5		simp2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℝ )
6		lesubadd	⊢ ( ( ( 𝐶 + 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐶 + 𝐴 ) − 𝐵 ) ≤ 𝐶 ↔ ( 𝐶 + 𝐴 ) ≤ ( 𝐶 + 𝐵 ) ) )
7	4 5 2 6	syl3anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐶 + 𝐴 ) − 𝐵 ) ≤ 𝐶 ↔ ( 𝐶 + 𝐴 ) ≤ ( 𝐶 + 𝐵 ) ) )
8	2	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℂ )
9	3	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℂ )
10	5	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℂ )
11	8 9 10	addsubd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐶 + 𝐴 ) − 𝐵 ) = ( ( 𝐶 − 𝐵 ) + 𝐴 ) )
12	11	breq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐶 + 𝐴 ) − 𝐵 ) ≤ 𝐶 ↔ ( ( 𝐶 − 𝐵 ) + 𝐴 ) ≤ 𝐶 ) )
13	1 7 12	3bitr2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ( ( 𝐶 − 𝐵 ) + 𝐴 ) ≤ 𝐶 ) )
14	2 5	resubcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 − 𝐵 ) ∈ ℝ )
15		leaddsub	⊢ ( ( ( 𝐶 − 𝐵 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐶 − 𝐵 ) + 𝐴 ) ≤ 𝐶 ↔ ( 𝐶 − 𝐵 ) ≤ ( 𝐶 − 𝐴 ) ) )
16	14 3 2 15	syl3anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐶 − 𝐵 ) + 𝐴 ) ≤ 𝐶 ↔ ( 𝐶 − 𝐵 ) ≤ ( 𝐶 − 𝐴 ) ) )
17	13 16	bitrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐶 − 𝐵 ) ≤ ( 𝐶 − 𝐴 ) ) )