Metamath Proof Explorer

Theorem leadd1

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 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A≤B↔A+C≤B+C

Proof

Step Hyp Ref Expression
1 ltadd1 ⊢B∈ℝ∧A∈ℝ∧C∈ℝ→B<A↔B+C<A+C
2 1 3com12 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→B<A↔B+C<A+C
3 2 notbid ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→¬B<A↔¬B+C<A+C
4 simp1 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A∈ℝ
5 simp2 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→B∈ℝ
6 4 5 lenltd ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A≤B↔¬B<A
7 simp3 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→C∈ℝ
8 4 7 readdcld ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A+C∈ℝ
9 5 7 readdcld ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→B+C∈ℝ
10 8 9 lenltd ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A+C≤B+C↔¬B+C<A+C
11 3 6 10 3bitr4d ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A≤B↔A+C≤B+C