This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xle2addd

Description: Adding both side of two inequalities. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses xle2addd.1 ⊢ φ → A ∈ ℝ *
xle2addd.2 ⊢ φ → B ∈ ℝ *
xle2addd.3 ⊢ φ → C ∈ ℝ *
xle2addd.4 ⊢ φ → D ∈ ℝ *
xle2addd.5 ⊢ φ → A ≤ C
xrle2addd.6 ⊢ φ → B ≤ D
Assertion xle2addd ⊢ φ → A + 𝑒 B ≤ C + 𝑒 D

Proof

Step Hyp Ref Expression
1 xle2addd.1 ⊢ φ → A ∈ ℝ *
2 xle2addd.2 ⊢ φ → B ∈ ℝ *
3 xle2addd.3 ⊢ φ → C ∈ ℝ *
4 xle2addd.4 ⊢ φ → D ∈ ℝ *
5 xle2addd.5 ⊢ φ → A ≤ C
6 xrle2addd.6 ⊢ φ → B ≤ D
7 1 2 xaddcld ⊢ φ → A + 𝑒 B ∈ ℝ *
8 1 4 xaddcld ⊢ φ → A + 𝑒 D ∈ ℝ *
9 3 4 xaddcld ⊢ φ → C + 𝑒 D ∈ ℝ *
10 2 4 1 6 xleadd2d ⊢ φ → A + 𝑒 B ≤ A + 𝑒 D
11 1 3 4 5 xleadd1d ⊢ φ → A + 𝑒 D ≤ C + 𝑒 D
12 7 8 9 10 11 xrletrd ⊢ φ → A + 𝑒 B ≤ C + 𝑒 D