Step |
Hyp |
Ref |
Expression |
1 |
|
abscld.1 |
|- ( ph -> A e. CC ) |
2 |
|
abssubd.2 |
|- ( ph -> B e. CC ) |
3 |
|
abs3difd.3 |
|- ( ph -> C e. CC ) |
4 |
|
abs3lemd.4 |
|- ( ph -> D e. RR ) |
5 |
|
abs3lemd.5 |
|- ( ph -> ( abs ` ( A - C ) ) < ( D / 2 ) ) |
6 |
|
abs3lemd.6 |
|- ( ph -> ( abs ` ( C - B ) ) < ( D / 2 ) ) |
7 |
|
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 ) ) |
8 |
1 2 3 4 7
|
syl22anc |
|- ( ph -> ( ( ( abs ` ( A - C ) ) < ( D / 2 ) /\ ( abs ` ( C - B ) ) < ( D / 2 ) ) -> ( abs ` ( A - B ) ) < D ) ) |
9 |
5 6 8
|
mp2and |
|- ( ph -> ( abs ` ( A - B ) ) < D ) |