Theorem xle2addd

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

	Ref	Expression
Hypotheses	xle2addd.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
	xle2addd.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
	xle2addd.3	⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
	xle2addd.4	⊢ ( 𝜑 → 𝐷 ∈ ℝ* )
	xle2addd.5	⊢ ( 𝜑 → 𝐴 ≤ 𝐶 )
	xrle2addd.6	⊢ ( 𝜑 → 𝐵 ≤ 𝐷 )
Assertion	xle2addd	⊢ ( 𝜑 → ( 𝐴 +𝑒 𝐵 ) ≤ ( 𝐶 +𝑒 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		xle2addd.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
2		xle2addd.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
3		xle2addd.3	⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
4		xle2addd.4	⊢ ( 𝜑 → 𝐷 ∈ ℝ* )
5		xle2addd.5	⊢ ( 𝜑 → 𝐴 ≤ 𝐶 )
6		xrle2addd.6	⊢ ( 𝜑 → 𝐵 ≤ 𝐷 )
7	1 2	xaddcld	⊢ ( 𝜑 → ( 𝐴 +𝑒 𝐵 ) ∈ ℝ* )
8	1 4	xaddcld	⊢ ( 𝜑 → ( 𝐴 +𝑒 𝐷 ) ∈ ℝ* )
9	3 4	xaddcld	⊢ ( 𝜑 → ( 𝐶 +𝑒 𝐷 ) ∈ ℝ* )
10	2 4 1 6	xleadd2d	⊢ ( 𝜑 → ( 𝐴 +𝑒 𝐵 ) ≤ ( 𝐴 +𝑒 𝐷 ) )
11	1 3 4 5	xleadd1d	⊢ ( 𝜑 → ( 𝐴 +𝑒 𝐷 ) ≤ ( 𝐶 +𝑒 𝐷 ) )
12	7 8 9 10 11	xrletrd	⊢ ( 𝜑 → ( 𝐴 +𝑒 𝐵 ) ≤ ( 𝐶 +𝑒 𝐷 ) )