Metamath Proof Explorer

Theorem abs3lemi

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

Ref Expression
Hypotheses absvalsqi.1 
|- A e. CC
abssub.2 
|- B e. CC
abs3dif.3 
|- C e. CC
abs3lem.4 
|- D e. RR
Assertion abs3lemi 
|- ( ( ( abs ` ( A - C ) ) < ( D / 2 ) /\ ( abs ` ( C - B ) ) < ( D / 2 ) ) -> ( abs ` ( A - B ) ) < D )

Proof

Step Hyp Ref Expression
1 absvalsqi.1 
 |-  A e. CC
2 abssub.2 
 |-  B e. CC
3 abs3dif.3 
 |-  C e. CC
4 abs3lem.4 
 |-  D e. RR
5 1 2 3 abs3difi 
 |-  ( abs ` ( A - B ) ) <_ ( ( abs ` ( A - C ) ) + ( abs ` ( C - B ) ) )
6 1 3 subcli 
 |-  ( A - C ) e. CC
7 6 abscli 
 |-  ( abs ` ( A - C ) ) e. RR
8 3 2 subcli 
 |-  ( C - B ) e. CC
9 8 abscli 
 |-  ( abs ` ( C - B ) ) e. RR
10 4 rehalfcli 
 |-  ( D / 2 ) e. RR
11 7 9 10 10 lt2addi 
 |-  ( ( ( abs ` ( A - C ) ) < ( D / 2 ) /\ ( abs ` ( C - B ) ) < ( D / 2 ) ) -> ( ( abs ` ( A - C ) ) + ( abs ` ( C - B ) ) ) < ( ( D / 2 ) + ( D / 2 ) ) )
12 1 2 subcli 
 |-  ( A - B ) e. CC
13 12 abscli 
 |-  ( abs ` ( A - B ) ) e. RR
14 7 9 readdcli 
 |-  ( ( abs ` ( A - C ) ) + ( abs ` ( C - B ) ) ) e. RR
15 10 10 readdcli 
 |-  ( ( D / 2 ) + ( D / 2 ) ) e. RR
16 13 14 15 lelttri 
 |-  ( ( ( abs ` ( A - B ) ) <_ ( ( abs ` ( A - C ) ) + ( abs ` ( C - B ) ) ) /\ ( ( abs ` ( A - C ) ) + ( abs ` ( C - B ) ) ) < ( ( D / 2 ) + ( D / 2 ) ) ) -> ( abs ` ( A - B ) ) < ( ( D / 2 ) + ( D / 2 ) ) )
17 5 11 16 sylancr 
 |-  ( ( ( abs ` ( A - C ) ) < ( D / 2 ) /\ ( abs ` ( C - B ) ) < ( D / 2 ) ) -> ( abs ` ( A - B ) ) < ( ( D / 2 ) + ( D / 2 ) ) )
18 10 recni 
 |-  ( D / 2 ) e. CC
19 18 2timesi 
 |-  ( 2 x. ( D / 2 ) ) = ( ( D / 2 ) + ( D / 2 ) )
20 4 recni 
 |-  D e. CC
21 2cn 
 |-  2 e. CC
22 2ne0 
 |-  2 =/= 0
23 20 21 22 divcan2i 
 |-  ( 2 x. ( D / 2 ) ) = D
24 19 23 eqtr3i 
 |-  ( ( D / 2 ) + ( D / 2 ) ) = D
25 17 24 breqtrdi 
 |-  ( ( ( abs ` ( A - C ) ) < ( D / 2 ) /\ ( abs ` ( C - B ) ) < ( D / 2 ) ) -> ( abs ` ( A - B ) ) < D )