Metamath Proof Explorer

Theorem lt2halves

Description: A sum is less than the whole if each term is less than half. (Contributed by NM, 13-Dec-2006)

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

Proof

Step Hyp Ref Expression
1 3simpa 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A e. RR /\ B e. RR ) )
2 rehalfcl 
 |-  ( C e. RR -> ( C / 2 ) e. RR )
3 2 2 jca 
 |-  ( C e. RR -> ( ( C / 2 ) e. RR /\ ( C / 2 ) e. RR ) )
4 3 3ad2ant3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( C / 2 ) e. RR /\ ( C / 2 ) e. RR ) )
5 lt2add 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( ( C / 2 ) e. RR /\ ( C / 2 ) e. RR ) ) -> ( ( A < ( C / 2 ) /\ B < ( C / 2 ) ) -> ( A + B ) < ( ( C / 2 ) + ( C / 2 ) ) ) )
6 1 4 5 syl2anc 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < ( C / 2 ) /\ B < ( C / 2 ) ) -> ( A + B ) < ( ( C / 2 ) + ( C / 2 ) ) ) )
7 recn 
 |-  ( C e. RR -> C e. CC )
8 2halves 
 |-  ( C e. CC -> ( ( C / 2 ) + ( C / 2 ) ) = C )
9 7 8 syl 
 |-  ( C e. RR -> ( ( C / 2 ) + ( C / 2 ) ) = C )
10 9 breq2d 
 |-  ( C e. RR -> ( ( A + B ) < ( ( C / 2 ) + ( C / 2 ) ) <-> ( A + B ) < C ) )
11 10 3ad2ant3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A + B ) < ( ( C / 2 ) + ( C / 2 ) ) <-> ( A + B ) < C ) )
12 6 11 sylibd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < ( C / 2 ) /\ B < ( C / 2 ) ) -> ( A + B ) < C ) )