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 24006

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 1196	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ (0[,]1))
2		elicc01 13244	. . . . . . . 8 ⊢ (𝑇 ∈ (0[,]1) ↔ (𝑇 ∈ ℝ ∧ 0 ≤ 𝑇 ∧ 𝑇 ≤ 1))
3	1, 2	sylib 217	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 ∈ ℝ ∧ 0 ≤ 𝑇 ∧ 𝑇 ≤ 1))
4	3	simp1d 1142	. . . . . 6 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ ℝ)
5	4	recnd 11049	. . . . 5 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ ℂ)
6		simpr1 1194	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝐴 ∈ 𝑆)
7		blcvx.s	. . . . . . . 8 ⊢ 𝑆 = (𝑃(ball‘(abs ∘ − ))𝑅)
8	6, 7	eleqtrdi 2847	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝐴 ∈ (𝑃(ball‘(abs ∘ − ))𝑅))
9		cnxmet 23981	. . . . . . . 8 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
10		simpll 765	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑃 ∈ ℂ)
11		simplr 767	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑅 ∈ ℝ^)
12		elbl 23586	. . . . . . . 8 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) → (𝐴 ∈ (𝑃(ball‘(abs ∘ − ))𝑅) ↔ (𝐴 ∈ ℂ ∧ (𝑃(abs ∘ − )𝐴) < 𝑅)))
13	9, 10, 11, 12	mp3an2i 1466	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝐴 ∈ (𝑃(ball‘(abs ∘ − ))𝑅) ↔ (𝐴 ∈ ℂ ∧ (𝑃(abs ∘ − )𝐴) < 𝑅)))
14	8, 13	mpbid 231	. . . . . 6 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝐴 ∈ ℂ ∧ (𝑃(abs ∘ − )𝐴) < 𝑅))
15	14	simpld 496	. . . . 5 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝐴 ∈ ℂ)
16	5, 15	mulcld 11041	. . . 4 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · 𝐴) ∈ ℂ)
17		1re 11021	. . . . . . 7 ⊢ 1 ∈ ℝ
18		resubcl 11331	. . . . . . 7 ⊢ ((1 ∈ ℝ ∧ 𝑇 ∈ ℝ) → (1 − 𝑇) ∈ ℝ)
19	17, 4, 18	sylancr 588	. . . . . 6 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℝ)
20	19	recnd 11049	. . . . 5 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℂ)
21		simpr2 1195	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝐵 ∈ 𝑆)
22	21, 7	eleqtrdi 2847	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝐵 ∈ (𝑃(ball‘(abs ∘ − ))𝑅))
23		elbl 23586	. . . . . . . 8 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) → (𝐵 ∈ (𝑃(ball‘(abs ∘ − ))𝑅) ↔ (𝐵 ∈ ℂ ∧ (𝑃(abs ∘ − )𝐵) < 𝑅)))
24	9, 10, 11, 23	mp3an2i 1466	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝐵 ∈ (𝑃(ball‘(abs ∘ − ))𝑅) ↔ (𝐵 ∈ ℂ ∧ (𝑃(abs ∘ − )𝐵) < 𝑅)))
25	22, 24	mpbid 231	. . . . . 6 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝐵 ∈ ℂ ∧ (𝑃(abs ∘ − )𝐵) < 𝑅))
26	25	simpld 496	. . . . 5 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝐵 ∈ ℂ)
27	20, 26	mulcld 11041	. . . 4 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · 𝐵) ∈ ℂ)
28	16, 27	addcld 11040	. . 3 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ ℂ)
29		eqid 2736	. . . . . . 7 ⊢ (abs ∘ − ) = (abs ∘ − )
30	29	cnmetdval 23979	. . . . . 6 ⊢ ((𝑃 ∈ ℂ ∧ ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ ℂ) → (𝑃(abs ∘ − )((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) = (abs‘(𝑃 − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)))))
31	10, 28, 30	syl2anc 585	. . . . 5 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) = (abs‘(𝑃 − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)))))
32	5, 10, 15	subdid 11477	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · (𝑃 − 𝐴)) = ((𝑇 · 𝑃) − (𝑇 · 𝐴)))
33	20, 10, 26	subdid 11477	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · (𝑃 − 𝐵)) = (((1 − 𝑇) · 𝑃) − ((1 − 𝑇) · 𝐵)))
34	32, 33	oveq12d 7325	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵))) = (((𝑇 · 𝑃) − (𝑇 · 𝐴)) + (((1 − 𝑇) · 𝑃) − ((1 − 𝑇) · 𝐵))))
35	5, 10	mulcld 11041	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · 𝑃) ∈ ℂ)
36	20, 10	mulcld 11041	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · 𝑃) ∈ ℂ)
37	35, 36, 16, 27	addsub4d 11425	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (((𝑇 · 𝑃) + ((1 − 𝑇) · 𝑃)) − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) = (((𝑇 · 𝑃) − (𝑇 · 𝐴)) + (((1 − 𝑇) · 𝑃) − ((1 − 𝑇) · 𝐵))))
38		ax-1cn 10975	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
39		pncan3 11275	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑇 + (1 − 𝑇)) = 1)
40	5, 38, 39	sylancl 587	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 + (1 − 𝑇)) = 1)
41	40	oveq1d 7322	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · 𝑃) = (1 · 𝑃))
42	5, 20, 10	adddird 11046	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · 𝑃) = ((𝑇 · 𝑃) + ((1 − 𝑇) · 𝑃)))
43		mulid2 11020	. . . . . . . . . 10 ⊢ (𝑃 ∈ ℂ → (1 · 𝑃) = 𝑃)
44	43	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (1 · 𝑃) = 𝑃)
45	41, 42, 44	3eqtr3d 2784	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝑃) + ((1 − 𝑇) · 𝑃)) = 𝑃)
46	45	oveq1d 7322	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (((𝑇 · 𝑃) + ((1 − 𝑇) · 𝑃)) − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) = (𝑃 − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))))
47	34, 37, 46	3eqtr2d 2782	. . . . . 6 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵))) = (𝑃 − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))))
48	47	fveq2d 6808	. . . . 5 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) = (abs‘(𝑃 − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)))))
49	31, 48	eqtr4d 2779	. . . 4 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) = (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))))
50	10, 15	subcld 11378	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃 − 𝐴) ∈ ℂ)
51	5, 50	mulcld 11041	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · (𝑃 − 𝐴)) ∈ ℂ)
52	10, 26	subcld 11378	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃 − 𝐵) ∈ ℂ)
53	20, 52	mulcld 11041	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · (𝑃 − 𝐵)) ∈ ℂ)
54	51, 53	addcld 11040	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵))) ∈ ℂ)
55	54	abscld 15193	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) ∈ ℝ)
56	55	adantr 482	. . . . . 6 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) ∈ ℝ)
57	51	abscld 15193	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑇 · (𝑃 − 𝐴))) ∈ ℝ)
58	53	abscld 15193	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) ∈ ℝ)
59	57, 58	readdcld 11050	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) ∈ ℝ)
60	59	adantr 482	. . . . . 6 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) ∈ ℝ)
61		simpr 486	. . . . . 6 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → 𝑅 ∈ ℝ)
62	51, 53	abstrid 15213	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) ≤ ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))))
63	62	adantr 482	. . . . . 6 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) ≤ ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))))
64		oveq1 7314	. . . . . . . . . . . 12 ⊢ (𝑇 = 0 → (𝑇 · (𝑃 − 𝐴)) = (0 · (𝑃 − 𝐴)))
65	50	mul02d 11219	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (0 · (𝑃 − 𝐴)) = 0)
66	64, 65	sylan9eqr 2798	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → (𝑇 · (𝑃 − 𝐴)) = 0)
67	66	abs00bd 15048	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → (abs‘(𝑇 · (𝑃 − 𝐴))) = 0)
68		oveq2 7315	. . . . . . . . . . . . . 14 ⊢ (𝑇 = 0 → (1 − 𝑇) = (1 − 0))
69		1m0e1 12140	. . . . . . . . . . . . . 14 ⊢ (1 − 0) = 1
70	68, 69	eqtrdi 2792	. . . . . . . . . . . . 13 ⊢ (𝑇 = 0 → (1 − 𝑇) = 1)
71	70	oveq1d 7322	. . . . . . . . . . . 12 ⊢ (𝑇 = 0 → ((1 − 𝑇) · (𝑃 − 𝐵)) = (1 · (𝑃 − 𝐵)))
72	52	mulid2d 11039	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (1 · (𝑃 − 𝐵)) = (𝑃 − 𝐵))
73	71, 72	sylan9eqr 2798	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → ((1 − 𝑇) · (𝑃 − 𝐵)) = (𝑃 − 𝐵))
74	73	fveq2d 6808	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) = (abs‘(𝑃 − 𝐵)))
75	67, 74	oveq12d 7325	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) = (0 + (abs‘(𝑃 − 𝐵))))
76	52	abscld 15193	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑃 − 𝐵)) ∈ ℝ)
77	76	recnd 11049	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑃 − 𝐵)) ∈ ℂ)
78	77	addid2d 11222	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (0 + (abs‘(𝑃 − 𝐵))) = (abs‘(𝑃 − 𝐵)))
79	29	cnmetdval 23979	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑃(abs ∘ − )𝐵) = (abs‘(𝑃 − 𝐵)))
80	10, 26, 79	syl2anc 585	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )𝐵) = (abs‘(𝑃 − 𝐵)))
81	78, 80	eqtr4d 2779	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (0 + (abs‘(𝑃 − 𝐵))) = (𝑃(abs ∘ − )𝐵))
82	25	simprd 497	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )𝐵) < 𝑅)
83	81, 82	eqbrtrd 5103	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (0 + (abs‘(𝑃 − 𝐵))) < 𝑅)
84	83	adantr 482	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → (0 + (abs‘(𝑃 − 𝐵))) < 𝑅)
85	75, 84	eqbrtrd 5103	. . . . . . . 8 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅)
86	85	adantlr 713	. . . . . . 7 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 = 0) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅)
87	5, 50	absmuld 15211	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑇 · (𝑃 − 𝐴))) = ((abs‘𝑇) · (abs‘(𝑃 − 𝐴))))
88	3	simp2d 1143	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 ≤ 𝑇)
89	4, 88	absidd 15179	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘𝑇) = 𝑇)
90	89	oveq1d 7322	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((abs‘𝑇) · (abs‘(𝑃 − 𝐴))) = (𝑇 · (abs‘(𝑃 − 𝐴))))
91	87, 90	eqtrd 2776	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑇 · (𝑃 − 𝐴))) = (𝑇 · (abs‘(𝑃 − 𝐴))))
92	91	ad2antrr 724	. . . . . . . . . 10 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (abs‘(𝑇 · (𝑃 − 𝐴))) = (𝑇 · (abs‘(𝑃 − 𝐴))))
93	29	cnmetdval 23979	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝑃(abs ∘ − )𝐴) = (abs‘(𝑃 − 𝐴)))
94	10, 15, 93	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )𝐴) = (abs‘(𝑃 − 𝐴)))
95	14	simprd 497	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )𝐴) < 𝑅)
96	94, 95	eqbrtrrd 5105	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑃 − 𝐴)) < 𝑅)
97	96	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (abs‘(𝑃 − 𝐴)) < 𝑅)
98	50	abscld 15193	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑃 − 𝐴)) ∈ ℝ)
99	98	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (abs‘(𝑃 − 𝐴)) ∈ ℝ)
100		simplr 767	. . . . . . . . . . . 12 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → 𝑅 ∈ ℝ)
101	4	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → 𝑇 ∈ ℝ)
102		0red 11024	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 ∈ ℝ)
103	102, 4, 88	leltned 11174	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (0 < 𝑇 ↔ 𝑇 ≠ 0))
104	103	biimpar 479	. . . . . . . . . . . . 13 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ≠ 0) → 0 < 𝑇)
105	104	adantlr 713	. . . . . . . . . . . 12 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → 0 < 𝑇)
106		ltmul2 11872	. . . . . . . . . . . 12 ⊢ (((abs‘(𝑃 − 𝐴)) ∈ ℝ ∧ 𝑅 ∈ ℝ ∧ (𝑇 ∈ ℝ ∧ 0 < 𝑇)) → ((abs‘(𝑃 − 𝐴)) < 𝑅 ↔ (𝑇 · (abs‘(𝑃 − 𝐴))) < (𝑇 · 𝑅)))
107	99, 100, 101, 105, 106	syl112anc 1374	. . . . . . . . . . 11 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → ((abs‘(𝑃 − 𝐴)) < 𝑅 ↔ (𝑇 · (abs‘(𝑃 − 𝐴))) < (𝑇 · 𝑅)))
108	97, 107	mpbid 231	. . . . . . . . . 10 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (𝑇 · (abs‘(𝑃 − 𝐴))) < (𝑇 · 𝑅))
109	92, 108	eqbrtrd 5103	. . . . . . . . 9 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (abs‘(𝑇 · (𝑃 − 𝐴))) < (𝑇 · 𝑅))
110	20, 52	absmuld 15211	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) = ((abs‘(1 − 𝑇)) · (abs‘(𝑃 − 𝐵))))
111	17	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 1 ∈ ℝ)
112	3	simp3d 1144	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ≤ 1)
113	4, 111, 112	abssubge0d 15188	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(1 − 𝑇)) = (1 − 𝑇))
114	113	oveq1d 7322	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((abs‘(1 − 𝑇)) · (abs‘(𝑃 − 𝐵))) = ((1 − 𝑇) · (abs‘(𝑃 − 𝐵))))
115	110, 114	eqtrd 2776	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) = ((1 − 𝑇) · (abs‘(𝑃 − 𝐵))))
116	115	adantr 482	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) = ((1 − 𝑇) · (abs‘(𝑃 − 𝐵))))
117	76	adantr 482	. . . . . . . . . . . 12 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘(𝑃 − 𝐵)) ∈ ℝ)
118		subge0 11534	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℝ ∧ 𝑇 ∈ ℝ) → (0 ≤ (1 − 𝑇) ↔ 𝑇 ≤ 1))
119	17, 4, 118	sylancr 588	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (0 ≤ (1 − 𝑇) ↔ 𝑇 ≤ 1))
120	112, 119	mpbird 257	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 ≤ (1 − 𝑇))
121	19, 120	jca 513	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) ∈ ℝ ∧ 0 ≤ (1 − 𝑇)))
122	121	adantr 482	. . . . . . . . . . . 12 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((1 − 𝑇) ∈ ℝ ∧ 0 ≤ (1 − 𝑇)))
123	80, 82	eqbrtrrd 5105	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑃 − 𝐵)) < 𝑅)
124	123	adantr 482	. . . . . . . . . . . . 13 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘(𝑃 − 𝐵)) < 𝑅)
125		ltle 11109	. . . . . . . . . . . . . 14 ⊢ (((abs‘(𝑃 − 𝐵)) ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((abs‘(𝑃 − 𝐵)) < 𝑅 → (abs‘(𝑃 − 𝐵)) ≤ 𝑅))
126	76, 125	sylan 581	. . . . . . . . . . . . 13 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((abs‘(𝑃 − 𝐵)) < 𝑅 → (abs‘(𝑃 − 𝐵)) ≤ 𝑅))
127	124, 126	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘(𝑃 − 𝐵)) ≤ 𝑅)
128		lemul2a 11876	. . . . . . . . . . . 12 ⊢ ((((abs‘(𝑃 − 𝐵)) ∈ ℝ ∧ 𝑅 ∈ ℝ ∧ ((1 − 𝑇) ∈ ℝ ∧ 0 ≤ (1 − 𝑇))) ∧ (abs‘(𝑃 − 𝐵)) ≤ 𝑅) → ((1 − 𝑇) · (abs‘(𝑃 − 𝐵))) ≤ ((1 − 𝑇) · 𝑅))
129	117, 61, 122, 127, 128	syl31anc 1373	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((1 − 𝑇) · (abs‘(𝑃 − 𝐵))) ≤ ((1 − 𝑇) · 𝑅))
130	116, 129	eqbrtrd 5103	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) ≤ ((1 − 𝑇) · 𝑅))
131	130	adantr 482	. . . . . . . . 9 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) ≤ ((1 − 𝑇) · 𝑅))
132	57	adantr 482	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘(𝑇 · (𝑃 − 𝐴))) ∈ ℝ)
133	58	adantr 482	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) ∈ ℝ)
134		remulcl 11002	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑇 · 𝑅) ∈ ℝ)
135	4, 134	sylan 581	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (𝑇 · 𝑅) ∈ ℝ)
136		remulcl 11002	. . . . . . . . . . . 12 ⊢ (((1 − 𝑇) ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((1 − 𝑇) · 𝑅) ∈ ℝ)
137	19, 136	sylan 581	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((1 − 𝑇) · 𝑅) ∈ ℝ)
138		ltleadd 11504	. . . . . . . . . . 11 ⊢ ((((abs‘(𝑇 · (𝑃 − 𝐴))) ∈ ℝ ∧ (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) ∈ ℝ) ∧ ((𝑇 · 𝑅) ∈ ℝ ∧ ((1 − 𝑇) · 𝑅) ∈ ℝ)) → (((abs‘(𝑇 · (𝑃 − 𝐴))) < (𝑇 · 𝑅) ∧ (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) ≤ ((1 − 𝑇) · 𝑅)) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅))))
139	132, 133, 135, 137, 138	syl22anc 837	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (((abs‘(𝑇 · (𝑃 − 𝐴))) < (𝑇 · 𝑅) ∧ (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) ≤ ((1 − 𝑇) · 𝑅)) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅))))
140	139	adantr 482	. . . . . . . . 9 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (((abs‘(𝑇 · (𝑃 − 𝐴))) < (𝑇 · 𝑅) ∧ (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) ≤ ((1 − 𝑇) · 𝑅)) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅))))
141	109, 131, 140	mp2and 697	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅)))
142	40	oveq1d 7322	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · 𝑅) = (1 · 𝑅))
143	142	adantr 482	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((𝑇 + (1 − 𝑇)) · 𝑅) = (1 · 𝑅))
144	5	adantr 482	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → 𝑇 ∈ ℂ)
145	20	adantr 482	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (1 − 𝑇) ∈ ℂ)
146	61	recnd 11049	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → 𝑅 ∈ ℂ)
147	144, 145, 146	adddird 11046	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((𝑇 + (1 − 𝑇)) · 𝑅) = ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅)))
148	146	mulid2d 11039	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (1 · 𝑅) = 𝑅)
149	143, 147, 148	3eqtr3d 2784	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅)) = 𝑅)
150	149	adantr 482	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅)) = 𝑅)
151	141, 150	breqtrd 5107	. . . . . . 7 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅)
152	86, 151	pm2.61dane 3030	. . . . . 6 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅)
153	56, 60, 61, 63, 152	lelttrd 11179	. . . . 5 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅)
154	55	adantr 482	. . . . . . 7 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 = +∞) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) ∈ ℝ)
155	154	ltpnfd 12903	. . . . . 6 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 = +∞) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) < +∞)
156		simpr 486	. . . . . 6 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 = +∞) → 𝑅 = +∞)
157	155, 156	breqtrrd 5109	. . . . 5 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 = +∞) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅)
158		0xr 11068	. . . . . . . . . 10 ⊢ 0 ∈ ℝ^*
159	158	a1i 11	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 ∈ ℝ^)
160	98	rexrd 11071	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑃 − 𝐴)) ∈ ℝ^)
161	50	absge0d 15201	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 ≤ (abs‘(𝑃 − 𝐴)))
162	159, 160, 11, 161, 96	xrlelttrd 12940	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 < 𝑅)
163	159, 11, 162	xrltled 12930	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 ≤ 𝑅)
164		ge0nemnf 12953	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ^* ∧ 0 ≤ 𝑅) → 𝑅 ≠ -∞)
165	11, 163, 164	syl2anc 585	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑅 ≠ -∞)
166	11, 165	jca 513	. . . . . 6 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑅 ∈ ℝ^ ∧ 𝑅 ≠ -∞))
167		xrnemnf 12899	. . . . . 6 ⊢ ((𝑅 ∈ ℝ^* ∧ 𝑅 ≠ -∞) ↔ (𝑅 ∈ ℝ ∨ 𝑅 = +∞))
168	166, 167	sylib 217	. . . . 5 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑅 ∈ ℝ ∨ 𝑅 = +∞))
169	153, 157, 168	mpjaodan 957	. . . 4 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅)
170	49, 169	eqbrtrd 5103	. . 3 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) < 𝑅)
171		elbl 23586	. . . 4 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) → (((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ (𝑃(ball‘(abs ∘ − ))𝑅) ↔ (((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ ℂ ∧ (𝑃(abs ∘ − )((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) < 𝑅)))
172	9, 10, 11, 171	mp3an2i 1466	. . 3 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ (𝑃(ball‘(abs ∘ − ))𝑅) ↔ (((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ ℂ ∧ (𝑃(abs ∘ − )((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) < 𝑅)))
173	28, 170, 172	mpbir2and 711	. 2 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ (𝑃(ball‘(abs ∘ − ))𝑅))
174	173, 7	eleqtrrdi 2848	1 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ 𝑆)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∨ wo 845 ∧ w3a 1087 = wceq 1539 ∈ wcel 2104 ≠ wne 2941 class class class wbr 5081 ∘ ccom 5604 ‘cfv 6458 (class class class)co 7307 ℂcc 10915 ℝcr 10916 0cc0 10917 1c1 10918 + caddc 10920 · cmul 10922 +∞cpnf 11052 -∞cmnf 11053 ℝ^*cxr 11054 < clt 11055 ≤ cle 11056 − cmin 11251 [,]cicc 13128 abscabs 14990 ∞Metcxmet 20627 ballcbl 20629

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2707 ax-sep 5232 ax-nul 5239 ax-pow 5297 ax-pr 5361 ax-un 7620 ax-cnex 10973 ax-resscn 10974 ax-1cn 10975 ax-icn 10976 ax-addcl 10977 ax-addrcl 10978 ax-mulcl 10979 ax-mulrcl 10980 ax-mulcom 10981 ax-addass 10982 ax-mulass 10983 ax-distr 10984 ax-i2m1 10985 ax-1ne0 10986 ax-1rid 10987 ax-rnegex 10988 ax-rrecex 10989 ax-cnre 10990 ax-pre-lttri 10991 ax-pre-lttrn 10992 ax-pre-ltadd 10993 ax-pre-mulgt0 10994 ax-pre-sup 10995

This theorem depends on definitions: df-bi 206 df-an 398 df-or 846 df-3or 1088 df-3an 1089 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3285 df-reu 3286 df-rab 3287 df-v 3439 df-sbc 3722 df-csb 3838 df-dif 3895 df-un 3897 df-in 3899 df-ss 3909 df-pss 3911 df-nul 4263 df-if 4466 df-pw 4541 df-sn 4566 df-pr 4568 df-op 4572 df-uni 4845 df-iun 4933 df-br 5082 df-opab 5144 df-mpt 5165 df-tr 5199 df-id 5500 df-eprel 5506 df-po 5514 df-so 5515 df-fr 5555 df-we 5557 df-xp 5606 df-rel 5607 df-cnv 5608 df-co 5609 df-dm 5610 df-rn 5611 df-res 5612 df-ima 5613 df-pred 6217 df-ord 6284 df-on 6285 df-lim 6286 df-suc 6287 df-iota 6410 df-fun 6460 df-fn 6461 df-f 6462 df-f1 6463 df-fo 6464 df-f1o 6465 df-fv 6466 df-riota 7264 df-ov 7310 df-oprab 7311 df-mpo 7312 df-om 7745 df-1st 7863 df-2nd 7864 df-frecs 8128 df-wrecs 8159 df-recs 8233 df-rdg 8272 df-er 8529 df-map 8648 df-en 8765 df-dom 8766 df-sdom 8767 df-sup 9245 df-pnf 11057 df-mnf 11058 df-xr 11059 df-ltxr 11060 df-le 11061 df-sub 11253 df-neg 11254 df-div 11679 df-nn 12020 df-2 12082 df-3 12083 df-n0 12280 df-z 12366 df-uz 12629 df-rp 12777 df-xadd 12895 df-icc 13132 df-seq 13768 df-exp 13829 df-cj 14855 df-re 14856 df-im 14857 df-sqrt 14991 df-abs 14992 df-psmet 20634 df-xmet 20635 df-met 20636 df-bl 20637

This theorem is referenced by: dvlipcn 25203 blsconn 33251

W3C validator