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 25150

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 1215	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ (0[,]1))
2		elicc01 13627	. . . . . . . 8 ⊢ (𝑇 ∈ (0[,]1) ↔ (𝑇 ∈ ℝ ∧ 0 ≤ 𝑇 ∧ 𝑇 ≤ 1))
3	1, 2	sylib 221	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 ∈ ℝ ∧ 0 ≤ 𝑇 ∧ 𝑇 ≤ 1))
4	3	simp1d 1160	. . . . . 6 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ ℝ)
5	4	recnd 11367	. . . . 5 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ ℂ)
6		simpr1 1213	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝐴 ∈ 𝑆)
7		blcvx.s	. . . . . . . 8 ⊢ 𝑆 = (𝑃(ball‘(abs ∘ − ))𝑅)
8	6, 7	eleqtrdi 2874	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝐴 ∈ (𝑃(ball‘(abs ∘ − ))𝑅))
9		cnxmet 25124	. . . . . . . 8 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
10		simpll 779	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑃 ∈ ℂ)
11		simplr 781	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑅 ∈ ℝ^)
12		elbl 24740	. . . . . . . 8 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) → (𝐴 ∈ (𝑃(ball‘(abs ∘ − ))𝑅) ↔ (𝐴 ∈ ℂ ∧ (𝑃(abs ∘ − )𝐴) < 𝑅)))
13	9, 10, 11, 12	mp3an2i 1496	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝐴 ∈ (𝑃(ball‘(abs ∘ − ))𝑅) ↔ (𝐴 ∈ ℂ ∧ (𝑃(abs ∘ − )𝐴) < 𝑅)))
14	8, 13	mpbid 235	. . . . . 6 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝐴 ∈ ℂ ∧ (𝑃(abs ∘ − )𝐴) < 𝑅))
15	14	simpld 500	. . . . 5 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝐴 ∈ ℂ)
16	5, 15	mulcld 11359	. . . 4 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · 𝐴) ∈ ℂ)
17		1re 11338	. . . . . . 7 ⊢ 1 ∈ ℝ
18		resubcl 11652	. . . . . . 7 ⊢ ((1 ∈ ℝ ∧ 𝑇 ∈ ℝ) → (1 − 𝑇) ∈ ℝ)
19	17, 4, 18	sylancr 599	. . . . . 6 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℝ)
20	19	recnd 11367	. . . . 5 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℂ)
21		simpr2 1214	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝐵 ∈ 𝑆)
22	21, 7	eleqtrdi 2874	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝐵 ∈ (𝑃(ball‘(abs ∘ − ))𝑅))
23		elbl 24740	. . . . . . . 8 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) → (𝐵 ∈ (𝑃(ball‘(abs ∘ − ))𝑅) ↔ (𝐵 ∈ ℂ ∧ (𝑃(abs ∘ − )𝐵) < 𝑅)))
24	9, 10, 11, 23	mp3an2i 1496	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝐵 ∈ (𝑃(ball‘(abs ∘ − ))𝑅) ↔ (𝐵 ∈ ℂ ∧ (𝑃(abs ∘ − )𝐵) < 𝑅)))
25	22, 24	mpbid 235	. . . . . 6 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝐵 ∈ ℂ ∧ (𝑃(abs ∘ − )𝐵) < 𝑅))
26	25	simpld 500	. . . . 5 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝐵 ∈ ℂ)
27	20, 26	mulcld 11359	. . . 4 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · 𝐵) ∈ ℂ)
28	16, 27	addcld 11358	. . 3 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ ℂ)
29		eqid 2763	. . . . . . 7 ⊢ (abs ∘ − ) = (abs ∘ − )
30	29	cnmetdval 25122	. . . . . 6 ⊢ ((𝑃 ∈ ℂ ∧ ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ ℂ) → (𝑃(abs ∘ − )((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) = (abs‘(𝑃 − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)))))
31	10, 28, 30	syl2anc 596	. . . . 5 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) = (abs‘(𝑃 − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)))))
32	5, 10, 15	subdid 11802	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · (𝑃 − 𝐴)) = ((𝑇 · 𝑃) − (𝑇 · 𝐴)))
33	20, 10, 26	subdid 11802	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · (𝑃 − 𝐵)) = (((1 − 𝑇) · 𝑃) − ((1 − 𝑇) · 𝐵)))
34	32, 33	oveq12d 7464	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵))) = (((𝑇 · 𝑃) − (𝑇 · 𝐴)) + (((1 − 𝑇) · 𝑃) − ((1 − 𝑇) · 𝐵))))
35	5, 10	mulcld 11359	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · 𝑃) ∈ ℂ)
36	20, 10	mulcld 11359	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · 𝑃) ∈ ℂ)
37	35, 36, 16, 27	addsub4d 11746	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (((𝑇 · 𝑃) + ((1 − 𝑇) · 𝑃)) − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) = (((𝑇 · 𝑃) − (𝑇 · 𝐴)) + (((1 − 𝑇) · 𝑃) − ((1 − 𝑇) · 𝐵))))
38		ax-1cn 11288	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
39		pncan3 11595	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑇 + (1 − 𝑇)) = 1)
40	5, 38, 39	sylancl 598	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 + (1 − 𝑇)) = 1)
41	40	oveq1d 7461	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · 𝑃) = (1 · 𝑃))
42	5, 20, 10	adddird 11364	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · 𝑃) = ((𝑇 · 𝑃) + ((1 − 𝑇) · 𝑃)))
43		mullid 11337	. . . . . . . . . 10 ⊢ (𝑃 ∈ ℂ → (1 · 𝑃) = 𝑃)
44	43	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (1 · 𝑃) = 𝑃)
45	41, 42, 44	3eqtr3d 2806	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝑃) + ((1 − 𝑇) · 𝑃)) = 𝑃)
46	45	oveq1d 7461	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (((𝑇 · 𝑃) + ((1 − 𝑇) · 𝑃)) − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) = (𝑃 − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))))
47	34, 37, 46	3eqtr2d 2804	. . . . . 6 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵))) = (𝑃 − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))))
48	47	fveq2d 6915	. . . . 5 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) = (abs‘(𝑃 − ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)))))
49	31, 48	eqtr4d 2801	. . . 4 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) = (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))))
50	10, 15	subcld 11699	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃 − 𝐴) ∈ ℂ)
51	5, 50	mulcld 11359	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · (𝑃 − 𝐴)) ∈ ℂ)
52	10, 26	subcld 11699	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃 − 𝐵) ∈ ℂ)
53	20, 52	mulcld 11359	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · (𝑃 − 𝐵)) ∈ ℂ)
54	51, 53	addcld 11358	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵))) ∈ ℂ)
55	54	abscld 15638	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) ∈ ℝ)
56	55	adantr 486	. . . . . 6 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) ∈ ℝ)
57	51	abscld 15638	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑇 · (𝑃 − 𝐴))) ∈ ℝ)
58	53	abscld 15638	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) ∈ ℝ)
59	57, 58	readdcld 11368	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) ∈ ℝ)
60	59	adantr 486	. . . . . 6 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) ∈ ℝ)
61		simpr 490	. . . . . 6 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → 𝑅 ∈ ℝ)
62	51, 53	abstrid 15658	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) ≤ ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))))
63	62	adantr 486	. . . . . 6 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) ≤ ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))))
64		oveq1 7453	. . . . . . . . . . . 12 ⊢ (𝑇 = 0 → (𝑇 · (𝑃 − 𝐴)) = (0 · (𝑃 − 𝐴)))
65	50	mul02d 11538	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (0 · (𝑃 − 𝐴)) = 0)
66	64, 65	sylan9eqr 2820	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → (𝑇 · (𝑃 − 𝐴)) = 0)
67	66	abs00bd 15490	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → (abs‘(𝑇 · (𝑃 − 𝐴))) = 0)
68		oveq2 7454	. . . . . . . . . . . . . 14 ⊢ (𝑇 = 0 → (1 − 𝑇) = (1 − 0))
69		1m0e1 12492	. . . . . . . . . . . . . 14 ⊢ (1 − 0) = 1
70	68, 69	eqtrdi 2814	. . . . . . . . . . . . 13 ⊢ (𝑇 = 0 → (1 − 𝑇) = 1)
71	70	oveq1d 7461	. . . . . . . . . . . 12 ⊢ (𝑇 = 0 → ((1 − 𝑇) · (𝑃 − 𝐵)) = (1 · (𝑃 − 𝐵)))
72	52	mullidd 11357	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (1 · (𝑃 − 𝐵)) = (𝑃 − 𝐵))
73	71, 72	sylan9eqr 2820	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → ((1 − 𝑇) · (𝑃 − 𝐵)) = (𝑃 − 𝐵))
74	73	fveq2d 6915	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) = (abs‘(𝑃 − 𝐵)))
75	67, 74	oveq12d 7464	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) = (0 + (abs‘(𝑃 − 𝐵))))
76	52	abscld 15638	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑃 − 𝐵)) ∈ ℝ)
77	76	recnd 11367	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑃 − 𝐵)) ∈ ℂ)
78	77	addlidd 11541	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (0 + (abs‘(𝑃 − 𝐵))) = (abs‘(𝑃 − 𝐵)))
79	29	cnmetdval 25122	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑃(abs ∘ − )𝐵) = (abs‘(𝑃 − 𝐵)))
80	10, 26, 79	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )𝐵) = (abs‘(𝑃 − 𝐵)))
81	78, 80	eqtr4d 2801	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (0 + (abs‘(𝑃 − 𝐵))) = (𝑃(abs ∘ − )𝐵))
82	25	simprd 501	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )𝐵) < 𝑅)
83	81, 82	eqbrtrd 5131	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (0 + (abs‘(𝑃 − 𝐵))) < 𝑅)
84	83	adantr 486	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → (0 + (abs‘(𝑃 − 𝐵))) < 𝑅)
85	75, 84	eqbrtrd 5131	. . . . . . . 8 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 = 0) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅)
86	85	adantlr 728	. . . . . . 7 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 = 0) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅)
87	5, 50	absmuld 15656	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑇 · (𝑃 − 𝐴))) = ((abs‘𝑇) · (abs‘(𝑃 − 𝐴))))
88	3	simp2d 1161	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 ≤ 𝑇)
89	4, 88	absidd 15622	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘𝑇) = 𝑇)
90	89	oveq1d 7461	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((abs‘𝑇) · (abs‘(𝑃 − 𝐴))) = (𝑇 · (abs‘(𝑃 − 𝐴))))
91	87, 90	eqtrd 2798	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑇 · (𝑃 − 𝐴))) = (𝑇 · (abs‘(𝑃 − 𝐴))))
92	91	ad2antrr 739	. . . . . . . . . 10 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (abs‘(𝑇 · (𝑃 − 𝐴))) = (𝑇 · (abs‘(𝑃 − 𝐴))))
93	29	cnmetdval 25122	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝑃(abs ∘ − )𝐴) = (abs‘(𝑃 − 𝐴)))
94	10, 15, 93	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )𝐴) = (abs‘(𝑃 − 𝐴)))
95	14	simprd 501	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )𝐴) < 𝑅)
96	94, 95	eqbrtrrd 5133	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑃 − 𝐴)) < 𝑅)
97	96	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (abs‘(𝑃 − 𝐴)) < 𝑅)
98	50	abscld 15638	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑃 − 𝐴)) ∈ ℝ)
99	98	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (abs‘(𝑃 − 𝐴)) ∈ ℝ)
100		simplr 781	. . . . . . . . . . . 12 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → 𝑅 ∈ ℝ)
101	4	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → 𝑇 ∈ ℝ)
102		0red 11341	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 ∈ ℝ)
103	102, 4, 88	leltned 11493	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (0 < 𝑇 ↔ 𝑇 ≠ 0))
104	103	biimpar 483	. . . . . . . . . . . . 13 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ≠ 0) → 0 < 𝑇)
105	104	adantlr 728	. . . . . . . . . . . 12 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → 0 < 𝑇)
106		ltmul2 12198	. . . . . . . . . . . 12 ⊢ (((abs‘(𝑃 − 𝐴)) ∈ ℝ ∧ 𝑅 ∈ ℝ ∧ (𝑇 ∈ ℝ ∧ 0 < 𝑇)) → ((abs‘(𝑃 − 𝐴)) < 𝑅 ↔ (𝑇 · (abs‘(𝑃 − 𝐴))) < (𝑇 · 𝑅)))
107	99, 100, 101, 105, 106	syl112anc 1402	. . . . . . . . . . 11 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → ((abs‘(𝑃 − 𝐴)) < 𝑅 ↔ (𝑇 · (abs‘(𝑃 − 𝐴))) < (𝑇 · 𝑅)))
108	97, 107	mpbid 235	. . . . . . . . . 10 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (𝑇 · (abs‘(𝑃 − 𝐴))) < (𝑇 · 𝑅))
109	92, 108	eqbrtrd 5131	. . . . . . . . 9 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (abs‘(𝑇 · (𝑃 − 𝐴))) < (𝑇 · 𝑅))
110	20, 52	absmuld 15656	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) = ((abs‘(1 − 𝑇)) · (abs‘(𝑃 − 𝐵))))
111	17	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 1 ∈ ℝ)
112	3	simp3d 1162	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ≤ 1)
113	4, 111, 112	abssubge0d 15633	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(1 − 𝑇)) = (1 − 𝑇))
114	113	oveq1d 7461	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((abs‘(1 − 𝑇)) · (abs‘(𝑃 − 𝐵))) = ((1 − 𝑇) · (abs‘(𝑃 − 𝐵))))
115	110, 114	eqtrd 2798	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) = ((1 − 𝑇) · (abs‘(𝑃 − 𝐵))))
116	115	adantr 486	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) = ((1 − 𝑇) · (abs‘(𝑃 − 𝐵))))
117	76	adantr 486	. . . . . . . . . . . 12 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘(𝑃 − 𝐵)) ∈ ℝ)
118		subge0 11859	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℝ ∧ 𝑇 ∈ ℝ) → (0 ≤ (1 − 𝑇) ↔ 𝑇 ≤ 1))
119	17, 4, 118	sylancr 599	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (0 ≤ (1 − 𝑇) ↔ 𝑇 ≤ 1))
120	112, 119	mpbird 260	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 ≤ (1 − 𝑇))
121	19, 120	jca 521	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) ∈ ℝ ∧ 0 ≤ (1 − 𝑇)))
122	121	adantr 486	. . . . . . . . . . . 12 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((1 − 𝑇) ∈ ℝ ∧ 0 ≤ (1 − 𝑇)))
123	80, 82	eqbrtrrd 5133	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑃 − 𝐵)) < 𝑅)
124	123	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘(𝑃 − 𝐵)) < 𝑅)
125		ltle 11428	. . . . . . . . . . . . . 14 ⊢ (((abs‘(𝑃 − 𝐵)) ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((abs‘(𝑃 − 𝐵)) < 𝑅 → (abs‘(𝑃 − 𝐵)) ≤ 𝑅))
126	76, 125	sylan 592	. . . . . . . . . . . . 13 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((abs‘(𝑃 − 𝐵)) < 𝑅 → (abs‘(𝑃 − 𝐵)) ≤ 𝑅))
127	124, 126	mpd 16	. . . . . . . . . . . 12 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘(𝑃 − 𝐵)) ≤ 𝑅)
128		lemul2a 12202	. . . . . . . . . . . 12 ⊢ ((((abs‘(𝑃 − 𝐵)) ∈ ℝ ∧ 𝑅 ∈ ℝ ∧ ((1 − 𝑇) ∈ ℝ ∧ 0 ≤ (1 − 𝑇))) ∧ (abs‘(𝑃 − 𝐵)) ≤ 𝑅) → ((1 − 𝑇) · (abs‘(𝑃 − 𝐵))) ≤ ((1 − 𝑇) · 𝑅))
129	117, 61, 122, 127, 128	syl31anc 1401	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((1 − 𝑇) · (abs‘(𝑃 − 𝐵))) ≤ ((1 − 𝑇) · 𝑅))
130	116, 129	eqbrtrd 5131	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) ≤ ((1 − 𝑇) · 𝑅))
131	130	adantr 486	. . . . . . . . 9 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) ≤ ((1 − 𝑇) · 𝑅))
132	57	adantr 486	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘(𝑇 · (𝑃 − 𝐴))) ∈ ℝ)
133	58	adantr 486	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) ∈ ℝ)
134		remulcl 11315	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑇 · 𝑅) ∈ ℝ)
135	4, 134	sylan 592	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (𝑇 · 𝑅) ∈ ℝ)
136		remulcl 11315	. . . . . . . . . . . 12 ⊢ (((1 − 𝑇) ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((1 − 𝑇) · 𝑅) ∈ ℝ)
137	19, 136	sylan 592	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((1 − 𝑇) · 𝑅) ∈ ℝ)
138		ltleadd 11829	. . . . . . . . . . 11 ⊢ ((((abs‘(𝑇 · (𝑃 − 𝐴))) ∈ ℝ ∧ (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) ∈ ℝ) ∧ ((𝑇 · 𝑅) ∈ ℝ ∧ ((1 − 𝑇) · 𝑅) ∈ ℝ)) → (((abs‘(𝑇 · (𝑃 − 𝐴))) < (𝑇 · 𝑅) ∧ (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) ≤ ((1 − 𝑇) · 𝑅)) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅))))
139	132, 133, 135, 137, 138	syl22anc 852	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (((abs‘(𝑇 · (𝑃 − 𝐴))) < (𝑇 · 𝑅) ∧ (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) ≤ ((1 − 𝑇) · 𝑅)) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅))))
140	139	adantr 486	. . . . . . . . 9 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → (((abs‘(𝑇 · (𝑃 − 𝐴))) < (𝑇 · 𝑅) ∧ (abs‘((1 − 𝑇) · (𝑃 − 𝐵))) ≤ ((1 − 𝑇) · 𝑅)) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅))))
141	109, 131, 140	mp2and 712	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅)))
142	40	oveq1d 7461	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · 𝑅) = (1 · 𝑅))
143	142	adantr 486	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((𝑇 + (1 − 𝑇)) · 𝑅) = (1 · 𝑅))
144	5	adantr 486	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → 𝑇 ∈ ℂ)
145	20	adantr 486	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (1 − 𝑇) ∈ ℂ)
146	61	recnd 11367	. . . . . . . . . . 11 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → 𝑅 ∈ ℂ)
147	144, 145, 146	adddird 11364	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((𝑇 + (1 − 𝑇)) · 𝑅) = ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅)))
148	146	mullidd 11357	. . . . . . . . . 10 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (1 · 𝑅) = 𝑅)
149	143, 147, 148	3eqtr3d 2806	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅)) = 𝑅)
150	149	adantr 486	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → ((𝑇 · 𝑅) + ((1 − 𝑇) · 𝑅)) = 𝑅)
151	141, 150	breqtrd 5135	. . . . . . 7 ⊢ (((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) ∧ 𝑇 ≠ 0) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅)
152	86, 151	pm2.61dane 3046	. . . . . 6 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → ((abs‘(𝑇 · (𝑃 − 𝐴))) + (abs‘((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅)
153	56, 60, 61, 63, 152	lelttrd 11498	. . . . 5 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 ∈ ℝ) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅)
154	55	adantr 486	. . . . . . 7 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 = +∞) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) ∈ ℝ)
155	154	ltpnfd 13280	. . . . . 6 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 = +∞) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) < +∞)
156		simpr 490	. . . . . 6 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 = +∞) → 𝑅 = +∞)
157	155, 156	breqtrrd 5137	. . . . 5 ⊢ ((((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑅 = +∞) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅)
158		0xr 11386	. . . . . . . . . 10 ⊢ 0 ∈ ℝ^*
159	158	a1i 11	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 ∈ ℝ^)
160	98	rexrd 11389	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘(𝑃 − 𝐴)) ∈ ℝ^)
161	50	absge0d 15646	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 ≤ (abs‘(𝑃 − 𝐴)))
162	159, 160, 11, 161, 96	xrlelttrd 13319	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 < 𝑅)
163	159, 11, 162	xrltled 13309	. . . . . . . 8 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 0 ≤ 𝑅)
164		ge0nemnf 13333	. . . . . . . 8 ⊢ ((𝑅 ∈ ℝ^* ∧ 0 ≤ 𝑅) → 𝑅 ≠ -∞)
165	11, 163, 164	syl2anc 596	. . . . . . 7 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → 𝑅 ≠ -∞)
166	11, 165	jca 521	. . . . . 6 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑅 ∈ ℝ^ ∧ 𝑅 ≠ -∞))
167		xrnemnf 13276	. . . . . 6 ⊢ ((𝑅 ∈ ℝ^* ∧ 𝑅 ≠ -∞) ↔ (𝑅 ∈ ℝ ∨ 𝑅 = +∞))
168	166, 167	sylib 221	. . . . 5 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑅 ∈ ℝ ∨ 𝑅 = +∞))
169	153, 157, 168	mpjaodan 973	. . . 4 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (abs‘((𝑇 · (𝑃 − 𝐴)) + ((1 − 𝑇) · (𝑃 − 𝐵)))) < 𝑅)
170	49, 169	eqbrtrd 5131	. . 3 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (𝑃(abs ∘ − )((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) < 𝑅)
171		elbl 24740	. . . 4 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) → (((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ (𝑃(ball‘(abs ∘ − ))𝑅) ↔ (((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ ℂ ∧ (𝑃(abs ∘ − )((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) < 𝑅)))
172	9, 10, 11, 171	mp3an2i 1496	. . 3 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → (((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ (𝑃(ball‘(abs ∘ − ))𝑅) ↔ (((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ ℂ ∧ (𝑃(abs ∘ − )((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) < 𝑅)))
173	28, 170, 172	mpbir2and 726	. 2 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ (𝑃(ball‘(abs ∘ − ))𝑅))
174	173, 7	eleqtrrdi 2875	1 ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ 𝑆)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 class class class wbr 5106 ∘ ccom 5660 ‘cfv 6561 (class class class)co 7446 ℂcc 11228 ℝcr 11229 0cc0 11230 1c1 11231 + caddc 11233 · cmul 11235 +∞cpnf 11370 -∞cmnf 11371 ℝ^*cxr 11372 < clt 11373 ≤ cle 11374 − cmin 11571 [,]cicc 13509 abscabs 15433 ∞Metcxmet 21696 ballcbl 21698

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7778 ax-cnex 11286 ax-resscn 11287 ax-1cn 11288 ax-icn 11289 ax-addcl 11290 ax-addrcl 11291 ax-mulcl 11292 ax-mulrcl 11293 ax-mulcom 11294 ax-addass 11295 ax-mulass 11296 ax-distr 11297 ax-i2m1 11298 ax-1ne0 11299 ax-1rid 11300 ax-rnegex 11301 ax-rrecex 11302 ax-cnre 11303 ax-pre-lttri 11304 ax-pre-lttrn 11305 ax-pre-ltadd 11306 ax-pre-mulgt0 11307 ax-pre-sup 11308

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-iun 4956 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-pred 6325 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6515 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-riota 7403 df-ov 7449 df-oprab 7450 df-mpo 7451 df-om 7905 df-1st 8028 df-2nd 8029 df-frecs 8330 df-wrecs 8361 df-recs 8410 df-rdg 8449 df-er 8748 df-map 8880 df-en 9005 df-dom 9006 df-sdom 9007 df-sup 9464 df-pnf 11375 df-mnf 11376 df-xr 11377 df-ltxr 11378 df-le 11379 df-sub 11573 df-neg 11574 df-div 12004 df-nn 12366 df-2 12435 df-3 12436 df-n0 12637 df-z 12724 df-uz 12996 df-rp 13151 df-xadd 13272 df-icc 13513 df-seq 14175 df-exp 14235 df-cj 15298 df-re 15299 df-im 15300 df-sqrt 15434 df-abs 15435 df-psmet 21703 df-xmet 21704 df-met 21705 df-bl 21706

This theorem is used by: dvlipcn 26347 blsconn 36189

W3C validator