Metamath Proof Explorer

Theorem abs3lem

Description: Lemma involving absolute value of differences. (Contributed by NM, 2-Oct-1999)

Ref Expression
Assertion abs3lem 
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. RR ) ) -> ( ( ( abs ` ( A - C ) ) < ( D / 2 ) /\ ( abs ` ( C - B ) ) < ( D / 2 ) ) -> ( abs ` ( A - B ) ) < D ) )

Proof

Step Hyp Ref Expression
1 simplll 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. RR ) ) /\ ( ( abs ` ( A - C ) ) < ( D / 2 ) /\ ( abs ` ( C - B ) ) < ( D / 2 ) ) ) -> A e. CC )
2 simpllr 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. RR ) ) /\ ( ( abs ` ( A - C ) ) < ( D / 2 ) /\ ( abs ` ( C - B ) ) < ( D / 2 ) ) ) -> B e. CC )
3 1 2 subcld 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. RR ) ) /\ ( ( abs ` ( A - C ) ) < ( D / 2 ) /\ ( abs ` ( C - B ) ) < ( D / 2 ) ) ) -> ( A - B ) e. CC )
4 abscl 
 |-  ( ( A - B ) e. CC -> ( abs ` ( A - B ) ) e. RR )
5 3 4 syl 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. RR ) ) /\ ( ( abs ` ( A - C ) ) < ( D / 2 ) /\ ( abs ` ( C - B ) ) < ( D / 2 ) ) ) -> ( abs ` ( A - B ) ) e. RR )
6 simplrl 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. RR ) ) /\ ( ( abs ` ( A - C ) ) < ( D / 2 ) /\ ( abs ` ( C - B ) ) < ( D / 2 ) ) ) -> C e. CC )
7 1 6 subcld 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. RR ) ) /\ ( ( abs ` ( A - C ) ) < ( D / 2 ) /\ ( abs ` ( C - B ) ) < ( D / 2 ) ) ) -> ( A - C ) e. CC )
8 abscl 
 |-  ( ( A - C ) e. CC -> ( abs ` ( A - C ) ) e. RR )
9 7 8 syl 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. RR ) ) /\ ( ( abs ` ( A - C ) ) < ( D / 2 ) /\ ( abs ` ( C - B ) ) < ( D / 2 ) ) ) -> ( abs ` ( A - C ) ) e. RR )
10 6 2 subcld 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. RR ) ) /\ ( ( abs ` ( A - C ) ) < ( D / 2 ) /\ ( abs ` ( C - B ) ) < ( D / 2 ) ) ) -> ( C - B ) e. CC )
11 abscl 
 |-  ( ( C - B ) e. CC -> ( abs ` ( C - B ) ) e. RR )
12 10 11 syl 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. RR ) ) /\ ( ( abs ` ( A - C ) ) < ( D / 2 ) /\ ( abs ` ( C - B ) ) < ( D / 2 ) ) ) -> ( abs ` ( C - B ) ) e. RR )
13 9 12 readdcld 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. RR ) ) /\ ( ( abs ` ( A - C ) ) < ( D / 2 ) /\ ( abs ` ( C - B ) ) < ( D / 2 ) ) ) -> ( ( abs ` ( A - C ) ) + ( abs ` ( C - B ) ) ) e. RR )
14 simplrr 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. RR ) ) /\ ( ( abs ` ( A - C ) ) < ( D / 2 ) /\ ( abs ` ( C - B ) ) < ( D / 2 ) ) ) -> D e. RR )
15 abs3dif 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( abs ` ( A - B ) ) <_ ( ( abs ` ( A - C ) ) + ( abs ` ( C - B ) ) ) )
16 1 2 6 15 syl3anc 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. RR ) ) /\ ( ( abs ` ( A - C ) ) < ( D / 2 ) /\ ( abs ` ( C - B ) ) < ( D / 2 ) ) ) -> ( abs ` ( A - B ) ) <_ ( ( abs ` ( A - C ) ) + ( abs ` ( C - B ) ) ) )
17 simprl 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. RR ) ) /\ ( ( abs ` ( A - C ) ) < ( D / 2 ) /\ ( abs ` ( C - B ) ) < ( D / 2 ) ) ) -> ( abs ` ( A - C ) ) < ( D / 2 ) )
18 simprr 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. RR ) ) /\ ( ( abs ` ( A - C ) ) < ( D / 2 ) /\ ( abs ` ( C - B ) ) < ( D / 2 ) ) ) -> ( abs ` ( C - B ) ) < ( D / 2 ) )
19 9 12 14 17 18 lt2halvesd 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. RR ) ) /\ ( ( abs ` ( A - C ) ) < ( D / 2 ) /\ ( abs ` ( C - B ) ) < ( D / 2 ) ) ) -> ( ( abs ` ( A - C ) ) + ( abs ` ( C - B ) ) ) < D )
20 5 13 14 16 19 lelttrd 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. RR ) ) /\ ( ( abs ` ( A - C ) ) < ( D / 2 ) /\ ( abs ` ( C - B ) ) < ( D / 2 ) ) ) -> ( abs ` ( A - B ) ) < D )
21 20 ex 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. RR ) ) -> ( ( ( abs ` ( A - C ) ) < ( D / 2 ) /\ ( abs ` ( C - B ) ) < ( D / 2 ) ) -> ( abs ` ( A - B ) ) < D ) )