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

Metamath Proof Explorer

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