Proof of Theorem blcvx
| Step | Hyp | Ref
| Expression |
| 1 | | simpr3 1197 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ (0[,]1)) |
| 2 | | elicc01 13506 |
. . . . . . . 8
⊢ (𝑇 ∈ (0[,]1) ↔ (𝑇 ∈ ℝ ∧ 0 ≤
𝑇 ∧ 𝑇 ≤ 1)) |
| 3 | 1, 2 | sylib 218 |
. . . . . . 7
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 ∈ ℝ ∧ 0 ≤ 𝑇 ∧ 𝑇 ≤ 1)) |
| 4 | 3 | simp1d 1143 |
. . . . . 6
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ ℝ) |
| 5 | 4 | recnd 11289 |
. . . . 5
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ ℂ) |
| 6 | | simpr1 1195 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝐴 ∈ 𝑆) |
| 7 | | blcvx.s |
. . . . . . . 8
⊢ 𝑆 = (𝑃(ball‘(abs ∘ − ))𝑅) |
| 8 | 6, 7 | eleqtrdi 2851 |
. . . . . . 7
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝐴 ∈ (𝑃(ball‘(abs ∘ − ))𝑅)) |
| 9 | | cnxmet 24793 |
. . . . . . . 8
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
| 10 | | simpll 767 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑃 ∈ ℂ) |
| 11 | | simplr 769 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑅 ∈
ℝ*) |
| 12 | | elbl 24398 |
. . . . . . . 8
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*) → (𝐴 ∈ (𝑃(ball‘(abs ∘ − ))𝑅) ↔ (𝐴 ∈ ℂ ∧ (𝑃(abs ∘ − )𝐴) < 𝑅))) |
| 13 | 9, 10, 11, 12 | mp3an2i 1468 |
. . . . . . 7
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝐴 ∈ (𝑃(ball‘(abs ∘ − ))𝑅) ↔ (𝐴 ∈ ℂ ∧ (𝑃(abs ∘ − )𝐴) < 𝑅))) |
| 14 | 8, 13 | mpbid 232 |
. . . . . 6
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝐴 ∈ ℂ ∧ (𝑃(abs ∘ − )𝐴) < 𝑅)) |
| 15 | 14 | simpld 494 |
. . . . 5
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝐴 ∈ ℂ) |
| 16 | 5, 15 | mulcld 11281 |
. . . 4
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · 𝐴) ∈ ℂ) |
| 17 | | 1re 11261 |
. . . . . . 7
⊢ 1 ∈
ℝ |
| 18 | | resubcl 11573 |
. . . . . . 7
⊢ ((1
∈ ℝ ∧ 𝑇
∈ ℝ) → (1 − 𝑇) ∈ ℝ) |
| 19 | 17, 4, 18 | sylancr 587 |
. . . . . 6
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (1 − 𝑇) ∈
ℝ) |
| 20 | 19 | recnd 11289 |
. . . . 5
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (1 − 𝑇) ∈
ℂ) |
| 21 | | simpr2 1196 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝐵 ∈ 𝑆) |
| 22 | 21, 7 | eleqtrdi 2851 |
. . . . . . 7
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝐵 ∈ (𝑃(ball‘(abs ∘ − ))𝑅)) |
| 23 | | elbl 24398 |
. . . . . . . 8
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*) → (𝐵 ∈ (𝑃(ball‘(abs ∘ − ))𝑅) ↔ (𝐵 ∈ ℂ ∧ (𝑃(abs ∘ − )𝐵) < 𝑅))) |
| 24 | 9, 10, 11, 23 | mp3an2i 1468 |
. . . . . . 7
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝐵 ∈ (𝑃(ball‘(abs ∘ − ))𝑅) ↔ (𝐵 ∈ ℂ ∧ (𝑃(abs ∘ − )𝐵) < 𝑅))) |
| 25 | 22, 24 | mpbid 232 |
. . . . . 6
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝐵 ∈ ℂ ∧ (𝑃(abs ∘ − )𝐵) < 𝑅)) |
| 26 | 25 | simpld 494 |
. . . . 5
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝐵 ∈ ℂ) |
| 27 | 20, 26 | mulcld 11281 |
. . . 4
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · 𝐵) ∈ ℂ) |
| 28 | 16, 27 | addcld 11280 |
. . 3
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ ℂ) |
| 29 | | eqid 2737 |
. . . . . . 7
⊢ (abs
∘ − ) = (abs ∘ − ) |
| 30 | 29 | cnmetdval 24791 |
. . . . . 6
⊢ ((𝑃 ∈ ℂ ∧ ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ ℂ) → (𝑃(abs ∘ − )((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) = (abs‘(𝑃 − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))))) |
| 31 | 10, 28, 30 | syl2anc 584 |
. . . . 5
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) = (abs‘(𝑃 − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))))) |
| 32 | 5, 10, 15 | subdid 11719 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · (𝑃 − 𝐴)) = ((𝑇 · 𝑃) − (𝑇 · 𝐴))) |
| 33 | 20, 10, 26 | subdid 11719 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · (𝑃 − 𝐵)) = (((1 − 𝑇) · 𝑃) − ((1 − 𝑇) · 𝐵))) |
| 34 | 32, 33 | oveq12d 7449 |
. . . . . . 7
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵))) = (((𝑇 · 𝑃) − (𝑇 · 𝐴)) + (((1 − 𝑇) · 𝑃) − ((1 − 𝑇) · 𝐵)))) |
| 35 | 5, 10 | mulcld 11281 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · 𝑃) ∈ ℂ) |
| 36 | 20, 10 | mulcld 11281 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · 𝑃) ∈ ℂ) |
| 37 | 35, 36, 16, 27 | addsub4d 11667 |
. . . . . . 7
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (((𝑇 · 𝑃) + ((1 − 𝑇) · 𝑃)) − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) = (((𝑇 · 𝑃) − (𝑇 · 𝐴)) + (((1 − 𝑇) · 𝑃) − ((1 − 𝑇) · 𝐵)))) |
| 38 | | ax-1cn 11213 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
| 39 | | pncan3 11516 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑇 + (1
− 𝑇)) =
1) |
| 40 | 5, 38, 39 | sylancl 586 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 + (1 − 𝑇)) = 1) |
| 41 | 40 | oveq1d 7446 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · 𝑃) = (1 · 𝑃)) |
| 42 | 5, 20, 10 | adddird 11286 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · 𝑃) = ((𝑇 · 𝑃) + ((1 − 𝑇) · 𝑃))) |
| 43 | | mullid 11260 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℂ → (1
· 𝑃) = 𝑃) |
| 44 | 43 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (1 · 𝑃) = 𝑃) |
| 45 | 41, 42, 44 | 3eqtr3d 2785 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝑃) + ((1 − 𝑇) · 𝑃)) = 𝑃) |
| 46 | 45 | oveq1d 7446 |
. . . . . . 7
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (((𝑇 · 𝑃) + ((1 − 𝑇) · 𝑃)) − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) = (𝑃 − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)))) |
| 47 | 34, 37, 46 | 3eqtr2d 2783 |
. . . . . 6
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵))) = (𝑃 − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)))) |
| 48 | 47 | fveq2d 6910 |
. . . . 5
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) = (abs‘(𝑃 − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))))) |
| 49 | 31, 48 | eqtr4d 2780 |
. . . 4
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) = (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵))))) |
| 50 | 10, 15 | subcld 11620 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃 − 𝐴) ∈ ℂ) |
| 51 | 5, 50 | mulcld 11281 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · (𝑃 − 𝐴)) ∈ ℂ) |
| 52 | 10, 26 | subcld 11620 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃 − 𝐵) ∈ ℂ) |
| 53 | 20, 52 | mulcld 11281 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · (𝑃 − 𝐵)) ∈ ℂ) |
| 54 | 51, 53 | addcld 11280 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵))) ∈ ℂ) |
| 55 | 54 | abscld 15475 |
. . . . . . 7
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) ∈ ℝ) |
| 56 | 55 | adantr 480 |
. . . . . 6
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) ∈ ℝ) |
| 57 | 51 | abscld 15475 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑇 · (𝑃 − 𝐴))) ∈ ℝ) |
| 58 | 53 | abscld 15475 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((1
− 𝑇) · (𝑃 − 𝐵))) ∈ ℝ) |
| 59 | 57, 58 | readdcld 11290 |
. . . . . . 7
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) ∈ ℝ) |
| 60 | 59 | adantr 480 |
. . . . . 6
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) ∈ ℝ) |
| 61 | | simpr 484 |
. . . . . 6
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → 𝑅 ∈ ℝ) |
| 62 | 51, 53 | abstrid 15495 |
. . . . . . 7
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) ≤ ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵))))) |
| 63 | 62 | adantr 480 |
. . . . . 6
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) ≤ ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵))))) |
| 64 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑇 = 0 → (𝑇 · (𝑃 − 𝐴)) = (0 · (𝑃 − 𝐴))) |
| 65 | 50 | mul02d 11459 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (0 · (𝑃 − 𝐴)) = 0) |
| 66 | 64, 65 | sylan9eqr 2799 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → (𝑇 · (𝑃 − 𝐴)) = 0) |
| 67 | 66 | abs00bd 15330 |
. . . . . . . . . 10
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → (abs‘(𝑇 · (𝑃 − 𝐴))) = 0) |
| 68 | | oveq2 7439 |
. . . . . . . . . . . . . 14
⊢ (𝑇 = 0 → (1 − 𝑇) = (1 −
0)) |
| 69 | | 1m0e1 12387 |
. . . . . . . . . . . . . 14
⊢ (1
− 0) = 1 |
| 70 | 68, 69 | eqtrdi 2793 |
. . . . . . . . . . . . 13
⊢ (𝑇 = 0 → (1 − 𝑇) = 1) |
| 71 | 70 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝑇 = 0 → ((1 − 𝑇) · (𝑃 − 𝐵)) = (1 · (𝑃 − 𝐵))) |
| 72 | 52 | mullidd 11279 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (1 · (𝑃 − 𝐵)) = (𝑃 − 𝐵)) |
| 73 | 71, 72 | sylan9eqr 2799 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → ((1 − 𝑇) · (𝑃 − 𝐵)) = (𝑃 − 𝐵)) |
| 74 | 73 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) = (abs‘(𝑃 − 𝐵))) |
| 75 | 67, 74 | oveq12d 7449 |
. . . . . . . . 9
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) = (0 + (abs‘(𝑃 − 𝐵)))) |
| 76 | 52 | abscld 15475 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑃 − 𝐵)) ∈ ℝ) |
| 77 | 76 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑃 − 𝐵)) ∈ ℂ) |
| 78 | 77 | addlidd 11462 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (0 +
(abs‘(𝑃 − 𝐵))) = (abs‘(𝑃 − 𝐵))) |
| 79 | 29 | cnmetdval 24791 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑃(abs ∘ − )𝐵) = (abs‘(𝑃 − 𝐵))) |
| 80 | 10, 26, 79 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )𝐵) = (abs‘(𝑃 − 𝐵))) |
| 81 | 78, 80 | eqtr4d 2780 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (0 +
(abs‘(𝑃 − 𝐵))) = (𝑃(abs ∘ − )𝐵)) |
| 82 | 25 | simprd 495 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )𝐵) < 𝑅) |
| 83 | 81, 82 | eqbrtrd 5165 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (0 +
(abs‘(𝑃 − 𝐵))) < 𝑅) |
| 84 | 83 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → (0 + (abs‘(𝑃 − 𝐵))) < 𝑅) |
| 85 | 75, 84 | eqbrtrd 5165 |
. . . . . . . 8
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅) |
| 86 | 85 | adantlr 715 |
. . . . . . 7
⊢
(((((𝑃 ∈
ℂ ∧ 𝑅 ∈
ℝ*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 = 0) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅) |
| 87 | 5, 50 | absmuld 15493 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑇 · (𝑃 − 𝐴))) = ((abs‘𝑇) · (abs‘(𝑃 − 𝐴)))) |
| 88 | 3 | simp2d 1144 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 ≤ 𝑇) |
| 89 | 4, 88 | absidd 15461 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘𝑇) = 𝑇) |
| 90 | 89 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((abs‘𝑇) · (abs‘(𝑃 − 𝐴))) = (𝑇 · (abs‘(𝑃 − 𝐴)))) |
| 91 | 87, 90 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑇 · (𝑃 − 𝐴))) = (𝑇 · (abs‘(𝑃 − 𝐴)))) |
| 92 | 91 | ad2antrr 726 |
. . . . . . . . . 10
⊢
(((((𝑃 ∈
ℂ ∧ 𝑅 ∈
ℝ*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (abs‘(𝑇 · (𝑃 − 𝐴))) = (𝑇 · (abs‘(𝑃 − 𝐴)))) |
| 93 | 29 | cnmetdval 24791 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝑃(abs ∘ − )𝐴) = (abs‘(𝑃 − 𝐴))) |
| 94 | 10, 15, 93 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )𝐴) = (abs‘(𝑃 − 𝐴))) |
| 95 | 14 | simprd 495 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )𝐴) < 𝑅) |
| 96 | 94, 95 | eqbrtrrd 5167 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑃 − 𝐴)) < 𝑅) |
| 97 | 96 | ad2antrr 726 |
. . . . . . . . . . 11
⊢
(((((𝑃 ∈
ℂ ∧ 𝑅 ∈
ℝ*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (abs‘(𝑃 − 𝐴)) < 𝑅) |
| 98 | 50 | abscld 15475 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑃 − 𝐴)) ∈ ℝ) |
| 99 | 98 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢
(((((𝑃 ∈
ℂ ∧ 𝑅 ∈
ℝ*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (abs‘(𝑃 − 𝐴)) ∈ ℝ) |
| 100 | | simplr 769 |
. . . . . . . . . . . 12
⊢
(((((𝑃 ∈
ℂ ∧ 𝑅 ∈
ℝ*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → 𝑅 ∈ ℝ) |
| 101 | 4 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢
(((((𝑃 ∈
ℂ ∧ 𝑅 ∈
ℝ*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → 𝑇 ∈ ℝ) |
| 102 | | 0red 11264 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 ∈
ℝ) |
| 103 | 102, 4, 88 | leltned 11414 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (0 < 𝑇 ↔ 𝑇 ≠ 0)) |
| 104 | 103 | biimpar 477 |
. . . . . . . . . . . . 13
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ≠ 0) → 0 < 𝑇) |
| 105 | 104 | adantlr 715 |
. . . . . . . . . . . 12
⊢
(((((𝑃 ∈
ℂ ∧ 𝑅 ∈
ℝ*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → 0 < 𝑇) |
| 106 | | ltmul2 12118 |
. . . . . . . . . . . 12
⊢
(((abs‘(𝑃
− 𝐴)) ∈ ℝ
∧ 𝑅 ∈ ℝ
∧ (𝑇 ∈ ℝ
∧ 0 < 𝑇)) →
((abs‘(𝑃 −
𝐴)) < 𝑅 ↔ (𝑇 · (abs‘(𝑃 − 𝐴))) < (𝑇 · 𝑅))) |
| 107 | 99, 100, 101, 105, 106 | syl112anc 1376 |
. . . . . . . . . . 11
⊢
(((((𝑃 ∈
ℂ ∧ 𝑅 ∈
ℝ*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → ((abs‘(𝑃 − 𝐴)) < 𝑅 ↔ (𝑇 · (abs‘(𝑃 − 𝐴))) < (𝑇 · 𝑅))) |
| 108 | 97, 107 | mpbid 232 |
. . . . . . . . . 10
⊢
(((((𝑃 ∈
ℂ ∧ 𝑅 ∈
ℝ*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (𝑇 · (abs‘(𝑃 − 𝐴))) < (𝑇 · 𝑅)) |
| 109 | 92, 108 | eqbrtrd 5165 |
. . . . . . . . 9
⊢
(((((𝑃 ∈
ℂ ∧ 𝑅 ∈
ℝ*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (abs‘(𝑇 · (𝑃 − 𝐴))) < (𝑇 · 𝑅)) |
| 110 | 20, 52 | absmuld 15493 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((1
− 𝑇) · (𝑃 − 𝐵))) = ((abs‘(1 − 𝑇)) · (abs‘(𝑃 − 𝐵)))) |
| 111 | 17 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 1 ∈
ℝ) |
| 112 | 3 | simp3d 1145 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ≤ 1) |
| 113 | 4, 111, 112 | abssubge0d 15470 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(1
− 𝑇)) = (1 −
𝑇)) |
| 114 | 113 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((abs‘(1
− 𝑇)) ·
(abs‘(𝑃 − 𝐵))) = ((1 − 𝑇) · (abs‘(𝑃 − 𝐵)))) |
| 115 | 110, 114 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((1
− 𝑇) · (𝑃 − 𝐵))) = ((1 − 𝑇) · (abs‘(𝑃 − 𝐵)))) |
| 116 | 115 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘((1
− 𝑇) · (𝑃 − 𝐵))) = ((1 − 𝑇) · (abs‘(𝑃 − 𝐵)))) |
| 117 | 76 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘(𝑃 − 𝐵)) ∈ ℝ) |
| 118 | | subge0 11776 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℝ ∧ 𝑇
∈ ℝ) → (0 ≤ (1 − 𝑇) ↔ 𝑇 ≤ 1)) |
| 119 | 17, 4, 118 | sylancr 587 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (0 ≤ (1 −
𝑇) ↔ 𝑇 ≤ 1)) |
| 120 | 112, 119 | mpbird 257 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 ≤ (1 −
𝑇)) |
| 121 | 19, 120 | jca 511 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) ∈ ℝ ∧ 0 ≤ (1
− 𝑇))) |
| 122 | 121 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((1 − 𝑇) ∈ ℝ ∧ 0 ≤ (1
− 𝑇))) |
| 123 | 80, 82 | eqbrtrrd 5167 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑃 − 𝐵)) < 𝑅) |
| 124 | 123 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘(𝑃 − 𝐵)) < 𝑅) |
| 125 | | ltle 11349 |
. . . . . . . . . . . . . 14
⊢
(((abs‘(𝑃
− 𝐵)) ∈ ℝ
∧ 𝑅 ∈ ℝ)
→ ((abs‘(𝑃
− 𝐵)) < 𝑅 → (abs‘(𝑃 − 𝐵)) ≤ 𝑅)) |
| 126 | 76, 125 | sylan 580 |
. . . . . . . . . . . . 13
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((abs‘(𝑃 − 𝐵)) < 𝑅 → (abs‘(𝑃 − 𝐵)) ≤ 𝑅)) |
| 127 | 124, 126 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘(𝑃 − 𝐵)) ≤ 𝑅) |
| 128 | | lemul2a 12122 |
. . . . . . . . . . . 12
⊢
((((abs‘(𝑃
− 𝐵)) ∈ ℝ
∧ 𝑅 ∈ ℝ
∧ ((1 − 𝑇) ∈
ℝ ∧ 0 ≤ (1 − 𝑇))) ∧ (abs‘(𝑃 − 𝐵)) ≤ 𝑅) → ((1 − 𝑇) · (abs‘(𝑃 − 𝐵))) ≤ ((1 − 𝑇) · 𝑅)) |
| 129 | 117, 61, 122, 127, 128 | syl31anc 1375 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((1 − 𝑇) · (abs‘(𝑃 − 𝐵))) ≤ ((1 − 𝑇) · 𝑅)) |
| 130 | 116, 129 | eqbrtrd 5165 |
. . . . . . . . . 10
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘((1
− 𝑇) · (𝑃 − 𝐵))) ≤ ((1 − 𝑇) · 𝑅)) |
| 131 | 130 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝑃 ∈
ℂ ∧ 𝑅 ∈
ℝ*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) ≤ ((1 − 𝑇) · 𝑅)) |
| 132 | 57 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘(𝑇 · (𝑃 − 𝐴))) ∈ ℝ) |
| 133 | 58 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘((1
− 𝑇) · (𝑃 − 𝐵))) ∈ ℝ) |
| 134 | | remulcl 11240 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑇 · 𝑅) ∈ ℝ) |
| 135 | 4, 134 | sylan 580 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (𝑇 · 𝑅) ∈ ℝ) |
| 136 | | remulcl 11240 |
. . . . . . . . . . . 12
⊢ (((1
− 𝑇) ∈ ℝ
∧ 𝑅 ∈ ℝ)
→ ((1 − 𝑇)
· 𝑅) ∈
ℝ) |
| 137 | 19, 136 | sylan 580 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((1 − 𝑇) · 𝑅) ∈ ℝ) |
| 138 | | ltleadd 11746 |
. . . . . . . . . . 11
⊢
((((abs‘(𝑇
· (𝑃 − 𝐴))) ∈ ℝ ∧
(abs‘((1 − 𝑇)
· (𝑃 − 𝐵))) ∈ ℝ) ∧
((𝑇 · 𝑅) ∈ ℝ ∧ ((1
− 𝑇) · 𝑅) ∈ ℝ)) →
(((abs‘(𝑇 ·
(𝑃 − 𝐴))) < (𝑇 · 𝑅) ∧ (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) ≤ ((1 − 𝑇) · 𝑅)) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅)))) |
| 139 | 132, 133,
135, 137, 138 | syl22anc 839 |
. . . . . . . . . 10
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (((abs‘(𝑇 · (𝑃 − 𝐴))) < (𝑇 · 𝑅) ∧ (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) ≤ ((1 − 𝑇) · 𝑅)) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅)))) |
| 140 | 139 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝑃 ∈
ℂ ∧ 𝑅 ∈
ℝ*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (((abs‘(𝑇 · (𝑃 − 𝐴))) < (𝑇 · 𝑅) ∧ (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) ≤ ((1 − 𝑇) · 𝑅)) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅)))) |
| 141 | 109, 131,
140 | mp2and 699 |
. . . . . . . 8
⊢
(((((𝑃 ∈
ℂ ∧ 𝑅 ∈
ℝ*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅))) |
| 142 | 40 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · 𝑅) = (1 · 𝑅)) |
| 143 | 142 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((𝑇 + (1 − 𝑇)) · 𝑅) = (1 · 𝑅)) |
| 144 | 5 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → 𝑇 ∈ ℂ) |
| 145 | 20 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (1 − 𝑇) ∈
ℂ) |
| 146 | 61 | recnd 11289 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → 𝑅 ∈ ℂ) |
| 147 | 144, 145,
146 | adddird 11286 |
. . . . . . . . . 10
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((𝑇 + (1 − 𝑇)) · 𝑅) = ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅))) |
| 148 | 146 | mullidd 11279 |
. . . . . . . . . 10
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (1 · 𝑅) = 𝑅) |
| 149 | 143, 147,
148 | 3eqtr3d 2785 |
. . . . . . . . 9
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅)) = 𝑅) |
| 150 | 149 | adantr 480 |
. . . . . . . 8
⊢
(((((𝑃 ∈
ℂ ∧ 𝑅 ∈
ℝ*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅)) = 𝑅) |
| 151 | 141, 150 | breqtrd 5169 |
. . . . . . 7
⊢
(((((𝑃 ∈
ℂ ∧ 𝑅 ∈
ℝ*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅) |
| 152 | 86, 151 | pm2.61dane 3029 |
. . . . . 6
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅) |
| 153 | 56, 60, 61, 63, 152 | lelttrd 11419 |
. . . . 5
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅) |
| 154 | 55 | adantr 480 |
. . . . . . 7
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 = +∞) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) ∈ ℝ) |
| 155 | 154 | ltpnfd 13163 |
. . . . . 6
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 = +∞) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) < +∞) |
| 156 | | simpr 484 |
. . . . . 6
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 = +∞) → 𝑅 = +∞) |
| 157 | 155, 156 | breqtrrd 5171 |
. . . . 5
⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 = +∞) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅) |
| 158 | | 0xr 11308 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ* |
| 159 | 158 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 ∈
ℝ*) |
| 160 | 98 | rexrd 11311 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑃 − 𝐴)) ∈
ℝ*) |
| 161 | 50 | absge0d 15483 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 ≤
(abs‘(𝑃 − 𝐴))) |
| 162 | 159, 160,
11, 161, 96 | xrlelttrd 13202 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 < 𝑅) |
| 163 | 159, 11, 162 | xrltled 13192 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 ≤ 𝑅) |
| 164 | | ge0nemnf 13215 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ*
∧ 0 ≤ 𝑅) →
𝑅 ≠
-∞) |
| 165 | 11, 163, 164 | syl2anc 584 |
. . . . . . 7
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑅 ≠ -∞) |
| 166 | 11, 165 | jca 511 |
. . . . . 6
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑅 ∈ ℝ* ∧ 𝑅 ≠
-∞)) |
| 167 | | xrnemnf 13159 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ*
∧ 𝑅 ≠ -∞)
↔ (𝑅 ∈ ℝ
∨ 𝑅 =
+∞)) |
| 168 | 166, 167 | sylib 218 |
. . . . 5
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑅 ∈ ℝ ∨ 𝑅 = +∞)) |
| 169 | 153, 157,
168 | mpjaodan 961 |
. . . 4
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅) |
| 170 | 49, 169 | eqbrtrd 5165 |
. . 3
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) < 𝑅) |
| 171 | | elbl 24398 |
. . . 4
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*) → (((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ (𝑃(ball‘(abs ∘ − ))𝑅) ↔ (((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ ℂ ∧ (𝑃(abs ∘ − )((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) < 𝑅))) |
| 172 | 9, 10, 11, 171 | mp3an2i 1468 |
. . 3
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ (𝑃(ball‘(abs ∘ − ))𝑅) ↔ (((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ ℂ ∧ (𝑃(abs ∘ − )((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) < 𝑅))) |
| 173 | 28, 170, 172 | mpbir2and 713 |
. 2
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ (𝑃(ball‘(abs ∘ − ))𝑅)) |
| 174 | 173, 7 | eleqtrrdi 2852 |
1
⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ 𝑆) |