This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )