Metamath Proof Explorer

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 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left({A}-{B}\le {C}↔{A}\le {C}+{B}\right)$

Proof

Step Hyp Ref Expression
1 simp1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to {A}\in ℝ$
2 simp2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to {B}\in ℝ$
3 1 2 resubcld ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to {A}-{B}\in ℝ$
4 simp3 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to {C}\in ℝ$
5 leadd1 ${⊢}\left({A}-{B}\in ℝ\wedge {C}\in ℝ\wedge {B}\in ℝ\right)\to \left({A}-{B}\le {C}↔{A}-{B}+{B}\le {C}+{B}\right)$
6 3 4 2 5 syl3anc ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left({A}-{B}\le {C}↔{A}-{B}+{B}\le {C}+{B}\right)$
7 1 recnd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to {A}\in ℂ$
8 2 recnd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to {B}\in ℂ$
9 7 8 npcand ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to {A}-{B}+{B}={A}$
10 9 breq1d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left({A}-{B}+{B}\le {C}+{B}↔{A}\le {C}+{B}\right)$
11 6 10 bitrd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left({A}-{B}\le {C}↔{A}\le {C}+{B}\right)$