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