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 ⊒ 𝑆 = ( 𝑃 ( ball β€˜ ( abs ∘ βˆ’ ) ) 𝑅 )
Assertion blcvx ( ( ( 𝑃 ∈ β„‚ ∧ 𝑅 ∈ ℝ* ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐡 ∈ 𝑆 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) β†’ ( ( 𝑇 Β· 𝐴 ) + ( ( 1 βˆ’ 𝑇 ) Β· 𝐡 ) ) ∈ 𝑆 )

Proof

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