MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  blcvx Unicode version

Theorem blcvx 18304
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.)
Hypothesis
Ref Expression
blcvx.s  |-  S  =  ( P ( ball `  ( abs  o.  -  ) ) R )
Assertion
Ref Expression
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 of Theorem blcvx
StepHypRef Expression
1 simpr3 963 . . . . . . . 8  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  T  e.  ( 0 [,] 1
) )
2 0re 8838 . . . . . . . . 9  |-  0  e.  RR
3 1re 8837 . . . . . . . . 9  |-  1  e.  RR
42, 3elicc2i 10716 . . . . . . . 8  |-  ( T  e.  ( 0 [,] 1 )  <->  ( T  e.  RR  /\  0  <_  T  /\  T  <_  1
) )
51, 4sylib 188 . . . . . . 7  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  ( T  e.  RR  /\  0  <_  T  /\  T  <_ 
1 ) )
65simp1d 967 . . . . . 6  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  T  e.  RR )
76recnd 8861 . . . . 5  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  T  e.  CC )
8 simpr1 961 . . . . . . . 8  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  A  e.  S )
9 blcvx.s . . . . . . . 8  |-  S  =  ( P ( ball `  ( abs  o.  -  ) ) R )
108, 9syl6eleq 2373 . . . . . . 7  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  A  e.  ( P ( ball `  ( abs  o.  -  ) ) R ) )
11 cnxmet 18282 . . . . . . . . 9  |-  ( abs 
o.  -  )  e.  ( * Met `  CC )
1211a1i 10 . . . . . . . 8  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  ( abs  o.  -  )  e.  ( * Met `  CC ) )
13 simpll 730 . . . . . . . 8  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  P  e.  CC )
14 simplr 731 . . . . . . . 8  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  R  e.  RR* )
15 elbl 17949 . . . . . . . 8  |-  ( ( ( 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
) ) )
1612, 13, 14, 15syl3anc 1182 . . . . . . 7  |-  ( ( ( 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
) ) )
1710, 16mpbid 201 . . . . . 6  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  ( A  e.  CC  /\  ( P ( abs  o.  -  ) A )  <  R ) )
1817simpld 445 . . . . 5  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  A  e.  CC )
197, 18mulcld 8855 . . . 4  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  ( T  x.  A )  e.  CC )
20 resubcl 9111 . . . . . . 7  |-  ( ( 1  e.  RR  /\  T  e.  RR )  ->  ( 1  -  T
)  e.  RR )
213, 6, 20sylancr 644 . . . . . 6  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  (
1  -  T )  e.  RR )
2221recnd 8861 . . . . 5  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  (
1  -  T )  e.  CC )
23 simpr2 962 . . . . . . . 8  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  B  e.  S )
2423, 9syl6eleq 2373 . . . . . . 7  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  B  e.  ( P ( ball `  ( abs  o.  -  ) ) R ) )
25 elbl 17949 . . . . . . . 8  |-  ( ( ( 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
) ) )
2612, 13, 14, 25syl3anc 1182 . . . . . . 7  |-  ( ( ( 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
) ) )
2724, 26mpbid 201 . . . . . 6  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  ( B  e.  CC  /\  ( P ( abs  o.  -  ) B )  <  R ) )
2827simpld 445 . . . . 5  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  B  e.  CC )
2922, 28mulcld 8855 . . . 4  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  (
( 1  -  T
)  x.  B )  e.  CC )
3019, 29addcld 8854 . . 3  |-  ( ( ( 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 )
31 eqid 2283 . . . . . . 7  |-  ( abs 
o.  -  )  =  ( abs  o.  -  )
3231cnmetdval 18280 . . . . . 6  |-  ( ( 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
) ) ) ) )
3313, 30, 32syl2anc 642 . . . . 5  |-  ( ( ( 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 ) ) ) ) )
347, 13, 18subdid 9235 . . . . . . . 8  |-  ( ( ( 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 )
) )
3522, 13, 28subdid 9235 . . . . . . . 8  |-  ( ( ( 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
) ) )
3634, 35oveq12d 5876 . . . . . . 7  |-  ( ( ( 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 ) ) ) )
377, 13mulcld 8855 . . . . . . . 8  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  ( T  x.  P )  e.  CC )
3822, 13mulcld 8855 . . . . . . . 8  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  (
( 1  -  T
)  x.  P )  e.  CC )
3937, 38, 19, 29addsub4d 9204 . . . . . . 7  |-  ( ( ( 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 ) ) ) )
40 ax-1cn 8795 . . . . . . . . . . 11  |-  1  e.  CC
41 pncan3 9059 . . . . . . . . . . 11  |-  ( ( T  e.  CC  /\  1  e.  CC )  ->  ( T  +  ( 1  -  T ) )  =  1 )
427, 40, 41sylancl 643 . . . . . . . . . 10  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  ( T  +  ( 1  -  T ) )  =  1 )
4342oveq1d 5873 . . . . . . . . 9  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  (
( T  +  ( 1  -  T ) )  x.  P )  =  ( 1  x.  P ) )
447, 22, 13adddird 8860 . . . . . . . . 9  |-  ( ( ( 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
) ) )
45 mulid2 8836 . . . . . . . . . 10  |-  ( P  e.  CC  ->  (
1  x.  P )  =  P )
4645ad2antrr 706 . . . . . . . . 9  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  (
1  x.  P )  =  P )
4743, 44, 463eqtr3d 2323 . . . . . . . 8  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  (
( T  x.  P
)  +  ( ( 1  -  T )  x.  P ) )  =  P )
4847oveq1d 5873 . . . . . . 7  |-  ( ( ( 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 ) ) ) )
4936, 39, 483eqtr2d 2321 . . . . . 6  |-  ( ( ( 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 ) ) ) )
5049fveq2d 5529 . . . . 5  |-  ( ( ( 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 ) ) ) ) )
5133, 50eqtr4d 2318 . . . 4  |-  ( ( ( 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 ) ) ) ) )
5213, 18subcld 9157 . . . . . . . . . 10  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  ( P  -  A )  e.  CC )
537, 52mulcld 8855 . . . . . . . . 9  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  ( T  x.  ( P  -  A ) )  e.  CC )
5413, 28subcld 9157 . . . . . . . . . 10  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  ( P  -  B )  e.  CC )
5522, 54mulcld 8855 . . . . . . . . 9  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  (
( 1  -  T
)  x.  ( P  -  B ) )  e.  CC )
5653, 55addcld 8854 . . . . . . . 8  |-  ( ( ( 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 )
5756abscld 11918 . . . . . . 7  |-  ( ( ( 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 )
5857adantr 451 . . . . . 6  |-  ( ( ( ( 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 )
5953abscld 11918 . . . . . . . 8  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  ( abs `  ( T  x.  ( P  -  A
) ) )  e.  RR )
6055abscld 11918 . . . . . . . 8  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  ( abs `  ( ( 1  -  T )  x.  ( P  -  B
) ) )  e.  RR )
6159, 60readdcld 8862 . . . . . . 7  |-  ( ( ( 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 )
6261adantr 451 . . . . . 6  |-  ( ( ( ( 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 )
63 simpr 447 . . . . . 6  |-  ( ( ( ( P  e.  CC  /\  R  e. 
RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  ( 0 [,] 1 ) ) )  /\  R  e.  RR )  ->  R  e.  RR )
6453, 55abstrid 11938 . . . . . . 7  |-  ( ( ( 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 ) ) ) ) )
6564adantr 451 . . . . . 6  |-  ( ( ( ( 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 ) ) ) ) )
66 oveq1 5865 . . . . . . . . . . . . 13  |-  ( T  =  0  ->  ( T  x.  ( P  -  A ) )  =  ( 0  x.  ( P  -  A )
) )
6752mul02d 9010 . . . . . . . . . . . . 13  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  (
0  x.  ( P  -  A ) )  =  0 )
6866, 67sylan9eqr 2337 . . . . . . . . . . . 12  |-  ( ( ( ( P  e.  CC  /\  R  e. 
RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  ( 0 [,] 1 ) ) )  /\  T  =  0 )  ->  ( T  x.  ( P  -  A ) )  =  0 )
6968fveq2d 5529 . . . . . . . . . . 11  |-  ( ( ( ( P  e.  CC  /\  R  e. 
RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  ( 0 [,] 1 ) ) )  /\  T  =  0 )  ->  ( abs `  ( T  x.  ( P  -  A
) ) )  =  ( abs `  0
) )
70 abs0 11770 . . . . . . . . . . 11  |-  ( abs `  0 )  =  0
7169, 70syl6eq 2331 . . . . . . . . . 10  |-  ( ( ( ( P  e.  CC  /\  R  e. 
RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  ( 0 [,] 1 ) ) )  /\  T  =  0 )  ->  ( abs `  ( T  x.  ( P  -  A
) ) )  =  0 )
72 oveq2 5866 . . . . . . . . . . . . . 14  |-  ( T  =  0  ->  (
1  -  T )  =  ( 1  -  0 ) )
7340subid1i 9118 . . . . . . . . . . . . . 14  |-  ( 1  -  0 )  =  1
7472, 73syl6eq 2331 . . . . . . . . . . . . 13  |-  ( T  =  0  ->  (
1  -  T )  =  1 )
7574oveq1d 5873 . . . . . . . . . . . 12  |-  ( T  =  0  ->  (
( 1  -  T
)  x.  ( P  -  B ) )  =  ( 1  x.  ( P  -  B
) ) )
7654mulid2d 8853 . . . . . . . . . . . 12  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  (
1  x.  ( P  -  B ) )  =  ( P  -  B ) )
7775, 76sylan9eqr 2337 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) )
7877fveq2d 5529 . . . . . . . . . 10  |-  ( ( ( ( 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 )
) )
7971, 78oveq12d 5876 . . . . . . . . 9  |-  ( ( ( ( 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
) ) ) )
8054abscld 11918 . . . . . . . . . . . . . 14  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  ( abs `  ( P  -  B ) )  e.  RR )
8180recnd 8861 . . . . . . . . . . . . 13  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  ( abs `  ( P  -  B ) )  e.  CC )
8281addid2d 9013 . . . . . . . . . . . 12  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  (
0  +  ( abs `  ( P  -  B
) ) )  =  ( abs `  ( P  -  B )
) )
8331cnmetdval 18280 . . . . . . . . . . . . 13  |-  ( ( P  e.  CC  /\  B  e.  CC )  ->  ( P ( abs 
o.  -  ) B
)  =  ( abs `  ( P  -  B
) ) )
8413, 28, 83syl2anc 642 . . . . . . . . . . . 12  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  ( P ( abs  o.  -  ) B )  =  ( abs `  ( P  -  B )
) )
8582, 84eqtr4d 2318 . . . . . . . . . . 11  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  (
0  +  ( abs `  ( P  -  B
) ) )  =  ( P ( abs 
o.  -  ) B
) )
8627simprd 449 . . . . . . . . . . 11  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  ( P ( abs  o.  -  ) B )  <  R )
8785, 86eqbrtrd 4043 . . . . . . . . . 10  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  (
0  +  ( abs `  ( P  -  B
) ) )  < 
R )
8887adantr 451 . . . . . . . . 9  |-  ( ( ( ( P  e.  CC  /\  R  e. 
RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  ( 0 [,] 1 ) ) )  /\  T  =  0 )  ->  (
0  +  ( abs `  ( P  -  B
) ) )  < 
R )
8979, 88eqbrtrd 4043 . . . . . . . 8  |-  ( ( ( ( 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
)
9089adantlr 695 . . . . . . 7  |-  ( ( ( ( ( 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
)
917, 52absmuld 11936 . . . . . . . . . . . 12  |-  ( ( ( 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
) ) ) )
925simp2d 968 . . . . . . . . . . . . . 14  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  0  <_  T )
936, 92absidd 11905 . . . . . . . . . . . . 13  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  ( abs `  T )  =  T )
9493oveq1d 5873 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) ) )
9591, 94eqtrd 2315 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) ) )
9695ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( ( ( 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 ) ) ) )
9731cnmetdval 18280 . . . . . . . . . . . . . 14  |-  ( ( P  e.  CC  /\  A  e.  CC )  ->  ( P ( abs 
o.  -  ) A
)  =  ( abs `  ( P  -  A
) ) )
9813, 18, 97syl2anc 642 . . . . . . . . . . . . 13  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  ( P ( abs  o.  -  ) A )  =  ( abs `  ( P  -  A )
) )
9917simprd 449 . . . . . . . . . . . . 13  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  ( P ( abs  o.  -  ) A )  <  R )
10098, 99eqbrtrrd 4045 . . . . . . . . . . . 12  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  ( abs `  ( P  -  A ) )  < 
R )
101100ad2antrr 706 . . . . . . . . . . 11  |-  ( ( ( ( ( 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 )
10252abscld 11918 . . . . . . . . . . . . 13  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  ( abs `  ( P  -  A ) )  e.  RR )
103102ad2antrr 706 . . . . . . . . . . . 12  |-  ( ( ( ( ( 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 )
104 simplr 731 . . . . . . . . . . . 12  |-  ( ( ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  ( 0 [,] 1 ) ) )  /\  R  e.  RR )  /\  T  =/=  0 )  ->  R  e.  RR )
1056ad2antrr 706 . . . . . . . . . . . 12  |-  ( ( ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  ( 0 [,] 1 ) ) )  /\  R  e.  RR )  /\  T  =/=  0 )  ->  T  e.  RR )
1062a1i 10 . . . . . . . . . . . . . . 15  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  0  e.  RR )
107106, 6, 92leltned 8970 . . . . . . . . . . . . . 14  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  (
0  <  T  <->  T  =/=  0 ) )
108107biimpar 471 . . . . . . . . . . . . 13  |-  ( ( ( ( P  e.  CC  /\  R  e. 
RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  ( 0 [,] 1 ) ) )  /\  T  =/=  0 )  ->  0  <  T )
109108adantlr 695 . . . . . . . . . . . 12  |-  ( ( ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  ( 0 [,] 1 ) ) )  /\  R  e.  RR )  /\  T  =/=  0 )  ->  0  <  T )
110 ltmul2 9607 . . . . . . . . . . . 12  |-  ( ( ( 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 )
) )
111103, 104, 105, 109, 110syl112anc 1186 . . . . . . . . . . 11  |-  ( ( ( ( ( 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 )
) )
112101, 111mpbid 201 . . . . . . . . . 10  |-  ( ( ( ( ( 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
) )
11396, 112eqbrtrd 4043 . . . . . . . . 9  |-  ( ( ( ( ( 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
) )
11422, 54absmuld 11936 . . . . . . . . . . . . 13  |-  ( ( ( 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
) ) ) )
1153a1i 10 . . . . . . . . . . . . . . 15  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  1  e.  RR )
1165simp3d 969 . . . . . . . . . . . . . . 15  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  T  <_  1 )
1176, 115, 116abssubge0d 11914 . . . . . . . . . . . . . 14  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  ( abs `  ( 1  -  T ) )  =  ( 1  -  T
) )
118117oveq1d 5873 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) ) ) )
119114, 118eqtrd 2315 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) ) )
120119adantr 451 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) ) ) )
12180adantr 451 . . . . . . . . . . . 12  |-  ( ( ( ( P  e.  CC  /\  R  e. 
RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  ( 0 [,] 1 ) ) )  /\  R  e.  RR )  ->  ( abs `  ( P  -  B ) )  e.  RR )
122 subge0 9287 . . . . . . . . . . . . . . . 16  |-  ( ( 1  e.  RR  /\  T  e.  RR )  ->  ( 0  <_  (
1  -  T )  <-> 
T  <_  1 ) )
1233, 6, 122sylancr 644 . . . . . . . . . . . . . . 15  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  (
0  <_  ( 1  -  T )  <->  T  <_  1 ) )
124116, 123mpbird 223 . . . . . . . . . . . . . 14  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  0  <_  ( 1  -  T
) )
12521, 124jca 518 . . . . . . . . . . . . 13  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  (
( 1  -  T
)  e.  RR  /\  0  <_  ( 1  -  T ) ) )
126125adantr 451 . . . . . . . . . . . 12  |-  ( ( ( ( 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 ) ) )
12784, 86eqbrtrrd 4045 . . . . . . . . . . . . . 14  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  ( abs `  ( P  -  B ) )  < 
R )
128127adantr 451 . . . . . . . . . . . . 13  |-  ( ( ( ( P  e.  CC  /\  R  e. 
RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  ( 0 [,] 1 ) ) )  /\  R  e.  RR )  ->  ( abs `  ( P  -  B ) )  < 
R )
129 ltle 8910 . . . . . . . . . . . . . 14  |-  ( ( ( abs `  ( P  -  B )
)  e.  RR  /\  R  e.  RR )  ->  ( ( abs `  ( P  -  B )
)  <  R  ->  ( abs `  ( P  -  B ) )  <_  R ) )
13080, 129sylan 457 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 ) )
131128, 130mpd 14 . . . . . . . . . . . 12  |-  ( ( ( ( P  e.  CC  /\  R  e. 
RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  ( 0 [,] 1 ) ) )  /\  R  e.  RR )  ->  ( abs `  ( P  -  B ) )  <_  R )
132 lemul2a 9611 . . . . . . . . . . . 12  |-  ( ( ( ( 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 ) )
133121, 63, 126, 131, 132syl31anc 1185 . . . . . . . . . . 11  |-  ( ( ( ( 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
) )
134120, 133eqbrtrd 4043 . . . . . . . . . 10  |-  ( ( ( ( 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
) )
135134adantr 451 . . . . . . . . 9  |-  ( ( ( ( ( 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
) )
13659adantr 451 . . . . . . . . . . 11  |-  ( ( ( ( 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 )
13760adantr 451 . . . . . . . . . . 11  |-  ( ( ( ( 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 )
138 remulcl 8822 . . . . . . . . . . . 12  |-  ( ( T  e.  RR  /\  R  e.  RR )  ->  ( T  x.  R
)  e.  RR )
1396, 138sylan 457 . . . . . . . . . . 11  |-  ( ( ( ( P  e.  CC  /\  R  e. 
RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  ( 0 [,] 1 ) ) )  /\  R  e.  RR )  ->  ( T  x.  R )  e.  RR )
140 remulcl 8822 . . . . . . . . . . . 12  |-  ( ( ( 1  -  T
)  e.  RR  /\  R  e.  RR )  ->  ( ( 1  -  T )  x.  R
)  e.  RR )
14121, 140sylan 457 . . . . . . . . . . 11  |-  ( ( ( ( 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 )
142 ltleadd 9257 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) ) ) )
143136, 137, 139, 141, 142syl22anc 1183 . . . . . . . . . 10  |-  ( ( ( ( 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 ) ) ) )
144143adantr 451 . . . . . . . . 9  |-  ( ( ( ( ( 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 ) ) ) )
145113, 135, 144mp2and 660 . . . . . . . 8  |-  ( ( ( ( ( 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 ) ) )
14642oveq1d 5873 . . . . . . . . . . 11  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  (
( T  +  ( 1  -  T ) )  x.  R )  =  ( 1  x.  R ) )
147146adantr 451 . . . . . . . . . 10  |-  ( ( ( ( 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 ) )
1487adantr 451 . . . . . . . . . . 11  |-  ( ( ( ( P  e.  CC  /\  R  e. 
RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  ( 0 [,] 1 ) ) )  /\  R  e.  RR )  ->  T  e.  CC )
14922adantr 451 . . . . . . . . . . 11  |-  ( ( ( ( P  e.  CC  /\  R  e. 
RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  ( 0 [,] 1 ) ) )  /\  R  e.  RR )  ->  (
1  -  T )  e.  CC )
15063recnd 8861 . . . . . . . . . . 11  |-  ( ( ( ( P  e.  CC  /\  R  e. 
RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  ( 0 [,] 1 ) ) )  /\  R  e.  RR )  ->  R  e.  CC )
151148, 149, 150adddird 8860 . . . . . . . . . 10  |-  ( ( ( ( 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
) ) )
152150mulid2d 8853 . . . . . . . . . 10  |-  ( ( ( ( P  e.  CC  /\  R  e. 
RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  ( 0 [,] 1 ) ) )  /\  R  e.  RR )  ->  (
1  x.  R )  =  R )
153147, 151, 1523eqtr3d 2323 . . . . . . . . 9  |-  ( ( ( ( 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 )
154153adantr 451 . . . . . . . 8  |-  ( ( ( ( ( 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 )
155145, 154breqtrd 4047 . . . . . . 7  |-  ( ( ( ( ( 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
)
15690, 155pm2.61dane 2524 . . . . . 6  |-  ( ( ( ( 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
)
15758, 62, 63, 65, 156lelttrd 8974 . . . . 5  |-  ( ( ( ( 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 )
15857adantr 451 . . . . . . 7  |-  ( ( ( ( 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 )
159 ltpnf 10463 . . . . . . 7  |-  ( ( abs `  ( ( T  x.  ( P  -  A ) )  +  ( ( 1  -  T )  x.  ( P  -  B
) ) ) )  e.  RR  ->  ( abs `  ( ( T  x.  ( P  -  A ) )  +  ( ( 1  -  T )  x.  ( P  -  B )
) ) )  <  +oo )
160158, 159syl 15 . . . . . 6  |-  ( ( ( ( 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 )
161 simpr 447 . . . . . 6  |-  ( ( ( ( P  e.  CC  /\  R  e. 
RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  ( 0 [,] 1 ) ) )  /\  R  = 
+oo )  ->  R  =  +oo )
162160, 161breqtrrd 4049 . . . . 5  |-  ( ( ( ( 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 )
163 0xr 8878 . . . . . . . . . . 11  |-  0  e.  RR*
164163a1i 10 . . . . . . . . . 10  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  0  e.  RR* )
165102rexrd 8881 . . . . . . . . . 10  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  ( abs `  ( P  -  A ) )  e. 
RR* )
16652absge0d 11926 . . . . . . . . . 10  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  0  <_  ( abs `  ( P  -  A )
) )
167164, 165, 14, 166, 100xrlelttrd 10491 . . . . . . . . 9  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  0  <  R )
168 xrltle 10483 . . . . . . . . . 10  |-  ( ( 0  e.  RR*  /\  R  e.  RR* )  ->  (
0  <  R  ->  0  <_  R ) )
169163, 14, 168sylancr 644 . . . . . . . . 9  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  (
0  <  R  ->  0  <_  R ) )
170167, 169mpd 14 . . . . . . . 8  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  0  <_  R )
171 ge0nemnf 10502 . . . . . . . 8  |-  ( ( R  e.  RR*  /\  0  <_  R )  ->  R  =/=  -oo )
17214, 170, 171syl2anc 642 . . . . . . 7  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  R  =/=  -oo )
17314, 172jca 518 . . . . . 6  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  ( R  e.  RR*  /\  R  =/=  -oo ) )
174 xrnemnf 10460 . . . . . 6  |-  ( ( R  e.  RR*  /\  R  =/=  -oo )  <->  ( R  e.  RR  \/  R  = 
+oo ) )
175173, 174sylib 188 . . . . 5  |-  ( ( ( P  e.  CC  /\  R  e.  RR* )  /\  ( A  e.  S  /\  B  e.  S  /\  T  e.  (
0 [,] 1 ) ) )  ->  ( R  e.  RR  \/  R  =  +oo ) )
176157, 162, 175mpjaodan 761 . . . 4  |-  ( ( ( 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 )
17751, 176eqbrtrd 4043 . . 3  |-  ( ( ( 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 )
178 elbl 17949 . . . 4  |-  ( ( ( 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 ) ) )
17912, 13, 14, 178syl3anc 1182 . . 3  |-  ( ( ( 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 ) ) )
18030, 177, 179mpbir2and 888 . 2  |-  ( ( ( 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 ) )
181180, 9syl6eleqr 2374 1  |-  ( ( ( 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 )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358    /\ w3a 934    = wceq 1623    e. wcel 1684    =/= wne 2446   class class class wbr 4023    o. ccom 4693   ` cfv 5255  (class class class)co 5858   CCcc 8735   RRcr 8736   0cc0 8737   1c1 8738    + caddc 8740    x. cmul 8742    +oocpnf 8864    -oocmnf 8865   RR*cxr 8866    < clt 8867    <_ cle 8868    - cmin 9037   [,]cicc 10659   abscabs 11719   * Metcxmt 16369   ballcbl 16371
This theorem is referenced by:  dvlipcn  19341  blscon  23775
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-cnex 8793  ax-resscn 8794  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-addrcl 8798  ax-mulcl 8799  ax-mulrcl 8800  ax-mulcom 8801  ax-addass 8802  ax-mulass 8803  ax-distr 8804  ax-i2m1 8805  ax-1ne0 8806  ax-1rid 8807  ax-rnegex 8808  ax-rrecex 8809  ax-cnre 8810  ax-pre-lttri 8811  ax-pre-lttrn 8812  ax-pre-ltadd 8813  ax-pre-mulgt0 8814  ax-pre-sup 8815
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-ral 2548  df-rex 2549  df-reu 2550  df-rmo 2551  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-1st 6122  df-2nd 6123  df-riota 6304  df-recs 6388  df-rdg 6423  df-er 6660  df-map 6774  df-en 6864  df-dom 6865  df-sdom 6866  df-sup 7194  df-pnf 8869  df-mnf 8870  df-xr 8871  df-ltxr 8872  df-le 8873  df-sub 9039  df-neg 9040  df-div 9424  df-nn 9747  df-2 9804  df-3 9805  df-n0 9966  df-z 10025  df-uz 10231  df-rp 10355  df-xadd 10453  df-icc 10663  df-seq 11047  df-exp 11105  df-cj 11584  df-re 11585  df-im 11586  df-sqr 11720  df-abs 11721  df-xmet 16373  df-met 16374  df-bl 16375
  Copyright terms: Public domain W3C validator