Metamath Proof Explorer

Theorem blcvx

Description: An open ball in the complex numbers is a convex set. (Contributed by Mario Carneiro, 12-Feb-2015) (Revised by Mario Carneiro, 8-Sep-2015)

Ref Expression
Hypothesis blcvx.s 
|- S = ( P ( ball ` ( abs o. - ) ) R )
Assertion blcvx 
|- ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( ( T x. A ) + ( ( 1 - T ) x. B ) ) e. S )

Proof

Step Hyp Ref Expression
1 blcvx.s 
 |-  S = ( P ( ball ` ( abs o. - ) ) R )
2 simpr3 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> T e. ( 0 [,] 1 ) )
3 elicc01 
 |-  ( T e. ( 0 [,] 1 ) <-> ( T e. RR /\ 0 <_ T /\ T <_ 1 ) )
4 2 3 sylib 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( T e. RR /\ 0 <_ T /\ T <_ 1 ) )
5 4 simp1d 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> T e. RR )
6 5 recnd 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> T e. CC )
7 simpr1 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> A e. S )
8 7 1 eleqtrdi 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> A e. ( P ( ball ` ( abs o. - ) ) R ) )
9 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
10 simpll 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> P e. CC )
11 simplr 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> R e. RR* )
12 elbl 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ P e. CC /\ R e. RR* ) -> ( A e. ( P ( ball ` ( abs o. - ) ) R ) <-> ( A e. CC /\ ( P ( abs o. - ) A ) < R ) ) )
13 9 10 11 12 mp3an2i 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( A e. ( P ( ball ` ( abs o. - ) ) R ) <-> ( A e. CC /\ ( P ( abs o. - ) A ) < R ) ) )
14 8 13 mpbid 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( A e. CC /\ ( P ( abs o. - ) A ) < R ) )
15 14 simpld 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> A e. CC )
16 6 15 mulcld 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( T x. A ) e. CC )
17 1re 
 |-  1 e. RR
18 resubcl 
 |-  ( ( 1 e. RR /\ T e. RR ) -> ( 1 - T ) e. RR )
19 17 5 18 sylancr 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( 1 - T ) e. RR )
20 19 recnd 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( 1 - T ) e. CC )
21 simpr2 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> B e. S )
22 21 1 eleqtrdi 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> B e. ( P ( ball ` ( abs o. - ) ) R ) )
23 elbl 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ P e. CC /\ R e. RR* ) -> ( B e. ( P ( ball ` ( abs o. - ) ) R ) <-> ( B e. CC /\ ( P ( abs o. - ) B ) < R ) ) )
24 9 10 11 23 mp3an2i 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( B e. ( P ( ball ` ( abs o. - ) ) R ) <-> ( B e. CC /\ ( P ( abs o. - ) B ) < R ) ) )
25 22 24 mpbid 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( B e. CC /\ ( P ( abs o. - ) B ) < R ) )
26 25 simpld 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> B e. CC )
27 20 26 mulcld 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( ( 1 - T ) x. B ) e. CC )
28 16 27 addcld 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( ( T x. A ) + ( ( 1 - T ) x. B ) ) e. CC )
29 eqid 
 |-  ( abs o. - ) = ( abs o. - )
30 29 cnmetdval 
 |-  ( ( P e. CC /\ ( ( T x. A ) + ( ( 1 - T ) x. B ) ) e. CC ) -> ( P ( abs o. - ) ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) = ( abs ` ( P - ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) ) )
31 10 28 30 syl2anc 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( P ( abs o. - ) ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) = ( abs ` ( P - ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) ) )
32 6 10 15 subdid 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( T x. ( P - A ) ) = ( ( T x. P ) - ( T x. A ) ) )
33 20 10 26 subdid 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( ( 1 - T ) x. ( P - B ) ) = ( ( ( 1 - T ) x. P ) - ( ( 1 - T ) x. B ) ) )
34 32 33 oveq12d 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( ( T x. ( P - A ) ) + ( ( 1 - T ) x. ( P - B ) ) ) = ( ( ( T x. P ) - ( T x. A ) ) + ( ( ( 1 - T ) x. P ) - ( ( 1 - T ) x. B ) ) ) )
35 6 10 mulcld 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( T x. P ) e. CC )
36 20 10 mulcld 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( ( 1 - T ) x. P ) e. CC )
37 35 36 16 27 addsub4d 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( ( ( T x. P ) + ( ( 1 - T ) x. P ) ) - ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) = ( ( ( T x. P ) - ( T x. A ) ) + ( ( ( 1 - T ) x. P ) - ( ( 1 - T ) x. B ) ) ) )
38 ax-1cn 
 |-  1 e. CC
39 pncan3 
 |-  ( ( T e. CC /\ 1 e. CC ) -> ( T + ( 1 - T ) ) = 1 )
40 6 38 39 sylancl 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( T + ( 1 - T ) ) = 1 )
41 40 oveq1d 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( ( T + ( 1 - T ) ) x. P ) = ( 1 x. P ) )
42 6 20 10 adddird 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( ( T + ( 1 - T ) ) x. P ) = ( ( T x. P ) + ( ( 1 - T ) x. P ) ) )
43 mullid 
 |-  ( P e. CC -> ( 1 x. P ) = P )
44 43 ad2antrr 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( 1 x. P ) = P )
45 41 42 44 3eqtr3d 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( ( T x. P ) + ( ( 1 - T ) x. P ) ) = P )
46 45 oveq1d 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( ( ( T x. P ) + ( ( 1 - T ) x. P ) ) - ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) = ( P - ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) )
47 34 37 46 3eqtr2d 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( ( T x. ( P - A ) ) + ( ( 1 - T ) x. ( P - B ) ) ) = ( P - ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) )
48 47 fveq2d 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( abs ` ( ( T x. ( P - A ) ) + ( ( 1 - T ) x. ( P - B ) ) ) ) = ( abs ` ( P - ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) ) )
49 31 48 eqtr4d 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( P ( abs o. - ) ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) = ( abs ` ( ( T x. ( P - A ) ) + ( ( 1 - T ) x. ( P - B ) ) ) ) )
50 10 15 subcld 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( P - A ) e. CC )
51 6 50 mulcld 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( T x. ( P - A ) ) e. CC )
52 10 26 subcld 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( P - B ) e. CC )
53 20 52 mulcld 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( ( 1 - T ) x. ( P - B ) ) e. CC )
54 51 53 addcld 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( ( T x. ( P - A ) ) + ( ( 1 - T ) x. ( P - B ) ) ) e. CC )
55 54 abscld 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( abs ` ( ( T x. ( P - A ) ) + ( ( 1 - T ) x. ( P - B ) ) ) ) e. RR )
56 55 adantr 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) -> ( abs ` ( ( T x. ( P - A ) ) + ( ( 1 - T ) x. ( P - B ) ) ) ) e. RR )
57 51 abscld 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( abs ` ( T x. ( P - A ) ) ) e. RR )
58 53 abscld 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( abs ` ( ( 1 - T ) x. ( P - B ) ) ) e. RR )
59 57 58 readdcld 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( ( abs ` ( T x. ( P - A ) ) ) + ( abs ` ( ( 1 - T ) x. ( P - B ) ) ) ) e. RR )
60 59 adantr 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) -> ( ( abs ` ( T x. ( P - A ) ) ) + ( abs ` ( ( 1 - T ) x. ( P - B ) ) ) ) e. RR )
61 simpr 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) -> R e. RR )
62 51 53 abstrid 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( abs ` ( ( T x. ( P - A ) ) + ( ( 1 - T ) x. ( P - B ) ) ) ) <_ ( ( abs ` ( T x. ( P - A ) ) ) + ( abs ` ( ( 1 - T ) x. ( P - B ) ) ) ) )
63 62 adantr 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) -> ( abs ` ( ( T x. ( P - A ) ) + ( ( 1 - T ) x. ( P - B ) ) ) ) <_ ( ( abs ` ( T x. ( P - A ) ) ) + ( abs ` ( ( 1 - T ) x. ( P - B ) ) ) ) )
64 oveq1 
 |-  ( T = 0 -> ( T x. ( P - A ) ) = ( 0 x. ( P - A ) ) )
65 50 mul02d 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( 0 x. ( P - A ) ) = 0 )
66 64 65 sylan9eqr 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ T = 0 ) -> ( T x. ( P - A ) ) = 0 )
67 66 abs00bd 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ T = 0 ) -> ( abs ` ( T x. ( P - A ) ) ) = 0 )
68 oveq2 
 |-  ( T = 0 -> ( 1 - T ) = ( 1 - 0 ) )
69 1m0e1 
 |-  ( 1 - 0 ) = 1
70 68 69 eqtrdi 
 |-  ( T = 0 -> ( 1 - T ) = 1 )
71 70 oveq1d 
 |-  ( T = 0 -> ( ( 1 - T ) x. ( P - B ) ) = ( 1 x. ( P - B ) ) )
72 52 mullidd 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( 1 x. ( P - B ) ) = ( P - B ) )
73 71 72 sylan9eqr 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ T = 0 ) -> ( ( 1 - T ) x. ( P - B ) ) = ( P - B ) )
74 73 fveq2d 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ T = 0 ) -> ( abs ` ( ( 1 - T ) x. ( P - B ) ) ) = ( abs ` ( P - B ) ) )
75 67 74 oveq12d 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ T = 0 ) -> ( ( abs ` ( T x. ( P - A ) ) ) + ( abs ` ( ( 1 - T ) x. ( P - B ) ) ) ) = ( 0 + ( abs ` ( P - B ) ) ) )
76 52 abscld 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( abs ` ( P - B ) ) e. RR )
77 76 recnd 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( abs ` ( P - B ) ) e. CC )
78 77 addlidd 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( 0 + ( abs ` ( P - B ) ) ) = ( abs ` ( P - B ) ) )
79 29 cnmetdval 
 |-  ( ( P e. CC /\ B e. CC ) -> ( P ( abs o. - ) B ) = ( abs ` ( P - B ) ) )
80 10 26 79 syl2anc 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( P ( abs o. - ) B ) = ( abs ` ( P - B ) ) )
81 78 80 eqtr4d 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( 0 + ( abs ` ( P - B ) ) ) = ( P ( abs o. - ) B ) )
82 25 simprd 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( P ( abs o. - ) B ) < R )
83 81 82 eqbrtrd 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( 0 + ( abs ` ( P - B ) ) ) < R )
84 83 adantr 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ T = 0 ) -> ( 0 + ( abs ` ( P - B ) ) ) < R )
85 75 84 eqbrtrd 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ T = 0 ) -> ( ( abs ` ( T x. ( P - A ) ) ) + ( abs ` ( ( 1 - T ) x. ( P - B ) ) ) ) < R )
86 85 adantlr 
 |-  ( ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) /\ T = 0 ) -> ( ( abs ` ( T x. ( P - A ) ) ) + ( abs ` ( ( 1 - T ) x. ( P - B ) ) ) ) < R )
87 6 50 absmuld 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( abs ` ( T x. ( P - A ) ) ) = ( ( abs ` T ) x. ( abs ` ( P - A ) ) ) )
88 4 simp2d 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> 0 <_ T )
89 5 88 absidd 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( abs ` T ) = T )
90 89 oveq1d 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( ( abs ` T ) x. ( abs ` ( P - A ) ) ) = ( T x. ( abs ` ( P - A ) ) ) )
91 87 90 eqtrd 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( abs ` ( T x. ( P - A ) ) ) = ( T x. ( abs ` ( P - A ) ) ) )
92 91 ad2antrr 
 |-  ( ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) /\ T =/= 0 ) -> ( abs ` ( T x. ( P - A ) ) ) = ( T x. ( abs ` ( P - A ) ) ) )
93 29 cnmetdval 
 |-  ( ( P e. CC /\ A e. CC ) -> ( P ( abs o. - ) A ) = ( abs ` ( P - A ) ) )
94 10 15 93 syl2anc 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( P ( abs o. - ) A ) = ( abs ` ( P - A ) ) )
95 14 simprd 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( P ( abs o. - ) A ) < R )
96 94 95 eqbrtrrd 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( abs ` ( P - A ) ) < R )
97 96 ad2antrr 
 |-  ( ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) /\ T =/= 0 ) -> ( abs ` ( P - A ) ) < R )
98 50 abscld 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( abs ` ( P - A ) ) e. RR )
99 98 ad2antrr 
 |-  ( ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) /\ T =/= 0 ) -> ( abs ` ( P - A ) ) e. RR )
100 simplr 
 |-  ( ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) /\ T =/= 0 ) -> R e. RR )
101 5 ad2antrr 
 |-  ( ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) /\ T =/= 0 ) -> T e. RR )
102 0red 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> 0 e. RR )
103 102 5 88 leltned 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( 0 < T <-> T =/= 0 ) )
104 103 biimpar 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ T =/= 0 ) -> 0 < T )
105 104 adantlr 
 |-  ( ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) /\ T =/= 0 ) -> 0 < T )
106 ltmul2 
 |-  ( ( ( abs ` ( P - A ) ) e. RR /\ R e. RR /\ ( T e. RR /\ 0 < T ) ) -> ( ( abs ` ( P - A ) ) < R <-> ( T x. ( abs ` ( P - A ) ) ) < ( T x. R ) ) )
107 99 100 101 105 106 syl112anc 
 |-  ( ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) /\ T =/= 0 ) -> ( ( abs ` ( P - A ) ) < R <-> ( T x. ( abs ` ( P - A ) ) ) < ( T x. R ) ) )
108 97 107 mpbid 
 |-  ( ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) /\ T =/= 0 ) -> ( T x. ( abs ` ( P - A ) ) ) < ( T x. R ) )
109 92 108 eqbrtrd 
 |-  ( ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) /\ T =/= 0 ) -> ( abs ` ( T x. ( P - A ) ) ) < ( T x. R ) )
110 20 52 absmuld 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( abs ` ( ( 1 - T ) x. ( P - B ) ) ) = ( ( abs ` ( 1 - T ) ) x. ( abs ` ( P - B ) ) ) )
111 17 a1i 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> 1 e. RR )
112 4 simp3d 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> T <_ 1 )
113 5 111 112 abssubge0d 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( abs ` ( 1 - T ) ) = ( 1 - T ) )
114 113 oveq1d 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( ( abs ` ( 1 - T ) ) x. ( abs ` ( P - B ) ) ) = ( ( 1 - T ) x. ( abs ` ( P - B ) ) ) )
115 110 114 eqtrd 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( abs ` ( ( 1 - T ) x. ( P - B ) ) ) = ( ( 1 - T ) x. ( abs ` ( P - B ) ) ) )
116 115 adantr 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) -> ( abs ` ( ( 1 - T ) x. ( P - B ) ) ) = ( ( 1 - T ) x. ( abs ` ( P - B ) ) ) )
117 76 adantr 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) -> ( abs ` ( P - B ) ) e. RR )
118 subge0 
 |-  ( ( 1 e. RR /\ T e. RR ) -> ( 0 <_ ( 1 - T ) <-> T <_ 1 ) )
119 17 5 118 sylancr 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( 0 <_ ( 1 - T ) <-> T <_ 1 ) )
120 112 119 mpbird 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> 0 <_ ( 1 - T ) )
121 19 120 jca 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( ( 1 - T ) e. RR /\ 0 <_ ( 1 - T ) ) )
122 121 adantr 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) -> ( ( 1 - T ) e. RR /\ 0 <_ ( 1 - T ) ) )
123 80 82 eqbrtrrd 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( abs ` ( P - B ) ) < R )
124 123 adantr 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) -> ( abs ` ( P - B ) ) < R )
125 ltle 
 |-  ( ( ( abs ` ( P - B ) ) e. RR /\ R e. RR ) -> ( ( abs ` ( P - B ) ) < R -> ( abs ` ( P - B ) ) <_ R ) )
126 76 125 sylan 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) -> ( ( abs ` ( P - B ) ) < R -> ( abs ` ( P - B ) ) <_ R ) )
127 124 126 mpd 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) -> ( abs ` ( P - B ) ) <_ R )
128 lemul2a 
 |-  ( ( ( ( abs ` ( P - B ) ) e. RR /\ R e. RR /\ ( ( 1 - T ) e. RR /\ 0 <_ ( 1 - T ) ) ) /\ ( abs ` ( P - B ) ) <_ R ) -> ( ( 1 - T ) x. ( abs ` ( P - B ) ) ) <_ ( ( 1 - T ) x. R ) )
129 117 61 122 127 128 syl31anc 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) -> ( ( 1 - T ) x. ( abs ` ( P - B ) ) ) <_ ( ( 1 - T ) x. R ) )
130 116 129 eqbrtrd 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) -> ( abs ` ( ( 1 - T ) x. ( P - B ) ) ) <_ ( ( 1 - T ) x. R ) )
131 130 adantr 
 |-  ( ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) /\ T =/= 0 ) -> ( abs ` ( ( 1 - T ) x. ( P - B ) ) ) <_ ( ( 1 - T ) x. R ) )
132 57 adantr 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) -> ( abs ` ( T x. ( P - A ) ) ) e. RR )
133 58 adantr 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) -> ( abs ` ( ( 1 - T ) x. ( P - B ) ) ) e. RR )
134 remulcl 
 |-  ( ( T e. RR /\ R e. RR ) -> ( T x. R ) e. RR )
135 5 134 sylan 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) -> ( T x. R ) e. RR )
136 remulcl 
 |-  ( ( ( 1 - T ) e. RR /\ R e. RR ) -> ( ( 1 - T ) x. R ) e. RR )
137 19 136 sylan 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) -> ( ( 1 - T ) x. R ) e. RR )
138 ltleadd 
 |-  ( ( ( ( abs ` ( T x. ( P - A ) ) ) e. RR /\ ( abs ` ( ( 1 - T ) x. ( P - B ) ) ) e. RR ) /\ ( ( T x. R ) e. RR /\ ( ( 1 - T ) x. R ) e. RR ) ) -> ( ( ( abs ` ( T x. ( P - A ) ) ) < ( T x. R ) /\ ( abs ` ( ( 1 - T ) x. ( P - B ) ) ) <_ ( ( 1 - T ) x. R ) ) -> ( ( abs ` ( T x. ( P - A ) ) ) + ( abs ` ( ( 1 - T ) x. ( P - B ) ) ) ) < ( ( T x. R ) + ( ( 1 - T ) x. R ) ) ) )
139 132 133 135 137 138 syl22anc 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) -> ( ( ( abs ` ( T x. ( P - A ) ) ) < ( T x. R ) /\ ( abs ` ( ( 1 - T ) x. ( P - B ) ) ) <_ ( ( 1 - T ) x. R ) ) -> ( ( abs ` ( T x. ( P - A ) ) ) + ( abs ` ( ( 1 - T ) x. ( P - B ) ) ) ) < ( ( T x. R ) + ( ( 1 - T ) x. R ) ) ) )
140 139 adantr 
 |-  ( ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) /\ T =/= 0 ) -> ( ( ( abs ` ( T x. ( P - A ) ) ) < ( T x. R ) /\ ( abs ` ( ( 1 - T ) x. ( P - B ) ) ) <_ ( ( 1 - T ) x. R ) ) -> ( ( abs ` ( T x. ( P - A ) ) ) + ( abs ` ( ( 1 - T ) x. ( P - B ) ) ) ) < ( ( T x. R ) + ( ( 1 - T ) x. R ) ) ) )
141 109 131 140 mp2and 
 |-  ( ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) /\ T =/= 0 ) -> ( ( abs ` ( T x. ( P - A ) ) ) + ( abs ` ( ( 1 - T ) x. ( P - B ) ) ) ) < ( ( T x. R ) + ( ( 1 - T ) x. R ) ) )
142 40 oveq1d 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( ( T + ( 1 - T ) ) x. R ) = ( 1 x. R ) )
143 142 adantr 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) -> ( ( T + ( 1 - T ) ) x. R ) = ( 1 x. R ) )
144 6 adantr 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) -> T e. CC )
145 20 adantr 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) -> ( 1 - T ) e. CC )
146 61 recnd 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) -> R e. CC )
147 144 145 146 adddird 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) -> ( ( T + ( 1 - T ) ) x. R ) = ( ( T x. R ) + ( ( 1 - T ) x. R ) ) )
148 146 mullidd 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) -> ( 1 x. R ) = R )
149 143 147 148 3eqtr3d 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) -> ( ( T x. R ) + ( ( 1 - T ) x. R ) ) = R )
150 149 adantr 
 |-  ( ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) /\ T =/= 0 ) -> ( ( T x. R ) + ( ( 1 - T ) x. R ) ) = R )
151 141 150 breqtrd 
 |-  ( ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) /\ T =/= 0 ) -> ( ( abs ` ( T x. ( P - A ) ) ) + ( abs ` ( ( 1 - T ) x. ( P - B ) ) ) ) < R )
152 86 151 pm2.61dane 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) -> ( ( abs ` ( T x. ( P - A ) ) ) + ( abs ` ( ( 1 - T ) x. ( P - B ) ) ) ) < R )
153 56 60 61 63 152 lelttrd 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R e. RR ) -> ( abs ` ( ( T x. ( P - A ) ) + ( ( 1 - T ) x. ( P - B ) ) ) ) < R )
154 55 adantr 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R = +oo ) -> ( abs ` ( ( T x. ( P - A ) ) + ( ( 1 - T ) x. ( P - B ) ) ) ) e. RR )
155 154 ltpnfd 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R = +oo ) -> ( abs ` ( ( T x. ( P - A ) ) + ( ( 1 - T ) x. ( P - B ) ) ) ) < +oo )
156 simpr 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R = +oo ) -> R = +oo )
157 155 156 breqtrrd 
 |-  ( ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) /\ R = +oo ) -> ( abs ` ( ( T x. ( P - A ) ) + ( ( 1 - T ) x. ( P - B ) ) ) ) < R )
158 0xr 
 |-  0 e. RR*
159 158 a1i 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> 0 e. RR* )
160 98 rexrd 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( abs ` ( P - A ) ) e. RR* )
161 50 absge0d 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> 0 <_ ( abs ` ( P - A ) ) )
162 159 160 11 161 96 xrlelttrd 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> 0 < R )
163 159 11 162 xrltled 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> 0 <_ R )
164 ge0nemnf 
 |-  ( ( R e. RR* /\ 0 <_ R ) -> R =/= -oo )
165 11 163 164 syl2anc 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> R =/= -oo )
166 11 165 jca 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( R e. RR* /\ R =/= -oo ) )
167 xrnemnf 
 |-  ( ( R e. RR* /\ R =/= -oo ) <-> ( R e. RR \/ R = +oo ) )
168 166 167 sylib 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( R e. RR \/ R = +oo ) )
169 153 157 168 mpjaodan 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( abs ` ( ( T x. ( P - A ) ) + ( ( 1 - T ) x. ( P - B ) ) ) ) < R )
170 49 169 eqbrtrd 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( P ( abs o. - ) ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) < R )
171 elbl 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ P e. CC /\ R e. RR* ) -> ( ( ( T x. A ) + ( ( 1 - T ) x. B ) ) e. ( P ( ball ` ( abs o. - ) ) R ) <-> ( ( ( T x. A ) + ( ( 1 - T ) x. B ) ) e. CC /\ ( P ( abs o. - ) ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) < R ) ) )
172 9 10 11 171 mp3an2i 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( ( ( T x. A ) + ( ( 1 - T ) x. B ) ) e. ( P ( ball ` ( abs o. - ) ) R ) <-> ( ( ( T x. A ) + ( ( 1 - T ) x. B ) ) e. CC /\ ( P ( abs o. - ) ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) < R ) ) )
173 28 170 172 mpbir2and 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( ( T x. A ) + ( ( 1 - T ) x. B ) ) e. ( P ( ball ` ( abs o. - ) ) R ) )
174 173 1 eleqtrrdi 
 |-  ( ( ( P e. CC /\ R e. RR* ) /\ ( A e. S /\ B e. S /\ T e. ( 0 [,] 1 ) ) ) -> ( ( T x. A ) + ( ( 1 - T ) x. B ) ) e. S )