Metamath Proof Explorer

Theorem leaddsub2

Description: 'Less than or equal to' relationship between and addition and subtraction. (Contributed by NM, 6-Apr-2005)

Ref Expression
Assertion leaddsub2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + B ≤ C ↔ B ≤ C − A

Proof

Step Hyp Ref Expression
1 recn ⊢ A ∈ ℝ → A ∈ ℂ
2 recn ⊢ B ∈ ℝ → B ∈ ℂ
3 addcom ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B = B + A
4 1 2 3 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B = B + A
5 4 3adant3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + B = B + A
6 5 breq1d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + B ≤ C ↔ B + A ≤ C
7 leaddsub ⊢ B ∈ ℝ ∧ A ∈ ℝ ∧ C ∈ ℝ → B + A ≤ C ↔ B ≤ C − A
8 7 3com12 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B + A ≤ C ↔ B ≤ C − A
9 6 8 bitrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + B ≤ C ↔ B ≤ C − A