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	|- ( ph -> A e. RR )
	lt4addmuld.b	|- ( ph -> B e. RR )
	lt4addmuld.c	|- ( ph -> C e. RR )
	lt4addmuld.d	|- ( ph -> D e. RR )
	lt4addmuld.e	|- ( ph -> E e. RR )
	lt4addmuld.alte	|- ( ph -> A < E )
	lt4addmuld.blte	|- ( ph -> B < E )
	lt4addmuld.clte	|- ( ph -> C < E )
	lt4addmuld.dlte	|- ( ph -> D < E )
Assertion	lt4addmuld	|- ( ph -> ( ( ( A + B ) + C ) + D ) < ( 4 x. E ) )

Proof

Step	Hyp	Ref	Expression
1		lt4addmuld.a	|- ( ph -> A e. RR )
2		lt4addmuld.b	|- ( ph -> B e. RR )
3		lt4addmuld.c	|- ( ph -> C e. RR )
4		lt4addmuld.d	|- ( ph -> D e. RR )
5		lt4addmuld.e	|- ( ph -> E e. RR )
6		lt4addmuld.alte	|- ( ph -> A < E )
7		lt4addmuld.blte	|- ( ph -> B < E )
8		lt4addmuld.clte	|- ( ph -> C < E )
9		lt4addmuld.dlte	|- ( ph -> D < E )
10	1 2	readdcld	|- ( ph -> ( A + B ) e. RR )
11	10 3	readdcld	|- ( ph -> ( ( A + B ) + C ) e. RR )
12		3re	|- 3 e. RR
13	12	a1i	|- ( ph -> 3 e. RR )
14	13 5	remulcld	|- ( ph -> ( 3 x. E ) e. RR )
15	1 2 3 5 6 7 8	lt3addmuld	|- ( ph -> ( ( A + B ) + C ) < ( 3 x. E ) )
16	11 4 14 5 15 9	lt2addd	|- ( ph -> ( ( ( A + B ) + C ) + D ) < ( ( 3 x. E ) + E ) )
17		df-4	|- 4 = ( 3 + 1 )
18	17	a1i	|- ( ph -> 4 = ( 3 + 1 ) )
19	18	oveq1d	|- ( ph -> ( 4 x. E ) = ( ( 3 + 1 ) x. E ) )
20	13	recnd	|- ( ph -> 3 e. CC )
21	5	recnd	|- ( ph -> E e. CC )
22	20 21	adddirp1d	|- ( ph -> ( ( 3 + 1 ) x. E ) = ( ( 3 x. E ) + E ) )
23	19 22	eqtr2d	|- ( ph -> ( ( 3 x. E ) + E ) = ( 4 x. E ) )
24	16 23	breqtrd	|- ( ph -> ( ( ( A + B ) + C ) + D ) < ( 4 x. E ) )