blcvx

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)

		Ref	Expression
	Hypothesis	blcvx.s	$⊢ S = P ball (abs \circ -) R$
	Assertion	blcvx	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to T A + (1 - T) B \in S$

Proof

Step	Hyp	Ref	Expression
1		blcvx.s	$⊢ S = P ball (abs \circ -) R$
2		simpr3	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to T \in [0, 1]$
3		elicc01	$⊢ T \in [0, 1] \leftrightarrow (T \in ℝ \land 0 \leq T \land T \leq 1)$
4	2 3	sylib	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to (T \in ℝ \land 0 \leq T \land T \leq 1)$
5	4	simp1d	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to T \in ℝ$
6	5	recnd	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to T \in ℂ$
7		simpr1	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to A \in S$
8	7 1	eleqtrdi	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to A \in (P ball (abs \circ -) R)$
9		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
10		simpll	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to P \in ℂ$
11		simplr	$⊢ ((P \in ℂ \land R \in ℝ^{}) \land (A \in S \land B \in S \land T \in [0, 1])) \to R \in ℝ^{}$
12		elbl	$⊢ (abs \circ - \in ∞Met (ℂ) \land P \in ℂ \land R \in ℝ^{*}) \to (A \in (P ball (abs \circ -) R) \leftrightarrow (A \in ℂ \land P (abs \circ -) A < R))$
13	9 10 11 12	mp3an2i	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to (A \in (P ball (abs \circ -) R) \leftrightarrow (A \in ℂ \land P (abs \circ -) A < R))$
14	8 13	mpbid	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to (A \in ℂ \land P (abs \circ -) A < R)$
15	14	simpld	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to A \in ℂ$
16	6 15	mulcld	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to T A \in ℂ$
17		1re	$⊢ 1 \in ℝ$
18		resubcl	$⊢ (1 \in ℝ \land T \in ℝ) \to 1 - T \in ℝ$
19	17 5 18	sylancr	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to 1 - T \in ℝ$
20	19	recnd	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to 1 - T \in ℂ$
21		simpr2	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to B \in S$
22	21 1	eleqtrdi	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to B \in (P ball (abs \circ -) R)$
23		elbl	$⊢ (abs \circ - \in ∞Met (ℂ) \land P \in ℂ \land R \in ℝ^{*}) \to (B \in (P ball (abs \circ -) R) \leftrightarrow (B \in ℂ \land P (abs \circ -) B < R))$
24	9 10 11 23	mp3an2i	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to (B \in (P ball (abs \circ -) R) \leftrightarrow (B \in ℂ \land P (abs \circ -) B < R))$
25	22 24	mpbid	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to (B \in ℂ \land P (abs \circ -) B < R)$
26	25	simpld	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to B \in ℂ$
27	20 26	mulcld	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to (1 - T) B \in ℂ$
28	16 27	addcld	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to T A + (1 - T) B \in ℂ$
29		eqid	$⊢ abs \circ - = abs \circ -$
30	29	cnmetdval	$⊢ (P \in ℂ \land T A + (1 - T) B \in ℂ) \to P (abs \circ -) (T A + (1 - T) B) = \|P - (T A + (1 - T) B)\|$
31	10 28 30	syl2anc	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to P (abs \circ -) (T A + (1 - T) B) = \|P - (T A + (1 - T) B)\|$
32	6 10 15	subdid	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to T (P - A) = T P - T A$
33	20 10 26	subdid	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to (1 - T) (P - B) = (1 - T) P - (1 - T) B$
34	32 33	oveq12d	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to T (P - A) + (1 - T) (P - B) = (T P - T A) + (1 - T) P - (1 - T) B$
35	6 10	mulcld	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to T P \in ℂ$
36	20 10	mulcld	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to (1 - T) P \in ℂ$
37	35 36 16 27	addsub4d	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to T P + (1 - T) P - (T A + (1 - T) B) = (T P - T A) + (1 - T) P - (1 - T) B$
38		ax-1cn	$⊢ 1 \in ℂ$
39		pncan3	$⊢ (T \in ℂ \land 1 \in ℂ) \to T + 1 - T = 1$
40	6 38 39	sylancl	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to T + 1 - T = 1$
41	40	oveq1d	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to (T + 1 - T) P = 1 P$
42	6 20 10	adddird	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to (T + 1 - T) P = T P + (1 - T) P$
43		mulid2	$⊢ P \in ℂ \to 1 P = P$
44	43	ad2antrr	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to 1 P = P$
45	41 42 44	3eqtr3d	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to T P + (1 - T) P = P$
46	45	oveq1d	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to T P + (1 - T) P - (T A + (1 - T) B) = P - (T A + (1 - T) B)$
47	34 37 46	3eqtr2d	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to T (P - A) + (1 - T) (P - B) = P - (T A + (1 - T) B)$
48	47	fveq2d	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to \|T (P - A) + (1 - T) (P - B)\| = \|P - (T A + (1 - T) B)\|$
49	31 48	eqtr4d	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to P (abs \circ -) (T A + (1 - T) B) = \|T (P - A) + (1 - T) (P - B)\|$
50	10 15	subcld	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to P - A \in ℂ$
51	6 50	mulcld	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to T (P - A) \in ℂ$
52	10 26	subcld	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to P - B \in ℂ$
53	20 52	mulcld	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to (1 - T) (P - B) \in ℂ$
54	51 53	addcld	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to T (P - A) + (1 - T) (P - B) \in ℂ$
55	54	abscld	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to \|T (P - A) + (1 - T) (P - B)\| \in ℝ$
56	55	adantr	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \to \|T (P - A) + (1 - T) (P - B)\| \in ℝ$
57	51	abscld	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to \|T (P - A)\| \in ℝ$
58	53	abscld	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to \|(1 - T) (P - B)\| \in ℝ$
59	57 58	readdcld	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to \|T (P - A)\| + \|(1 - T) (P - B)\| \in ℝ$
60	59	adantr	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \to \|T (P - A)\| + \|(1 - T) (P - B)\| \in ℝ$
61		simpr	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \to R \in ℝ$
62	51 53	abstrid	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to \|T (P - A) + (1 - T) (P - B)\| \leq \|T (P - A)\| + \|(1 - T) (P - B)\|$
63	62	adantr	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \to \|T (P - A) + (1 - T) (P - B)\| \leq \|T (P - A)\| + \|(1 - T) (P - B)\|$
64		oveq1	$⊢ T = 0 \to T (P - A) = 0 \cdot (P - A)$
65	50	mul02d	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to 0 \cdot (P - A) = 0$
66	64 65	sylan9eqr	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land T = 0) \to T (P - A) = 0$
67	66	abs00bd	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land T = 0) \to \|T (P - A)\| = 0$
68		oveq2	$⊢ T = 0 \to 1 - T = 1 - 0$
69		1m0e1	$⊢ 1 - 0 = 1$
70	68 69	eqtrdi	$⊢ T = 0 \to 1 - T = 1$
71	70	oveq1d	$⊢ T = 0 \to (1 - T) (P - B) = 1 (P - B)$
72	52	mulid2d	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to 1 (P - B) = P - B$
73	71 72	sylan9eqr	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land T = 0) \to (1 - T) (P - B) = P - B$
74	73	fveq2d	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land T = 0) \to \|(1 - T) (P - B)\| = \|P - B\|$
75	67 74	oveq12d	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land T = 0) \to \|T (P - A)\| + \|(1 - T) (P - B)\| = 0 + \|P - B\|$
76	52	abscld	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to \|P - B\| \in ℝ$
77	76	recnd	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to \|P - B\| \in ℂ$
78	77	addid2d	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to 0 + \|P - B\| = \|P - B\|$
79	29	cnmetdval	$⊢ (P \in ℂ \land B \in ℂ) \to P (abs \circ -) B = \|P - B\|$
80	10 26 79	syl2anc	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to P (abs \circ -) B = \|P - B\|$
81	78 80	eqtr4d	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to 0 + \|P - B\| = P (abs \circ -) B$
82	25	simprd	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to P (abs \circ -) B < R$
83	81 82	eqbrtrd	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to 0 + \|P - B\| < R$
84	83	adantr	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land T = 0) \to 0 + \|P - B\| < R$
85	75 84	eqbrtrd	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land T = 0) \to \|T (P - A)\| + \|(1 - T) (P - B)\| < R$
86	85	adantlr	$⊢ ((((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \land T = 0) \to \|T (P - A)\| + \|(1 - T) (P - B)\| < R$
87	6 50	absmuld	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to \|T (P - A)\| = \|T\| \|P - A\|$
88	4	simp2d	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to 0 \leq T$
89	5 88	absidd	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to \|T\| = T$
90	89	oveq1d	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to \|T\| \|P - A\| = T \|P - A\|$
91	87 90	eqtrd	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to \|T (P - A)\| = T \|P - A\|$
92	91	ad2antrr	$⊢ ((((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \land T \neq 0) \to \|T (P - A)\| = T \|P - A\|$
93	29	cnmetdval	$⊢ (P \in ℂ \land A \in ℂ) \to P (abs \circ -) A = \|P - A\|$
94	10 15 93	syl2anc	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to P (abs \circ -) A = \|P - A\|$
95	14	simprd	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to P (abs \circ -) A < R$
96	94 95	eqbrtrrd	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to \|P - A\| < R$
97	96	ad2antrr	$⊢ ((((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \land T \neq 0) \to \|P - A\| < R$
98	50	abscld	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to \|P - A\| \in ℝ$
99	98	ad2antrr	$⊢ ((((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \land T \neq 0) \to \|P - A\| \in ℝ$
100		simplr	$⊢ ((((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \land T \neq 0) \to R \in ℝ$
101	5	ad2antrr	$⊢ ((((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \land T \neq 0) \to T \in ℝ$
102		0red	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to 0 \in ℝ$
103	102 5 88	leltned	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to (0 < T \leftrightarrow T \neq 0)$
104	103	biimpar	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land T \neq 0) \to 0 < T$
105	104	adantlr	$⊢ ((((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \land T \neq 0) \to 0 < T$
106		ltmul2	$⊢ (\|P - A\| \in ℝ \land R \in ℝ \land (T \in ℝ \land 0 < T)) \to (\|P - A\| < R \leftrightarrow T \|P - A\| < T R)$
107	99 100 101 105 106	syl112anc	$⊢ ((((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \land T \neq 0) \to (\|P - A\| < R \leftrightarrow T \|P - A\| < T R)$
108	97 107	mpbid	$⊢ ((((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \land T \neq 0) \to T \|P - A\| < T R$
109	92 108	eqbrtrd	$⊢ ((((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \land T \neq 0) \to \|T (P - A)\| < T R$
110	20 52	absmuld	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to \|(1 - T) (P - B)\| = \|1 - T\| \|P - B\|$
111	17	a1i	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to 1 \in ℝ$
112	4	simp3d	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to T \leq 1$
113	5 111 112	abssubge0d	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to \|1 - T\| = 1 - T$
114	113	oveq1d	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to \|1 - T\| \|P - B\| = (1 - T) \|P - B\|$
115	110 114	eqtrd	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to \|(1 - T) (P - B)\| = (1 - T) \|P - B\|$
116	115	adantr	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \to \|(1 - T) (P - B)\| = (1 - T) \|P - B\|$
117	76	adantr	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \to \|P - B\| \in ℝ$
118		subge0	$⊢ (1 \in ℝ \land T \in ℝ) \to (0 \leq 1 - T \leftrightarrow T \leq 1)$
119	17 5 118	sylancr	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to (0 \leq 1 - T \leftrightarrow T \leq 1)$
120	112 119	mpbird	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to 0 \leq 1 - T$
121	19 120	jca	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to (1 - T \in ℝ \land 0 \leq 1 - T)$
122	121	adantr	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \to (1 - T \in ℝ \land 0 \leq 1 - T)$
123	80 82	eqbrtrrd	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to \|P - B\| < R$
124	123	adantr	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \to \|P - B\| < R$
125		ltle	$⊢ (\|P - B\| \in ℝ \land R \in ℝ) \to (\|P - B\| < R \to \|P - B\| \leq R)$
126	76 125	sylan	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \to (\|P - B\| < R \to \|P - B\| \leq R)$
127	124 126	mpd	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \to \|P - B\| \leq R$
128		lemul2a	$⊢ ((\|P - B\| \in ℝ \land R \in ℝ \land (1 - T \in ℝ \land 0 \leq 1 - T)) \land \|P - B\| \leq R) \to (1 - T) \|P - B\| \leq (1 - T) R$
129	117 61 122 127 128	syl31anc	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \to (1 - T) \|P - B\| \leq (1 - T) R$
130	116 129	eqbrtrd	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \to \|(1 - T) (P - B)\| \leq (1 - T) R$
131	130	adantr	$⊢ ((((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \land T \neq 0) \to \|(1 - T) (P - B)\| \leq (1 - T) R$
132	57	adantr	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \to \|T (P - A)\| \in ℝ$
133	58	adantr	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \to \|(1 - T) (P - B)\| \in ℝ$
134		remulcl	$⊢ (T \in ℝ \land R \in ℝ) \to T R \in ℝ$
135	5 134	sylan	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \to T R \in ℝ$
136		remulcl	$⊢ (1 - T \in ℝ \land R \in ℝ) \to (1 - T) R \in ℝ$
137	19 136	sylan	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \to (1 - T) R \in ℝ$
138		ltleadd	$⊢ ((\|T (P - A)\| \in ℝ \land \|(1 - T) (P - B)\| \in ℝ) \land (T R \in ℝ \land (1 - T) R \in ℝ)) \to ((\|T (P - A)\| < T R \land \|(1 - T) (P - B)\| \leq (1 - T) R) \to \|T (P - A)\| + \|(1 - T) (P - B)\| < T R + (1 - T) R)$
139	132 133 135 137 138	syl22anc	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \to ((\|T (P - A)\| < T R \land \|(1 - T) (P - B)\| \leq (1 - T) R) \to \|T (P - A)\| + \|(1 - T) (P - B)\| < T R + (1 - T) R)$
140	139	adantr	$⊢ ((((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \land T \neq 0) \to ((\|T (P - A)\| < T R \land \|(1 - T) (P - B)\| \leq (1 - T) R) \to \|T (P - A)\| + \|(1 - T) (P - B)\| < T R + (1 - T) R)$
141	109 131 140	mp2and	$⊢ ((((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \land T \neq 0) \to \|T (P - A)\| + \|(1 - T) (P - B)\| < T R + (1 - T) R$
142	40	oveq1d	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to (T + 1 - T) R = 1 R$
143	142	adantr	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \to (T + 1 - T) R = 1 R$
144	6	adantr	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \to T \in ℂ$
145	20	adantr	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \to 1 - T \in ℂ$
146	61	recnd	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \to R \in ℂ$
147	144 145 146	adddird	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \to (T + 1 - T) R = T R + (1 - T) R$
148	146	mulid2d	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \to 1 R = R$
149	143 147 148	3eqtr3d	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \to T R + (1 - T) R = R$
150	149	adantr	$⊢ ((((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \land T \neq 0) \to T R + (1 - T) R = R$
151	141 150	breqtrd	$⊢ ((((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \land T \neq 0) \to \|T (P - A)\| + \|(1 - T) (P - B)\| < R$
152	86 151	pm2.61dane	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \to \|T (P - A)\| + \|(1 - T) (P - B)\| < R$
153	56 60 61 63 152	lelttrd	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R \in ℝ) \to \|T (P - A) + (1 - T) (P - B)\| < R$
154	55	adantr	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R = +∞) \to \|T (P - A) + (1 - T) (P - B)\| \in ℝ$
155	154	ltpnfd	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R = +∞) \to \|T (P - A) + (1 - T) (P - B)\| < +∞$
156		simpr	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R = +∞) \to R = +∞$
157	155 156	breqtrrd	$⊢ (((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \land R = +∞) \to \|T (P - A) + (1 - T) (P - B)\| < R$
158		0xr	$⊢ 0 \in ℝ^{*}$
159	158	a1i	$⊢ ((P \in ℂ \land R \in ℝ^{}) \land (A \in S \land B \in S \land T \in [0, 1])) \to 0 \in ℝ^{}$
160	98	rexrd	$⊢ ((P \in ℂ \land R \in ℝ^{}) \land (A \in S \land B \in S \land T \in [0, 1])) \to \|P - A\| \in ℝ^{}$
161	50	absge0d	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to 0 \leq \|P - A\|$
162	159 160 11 161 96	xrlelttrd	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to 0 < R$
163	159 11 162	xrltled	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to 0 \leq R$
164		ge0nemnf	$⊢ (R \in ℝ^{*} \land 0 \leq R) \to R \neq −∞$
165	11 163 164	syl2anc	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to R \neq −∞$
166	11 165	jca	$⊢ ((P \in ℂ \land R \in ℝ^{}) \land (A \in S \land B \in S \land T \in [0, 1])) \to (R \in ℝ^{} \land R \neq −∞)$
167		xrnemnf	$⊢ (R \in ℝ^{*} \land R \neq −∞) \leftrightarrow (R \in ℝ \lor R = +∞)$
168	166 167	sylib	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to (R \in ℝ \lor R = +∞)$
169	153 157 168	mpjaodan	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to \|T (P - A) + (1 - T) (P - B)\| < R$
170	49 169	eqbrtrd	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to P (abs \circ -) (T A + (1 - T) B) < R$
171		elbl	$⊢ (abs \circ - \in ∞Met (ℂ) \land P \in ℂ \land R \in ℝ^{*}) \to (T A + (1 - T) B \in (P ball (abs \circ -) R) \leftrightarrow (T A + (1 - T) B \in ℂ \land P (abs \circ -) (T A + (1 - T) B) < R))$
172	9 10 11 171	mp3an2i	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to (T A + (1 - T) B \in (P ball (abs \circ -) R) \leftrightarrow (T A + (1 - T) B \in ℂ \land P (abs \circ -) (T A + (1 - T) B) < R))$
173	28 170 172	mpbir2and	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to T A + (1 - T) B \in (P ball (abs \circ -) R)$
174	173 1	eleqtrrdi	$⊢ ((P \in ℂ \land R \in ℝ^{*}) \land (A \in S \land B \in S \land T \in [0, 1])) \to T A + (1 - T) B \in S$

Metamath Proof Explorer

Theorem blcvx

Proof