Theorem lesubadd

Description: 'Less than or equal to' relationship between subtraction and addition. (Contributed by NM, 17-Nov-2004) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

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