Metamath Proof Explorer

Theorem xle2add

Description: Extended real version of le2add . (Contributed by Mario Carneiro, 23-Aug-2015)

Ref Expression
Assertion xle2add ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧D∈ℝ*→A≤C∧B≤D→A+𝑒B≤C+𝑒D

Proof

Step Hyp Ref Expression
1 simpll ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧D∈ℝ*→A∈ℝ*
2 simprl ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧D∈ℝ*→C∈ℝ*
3 simplr ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧D∈ℝ*→B∈ℝ*
4 xleadd1a ⊢A∈ℝ*∧C∈ℝ*∧B∈ℝ*∧A≤C→A+𝑒B≤C+𝑒B
5 4 ex ⊢A∈ℝ*∧C∈ℝ*∧B∈ℝ*→A≤C→A+𝑒B≤C+𝑒B
6 1 2 3 5 syl3anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧D∈ℝ*→A≤C→A+𝑒B≤C+𝑒B
7 simprr ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧D∈ℝ*→D∈ℝ*
8 xleadd2a ⊢B∈ℝ*∧D∈ℝ*∧C∈ℝ*∧B≤D→C+𝑒B≤C+𝑒D
9 8 ex ⊢B∈ℝ*∧D∈ℝ*∧C∈ℝ*→B≤D→C+𝑒B≤C+𝑒D
10 3 7 2 9 syl3anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧D∈ℝ*→B≤D→C+𝑒B≤C+𝑒D
11 xaddcl ⊢A∈ℝ*∧B∈ℝ*→A+𝑒B∈ℝ*
12 11 adantr ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧D∈ℝ*→A+𝑒B∈ℝ*
13 xaddcl ⊢C∈ℝ*∧B∈ℝ*→C+𝑒B∈ℝ*
14 2 3 13 syl2anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧D∈ℝ*→C+𝑒B∈ℝ*
15 xaddcl ⊢C∈ℝ*∧D∈ℝ*→C+𝑒D∈ℝ*
16 15 adantl ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧D∈ℝ*→C+𝑒D∈ℝ*
17 xrletr ⊢A+𝑒B∈ℝ*∧C+𝑒B∈ℝ*∧C+𝑒D∈ℝ*→A+𝑒B≤C+𝑒B∧C+𝑒B≤C+𝑒D→A+𝑒B≤C+𝑒D
18 12 14 16 17 syl3anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧D∈ℝ*→A+𝑒B≤C+𝑒B∧C+𝑒B≤C+𝑒D→A+𝑒B≤C+𝑒D
19 6 10 18 syl2and ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧D∈ℝ*→A≤C∧B≤D→A+𝑒B≤C+𝑒D