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