Metamath Proof Explorer

Theorem leltadd

Description: Adding both sides of two orderings. (Contributed by NM, 15-Aug-2008)

Ref Expression
Assertion leltadd ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧D∈ℝ→A≤C∧B<D→A+B<C+D

Proof

Step Hyp Ref Expression
1 ltleadd ⊢B∈ℝ∧A∈ℝ∧D∈ℝ∧C∈ℝ→B<D∧A≤C→B+A<D+C
2 1 ancomsd ⊢B∈ℝ∧A∈ℝ∧D∈ℝ∧C∈ℝ→A≤C∧B<D→B+A<D+C
3 2 ancom2s ⊢B∈ℝ∧A∈ℝ∧C∈ℝ∧D∈ℝ→A≤C∧B<D→B+A<D+C
4 3 ancom1s ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧D∈ℝ→A≤C∧B<D→B+A<D+C
5 recn ⊢A∈ℝ→A∈ℂ
6 recn ⊢B∈ℝ→B∈ℂ
7 addcom ⊢A∈ℂ∧B∈ℂ→A+B=B+A
8 5 6 7 syl2an ⊢A∈ℝ∧B∈ℝ→A+B=B+A
9 recn ⊢C∈ℝ→C∈ℂ
10 recn ⊢D∈ℝ→D∈ℂ
11 addcom ⊢C∈ℂ∧D∈ℂ→C+D=D+C
12 9 10 11 syl2an ⊢C∈ℝ∧D∈ℝ→C+D=D+C
13 8 12 breqan12d ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧D∈ℝ→A+B<C+D↔B+A<D+C
14 4 13 sylibrd ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧D∈ℝ→A≤C∧B<D→A+B<C+D