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