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