blcvx - Metamath Proof Explorer

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

Theorem blcvx 22409

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	⊢ 𝑆 = (𝑃(ball‘(abs ∘ − ))𝑅)

**Assertion**
Ref	Expression
blcvx	⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ 𝑆)

**Proof of Theorem blcvx**
Step	Hyp	Ref	Expression
1		simpr3 1062	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ (0[,]1))
2		0re 9919	. . . . . . . . 9 ⊢ 0 ∈ ℝ
3		1re 9918	. . . . . . . . 9 ⊢ 1 ∈ ℝ
4	2, 3	elicc2i 12110	. . . . . . . 8 ⊢ (𝑇 ∈ (0[,]1) ↔ (𝑇 ∈ ℝ ∧ 0 ≤ 𝑇 ∧ 𝑇 ≤ 1))
5	1, 4	sylib 207	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 ∈ ℝ ∧ 0 ≤ 𝑇 ∧ 𝑇 ≤ 1))
6	5	simp1d 1066	. . . . . 6 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ ℝ)
7	6	recnd 9947	. . . . 5 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ ℂ)
8		simpr1 1060	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝐴 ∈ 𝑆)
9		blcvx.s	. . . . . . . 8 ⊢ 𝑆 = (𝑃(ball‘(abs ∘ − ))𝑅)
10	8, 9	syl6eleq 2698	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝐴 ∈ (𝑃(ball‘(abs ∘ − ))𝑅))
11		cnxmet 22386	. . . . . . . . 9 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
12	11	a1i 11	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs ∘ − ) ∈ (∞Met‘ℂ))
13		simpll 786	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑃 ∈ ℂ)
14		simplr 788	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑅 ∈ ℝ^)
15		elbl 22003	. . . . . . . 8 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) → (𝐴 ∈ (𝑃(ball‘(abs ∘ − ))𝑅) ↔ (𝐴 ∈ ℂ ∧ (𝑃(abs ∘ − )𝐴) < 𝑅)))
16	12, 13, 14, 15	syl3anc 1318	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝐴 ∈ (𝑃(ball‘(abs ∘ − ))𝑅) ↔ (𝐴 ∈ ℂ ∧ (𝑃(abs ∘ − )𝐴) < 𝑅)))
17	10, 16	mpbid 221	. . . . . 6 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝐴 ∈ ℂ ∧ (𝑃(abs ∘ − )𝐴) < 𝑅))
18	17	simpld 474	. . . . 5 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝐴 ∈ ℂ)
19	7, 18	mulcld 9939	. . . 4 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · 𝐴) ∈ ℂ)
20		resubcl 10224	. . . . . . 7 ⊢ ((1 ∈ ℝ ∧ 𝑇 ∈ ℝ) → (1 − 𝑇) ∈ ℝ)
21	3, 6, 20	sylancr 694	. . . . . 6 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℝ)
22	21	recnd 9947	. . . . 5 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℂ)
23		simpr2 1061	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝐵 ∈ 𝑆)
24	23, 9	syl6eleq 2698	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝐵 ∈ (𝑃(ball‘(abs ∘ − ))𝑅))
25		elbl 22003	. . . . . . . 8 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) → (𝐵 ∈ (𝑃(ball‘(abs ∘ − ))𝑅) ↔ (𝐵 ∈ ℂ ∧ (𝑃(abs ∘ − )𝐵) < 𝑅)))
26	12, 13, 14, 25	syl3anc 1318	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝐵 ∈ (𝑃(ball‘(abs ∘ − ))𝑅) ↔ (𝐵 ∈ ℂ ∧ (𝑃(abs ∘ − )𝐵) < 𝑅)))
27	24, 26	mpbid 221	. . . . . 6 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝐵 ∈ ℂ ∧ (𝑃(abs ∘ − )𝐵) < 𝑅))
28	27	simpld 474	. . . . 5 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝐵 ∈ ℂ)
29	22, 28	mulcld 9939	. . . 4 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · 𝐵) ∈ ℂ)
30	19, 29	addcld 9938	. . 3 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ ℂ)
31		eqid 2610	. . . . . . 7 ⊢ (abs ∘ − ) = (abs ∘ − )
32	31	cnmetdval 22384	. . . . . 6 ⊢ ((𝑃 ∈ ℂ ∧ ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ ℂ) → (𝑃(abs ∘ − )((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) = (abs‘(𝑃 − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)))))
33	13, 30, 32	syl2anc 691	. . . . 5 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) = (abs‘(𝑃 − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)))))
34	7, 13, 18	subdid 10365	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · (𝑃 − 𝐴)) = ((𝑇 · 𝑃) − (𝑇 · 𝐴)))
35	22, 13, 28	subdid 10365	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · (𝑃 − 𝐵)) = (((1 − 𝑇) · 𝑃) − ((1 − 𝑇) · 𝐵)))
36	34, 35	oveq12d 6567	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵))) = (((𝑇 · 𝑃) − (𝑇 · 𝐴)) + (((1 − 𝑇) · 𝑃) − ((1 − 𝑇) · 𝐵))))
37	7, 13	mulcld 9939	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · 𝑃) ∈ ℂ)
38	22, 13	mulcld 9939	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · 𝑃) ∈ ℂ)
39	37, 38, 19, 29	addsub4d 10318	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (((𝑇 · 𝑃) + ((1 − 𝑇) · 𝑃)) − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) = (((𝑇 · 𝑃) − (𝑇 · 𝐴)) + (((1 − 𝑇) · 𝑃) − ((1 − 𝑇) · 𝐵))))
40		ax-1cn 9873	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
41		pncan3 10168	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑇 + (1 − 𝑇)) = 1)
42	7, 40, 41	sylancl 693	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 + (1 − 𝑇)) = 1)
43	42	oveq1d 6564	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · 𝑃) = (1 · 𝑃))
44	7, 22, 13	adddird 9944	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · 𝑃) = ((𝑇 · 𝑃) + ((1 − 𝑇) · 𝑃)))
45		mulid2 9917	. . . . . . . . . 10 ⊢ (𝑃 ∈ ℂ → (1 · 𝑃) = 𝑃)
46	45	ad2antrr 758	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (1 · 𝑃) = 𝑃)
47	43, 44, 46	3eqtr3d 2652	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝑃) + ((1 − 𝑇) · 𝑃)) = 𝑃)
48	47	oveq1d 6564	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (((𝑇 · 𝑃) + ((1 − 𝑇) · 𝑃)) − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) = (𝑃 − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))))
49	36, 39, 48	3eqtr2d 2650	. . . . . 6 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵))) = (𝑃 − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))))
50	49	fveq2d 6107	. . . . 5 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) = (abs‘(𝑃 − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)))))
51	33, 50	eqtr4d 2647	. . . 4 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) = (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))))
52	13, 18	subcld 10271	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃 − 𝐴) ∈ ℂ)
53	7, 52	mulcld 9939	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · (𝑃 − 𝐴)) ∈ ℂ)
54	13, 28	subcld 10271	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃 − 𝐵) ∈ ℂ)
55	22, 54	mulcld 9939	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · (𝑃 − 𝐵)) ∈ ℂ)
56	53, 55	addcld 9938	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵))) ∈ ℂ)
57	56	abscld 14023	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) ∈ ℝ)
58	57	adantr 480	. . . . . 6 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) ∈ ℝ)
59	53	abscld 14023	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑇 · (𝑃 − 𝐴))) ∈ ℝ)
60	55	abscld 14023	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) ∈ ℝ)
61	59, 60	readdcld 9948	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) ∈ ℝ)
62	61	adantr 480	. . . . . 6 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) ∈ ℝ)
63		simpr 476	. . . . . 6 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → 𝑅 ∈ ℝ)
64	53, 55	abstrid 14043	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) ≤ ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))))
65	64	adantr 480	. . . . . 6 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) ≤ ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))))
66		oveq1 6556	. . . . . . . . . . . 12 ⊢ (𝑇 = 0 → (𝑇 · (𝑃 − 𝐴)) = (0 · (𝑃 − 𝐴)))
67	52	mul02d 10113	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (0 · (𝑃 − 𝐴)) = 0)
68	66, 67	sylan9eqr 2666	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → (𝑇 · (𝑃 − 𝐴)) = 0)
69	68	abs00bd 13879	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → (abs‘(𝑇 · (𝑃 − 𝐴))) = 0)
70		oveq2 6557	. . . . . . . . . . . . . 14 ⊢ (𝑇 = 0 → (1 − 𝑇) = (1 − 0))
71		1m0e1 11008	. . . . . . . . . . . . . 14 ⊢ (1 − 0) = 1
72	70, 71	syl6eq 2660	. . . . . . . . . . . . 13 ⊢ (𝑇 = 0 → (1 − 𝑇) = 1)
73	72	oveq1d 6564	. . . . . . . . . . . 12 ⊢ (𝑇 = 0 → ((1 − 𝑇) · (𝑃 − 𝐵)) = (1 · (𝑃 − 𝐵)))
74	54	mulid2d 9937	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (1 · (𝑃 − 𝐵)) = (𝑃 − 𝐵))
75	73, 74	sylan9eqr 2666	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → ((1 − 𝑇) · (𝑃 − 𝐵)) = (𝑃 − 𝐵))
76	75	fveq2d 6107	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) = (abs‘(𝑃 − 𝐵)))
77	69, 76	oveq12d 6567	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) = (0 + (abs‘(𝑃 − 𝐵))))
78	54	abscld 14023	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑃 − 𝐵)) ∈ ℝ)
79	78	recnd 9947	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑃 − 𝐵)) ∈ ℂ)
80	79	addid2d 10116	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (0 + (abs‘(𝑃 − 𝐵))) = (abs‘(𝑃 − 𝐵)))
81	31	cnmetdval 22384	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑃(abs ∘ − )𝐵) = (abs‘(𝑃 − 𝐵)))
82	13, 28, 81	syl2anc 691	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )𝐵) = (abs‘(𝑃 − 𝐵)))
83	80, 82	eqtr4d 2647	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (0 + (abs‘(𝑃 − 𝐵))) = (𝑃(abs ∘ − )𝐵))
84	27	simprd 478	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )𝐵) < 𝑅)
85	83, 84	eqbrtrd 4605	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (0 + (abs‘(𝑃 − 𝐵))) < 𝑅)
86	85	adantr 480	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → (0 + (abs‘(𝑃 − 𝐵))) < 𝑅)
87	77, 86	eqbrtrd 4605	. . . . . . . 8 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅)
88	87	adantlr 747	. . . . . . 7 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 = 0) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅)
89	7, 52	absmuld 14041	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑇 · (𝑃 − 𝐴))) = ((abs‘𝑇) · (abs‘(𝑃 − 𝐴))))
90	5	simp2d 1067	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 ≤ 𝑇)
91	6, 90	absidd 14009	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘𝑇) = 𝑇)
92	91	oveq1d 6564	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((abs‘𝑇) · (abs‘(𝑃 − 𝐴))) = (𝑇 · (abs‘(𝑃 − 𝐴))))
93	89, 92	eqtrd 2644	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑇 · (𝑃 − 𝐴))) = (𝑇 · (abs‘(𝑃 − 𝐴))))
94	93	ad2antrr 758	. . . . . . . . . 10 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (abs‘(𝑇 · (𝑃 − 𝐴))) = (𝑇 · (abs‘(𝑃 − 𝐴))))
95	31	cnmetdval 22384	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝑃(abs ∘ − )𝐴) = (abs‘(𝑃 − 𝐴)))
96	13, 18, 95	syl2anc 691	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )𝐴) = (abs‘(𝑃 − 𝐴)))
97	17	simprd 478	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )𝐴) < 𝑅)
98	96, 97	eqbrtrrd 4607	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑃 − 𝐴)) < 𝑅)
99	98	ad2antrr 758	. . . . . . . . . . 11 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (abs‘(𝑃 − 𝐴)) < 𝑅)
100	52	abscld 14023	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑃 − 𝐴)) ∈ ℝ)
101	100	ad2antrr 758	. . . . . . . . . . . 12 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (abs‘(𝑃 − 𝐴)) ∈ ℝ)
102		simplr 788	. . . . . . . . . . . 12 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → 𝑅 ∈ ℝ)
103	6	ad2antrr 758	. . . . . . . . . . . 12 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → 𝑇 ∈ ℝ)
104	2	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 ∈ ℝ)
105	104, 6, 90	leltned 10069	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (0 < 𝑇 ↔ 𝑇 ≠ 0))
106	105	biimpar 501	. . . . . . . . . . . . 13 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ≠ 0) → 0 < 𝑇)
107	106	adantlr 747	. . . . . . . . . . . 12 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → 0 < 𝑇)
108		ltmul2 10753	. . . . . . . . . . . 12 ⊢ (((abs‘(𝑃 − 𝐴)) ∈ ℝ ∧ 𝑅 ∈ ℝ ∧ (𝑇 ∈ ℝ ∧ 0 < 𝑇)) → ((abs‘(𝑃 − 𝐴)) < 𝑅 ↔ (𝑇 · (abs‘(𝑃 − 𝐴))) < (𝑇 · 𝑅)))
109	101, 102, 103, 107, 108	syl112anc 1322	. . . . . . . . . . 11 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → ((abs‘(𝑃 − 𝐴)) < 𝑅 ↔ (𝑇 · (abs‘(𝑃 − 𝐴))) < (𝑇 · 𝑅)))
110	99, 109	mpbid 221	. . . . . . . . . 10 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (𝑇 · (abs‘(𝑃 − 𝐴))) < (𝑇 · 𝑅))
111	94, 110	eqbrtrd 4605	. . . . . . . . 9 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (abs‘(𝑇 · (𝑃 − 𝐴))) < (𝑇 · 𝑅))
112	22, 54	absmuld 14041	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) = ((abs‘(1 − 𝑇)) · (abs‘(𝑃 − 𝐵))))
113	3	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 1 ∈ ℝ)
114	5	simp3d 1068	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ≤ 1)
115	6, 113, 114	abssubge0d 14018	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(1 − 𝑇)) = (1 − 𝑇))
116	115	oveq1d 6564	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((abs‘(1 − 𝑇)) · (abs‘(𝑃 − 𝐵))) = ((1 − 𝑇) · (abs‘(𝑃 − 𝐵))))
117	112, 116	eqtrd 2644	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) = ((1 − 𝑇) · (abs‘(𝑃 − 𝐵))))
118	117	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) = ((1 − 𝑇) · (abs‘(𝑃 − 𝐵))))
119	78	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘(𝑃 − 𝐵)) ∈ ℝ)
120		subge0 10420	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℝ ∧ 𝑇 ∈ ℝ) → (0 ≤ (1 − 𝑇) ↔ 𝑇 ≤ 1))
121	3, 6, 120	sylancr 694	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (0 ≤ (1 − 𝑇) ↔ 𝑇 ≤ 1))
122	114, 121	mpbird 246	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 ≤ (1 − 𝑇))
123	21, 122	jca 553	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) ∈ ℝ ∧ 0 ≤ (1 − 𝑇)))
124	123	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((1 − 𝑇) ∈ ℝ ∧ 0 ≤ (1 − 𝑇)))
125	82, 84	eqbrtrrd 4607	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑃 − 𝐵)) < 𝑅)
126	125	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘(𝑃 − 𝐵)) < 𝑅)
127		ltle 10005	. . . . . . . . . . . . . 14 ⊢ (((abs‘(𝑃 − 𝐵)) ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((abs‘(𝑃 − 𝐵)) < 𝑅 → (abs‘(𝑃 − 𝐵)) ≤ 𝑅))
128	78, 127	sylan 487	. . . . . . . . . . . . 13 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((abs‘(𝑃 − 𝐵)) < 𝑅 → (abs‘(𝑃 − 𝐵)) ≤ 𝑅))
129	126, 128	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘(𝑃 − 𝐵)) ≤ 𝑅)
130		lemul2a 10757	. . . . . . . . . . . 12 ⊢ ((((abs‘(𝑃 − 𝐵)) ∈ ℝ ∧ 𝑅 ∈ ℝ ∧ ((1 − 𝑇) ∈ ℝ ∧ 0 ≤ (1 − 𝑇))) ∧ (abs‘(𝑃 − 𝐵)) ≤ 𝑅) → ((1 − 𝑇) · (abs‘(𝑃 − 𝐵))) ≤ ((1 − 𝑇) · 𝑅))
131	119, 63, 124, 129, 130	syl31anc 1321	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((1 − 𝑇) · (abs‘(𝑃 − 𝐵))) ≤ ((1 − 𝑇) · 𝑅))
132	118, 131	eqbrtrd 4605	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) ≤ ((1 − 𝑇) · 𝑅))
133	132	adantr 480	. . . . . . . . 9 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) ≤ ((1 − 𝑇) · 𝑅))
134	59	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘(𝑇 · (𝑃 − 𝐴))) ∈ ℝ)
135	60	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) ∈ ℝ)
136		remulcl 9900	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑇 · 𝑅) ∈ ℝ)
137	6, 136	sylan 487	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (𝑇 · 𝑅) ∈ ℝ)
138		remulcl 9900	. . . . . . . . . . . 12 ⊢ (((1 − 𝑇) ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((1 − 𝑇) · 𝑅) ∈ ℝ)
139	21, 138	sylan 487	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((1 − 𝑇) · 𝑅) ∈ ℝ)
140		ltleadd 10390	. . . . . . . . . . 11 ⊢ ((((abs‘(𝑇 · (𝑃 − 𝐴))) ∈ ℝ ∧ (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) ∈ ℝ) ∧ ((𝑇 · 𝑅) ∈ ℝ ∧ ((1 − 𝑇) · 𝑅) ∈ ℝ)) → (((abs‘(𝑇 · (𝑃 − 𝐴))) < (𝑇 · 𝑅) ∧ (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) ≤ ((1 − 𝑇) · 𝑅)) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅))))
141	134, 135, 137, 139, 140	syl22anc 1319	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (((abs‘(𝑇 · (𝑃 − 𝐴))) < (𝑇 · 𝑅) ∧ (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) ≤ ((1 − 𝑇) · 𝑅)) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅))))
142	141	adantr 480	. . . . . . . . 9 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (((abs‘(𝑇 · (𝑃 − 𝐴))) < (𝑇 · 𝑅) ∧ (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) ≤ ((1 − 𝑇) · 𝑅)) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅))))
143	111, 133, 142	mp2and 711	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅)))
144	42	oveq1d 6564	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · 𝑅) = (1 · 𝑅))
145	144	adantr 480	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((𝑇 + (1 − 𝑇)) · 𝑅) = (1 · 𝑅))
146	7	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → 𝑇 ∈ ℂ)
147	22	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (1 − 𝑇) ∈ ℂ)
148	63	recnd 9947	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → 𝑅 ∈ ℂ)
149	146, 147, 148	adddird 9944	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((𝑇 + (1 − 𝑇)) · 𝑅) = ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅)))
150	148	mulid2d 9937	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (1 · 𝑅) = 𝑅)
151	145, 149, 150	3eqtr3d 2652	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅)) = 𝑅)
152	151	adantr 480	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅)) = 𝑅)
153	143, 152	breqtrd 4609	. . . . . . 7 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅)
154	88, 153	pm2.61dane 2869	. . . . . 6 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅)
155	58, 62, 63, 65, 154	lelttrd 10074	. . . . 5 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅)
156	57	adantr 480	. . . . . . 7 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 = +∞) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) ∈ ℝ)
157		ltpnf 11830	. . . . . . 7 ⊢ ((abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) ∈ ℝ → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) < +∞)
158	156, 157	syl 17	. . . . . 6 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 = +∞) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) < +∞)
159		simpr 476	. . . . . 6 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 = +∞) → 𝑅 = +∞)
160	158, 159	breqtrrd 4611	. . . . 5 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 = +∞) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅)
161		0xr 9965	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ^*
162	161	a1i 11	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 ∈ ℝ^)
163	100	rexrd 9968	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑃 − 𝐴)) ∈ ℝ^)
164	52	absge0d 14031	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 ≤ (abs‘(𝑃 − 𝐴)))
165	162, 163, 14, 164, 98	xrlelttrd 11867	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 < 𝑅)
166		xrltle 11858	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ^* ∧ 𝑅 ∈ ℝ^*) → (0 < 𝑅 → 0 ≤ 𝑅))
167	161, 14, 166	sylancr 694	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (0 < 𝑅 → 0 ≤ 𝑅))
168	165, 167	mpd 15	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 ≤ 𝑅)
169		ge0nemnf 11878	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ^* ∧ 0 ≤ 𝑅) → 𝑅 ≠ -∞)
170	14, 168, 169	syl2anc 691	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑅 ≠ -∞)
171	14, 170	jca 553	. . . . . 6 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑅 ∈ ℝ^ ∧ 𝑅 ≠ -∞))
172		xrnemnf 11827	. . . . . 6 ⊢ ((𝑅 ∈ ℝ^* ∧ 𝑅 ≠ -∞) ↔ (𝑅 ∈ ℝ ∨ 𝑅 = +∞))
173	171, 172	sylib 207	. . . . 5 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑅 ∈ ℝ ∨ 𝑅 = +∞))
174	155, 160, 173	mpjaodan 823	. . . 4 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅)
175	51, 174	eqbrtrd 4605	. . 3 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) < 𝑅)
176		elbl 22003	. . . 4 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) → (((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ (𝑃(ball‘(abs ∘ − ))𝑅) ↔ (((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ ℂ ∧ (𝑃(abs ∘ − )((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) < 𝑅)))
177	12, 13, 14, 176	syl3anc 1318	. . 3 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ (𝑃(ball‘(abs ∘ − ))𝑅) ↔ (((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ ℂ ∧ (𝑃(abs ∘ − )((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) < 𝑅)))
178	30, 175, 177	mpbir2and 959	. 2 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ (𝑃(ball‘(abs ∘ − ))𝑅))
179	178, 9	syl6eleqr 2699	1 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ 𝑆)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 195 ∨ wo 382 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ≠ wne 2780 class class class wbr 4583 ∘ ccom 5042 ‘cfv 5804 (class class class)co 6549 ℂcc 9813 ℝcr 9814 0cc0 9815 1c1 9816 + caddc 9818 · cmul 9820 +∞cpnf 9950 -∞cmnf 9951 ℝ^*cxr 9952 < clt 9953 ≤ cle 9954 − cmin 10145 [,]cicc 12049 abscabs 13822 ∞Metcxmt 19552 ballcbl 19554

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892 ax-pre-sup 9893

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-er 7629 df-map 7746 df-en 7842 df-dom 7843 df-sdom 7844 df-sup 8231 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-2 10956 df-3 10957 df-n0 11170 df-z 11255 df-uz 11564 df-rp 11709 df-xadd 11823 df-icc 12053 df-seq 12664 df-exp 12723 df-cj 13687 df-re 13688 df-im 13689 df-sqrt 13823 df-abs 13824 df-psmet 19559 df-xmet 19560 df-met 19561 df-bl 19562

This theorem is referenced by: dvlipcn 23561 blscon 30480

W3C validator