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	$$⊢\phi \to A\in ℝ$$
	lt4addmuld.b	$$⊢\phi \to B\in ℝ$$
	lt4addmuld.c	$$⊢\phi \to C\in ℝ$$
	lt4addmuld.d	$$⊢\phi \to D\in ℝ$$
	lt4addmuld.e	$$⊢\phi \to E\in ℝ$$
	lt4addmuld.alte	$$⊢\phi \to A<E$$
	lt4addmuld.blte	$$⊢\phi \to B<E$$
	lt4addmuld.clte	$$⊢\phi \to C<E$$
	lt4addmuld.dlte	$$⊢\phi \to D<E$$
Assertion	lt4addmuld	$$⊢\phi \to \left(A+B\right)+C+D<4E$$

Proof

Step	Hyp	Ref	Expression
1		lt4addmuld.a	$$⊢\phi \to A\in ℝ$$
2		lt4addmuld.b	$$⊢\phi \to B\in ℝ$$
3		lt4addmuld.c	$$⊢\phi \to C\in ℝ$$
4		lt4addmuld.d	$$⊢\phi \to D\in ℝ$$
5		lt4addmuld.e	$$⊢\phi \to E\in ℝ$$
6		lt4addmuld.alte	$$⊢\phi \to A<E$$
7		lt4addmuld.blte	$$⊢\phi \to B<E$$
8		lt4addmuld.clte	$$⊢\phi \to C<E$$
9		lt4addmuld.dlte	$$⊢\phi \to D<E$$
10	1 2	readdcld	$$⊢\phi \to A+B\in ℝ$$
11	10 3	readdcld	$$⊢\phi \to A+B+C\in ℝ$$
12		3re	$$⊢3\in ℝ$$
13	12	a1i	$$⊢\phi \to 3\in ℝ$$
14	13 5	remulcld	$$⊢\phi \to 3E\in ℝ$$
15	1 2 3 5 6 7 8	lt3addmuld	$$⊢\phi \to A+B+C<3E$$
16	11 4 14 5 15 9	lt2addd	$$⊢\phi \to \left(A+B\right)+C+D<3E+E$$
17		df-4	$$⊢4=3+1$$
18	17	a1i	$$⊢\phi \to 4=3+1$$
19	18	oveq1d	$$⊢\phi \to 4E=\left(3+1\right)E$$
20	13	recnd	$$⊢\phi \to 3\in ℂ$$
21	5	recnd	$$⊢\phi \to E\in ℂ$$
22	20 21	adddirp1d	$$⊢\phi \to \left(3+1\right)E=3E+E$$
23	19 22	eqtr2d	$$⊢\phi \to 3E+E=4E$$
24	16 23	breqtrd	$$⊢\phi \to \left(A+B\right)+C+D<4E$$