Metamath Proof Explorer

Theorem 2leaddle2

Description: If two real numbers are less than a third real number, the sum of the real numbers is less than twice the third real number. (Contributed by Alexander van der Vekens, 21-May-2018)

Ref Expression
Assertion 2leaddle2 
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < C /\ B < C ) -> ( A + B ) < ( 2 x. C ) ) )

Proof

Step Hyp Ref Expression
1 readdcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
2 1 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A + B ) e. RR )
3 readdcl 
 |-  ( ( C e. RR /\ C e. RR ) -> ( C + C ) e. RR )
4 3 anidms 
 |-  ( C e. RR -> ( C + C ) e. RR )
5 4 3ad2ant3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C + C ) e. RR )
6 2re 
 |-  2 e. RR
7 remulcl 
 |-  ( ( 2 e. RR /\ C e. RR ) -> ( 2 x. C ) e. RR )
8 6 7 mpan 
 |-  ( C e. RR -> ( 2 x. C ) e. RR )
9 8 3ad2ant3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( 2 x. C ) e. RR )
10 2 5 9 3jca 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A + B ) e. RR /\ ( C + C ) e. RR /\ ( 2 x. C ) e. RR ) )
11 10 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A < C /\ B < C ) ) -> ( ( A + B ) e. RR /\ ( C + C ) e. RR /\ ( 2 x. C ) e. RR ) )
12 id 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A e. RR /\ B e. RR ) )
13 12 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A e. RR /\ B e. RR ) )
14 id 
 |-  ( C e. RR -> C e. RR )
15 14 14 jca 
 |-  ( C e. RR -> ( C e. RR /\ C e. RR ) )
16 15 3ad2ant3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C e. RR /\ C e. RR ) )
17 13 16 jca 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ C e. RR ) ) )
18 17 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A < C /\ B < C ) ) -> ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ C e. RR ) ) )
19 simpr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A < C /\ B < C ) ) -> ( A < C /\ B < C ) )
20 lt2add 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ C e. RR ) ) -> ( ( A < C /\ B < C ) -> ( A + B ) < ( C + C ) ) )
21 18 19 20 sylc 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A < C /\ B < C ) ) -> ( A + B ) < ( C + C ) )
22 recn 
 |-  ( C e. RR -> C e. CC )
23 22 2timesd 
 |-  ( C e. RR -> ( 2 x. C ) = ( C + C ) )
24 8 leidd 
 |-  ( C e. RR -> ( 2 x. C ) <_ ( 2 x. C ) )
25 23 24 eqbrtrrd 
 |-  ( C e. RR -> ( C + C ) <_ ( 2 x. C ) )
26 25 3ad2ant3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C + C ) <_ ( 2 x. C ) )
27 26 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A < C /\ B < C ) ) -> ( C + C ) <_ ( 2 x. C ) )
28 21 27 jca 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A < C /\ B < C ) ) -> ( ( A + B ) < ( C + C ) /\ ( C + C ) <_ ( 2 x. C ) ) )
29 ltletr 
 |-  ( ( ( A + B ) e. RR /\ ( C + C ) e. RR /\ ( 2 x. C ) e. RR ) -> ( ( ( A + B ) < ( C + C ) /\ ( C + C ) <_ ( 2 x. C ) ) -> ( A + B ) < ( 2 x. C ) ) )
30 11 28 29 sylc 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A < C /\ B < C ) ) -> ( A + B ) < ( 2 x. C ) )
31 30 ex 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < C /\ B < C ) -> ( A + B ) < ( 2 x. C ) ) )