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 24707

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 1194	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ (0[,]1))
2		elicc01 13469	. . . . . . . 8 ⊢ (𝑇 ∈ (0[,]1) ↔ (𝑇 ∈ ℝ ∧ 0 ≤ 𝑇 ∧ 𝑇 ≤ 1))
3	1, 2	sylib 217	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 ∈ ℝ ∧ 0 ≤ 𝑇 ∧ 𝑇 ≤ 1))
4	3	simp1d 1140	. . . . . 6 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ ℝ)
5	4	recnd 11266	. . . . 5 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ ℂ)
6		simpr1 1192	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝐴 ∈ 𝑆)
7		blcvx.s	. . . . . . . 8 ⊢ 𝑆 = (𝑃(ball‘(abs ∘ − ))𝑅)
8	6, 7	eleqtrdi 2839	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝐴 ∈ (𝑃(ball‘(abs ∘ − ))𝑅))
9		cnxmet 24682	. . . . . . . 8 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
10		simpll 766	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑃 ∈ ℂ)
11		simplr 768	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑅 ∈ ℝ^)
12		elbl 24287	. . . . . . . 8 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) → (𝐴 ∈ (𝑃(ball‘(abs ∘ − ))𝑅) ↔ (𝐴 ∈ ℂ ∧ (𝑃(abs ∘ − )𝐴) < 𝑅)))
13	9, 10, 11, 12	mp3an2i 1463	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝐴 ∈ (𝑃(ball‘(abs ∘ − ))𝑅) ↔ (𝐴 ∈ ℂ ∧ (𝑃(abs ∘ − )𝐴) < 𝑅)))
14	8, 13	mpbid 231	. . . . . 6 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝐴 ∈ ℂ ∧ (𝑃(abs ∘ − )𝐴) < 𝑅))
15	14	simpld 494	. . . . 5 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝐴 ∈ ℂ)
16	5, 15	mulcld 11258	. . . 4 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · 𝐴) ∈ ℂ)
17		1re 11238	. . . . . . 7 ⊢ 1 ∈ ℝ
18		resubcl 11548	. . . . . . 7 ⊢ ((1 ∈ ℝ ∧ 𝑇 ∈ ℝ) → (1 − 𝑇) ∈ ℝ)
19	17, 4, 18	sylancr 586	. . . . . 6 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℝ)
20	19	recnd 11266	. . . . 5 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℂ)
21		simpr2 1193	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝐵 ∈ 𝑆)
22	21, 7	eleqtrdi 2839	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝐵 ∈ (𝑃(ball‘(abs ∘ − ))𝑅))
23		elbl 24287	. . . . . . . 8 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) → (𝐵 ∈ (𝑃(ball‘(abs ∘ − ))𝑅) ↔ (𝐵 ∈ ℂ ∧ (𝑃(abs ∘ − )𝐵) < 𝑅)))
24	9, 10, 11, 23	mp3an2i 1463	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝐵 ∈ (𝑃(ball‘(abs ∘ − ))𝑅) ↔ (𝐵 ∈ ℂ ∧ (𝑃(abs ∘ − )𝐵) < 𝑅)))
25	22, 24	mpbid 231	. . . . . 6 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝐵 ∈ ℂ ∧ (𝑃(abs ∘ − )𝐵) < 𝑅))
26	25	simpld 494	. . . . 5 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝐵 ∈ ℂ)
27	20, 26	mulcld 11258	. . . 4 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · 𝐵) ∈ ℂ)
28	16, 27	addcld 11257	. . 3 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ ℂ)
29		eqid 2728	. . . . . . 7 ⊢ (abs ∘ − ) = (abs ∘ − )
30	29	cnmetdval 24680	. . . . . 6 ⊢ ((𝑃 ∈ ℂ ∧ ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ ℂ) → (𝑃(abs ∘ − )((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) = (abs‘(𝑃 − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)))))
31	10, 28, 30	syl2anc 583	. . . . 5 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) = (abs‘(𝑃 − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)))))
32	5, 10, 15	subdid 11694	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · (𝑃 − 𝐴)) = ((𝑇 · 𝑃) − (𝑇 · 𝐴)))
33	20, 10, 26	subdid 11694	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · (𝑃 − 𝐵)) = (((1 − 𝑇) · 𝑃) − ((1 − 𝑇) · 𝐵)))
34	32, 33	oveq12d 7432	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵))) = (((𝑇 · 𝑃) − (𝑇 · 𝐴)) + (((1 − 𝑇) · 𝑃) − ((1 − 𝑇) · 𝐵))))
35	5, 10	mulcld 11258	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · 𝑃) ∈ ℂ)
36	20, 10	mulcld 11258	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · 𝑃) ∈ ℂ)
37	35, 36, 16, 27	addsub4d 11642	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (((𝑇 · 𝑃) + ((1 − 𝑇) · 𝑃)) − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) = (((𝑇 · 𝑃) − (𝑇 · 𝐴)) + (((1 − 𝑇) · 𝑃) − ((1 − 𝑇) · 𝐵))))
38		ax-1cn 11190	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
39		pncan3 11492	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑇 + (1 − 𝑇)) = 1)
40	5, 38, 39	sylancl 585	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 + (1 − 𝑇)) = 1)
41	40	oveq1d 7429	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · 𝑃) = (1 · 𝑃))
42	5, 20, 10	adddird 11263	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · 𝑃) = ((𝑇 · 𝑃) + ((1 − 𝑇) · 𝑃)))
43		mullid 11237	. . . . . . . . . 10 ⊢ (𝑃 ∈ ℂ → (1 · 𝑃) = 𝑃)
44	43	ad2antrr 725	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (1 · 𝑃) = 𝑃)
45	41, 42, 44	3eqtr3d 2776	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝑃) + ((1 − 𝑇) · 𝑃)) = 𝑃)
46	45	oveq1d 7429	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (((𝑇 · 𝑃) + ((1 − 𝑇) · 𝑃)) − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) = (𝑃 − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))))
47	34, 37, 46	3eqtr2d 2774	. . . . . 6 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵))) = (𝑃 − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))))
48	47	fveq2d 6895	. . . . 5 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) = (abs‘(𝑃 − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)))))
49	31, 48	eqtr4d 2771	. . . 4 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) = (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))))
50	10, 15	subcld 11595	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃 − 𝐴) ∈ ℂ)
51	5, 50	mulcld 11258	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · (𝑃 − 𝐴)) ∈ ℂ)
52	10, 26	subcld 11595	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃 − 𝐵) ∈ ℂ)
53	20, 52	mulcld 11258	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · (𝑃 − 𝐵)) ∈ ℂ)
54	51, 53	addcld 11257	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵))) ∈ ℂ)
55	54	abscld 15409	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) ∈ ℝ)
56	55	adantr 480	. . . . . 6 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) ∈ ℝ)
57	51	abscld 15409	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑇 · (𝑃 − 𝐴))) ∈ ℝ)
58	53	abscld 15409	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) ∈ ℝ)
59	57, 58	readdcld 11267	. . . . . . 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 15429	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) ≤ ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))))
63	62	adantr 480	. . . . . 6 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) ≤ ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))))
64		oveq1 7421	. . . . . . . . . . . 12 ⊢ (𝑇 = 0 → (𝑇 · (𝑃 − 𝐴)) = (0 · (𝑃 − 𝐴)))
65	50	mul02d 11436	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (0 · (𝑃 − 𝐴)) = 0)
66	64, 65	sylan9eqr 2790	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → (𝑇 · (𝑃 − 𝐴)) = 0)
67	66	abs00bd 15264	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → (abs‘(𝑇 · (𝑃 − 𝐴))) = 0)
68		oveq2 7422	. . . . . . . . . . . . . 14 ⊢ (𝑇 = 0 → (1 − 𝑇) = (1 − 0))
69		1m0e1 12357	. . . . . . . . . . . . . 14 ⊢ (1 − 0) = 1
70	68, 69	eqtrdi 2784	. . . . . . . . . . . . 13 ⊢ (𝑇 = 0 → (1 − 𝑇) = 1)
71	70	oveq1d 7429	. . . . . . . . . . . 12 ⊢ (𝑇 = 0 → ((1 − 𝑇) · (𝑃 − 𝐵)) = (1 · (𝑃 − 𝐵)))
72	52	mullidd 11256	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (1 · (𝑃 − 𝐵)) = (𝑃 − 𝐵))
73	71, 72	sylan9eqr 2790	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → ((1 − 𝑇) · (𝑃 − 𝐵)) = (𝑃 − 𝐵))
74	73	fveq2d 6895	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) = (abs‘(𝑃 − 𝐵)))
75	67, 74	oveq12d 7432	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) = (0 + (abs‘(𝑃 − 𝐵))))
76	52	abscld 15409	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑃 − 𝐵)) ∈ ℝ)
77	76	recnd 11266	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑃 − 𝐵)) ∈ ℂ)
78	77	addlidd 11439	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (0 + (abs‘(𝑃 − 𝐵))) = (abs‘(𝑃 − 𝐵)))
79	29	cnmetdval 24680	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑃(abs ∘ − )𝐵) = (abs‘(𝑃 − 𝐵)))
80	10, 26, 79	syl2anc 583	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )𝐵) = (abs‘(𝑃 − 𝐵)))
81	78, 80	eqtr4d 2771	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (0 + (abs‘(𝑃 − 𝐵))) = (𝑃(abs ∘ − )𝐵))
82	25	simprd 495	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )𝐵) < 𝑅)
83	81, 82	eqbrtrd 5164	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (0 + (abs‘(𝑃 − 𝐵))) < 𝑅)
84	83	adantr 480	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → (0 + (abs‘(𝑃 − 𝐵))) < 𝑅)
85	75, 84	eqbrtrd 5164	. . . . . . . 8 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅)
86	85	adantlr 714	. . . . . . 7 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 = 0) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅)
87	5, 50	absmuld 15427	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑇 · (𝑃 − 𝐴))) = ((abs‘𝑇) · (abs‘(𝑃 − 𝐴))))
88	3	simp2d 1141	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 ≤ 𝑇)
89	4, 88	absidd 15395	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘𝑇) = 𝑇)
90	89	oveq1d 7429	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((abs‘𝑇) · (abs‘(𝑃 − 𝐴))) = (𝑇 · (abs‘(𝑃 − 𝐴))))
91	87, 90	eqtrd 2768	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑇 · (𝑃 − 𝐴))) = (𝑇 · (abs‘(𝑃 − 𝐴))))
92	91	ad2antrr 725	. . . . . . . . . 10 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (abs‘(𝑇 · (𝑃 − 𝐴))) = (𝑇 · (abs‘(𝑃 − 𝐴))))
93	29	cnmetdval 24680	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝑃(abs ∘ − )𝐴) = (abs‘(𝑃 − 𝐴)))
94	10, 15, 93	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )𝐴) = (abs‘(𝑃 − 𝐴)))
95	14	simprd 495	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )𝐴) < 𝑅)
96	94, 95	eqbrtrrd 5166	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑃 − 𝐴)) < 𝑅)
97	96	ad2antrr 725	. . . . . . . . . . 11 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (abs‘(𝑃 − 𝐴)) < 𝑅)
98	50	abscld 15409	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑃 − 𝐴)) ∈ ℝ)
99	98	ad2antrr 725	. . . . . . . . . . . 12 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (abs‘(𝑃 − 𝐴)) ∈ ℝ)
100		simplr 768	. . . . . . . . . . . 12 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → 𝑅 ∈ ℝ)
101	4	ad2antrr 725	. . . . . . . . . . . 12 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → 𝑇 ∈ ℝ)
102		0red 11241	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 ∈ ℝ)
103	102, 4, 88	leltned 11391	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (0 < 𝑇 ↔ 𝑇 ≠ 0))
104	103	biimpar 477	. . . . . . . . . . . . 13 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ≠ 0) → 0 < 𝑇)
105	104	adantlr 714	. . . . . . . . . . . 12 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → 0 < 𝑇)
106		ltmul2 12089	. . . . . . . . . . . 12 ⊢ (((abs‘(𝑃 − 𝐴)) ∈ ℝ ∧ 𝑅 ∈ ℝ ∧ (𝑇 ∈ ℝ ∧ 0 < 𝑇)) → ((abs‘(𝑃 − 𝐴)) < 𝑅 ↔ (𝑇 · (abs‘(𝑃 − 𝐴))) < (𝑇 · 𝑅)))
107	99, 100, 101, 105, 106	syl112anc 1372	. . . . . . . . . . 11 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → ((abs‘(𝑃 − 𝐴)) < 𝑅 ↔ (𝑇 · (abs‘(𝑃 − 𝐴))) < (𝑇 · 𝑅)))
108	97, 107	mpbid 231	. . . . . . . . . 10 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (𝑇 · (abs‘(𝑃 − 𝐴))) < (𝑇 · 𝑅))
109	92, 108	eqbrtrd 5164	. . . . . . . . 9 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (abs‘(𝑇 · (𝑃 − 𝐴))) < (𝑇 · 𝑅))
110	20, 52	absmuld 15427	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) = ((abs‘(1 − 𝑇)) · (abs‘(𝑃 − 𝐵))))
111	17	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 1 ∈ ℝ)
112	3	simp3d 1142	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ≤ 1)
113	4, 111, 112	abssubge0d 15404	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(1 − 𝑇)) = (1 − 𝑇))
114	113	oveq1d 7429	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((abs‘(1 − 𝑇)) · (abs‘(𝑃 − 𝐵))) = ((1 − 𝑇) · (abs‘(𝑃 − 𝐵))))
115	110, 114	eqtrd 2768	. . . . . . . . . . . 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 11751	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℝ ∧ 𝑇 ∈ ℝ) → (0 ≤ (1 − 𝑇) ↔ 𝑇 ≤ 1))
119	17, 4, 118	sylancr 586	. . . . . . . . . . . . . . 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 5166	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑃 − 𝐵)) < 𝑅)
124	123	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘(𝑃 − 𝐵)) < 𝑅)
125		ltle 11326	. . . . . . . . . . . . . 14 ⊢ (((abs‘(𝑃 − 𝐵)) ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((abs‘(𝑃 − 𝐵)) < 𝑅 → (abs‘(𝑃 − 𝐵)) ≤ 𝑅))
126	76, 125	sylan 579	. . . . . . . . . . . . 13 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((abs‘(𝑃 − 𝐵)) < 𝑅 → (abs‘(𝑃 − 𝐵)) ≤ 𝑅))
127	124, 126	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘(𝑃 − 𝐵)) ≤ 𝑅)
128		lemul2a 12093	. . . . . . . . . . . 12 ⊢ ((((abs‘(𝑃 − 𝐵)) ∈ ℝ ∧ 𝑅 ∈ ℝ ∧ ((1 − 𝑇) ∈ ℝ ∧ 0 ≤ (1 − 𝑇))) ∧ (abs‘(𝑃 − 𝐵)) ≤ 𝑅) → ((1 − 𝑇) · (abs‘(𝑃 − 𝐵))) ≤ ((1 − 𝑇) · 𝑅))
129	117, 61, 122, 127, 128	syl31anc 1371	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((1 − 𝑇) · (abs‘(𝑃 − 𝐵))) ≤ ((1 − 𝑇) · 𝑅))
130	116, 129	eqbrtrd 5164	. . . . . . . . . 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 11217	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑇 · 𝑅) ∈ ℝ)
135	4, 134	sylan 579	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (𝑇 · 𝑅) ∈ ℝ)
136		remulcl 11217	. . . . . . . . . . . 12 ⊢ (((1 − 𝑇) ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((1 − 𝑇) · 𝑅) ∈ ℝ)
137	19, 136	sylan 579	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((1 − 𝑇) · 𝑅) ∈ ℝ)
138		ltleadd 11721	. . . . . . . . . . 11 ⊢ ((((abs‘(𝑇 · (𝑃 − 𝐴))) ∈ ℝ ∧ (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) ∈ ℝ) ∧ ((𝑇 · 𝑅) ∈ ℝ ∧ ((1 − 𝑇) · 𝑅) ∈ ℝ)) → (((abs‘(𝑇 · (𝑃 − 𝐴))) < (𝑇 · 𝑅) ∧ (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) ≤ ((1 − 𝑇) · 𝑅)) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅))))
139	132, 133, 135, 137, 138	syl22anc 838	. . . . . . . . . 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 698	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅)))
142	40	oveq1d 7429	. . . . . . . . . . 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 11266	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → 𝑅 ∈ ℂ)
147	144, 145, 146	adddird 11263	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((𝑇 + (1 − 𝑇)) · 𝑅) = ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅)))
148	146	mullidd 11256	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (1 · 𝑅) = 𝑅)
149	143, 147, 148	3eqtr3d 2776	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅)) = 𝑅)
150	149	adantr 480	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅)) = 𝑅)
151	141, 150	breqtrd 5168	. . . . . . 7 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅)
152	86, 151	pm2.61dane 3025	. . . . . 6 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅)
153	56, 60, 61, 63, 152	lelttrd 11396	. . . . 5 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅)
154	55	adantr 480	. . . . . . 7 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 = +∞) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) ∈ ℝ)
155	154	ltpnfd 13127	. . . . . 6 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 = +∞) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) < +∞)
156		simpr 484	. . . . . 6 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 = +∞) → 𝑅 = +∞)
157	155, 156	breqtrrd 5170	. . . . 5 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 = +∞) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅)
158		0xr 11285	. . . . . . . . . 10 ⊢ 0 ∈ ℝ^*
159	158	a1i 11	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 ∈ ℝ^)
160	98	rexrd 11288	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑃 − 𝐴)) ∈ ℝ^)
161	50	absge0d 15417	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 ≤ (abs‘(𝑃 − 𝐴)))
162	159, 160, 11, 161, 96	xrlelttrd 13165	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 < 𝑅)
163	159, 11, 162	xrltled 13155	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 ≤ 𝑅)
164		ge0nemnf 13178	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ^* ∧ 0 ≤ 𝑅) → 𝑅 ≠ -∞)
165	11, 163, 164	syl2anc 583	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑅 ≠ -∞)
166	11, 165	jca 511	. . . . . 6 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑅 ∈ ℝ^ ∧ 𝑅 ≠ -∞))
167		xrnemnf 13123	. . . . . 6 ⊢ ((𝑅 ∈ ℝ^* ∧ 𝑅 ≠ -∞) ↔ (𝑅 ∈ ℝ ∨ 𝑅 = +∞))
168	166, 167	sylib 217	. . . . 5 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑅 ∈ ℝ ∨ 𝑅 = +∞))
169	153, 157, 168	mpjaodan 957	. . . 4 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅)
170	49, 169	eqbrtrd 5164	. . 3 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) < 𝑅)
171		elbl 24287	. . . 4 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) → (((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ (𝑃(ball‘(abs ∘ − ))𝑅) ↔ (((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ ℂ ∧ (𝑃(abs ∘ − )((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) < 𝑅)))
172	9, 10, 11, 171	mp3an2i 1463	. . 3 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ (𝑃(ball‘(abs ∘ − ))𝑅) ↔ (((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ ℂ ∧ (𝑃(abs ∘ − )((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) < 𝑅)))
173	28, 170, 172	mpbir2and 712	. 2 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ (𝑃(ball‘(abs ∘ − ))𝑅))
174	173, 7	eleqtrrdi 2840	1 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ 𝑆)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 846 ∧ w3a 1085 = wceq 1534 ∈ wcel 2099 ≠ wne 2936 class class class wbr 5142 ∘ ccom 5676 ‘cfv 6542 (class class class)co 7414 ℂcc 11130 ℝcr 11131 0cc0 11132 1c1 11133 + caddc 11135 · cmul 11137 +∞cpnf 11269 -∞cmnf 11270 ℝ^*cxr 11271 < clt 11272 ≤ cle 11273 − cmin 11468 [,]cicc 13353 abscabs 15207 ∞Metcxmet 21257 ballcbl 21259

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2699 ax-sep 5293 ax-nul 5300 ax-pow 5359 ax-pr 5423 ax-un 7734 ax-cnex 11188 ax-resscn 11189 ax-1cn 11190 ax-icn 11191 ax-addcl 11192 ax-addrcl 11193 ax-mulcl 11194 ax-mulrcl 11195 ax-mulcom 11196 ax-addass 11197 ax-mulass 11198 ax-distr 11199 ax-i2m1 11200 ax-1ne0 11201 ax-1rid 11202 ax-rnegex 11203 ax-rrecex 11204 ax-cnre 11205 ax-pre-lttri 11206 ax-pre-lttrn 11207 ax-pre-ltadd 11208 ax-pre-mulgt0 11209 ax-pre-sup 11210

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2530 df-eu 2559 df-clab 2706 df-cleq 2720 df-clel 2806 df-nfc 2881 df-ne 2937 df-nel 3043 df-ral 3058 df-rex 3067 df-rmo 3372 df-reu 3373 df-rab 3429 df-v 3472 df-sbc 3776 df-csb 3891 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-pss 3964 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-iun 4993 df-br 5143 df-opab 5205 df-mpt 5226 df-tr 5260 df-id 5570 df-eprel 5576 df-po 5584 df-so 5585 df-fr 5627 df-we 5629 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-riota 7370 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7865 df-1st 7987 df-2nd 7988 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-er 8718 df-map 8840 df-en 8958 df-dom 8959 df-sdom 8960 df-sup 9459 df-pnf 11274 df-mnf 11275 df-xr 11276 df-ltxr 11277 df-le 11278 df-sub 11470 df-neg 11471 df-div 11896 df-nn 12237 df-2 12299 df-3 12300 df-n0 12497 df-z 12583 df-uz 12847 df-rp 13001 df-xadd 13119 df-icc 13357 df-seq 13993 df-exp 14053 df-cj 15072 df-re 15073 df-im 15074 df-sqrt 15208 df-abs 15209 df-psmet 21264 df-xmet 21265 df-met 21266 df-bl 21267

This theorem is referenced by: dvlipcn 25920 blsconn 34848

W3C validator