Theorem lt3addmuld

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

	Ref	Expression
Hypotheses	lt3addmuld.a	$$⊢\phi \to A\in ℝ$$
	lt3addmuld.b	$$⊢\phi \to B\in ℝ$$
	lt3addmuld.c	$$⊢\phi \to C\in ℝ$$
	lt3addmuld.d	$$⊢\phi \to D\in ℝ$$
	lt3addmuld.altd	$$⊢\phi \to A<D$$
	lt3addmuld.bltd	$$⊢\phi \to B<D$$
	lt3addmuld.cltd	$$⊢\phi \to C<D$$
Assertion	lt3addmuld	$$⊢\phi \to A+B+C<3D$$

Proof

Step	Hyp	Ref	Expression
1		lt3addmuld.a	$$⊢\phi \to A\in ℝ$$
2		lt3addmuld.b	$$⊢\phi \to B\in ℝ$$
3		lt3addmuld.c	$$⊢\phi \to C\in ℝ$$
4		lt3addmuld.d	$$⊢\phi \to D\in ℝ$$
5		lt3addmuld.altd	$$⊢\phi \to A<D$$
6		lt3addmuld.bltd	$$⊢\phi \to B<D$$
7		lt3addmuld.cltd	$$⊢\phi \to C<D$$
8	1 2	readdcld	$$⊢\phi \to A+B\in ℝ$$
9		2re	$$⊢2\in ℝ$$
10	9	a1i	$$⊢\phi \to 2\in ℝ$$
11	10 4	remulcld	$$⊢\phi \to 2D\in ℝ$$
12	1 2 4 5 6	lt2addmuld	$$⊢\phi \to A+B<2D$$
13	8 3 11 4 12 7	lt2addd	$$⊢\phi \to A+B+C<2D+D$$
14	10	recnd	$$⊢\phi \to 2\in ℂ$$
15	4	recnd	$$⊢\phi \to D\in ℂ$$
16	14 15	adddirp1d	$$⊢\phi \to \left(2+1\right)D=2D+D$$
17		2p1e3	$$⊢2+1=3$$
18	17	a1i	$$⊢\phi \to 2+1=3$$
19	18	oveq1d	$$⊢\phi \to \left(2+1\right)D=3D$$
20	16 19	eqtr3d	$$⊢\phi \to 2D+D=3D$$
21	13 20	breqtrd	$$⊢\phi \to A+B+C<3D$$