This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 − 𝑇 ) · 𝐵 ) ) ∈ 𝑆 )