Theorem lt4addmuld

Description: If four real numbers are less than a fifth real number, the sum of the four real numbers is less than four times the fifth real number. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	lt4addmuld.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	lt4addmuld.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	lt4addmuld.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	lt4addmuld.d	⊢ ( 𝜑 → 𝐷 ∈ ℝ )
	lt4addmuld.e	⊢ ( 𝜑 → 𝐸 ∈ ℝ )
	lt4addmuld.alte	⊢ ( 𝜑 → 𝐴 < 𝐸 )
	lt4addmuld.blte	⊢ ( 𝜑 → 𝐵 < 𝐸 )
	lt4addmuld.clte	⊢ ( 𝜑 → 𝐶 < 𝐸 )
	lt4addmuld.dlte	⊢ ( 𝜑 → 𝐷 < 𝐸 )
Assertion	lt4addmuld	⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) + 𝐶 ) + 𝐷 ) < ( 4 · 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		lt4addmuld.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		lt4addmuld.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		lt4addmuld.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4		lt4addmuld.d	⊢ ( 𝜑 → 𝐷 ∈ ℝ )
5		lt4addmuld.e	⊢ ( 𝜑 → 𝐸 ∈ ℝ )
6		lt4addmuld.alte	⊢ ( 𝜑 → 𝐴 < 𝐸 )
7		lt4addmuld.blte	⊢ ( 𝜑 → 𝐵 < 𝐸 )
8		lt4addmuld.clte	⊢ ( 𝜑 → 𝐶 < 𝐸 )
9		lt4addmuld.dlte	⊢ ( 𝜑 → 𝐷 < 𝐸 )
10	1 2	readdcld	⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ ℝ )
11	10 3	readdcld	⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) + 𝐶 ) ∈ ℝ )
12		3re	⊢ 3 ∈ ℝ
13	12	a1i	⊢ ( 𝜑 → 3 ∈ ℝ )
14	13 5	remulcld	⊢ ( 𝜑 → ( 3 · 𝐸 ) ∈ ℝ )
15	1 2 3 5 6 7 8	lt3addmuld	⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) + 𝐶 ) < ( 3 · 𝐸 ) )
16	11 4 14 5 15 9	lt2addd	⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) + 𝐶 ) + 𝐷 ) < ( ( 3 · 𝐸 ) + 𝐸 ) )
17		df-4	⊢ 4 = ( 3 + 1 )
18	17	a1i	⊢ ( 𝜑 → 4 = ( 3 + 1 ) )
19	18	oveq1d	⊢ ( 𝜑 → ( 4 · 𝐸 ) = ( ( 3 + 1 ) · 𝐸 ) )
20	13	recnd	⊢ ( 𝜑 → 3 ∈ ℂ )
21	5	recnd	⊢ ( 𝜑 → 𝐸 ∈ ℂ )
22	20 21	adddirp1d	⊢ ( 𝜑 → ( ( 3 + 1 ) · 𝐸 ) = ( ( 3 · 𝐸 ) + 𝐸 ) )
23	19 22	eqtr2d	⊢ ( 𝜑 → ( ( 3 · 𝐸 ) + 𝐸 ) = ( 4 · 𝐸 ) )
24	16 23	breqtrd	⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) + 𝐶 ) + 𝐷 ) < ( 4 · 𝐸 ) )