Metamath Proof Explorer

Theorem ltleadd

Description: Adding both sides of two orderings. (Contributed by NM, 23-Dec-2007)

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

Proof

Step Hyp Ref Expression
1 ltadd1 ⊢ A ∈ ℝ ∧ C ∈ ℝ ∧ B ∈ ℝ → A < C ↔ A + B < C + B
2 1 3com23 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < C ↔ A + B < C + B
3 2 3expa ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < C ↔ A + B < C + B
4 3 adantrr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → A < C ↔ A + B < C + B
5 leadd2 ⊢ B ∈ ℝ ∧ D ∈ ℝ ∧ C ∈ ℝ → B ≤ D ↔ C + B ≤ C + D
6 5 3com23 ⊢ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → B ≤ D ↔ C + B ≤ C + D
7 6 3expb ⊢ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → B ≤ D ↔ C + B ≤ C + D
8 7 adantll ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → B ≤ D ↔ C + B ≤ C + D
9 4 8 anbi12d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → A < C ∧ B ≤ D ↔ A + B < C + B ∧ C + B ≤ C + D
10 readdcl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B ∈ ℝ
11 10 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → A + B ∈ ℝ
12 readdcl ⊢ C ∈ ℝ ∧ B ∈ ℝ → C + B ∈ ℝ
13 12 ancoms ⊢ B ∈ ℝ ∧ C ∈ ℝ → C + B ∈ ℝ
14 13 ad2ant2lr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → C + B ∈ ℝ
15 readdcl ⊢ C ∈ ℝ ∧ D ∈ ℝ → C + D ∈ ℝ
16 15 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → C + D ∈ ℝ
17 ltletr ⊢ A + B ∈ ℝ ∧ C + B ∈ ℝ ∧ C + D ∈ ℝ → A + B < C + B ∧ C + B ≤ C + D → A + B < C + D
18 11 14 16 17 syl3anc ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → A + B < C + B ∧ C + B ≤ C + D → A + B < C + D
19 9 18 sylbid ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → A < C ∧ B ≤ D → A + B < C + D