Theorem leaddsuble

Description: Addition and subtraction on one side of "less than or equal to". (Contributed by Alexander van der Vekens, 18-Mar-2018)

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

Proof

Step	Hyp	Ref	Expression
1		leadd2	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐵 ≤ 𝐶 ↔ ( 𝐴 + 𝐵 ) ≤ ( 𝐴 + 𝐶 ) ) )
2	1	3comr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 ≤ 𝐶 ↔ ( 𝐴 + 𝐵 ) ≤ ( 𝐴 + 𝐶 ) ) )
3		readdcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
4	3	3adant3	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
5		simp3	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ )
6		simp1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℝ )
7	4 5 6	lesubaddd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐴 + 𝐵 ) − 𝐶 ) ≤ 𝐴 ↔ ( 𝐴 + 𝐵 ) ≤ ( 𝐴 + 𝐶 ) ) )
8	2 7	bitr4d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 ≤ 𝐶 ↔ ( ( 𝐴 + 𝐵 ) − 𝐶 ) ≤ 𝐴 ) )