# Metamath Proof Explorer

Description: Addition to both sides of 'less than or equal to'. (Contributed by NM, 18-Oct-1999) (Proof shortened by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion leadd1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left({A}\le {B}↔{A}+{C}\le {B}+{C}\right)$

### Proof

Step Hyp Ref Expression
1 ltadd1 ${⊢}\left({B}\in ℝ\wedge {A}\in ℝ\wedge {C}\in ℝ\right)\to \left({B}<{A}↔{B}+{C}<{A}+{C}\right)$
2 1 3com12 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left({B}<{A}↔{B}+{C}<{A}+{C}\right)$
3 2 notbid ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left(¬{B}<{A}↔¬{B}+{C}<{A}+{C}\right)$
4 simp1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to {A}\in ℝ$
5 simp2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to {B}\in ℝ$
6 4 5 lenltd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left({A}\le {B}↔¬{B}<{A}\right)$
7 simp3 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to {C}\in ℝ$
8 4 7 readdcld ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to {A}+{C}\in ℝ$
9 5 7 readdcld ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to {B}+{C}\in ℝ$
10 8 9 lenltd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left({A}+{C}\le {B}+{C}↔¬{B}+{C}<{A}+{C}\right)$
11 3 6 10 3bitr4d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left({A}\le {B}↔{A}+{C}\le {B}+{C}\right)$