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	|- ( ph -> A e. RR )
	lt3addmuld.b	|- ( ph -> B e. RR )
	lt3addmuld.c	|- ( ph -> C e. RR )
	lt3addmuld.d	|- ( ph -> D e. RR )
	lt3addmuld.altd	|- ( ph -> A < D )
	lt3addmuld.bltd	|- ( ph -> B < D )
	lt3addmuld.cltd	|- ( ph -> C < D )
Assertion	lt3addmuld	|- ( ph -> ( ( A + B ) + C ) < ( 3 x. D ) )

Proof

Step	Hyp	Ref	Expression
1		lt3addmuld.a	|- ( ph -> A e. RR )
2		lt3addmuld.b	|- ( ph -> B e. RR )
3		lt3addmuld.c	|- ( ph -> C e. RR )
4		lt3addmuld.d	|- ( ph -> D e. RR )
5		lt3addmuld.altd	|- ( ph -> A < D )
6		lt3addmuld.bltd	|- ( ph -> B < D )
7		lt3addmuld.cltd	|- ( ph -> C < D )
8	1 2	readdcld	|- ( ph -> ( A + B ) e. RR )
9		2re	|- 2 e. RR
10	9	a1i	|- ( ph -> 2 e. RR )
11	10 4	remulcld	|- ( ph -> ( 2 x. D ) e. RR )
12	1 2 4 5 6	lt2addmuld	|- ( ph -> ( A + B ) < ( 2 x. D ) )
13	8 3 11 4 12 7	lt2addd	|- ( ph -> ( ( A + B ) + C ) < ( ( 2 x. D ) + D ) )
14	10	recnd	|- ( ph -> 2 e. CC )
15	4	recnd	|- ( ph -> D e. CC )
16	14 15	adddirp1d	|- ( ph -> ( ( 2 + 1 ) x. D ) = ( ( 2 x. D ) + D ) )
17		2p1e3	|- ( 2 + 1 ) = 3
18	17	a1i	|- ( ph -> ( 2 + 1 ) = 3 )
19	18	oveq1d	|- ( ph -> ( ( 2 + 1 ) x. D ) = ( 3 x. D ) )
20	16 19	eqtr3d	|- ( ph -> ( ( 2 x. D ) + D ) = ( 3 x. D ) )
21	13 20	breqtrd	|- ( ph -> ( ( A + B ) + C ) < ( 3 x. D ) )