dvlipcn

Description: A complex function with derivative bounded by M on an open ball is M-Lipschitz continuous. (Contributed by Mario Carneiro, 18-Mar-2015)

	Ref	Expression
Hypotheses	dvlipcn.x	$⊢ φ \to X \subseteq ℂ$
	dvlipcn.f	$⊢ φ \to F : X ⟶ ℂ$
	dvlipcn.a	$⊢ φ \to A \in ℂ$
	dvlipcn.r	$⊢ φ \to R \in ℝ^{*}$
	dvlipcn.b	$⊢ B = A ball (abs \circ -) R$
	dvlipcn.d	$⊢ φ \to B \subseteq dom F_{ℂ}^{'}$
	dvlipcn.m	$⊢ φ \to M \in ℝ$
	dvlipcn.l	$⊢ (φ \land x \in B) \to \|F_{ℂ}^{'} (x)\| \leq M$
Assertion	dvlipcn	$⊢ (φ \land (Y \in B \land Z \in B)) \to \|F (Y) - F (Z)\| \leq M \|Y - Z\|$

Proof

Step	Hyp	Ref	Expression
1		dvlipcn.x	$⊢ φ \to X \subseteq ℂ$
2		dvlipcn.f	$⊢ φ \to F : X ⟶ ℂ$
3		dvlipcn.a	$⊢ φ \to A \in ℂ$
4		dvlipcn.r	$⊢ φ \to R \in ℝ^{*}$
5		dvlipcn.b	$⊢ B = A ball (abs \circ -) R$
6		dvlipcn.d	$⊢ φ \to B \subseteq dom F_{ℂ}^{'}$
7		dvlipcn.m	$⊢ φ \to M \in ℝ$
8		dvlipcn.l	$⊢ (φ \land x \in B) \to \|F_{ℂ}^{'} (x)\| \leq M$
9		1elunit	$⊢ 1 \in [0, 1]$
10		0elunit	$⊢ 0 \in [0, 1]$
11		0red	$⊢ (φ \land (Y \in B \land Z \in B)) \to 0 \in ℝ$
12		1red	$⊢ (φ \land (Y \in B \land Z \in B)) \to 1 \in ℝ$
13		ssidd	$⊢ φ \to ℂ \subseteq ℂ$
14	13 2 1	dvbss	$⊢ φ \to dom F_{ℂ}^{'} \subseteq X$
15	6 14	sstrd	$⊢ φ \to B \subseteq X$
16	15 1	sstrd	$⊢ φ \to B \subseteq ℂ$
17	16	adantr	$⊢ (φ \land (Y \in B \land Z \in B)) \to B \subseteq ℂ$
18		simprl	$⊢ (φ \land (Y \in B \land Z \in B)) \to Y \in B$
19	17 18	sseldd	$⊢ (φ \land (Y \in B \land Z \in B)) \to Y \in ℂ$
20	19	adantr	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in [0, 1]) \to Y \in ℂ$
21		unitssre	$⊢ [0, 1] \subseteq ℝ$
22		ax-resscn	$⊢ ℝ \subseteq ℂ$
23	21 22	sstri	$⊢ [0, 1] \subseteq ℂ$
24		simpr	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in [0, 1]) \to t \in [0, 1]$
25	23 24	sselid	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in [0, 1]) \to t \in ℂ$
26	20 25	mulcomd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in [0, 1]) \to Y t = t Y$
27		simprr	$⊢ (φ \land (Y \in B \land Z \in B)) \to Z \in B$
28	17 27	sseldd	$⊢ (φ \land (Y \in B \land Z \in B)) \to Z \in ℂ$
29	28	adantr	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in [0, 1]) \to Z \in ℂ$
30		iirev	$⊢ t \in [0, 1] \to 1 - t \in [0, 1]$
31	30	adantl	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in [0, 1]) \to 1 - t \in [0, 1]$
32	23 31	sselid	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in [0, 1]) \to 1 - t \in ℂ$
33	29 32	mulcomd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in [0, 1]) \to Z (1 - t) = (1 - t) Z$
34	26 33	oveq12d	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in [0, 1]) \to Y t + Z (1 - t) = t Y + (1 - t) Z$
35	3	ad2antrr	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in [0, 1]) \to A \in ℂ$
36	4	ad2antrr	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in [0, 1]) \to R \in ℝ^{*}$
37	18	adantr	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in [0, 1]) \to Y \in B$
38	27	adantr	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in [0, 1]) \to Z \in B$
39	5	blcvx	$⊢ ((A \in ℂ \land R \in ℝ^{*}) \land (Y \in B \land Z \in B \land t \in [0, 1])) \to t Y + (1 - t) Z \in B$
40	35 36 37 38 24 39	syl23anc	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in [0, 1]) \to t Y + (1 - t) Z \in B$
41	34 40	eqeltrd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in [0, 1]) \to Y t + Z (1 - t) \in B$
42		eqidd	$⊢ (φ \land (Y \in B \land Z \in B)) \to (t \in [0, 1] ⟼ Y t + Z (1 - t)) = (t \in [0, 1] ⟼ Y t + Z (1 - t))$
43	2 15	fssresd	$⊢ φ \to ({F ↾}_{B}) : B ⟶ ℂ$
44	43	feqmptd	$⊢ φ \to {F ↾}_{B} = (z \in B ⟼ ({F ↾}_{B}) (z))$
45		fvres	$⊢ z \in B \to ({F ↾}_{B}) (z) = F (z)$
46	45	mpteq2ia	$⊢ (z \in B ⟼ ({F ↾}_{B}) (z)) = (z \in B ⟼ F (z))$
47	44 46	eqtrdi	$⊢ φ \to {F ↾}_{B} = (z \in B ⟼ F (z))$
48	47	adantr	$⊢ (φ \land (Y \in B \land Z \in B)) \to {F ↾}_{B} = (z \in B ⟼ F (z))$
49		fveq2	$⊢ z = Y t + Z (1 - t) \to F (z) = F (Y t + Z (1 - t))$
50	41 42 48 49	fmptco	$⊢ (φ \land (Y \in B \land Z \in B)) \to ({F ↾}_{B}) \circ (t \in [0, 1] ⟼ Y t + Z (1 - t)) = (t \in [0, 1] ⟼ F (Y t + Z (1 - t)))$
51	41	fmpttd	$⊢ (φ \land (Y \in B \land Z \in B)) \to (t \in [0, 1] ⟼ Y t + Z (1 - t)) : [0, 1] ⟶ B$
52		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
53	52	addcn	$⊢ + \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
54	53	a1i	$⊢ (φ \land (Y \in B \land Z \in B)) \to + \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
55		ssid	$⊢ ℂ \subseteq ℂ$
56		cncfmptc	$⊢ (Y \in ℂ \land [0, 1] \subseteq ℂ \land ℂ \subseteq ℂ) \to (t \in [0, 1] ⟼ Y) : [0, 1] \underset{cn}{⟶} ℂ$
57	23 55 56	mp3an23	$⊢ Y \in ℂ \to (t \in [0, 1] ⟼ Y) : [0, 1] \underset{cn}{⟶} ℂ$
58	19 57	syl	$⊢ (φ \land (Y \in B \land Z \in B)) \to (t \in [0, 1] ⟼ Y) : [0, 1] \underset{cn}{⟶} ℂ$
59		cncfmptid	$⊢ ([0, 1] \subseteq ℂ \land ℂ \subseteq ℂ) \to (t \in [0, 1] ⟼ t) : [0, 1] \underset{cn}{⟶} ℂ$
60	23 55 59	mp2an	$⊢ (t \in [0, 1] ⟼ t) : [0, 1] \underset{cn}{⟶} ℂ$
61	60	a1i	$⊢ (φ \land (Y \in B \land Z \in B)) \to (t \in [0, 1] ⟼ t) : [0, 1] \underset{cn}{⟶} ℂ$
62	58 61	mulcncf	$⊢ (φ \land (Y \in B \land Z \in B)) \to (t \in [0, 1] ⟼ Y t) : [0, 1] \underset{cn}{⟶} ℂ$
63		cncfmptc	$⊢ (Z \in ℂ \land [0, 1] \subseteq ℂ \land ℂ \subseteq ℂ) \to (t \in [0, 1] ⟼ Z) : [0, 1] \underset{cn}{⟶} ℂ$
64	23 55 63	mp3an23	$⊢ Z \in ℂ \to (t \in [0, 1] ⟼ Z) : [0, 1] \underset{cn}{⟶} ℂ$
65	28 64	syl	$⊢ (φ \land (Y \in B \land Z \in B)) \to (t \in [0, 1] ⟼ Z) : [0, 1] \underset{cn}{⟶} ℂ$
66	52	subcn	$⊢ - \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
67	66	a1i	$⊢ (φ \land (Y \in B \land Z \in B)) \to - \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
68		ax-1cn	$⊢ 1 \in ℂ$
69		cncfmptc	$⊢ (1 \in ℂ \land [0, 1] \subseteq ℂ \land ℂ \subseteq ℂ) \to (t \in [0, 1] ⟼ 1) : [0, 1] \underset{cn}{⟶} ℂ$
70	68 23 55 69	mp3an	$⊢ (t \in [0, 1] ⟼ 1) : [0, 1] \underset{cn}{⟶} ℂ$
71	70	a1i	$⊢ (φ \land (Y \in B \land Z \in B)) \to (t \in [0, 1] ⟼ 1) : [0, 1] \underset{cn}{⟶} ℂ$
72	52 67 71 61	cncfmpt2f	$⊢ (φ \land (Y \in B \land Z \in B)) \to (t \in [0, 1] ⟼ 1 - t) : [0, 1] \underset{cn}{⟶} ℂ$
73	65 72	mulcncf	$⊢ (φ \land (Y \in B \land Z \in B)) \to (t \in [0, 1] ⟼ Z (1 - t)) : [0, 1] \underset{cn}{⟶} ℂ$
74	52 54 62 73	cncfmpt2f	$⊢ (φ \land (Y \in B \land Z \in B)) \to (t \in [0, 1] ⟼ Y t + Z (1 - t)) : [0, 1] \underset{cn}{⟶} ℂ$
75		cncffvrn	$⊢ (B \subseteq ℂ \land (t \in [0, 1] ⟼ Y t + Z (1 - t)) : [0, 1] \underset{cn}{⟶} ℂ) \to ((t \in [0, 1] ⟼ Y t + Z (1 - t)) : [0, 1] \underset{cn}{⟶} B \leftrightarrow (t \in [0, 1] ⟼ Y t + Z (1 - t)) : [0, 1] ⟶ B)$
76	17 74 75	syl2anc	$⊢ (φ \land (Y \in B \land Z \in B)) \to ((t \in [0, 1] ⟼ Y t + Z (1 - t)) : [0, 1] \underset{cn}{⟶} B \leftrightarrow (t \in [0, 1] ⟼ Y t + Z (1 - t)) : [0, 1] ⟶ B)$
77	51 76	mpbird	$⊢ (φ \land (Y \in B \land Z \in B)) \to (t \in [0, 1] ⟼ Y t + Z (1 - t)) : [0, 1] \underset{cn}{⟶} B$
78		ssidd	$⊢ (φ \land (Y \in B \land Z \in B)) \to ℂ \subseteq ℂ$
79	43	adantr	$⊢ (φ \land (Y \in B \land Z \in B)) \to ({F ↾}_{B}) : B ⟶ ℂ$
80	52	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
81	80	toponrestid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
82	52 81	dvres	$⊢ ((ℂ \subseteq ℂ \land F : X ⟶ ℂ) \land (X \subseteq ℂ \land B \subseteq ℂ)) \to ℂ D ({F ↾}_{B}) = {F_{ℂ}^{'} ↾}_{int (TopOpen (ℂ_{fld})) (B)}$
83	13 2 1 16 82	syl22anc	$⊢ φ \to ℂ D ({F ↾}_{B}) = {F_{ℂ}^{'} ↾}_{int (TopOpen (ℂ_{fld})) (B)}$
84	52	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
85		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
86	52	cnfldtopn	$⊢ TopOpen (ℂ_{fld}) = MetOpen (abs \circ -)$
87	86	blopn	$⊢ (abs \circ - \in ∞Met (ℂ) \land A \in ℂ \land R \in ℝ^{*}) \to A ball (abs \circ -) R \in TopOpen (ℂ_{fld})$
88	85 3 4 87	mp3an2i	$⊢ φ \to A ball (abs \circ -) R \in TopOpen (ℂ_{fld})$
89	5 88	eqeltrid	$⊢ φ \to B \in TopOpen (ℂ_{fld})$
90		isopn3i	$⊢ (TopOpen (ℂ_{fld}) \in Top \land B \in TopOpen (ℂ_{fld})) \to int (TopOpen (ℂ_{fld})) (B) = B$
91	84 89 90	sylancr	$⊢ φ \to int (TopOpen (ℂ_{fld})) (B) = B$
92	91	reseq2d	$⊢ φ \to {F_{ℂ}^{'} ↾}_{int (TopOpen (ℂ_{fld})) (B)} = {F_{ℂ}^{'} ↾}_{B}$
93	83 92	eqtrd	$⊢ φ \to ℂ D ({F ↾}_{B}) = {F_{ℂ}^{'} ↾}_{B}$
94	93	dmeqd	$⊢ φ \to dom {({F ↾}_{B})}_{ℂ}^{'} = dom ({F_{ℂ}^{'} ↾}_{B})$
95		dmres	$⊢ dom ({F_{ℂ}^{'} ↾}_{B}) = B \cap dom F_{ℂ}^{'}$
96		df-ss	$⊢ B \subseteq dom F_{ℂ}^{'} \leftrightarrow B \cap dom F_{ℂ}^{'} = B$
97	6 96	sylib	$⊢ φ \to B \cap dom F_{ℂ}^{'} = B$
98	95 97	syl5eq	$⊢ φ \to dom ({F_{ℂ}^{'} ↾}_{B}) = B$
99	94 98	eqtrd	$⊢ φ \to dom {({F ↾}_{B})}_{ℂ}^{'} = B$
100	99	adantr	$⊢ (φ \land (Y \in B \land Z \in B)) \to dom {({F ↾}_{B})}_{ℂ}^{'} = B$
101		dvcn	$⊢ ((ℂ \subseteq ℂ \land ({F ↾}_{B}) : B ⟶ ℂ \land B \subseteq ℂ) \land dom {({F ↾}_{B})}_{ℂ}^{'} = B) \to ({F ↾}_{B}) : B \underset{cn}{⟶} ℂ$
102	78 79 17 100 101	syl31anc	$⊢ (φ \land (Y \in B \land Z \in B)) \to ({F ↾}_{B}) : B \underset{cn}{⟶} ℂ$
103	77 102	cncfco	$⊢ (φ \land (Y \in B \land Z \in B)) \to (({F ↾}_{B}) \circ (t \in [0, 1] ⟼ Y t + Z (1 - t))) : [0, 1] \underset{cn}{⟶} ℂ$
104	50 103	eqeltrrd	$⊢ (φ \land (Y \in B \land Z \in B)) \to (t \in [0, 1] ⟼ F (Y t + Z (1 - t))) : [0, 1] \underset{cn}{⟶} ℂ$
105	22	a1i	$⊢ (φ \land (Y \in B \land Z \in B)) \to ℝ \subseteq ℂ$
106	21	a1i	$⊢ (φ \land (Y \in B \land Z \in B)) \to [0, 1] \subseteq ℝ$
107	2	ad2antrr	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in [0, 1]) \to F : X ⟶ ℂ$
108	15	ad2antrr	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in [0, 1]) \to B \subseteq X$
109	108 41	sseldd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in [0, 1]) \to Y t + Z (1 - t) \in X$
110	107 109	ffvelrnd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in [0, 1]) \to F (Y t + Z (1 - t)) \in ℂ$
111	52	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
112		1re	$⊢ 1 \in ℝ$
113		iccntr	$⊢ (0 \in ℝ \land 1 \in ℝ) \to int (topGen (ran (.))) ([0, 1]) = (0, 1)$
114	11 112 113	sylancl	$⊢ (φ \land (Y \in B \land Z \in B)) \to int (topGen (ran (.))) ([0, 1]) = (0, 1)$
115	105 106 110 111 52 114	dvmptntr	$⊢ (φ \land (Y \in B \land Z \in B)) \to \frac{d (t \in [0, 1]⟼ F (Y t + Z (1 - t)))}{d_{ℝ} t} = \frac{d (t \in (0, 1)⟼ F (Y t + Z (1 - t)))}{d_{ℝ} t}$
116		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
117	116	a1i	$⊢ (φ \land (Y \in B \land Z \in B)) \to ℝ \in \{ℝ, ℂ\}$
118		cnelprrecn	$⊢ ℂ \in \{ℝ, ℂ\}$
119	118	a1i	$⊢ (φ \land (Y \in B \land Z \in B)) \to ℂ \in \{ℝ, ℂ\}$
120		ioossicc	$⊢ (0, 1) \subseteq [0, 1]$
121	120	sseli	$⊢ t \in (0, 1) \to t \in [0, 1]$
122	121 41	sylan2	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in (0, 1)) \to Y t + Z (1 - t) \in B$
123	19 28	subcld	$⊢ (φ \land (Y \in B \land Z \in B)) \to Y - Z \in ℂ$
124	123	adantr	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in (0, 1)) \to Y - Z \in ℂ$
125	15	adantr	$⊢ (φ \land (Y \in B \land Z \in B)) \to B \subseteq X$
126	125	sselda	$⊢ ((φ \land (Y \in B \land Z \in B)) \land z \in B) \to z \in X$
127	2	adantr	$⊢ (φ \land (Y \in B \land Z \in B)) \to F : X ⟶ ℂ$
128	127	ffvelrnda	$⊢ ((φ \land (Y \in B \land Z \in B)) \land z \in X) \to F (z) \in ℂ$
129	126 128	syldan	$⊢ ((φ \land (Y \in B \land Z \in B)) \land z \in B) \to F (z) \in ℂ$
130		fvexd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land z \in B) \to F_{ℂ}^{'} (z) \in V$
131	19	adantr	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in (0, 1)) \to Y \in ℂ$
132	121 25	sylan2	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in (0, 1)) \to t \in ℂ$
133	131 132	mulcld	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in (0, 1)) \to Y t \in ℂ$
134		1red	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in (0, 1)) \to 1 \in ℝ$
135		simpr	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in ℝ) \to t \in ℝ$
136	135	recnd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in ℝ) \to t \in ℂ$
137		1red	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in ℝ) \to 1 \in ℝ$
138	117	dvmptid	$⊢ (φ \land (Y \in B \land Z \in B)) \to \frac{d (t \in ℝ⟼ t)}{d_{ℝ} t} = (t \in ℝ ⟼ 1)$
139		ioossre	$⊢ (0, 1) \subseteq ℝ$
140	139	a1i	$⊢ (φ \land (Y \in B \land Z \in B)) \to (0, 1) \subseteq ℝ$
141		iooretop	$⊢ (0, 1) \in topGen (ran (.))$
142	141	a1i	$⊢ (φ \land (Y \in B \land Z \in B)) \to (0, 1) \in topGen (ran (.))$
143	117 136 137 138 140 111 52 142	dvmptres	$⊢ (φ \land (Y \in B \land Z \in B)) \to \frac{d (t \in (0, 1)⟼ t)}{d_{ℝ} t} = (t \in (0, 1) ⟼ 1)$
144	117 132 134 143 19	dvmptcmul	$⊢ (φ \land (Y \in B \land Z \in B)) \to \frac{d (t \in (0, 1)⟼ Y t)}{d_{ℝ} t} = (t \in (0, 1) ⟼ Y \cdot 1)$
145	19	mulid1d	$⊢ (φ \land (Y \in B \land Z \in B)) \to Y \cdot 1 = Y$
146	145	mpteq2dv	$⊢ (φ \land (Y \in B \land Z \in B)) \to (t \in (0, 1) ⟼ Y \cdot 1) = (t \in (0, 1) ⟼ Y)$
147	144 146	eqtrd	$⊢ (φ \land (Y \in B \land Z \in B)) \to \frac{d (t \in (0, 1)⟼ Y t)}{d_{ℝ} t} = (t \in (0, 1) ⟼ Y)$
148	28	adantr	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in (0, 1)) \to Z \in ℂ$
149	121 32	sylan2	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in (0, 1)) \to 1 - t \in ℂ$
150	148 149	mulcld	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in (0, 1)) \to Z (1 - t) \in ℂ$
151		negex	$⊢ - Z \in V$
152	151	a1i	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in (0, 1)) \to - Z \in V$
153		negex	$⊢ - 1 \in V$
154	153	a1i	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in (0, 1)) \to - 1 \in V$
155		1cnd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in (0, 1)) \to 1 \in ℂ$
156		0red	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in (0, 1)) \to 0 \in ℝ$
157		1cnd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in ℝ) \to 1 \in ℂ$
158		0red	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in ℝ) \to 0 \in ℝ$
159		1cnd	$⊢ (φ \land (Y \in B \land Z \in B)) \to 1 \in ℂ$
160	117 159	dvmptc	$⊢ (φ \land (Y \in B \land Z \in B)) \to \frac{d (t \in ℝ⟼ 1)}{d_{ℝ} t} = (t \in ℝ ⟼ 0)$
161	117 157 158 160 140 111 52 142	dvmptres	$⊢ (φ \land (Y \in B \land Z \in B)) \to \frac{d (t \in (0, 1)⟼ 1)}{d_{ℝ} t} = (t \in (0, 1) ⟼ 0)$
162	117 155 156 161 132 134 143	dvmptsub	$⊢ (φ \land (Y \in B \land Z \in B)) \to \frac{d (t \in (0, 1)⟼ 1 - t)}{d_{ℝ} t} = (t \in (0, 1) ⟼ 0 - 1)$
163		df-neg	$⊢ - 1 = 0 - 1$
164	163	mpteq2i	$⊢ (t \in (0, 1) ⟼ - 1) = (t \in (0, 1) ⟼ 0 - 1)$
165	162 164	eqtr4di	$⊢ (φ \land (Y \in B \land Z \in B)) \to \frac{d (t \in (0, 1)⟼ 1 - t)}{d_{ℝ} t} = (t \in (0, 1) ⟼ - 1)$
166	117 149 154 165 28	dvmptcmul	$⊢ (φ \land (Y \in B \land Z \in B)) \to \frac{d (t \in (0, 1)⟼ Z (1 - t))}{d_{ℝ} t} = (t \in (0, 1) ⟼ Z -1)$
167		neg1cn	$⊢ - 1 \in ℂ$
168		mulcom	$⊢ (Z \in ℂ \land - 1 \in ℂ) \to Z -1 = -1 Z$
169	28 167 168	sylancl	$⊢ (φ \land (Y \in B \land Z \in B)) \to Z -1 = -1 Z$
170	28	mulm1d	$⊢ (φ \land (Y \in B \land Z \in B)) \to -1 Z = - Z$
171	169 170	eqtrd	$⊢ (φ \land (Y \in B \land Z \in B)) \to Z -1 = - Z$
172	171	mpteq2dv	$⊢ (φ \land (Y \in B \land Z \in B)) \to (t \in (0, 1) ⟼ Z -1) = (t \in (0, 1) ⟼ - Z)$
173	166 172	eqtrd	$⊢ (φ \land (Y \in B \land Z \in B)) \to \frac{d (t \in (0, 1)⟼ Z (1 - t))}{d_{ℝ} t} = (t \in (0, 1) ⟼ - Z)$
174	117 133 131 147 150 152 173	dvmptadd	$⊢ (φ \land (Y \in B \land Z \in B)) \to \frac{d (t \in (0, 1)⟼ Y t + Z (1 - t))}{d_{ℝ} t} = (t \in (0, 1) ⟼ Y + (- Z))$
175	19 28	negsubd	$⊢ (φ \land (Y \in B \land Z \in B)) \to Y + (- Z) = Y - Z$
176	175	mpteq2dv	$⊢ (φ \land (Y \in B \land Z \in B)) \to (t \in (0, 1) ⟼ Y + (- Z)) = (t \in (0, 1) ⟼ Y - Z)$
177	174 176	eqtrd	$⊢ (φ \land (Y \in B \land Z \in B)) \to \frac{d (t \in (0, 1)⟼ Y t + Z (1 - t))}{d_{ℝ} t} = (t \in (0, 1) ⟼ Y - Z)$
178	1	adantr	$⊢ (φ \land (Y \in B \land Z \in B)) \to X \subseteq ℂ$
179	78 127 178 17 82	syl22anc	$⊢ (φ \land (Y \in B \land Z \in B)) \to ℂ D ({F ↾}_{B}) = {F_{ℂ}^{'} ↾}_{int (TopOpen (ℂ_{fld})) (B)}$
180	91	adantr	$⊢ (φ \land (Y \in B \land Z \in B)) \to int (TopOpen (ℂ_{fld})) (B) = B$
181	180	reseq2d	$⊢ (φ \land (Y \in B \land Z \in B)) \to {F_{ℂ}^{'} ↾}_{int (TopOpen (ℂ_{fld})) (B)} = {F_{ℂ}^{'} ↾}_{B}$
182	179 181	eqtrd	$⊢ (φ \land (Y \in B \land Z \in B)) \to ℂ D ({F ↾}_{B}) = {F_{ℂ}^{'} ↾}_{B}$
183	48	oveq2d	$⊢ (φ \land (Y \in B \land Z \in B)) \to ℂ D ({F ↾}_{B}) = \frac{d (z \in B⟼ F (z))}{d_{ℂ} z}$
184		dvfcn	$⊢ {({F ↾}_{B})}_{ℂ}^{'} : dom {({F ↾}_{B})}_{ℂ}^{'} ⟶ ℂ$
185	100	feq2d	$⊢ (φ \land (Y \in B \land Z \in B)) \to ({({F ↾}_{B})}_{ℂ}^{'} : dom {({F ↾}_{B})}_{ℂ}^{'} ⟶ ℂ \leftrightarrow {({F ↾}_{B})}_{ℂ}^{'} : B ⟶ ℂ)$
186	184 185	mpbii	$⊢ (φ \land (Y \in B \land Z \in B)) \to {({F ↾}_{B})}_{ℂ}^{'} : B ⟶ ℂ$
187	182	feq1d	$⊢ (φ \land (Y \in B \land Z \in B)) \to ({({F ↾}_{B})}_{ℂ}^{'} : B ⟶ ℂ \leftrightarrow ({F_{ℂ}^{'} ↾}_{B}) : B ⟶ ℂ)$
188	186 187	mpbid	$⊢ (φ \land (Y \in B \land Z \in B)) \to ({F_{ℂ}^{'} ↾}_{B}) : B ⟶ ℂ$
189	188	feqmptd	$⊢ (φ \land (Y \in B \land Z \in B)) \to {F_{ℂ}^{'} ↾}_{B} = (z \in B ⟼ ({F_{ℂ}^{'} ↾}_{B}) (z))$
190		fvres	$⊢ z \in B \to ({F_{ℂ}^{'} ↾}_{B}) (z) = F_{ℂ}^{'} (z)$
191	190	mpteq2ia	$⊢ (z \in B ⟼ ({F_{ℂ}^{'} ↾}_{B}) (z)) = (z \in B ⟼ F_{ℂ}^{'} (z))$
192	189 191	eqtrdi	$⊢ (φ \land (Y \in B \land Z \in B)) \to {F_{ℂ}^{'} ↾}_{B} = (z \in B ⟼ F_{ℂ}^{'} (z))$
193	182 183 192	3eqtr3d	$⊢ (φ \land (Y \in B \land Z \in B)) \to \frac{d (z \in B⟼ F (z))}{d_{ℂ} z} = (z \in B ⟼ F_{ℂ}^{'} (z))$
194		fveq2	$⊢ z = Y t + Z (1 - t) \to F_{ℂ}^{'} (z) = F_{ℂ}^{'} (Y t + Z (1 - t))$
195	117 119 122 124 129 130 177 193 49 194	dvmptco	$⊢ (φ \land (Y \in B \land Z \in B)) \to \frac{d (t \in (0, 1)⟼ F (Y t + Z (1 - t)))}{d_{ℝ} t} = (t \in (0, 1) ⟼ F_{ℂ}^{'} (Y t + Z (1 - t)) (Y - Z))$
196	115 195	eqtrd	$⊢ (φ \land (Y \in B \land Z \in B)) \to \frac{d (t \in [0, 1]⟼ F (Y t + Z (1 - t)))}{d_{ℝ} t} = (t \in (0, 1) ⟼ F_{ℂ}^{'} (Y t + Z (1 - t)) (Y - Z))$
197	196	dmeqd	$⊢ (φ \land (Y \in B \land Z \in B)) \to dom \frac{d (t \in [0, 1]⟼ F (Y t + Z (1 - t)))}{d_{ℝ} t} = dom (t \in (0, 1) ⟼ F_{ℂ}^{'} (Y t + Z (1 - t)) (Y - Z))$
198		ovex	$⊢ F_{ℂ}^{'} (Y t + Z (1 - t)) (Y - Z) \in V$
199	198	rgenw	$⊢ \forall t \in (0, 1) F_{ℂ}^{'} (Y t + Z (1 - t)) (Y - Z) \in V$
200		dmmptg	$⊢ \forall t \in (0, 1) F_{ℂ}^{'} (Y t + Z (1 - t)) (Y - Z) \in V \to dom (t \in (0, 1) ⟼ F_{ℂ}^{'} (Y t + Z (1 - t)) (Y - Z)) = (0, 1)$
201	199 200	mp1i	$⊢ (φ \land (Y \in B \land Z \in B)) \to dom (t \in (0, 1) ⟼ F_{ℂ}^{'} (Y t + Z (1 - t)) (Y - Z)) = (0, 1)$
202	197 201	eqtrd	$⊢ (φ \land (Y \in B \land Z \in B)) \to dom \frac{d (t \in [0, 1]⟼ F (Y t + Z (1 - t)))}{d_{ℝ} t} = (0, 1)$
203	7	adantr	$⊢ (φ \land (Y \in B \land Z \in B)) \to M \in ℝ$
204	123	abscld	$⊢ (φ \land (Y \in B \land Z \in B)) \to \|Y - Z\| \in ℝ$
205	203 204	remulcld	$⊢ (φ \land (Y \in B \land Z \in B)) \to M \|Y - Z\| \in ℝ$
206	196	fveq1d	$⊢ (φ \land (Y \in B \land Z \in B)) \to \frac{d (t \in [0, 1]⟼ F (Y t + Z (1 - t)))}{d_{ℝ} t} (t) = (t \in (0, 1) ⟼ F_{ℂ}^{'} (Y t + Z (1 - t)) (Y - Z)) (t)$
207		eqid	$⊢ (t \in (0, 1) ⟼ F_{ℂ}^{'} (Y t + Z (1 - t)) (Y - Z)) = (t \in (0, 1) ⟼ F_{ℂ}^{'} (Y t + Z (1 - t)) (Y - Z))$
208	207	fvmpt2	$⊢ (t \in (0, 1) \land F_{ℂ}^{'} (Y t + Z (1 - t)) (Y - Z) \in V) \to (t \in (0, 1) ⟼ F_{ℂ}^{'} (Y t + Z (1 - t)) (Y - Z)) (t) = F_{ℂ}^{'} (Y t + Z (1 - t)) (Y - Z)$
209	198 208	mpan2	$⊢ t \in (0, 1) \to (t \in (0, 1) ⟼ F_{ℂ}^{'} (Y t + Z (1 - t)) (Y - Z)) (t) = F_{ℂ}^{'} (Y t + Z (1 - t)) (Y - Z)$
210	206 209	sylan9eq	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in (0, 1)) \to \frac{d (t \in [0, 1]⟼ F (Y t + Z (1 - t)))}{d_{ℝ} t} (t) = F_{ℂ}^{'} (Y t + Z (1 - t)) (Y - Z)$
211	210	fveq2d	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in (0, 1)) \to \|\frac{d (t \in [0, 1]⟼ F (Y t + Z (1 - t)))}{d_{ℝ} t} (t)\| = \|F_{ℂ}^{'} (Y t + Z (1 - t)) (Y - Z)\|$
212		dvfcn	$⊢ F_{ℂ}^{'} : dom F_{ℂ}^{'} ⟶ ℂ$
213	6	ad2antrr	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in (0, 1)) \to B \subseteq dom F_{ℂ}^{'}$
214	213 122	sseldd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in (0, 1)) \to Y t + Z (1 - t) \in dom F_{ℂ}^{'}$
215		ffvelrn	$⊢ (F_{ℂ}^{'} : dom F_{ℂ}^{'} ⟶ ℂ \land Y t + Z (1 - t) \in dom F_{ℂ}^{'}) \to F_{ℂ}^{'} (Y t + Z (1 - t)) \in ℂ$
216	212 214 215	sylancr	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in (0, 1)) \to F_{ℂ}^{'} (Y t + Z (1 - t)) \in ℂ$
217	216 124	absmuld	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in (0, 1)) \to \|F_{ℂ}^{'} (Y t + Z (1 - t)) (Y - Z)\| = \|F_{ℂ}^{'} (Y t + Z (1 - t))\| \|Y - Z\|$
218	211 217	eqtrd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in (0, 1)) \to \|\frac{d (t \in [0, 1]⟼ F (Y t + Z (1 - t)))}{d_{ℝ} t} (t)\| = \|F_{ℂ}^{'} (Y t + Z (1 - t))\| \|Y - Z\|$
219	216	abscld	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in (0, 1)) \to \|F_{ℂ}^{'} (Y t + Z (1 - t))\| \in ℝ$
220	7	ad2antrr	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in (0, 1)) \to M \in ℝ$
221	124	abscld	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in (0, 1)) \to \|Y - Z\| \in ℝ$
222	124	absge0d	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in (0, 1)) \to 0 \leq \|Y - Z\|$
223		2fveq3	$⊢ y = Y t + Z (1 - t) \to \|F_{ℂ}^{'} (y)\| = \|F_{ℂ}^{'} (Y t + Z (1 - t))\|$
224	223	breq1d	$⊢ y = Y t + Z (1 - t) \to (\|F_{ℂ}^{'} (y)\| \leq M \leftrightarrow \|F_{ℂ}^{'} (Y t + Z (1 - t))\| \leq M)$
225	8	ralrimiva	$⊢ φ \to \forall x \in B \|F_{ℂ}^{'} (x)\| \leq M$
226		2fveq3	$⊢ x = y \to \|F_{ℂ}^{'} (x)\| = \|F_{ℂ}^{'} (y)\|$
227	226	breq1d	$⊢ x = y \to (\|F_{ℂ}^{'} (x)\| \leq M \leftrightarrow \|F_{ℂ}^{'} (y)\| \leq M)$
228	227	cbvralvw	$⊢ \forall x \in B \|F_{ℂ}^{'} (x)\| \leq M \leftrightarrow \forall y \in B \|F_{ℂ}^{'} (y)\| \leq M$
229	225 228	sylib	$⊢ φ \to \forall y \in B \|F_{ℂ}^{'} (y)\| \leq M$
230	229	ad2antrr	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in (0, 1)) \to \forall y \in B \|F_{ℂ}^{'} (y)\| \leq M$
231	224 230 122	rspcdva	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in (0, 1)) \to \|F_{ℂ}^{'} (Y t + Z (1 - t))\| \leq M$
232	219 220 221 222 231	lemul1ad	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in (0, 1)) \to \|F_{ℂ}^{'} (Y t + Z (1 - t))\| \|Y - Z\| \leq M \|Y - Z\|$
233	218 232	eqbrtrd	$⊢ ((φ \land (Y \in B \land Z \in B)) \land t \in (0, 1)) \to \|\frac{d (t \in [0, 1]⟼ F (Y t + Z (1 - t)))}{d_{ℝ} t} (t)\| \leq M \|Y - Z\|$
234	233	ralrimiva	$⊢ (φ \land (Y \in B \land Z \in B)) \to \forall t \in (0, 1) \|\frac{d (t \in [0, 1]⟼ F (Y t + Z (1 - t)))}{d_{ℝ} t} (t)\| \leq M \|Y - Z\|$
235		nfv	$⊢ Ⅎ z \|\frac{d (t \in [0, 1]⟼ F (Y t + Z (1 - t)))}{d_{ℝ} t} (t)\| \leq M \|Y - Z\|$
236		nfcv	$⊢ \underline{Ⅎ} t abs$
237		nfcv	$⊢ \underline{Ⅎ} t ℝ$
238		nfcv	$⊢ \underline{Ⅎ} t D$
239		nfmpt1	$⊢ \underline{Ⅎ} t (t \in [0, 1] ⟼ F (Y t + Z (1 - t)))$
240	237 238 239	nfov	$⊢ \underline{Ⅎ} t \frac{d (t \in [0, 1]⟼ F (Y t + Z (1 - t)))}{d_{ℝ} t}$
241		nfcv	$⊢ \underline{Ⅎ} t z$
242	240 241	nffv	$⊢ \underline{Ⅎ} t \frac{d (t \in [0, 1]⟼ F (Y t + Z (1 - t)))}{d_{ℝ} t} (z)$
243	236 242	nffv	$⊢ \underline{Ⅎ} t \|\frac{d (t \in [0, 1]⟼ F (Y t + Z (1 - t)))}{d_{ℝ} t} (z)\|$
244		nfcv	$⊢ \underline{Ⅎ} t \leq$
245		nfcv	$⊢ \underline{Ⅎ} t M \|Y - Z\|$
246	243 244 245	nfbr	$⊢ Ⅎ t \|\frac{d (t \in [0, 1]⟼ F (Y t + Z (1 - t)))}{d_{ℝ} t} (z)\| \leq M \|Y - Z\|$
247		2fveq3	$⊢ t = z \to \|\frac{d (t \in [0, 1]⟼ F (Y t + Z (1 - t)))}{d_{ℝ} t} (t)\| = \|\frac{d (t \in [0, 1]⟼ F (Y t + Z (1 - t)))}{d_{ℝ} t} (z)\|$
248	247	breq1d	$⊢ t = z \to (\|\frac{d (t \in [0, 1]⟼ F (Y t + Z (1 - t)))}{d_{ℝ} t} (t)\| \leq M \|Y - Z\| \leftrightarrow \|\frac{d (t \in [0, 1]⟼ F (Y t + Z (1 - t)))}{d_{ℝ} t} (z)\| \leq M \|Y - Z\|)$
249	235 246 248	cbvralw	$⊢ \forall t \in (0, 1) \|\frac{d (t \in [0, 1]⟼ F (Y t + Z (1 - t)))}{d_{ℝ} t} (t)\| \leq M \|Y - Z\| \leftrightarrow \forall z \in (0, 1) \|\frac{d (t \in [0, 1]⟼ F (Y t + Z (1 - t)))}{d_{ℝ} t} (z)\| \leq M \|Y - Z\|$
250	234 249	sylib	$⊢ (φ \land (Y \in B \land Z \in B)) \to \forall z \in (0, 1) \|\frac{d (t \in [0, 1]⟼ F (Y t + Z (1 - t)))}{d_{ℝ} t} (z)\| \leq M \|Y - Z\|$
251	250	r19.21bi	$⊢ ((φ \land (Y \in B \land Z \in B)) \land z \in (0, 1)) \to \|\frac{d (t \in [0, 1]⟼ F (Y t + Z (1 - t)))}{d_{ℝ} t} (z)\| \leq M \|Y - Z\|$
252	11 12 104 202 205 251	dvlip	$⊢ ((φ \land (Y \in B \land Z \in B)) \land (1 \in [0, 1] \land 0 \in [0, 1])) \to \|(t \in [0, 1] ⟼ F (Y t + Z (1 - t))) (1) - (t \in [0, 1] ⟼ F (Y t + Z (1 - t))) (0)\| \leq M \|Y - Z\| \|1 - 0\|$
253	9 10 252	mpanr12	$⊢ (φ \land (Y \in B \land Z \in B)) \to \|(t \in [0, 1] ⟼ F (Y t + Z (1 - t))) (1) - (t \in [0, 1] ⟼ F (Y t + Z (1 - t))) (0)\| \leq M \|Y - Z\| \|1 - 0\|$
254		oveq2	$⊢ t = 1 \to Y t = Y \cdot 1$
255		oveq2	$⊢ t = 1 \to 1 - t = 1 - 1$
256		1m1e0	$⊢ 1 - 1 = 0$
257	255 256	eqtrdi	$⊢ t = 1 \to 1 - t = 0$
258	257	oveq2d	$⊢ t = 1 \to Z (1 - t) = Z \cdot 0$
259	254 258	oveq12d	$⊢ t = 1 \to Y t + Z (1 - t) = Y \cdot 1 + Z \cdot 0$
260	259	fveq2d	$⊢ t = 1 \to F (Y t + Z (1 - t)) = F (Y \cdot 1 + Z \cdot 0)$
261		eqid	$⊢ (t \in [0, 1] ⟼ F (Y t + Z (1 - t))) = (t \in [0, 1] ⟼ F (Y t + Z (1 - t)))$
262		fvex	$⊢ F (Y \cdot 1 + Z \cdot 0) \in V$
263	260 261 262	fvmpt	$⊢ 1 \in [0, 1] \to (t \in [0, 1] ⟼ F (Y t + Z (1 - t))) (1) = F (Y \cdot 1 + Z \cdot 0)$
264	9 263	ax-mp	$⊢ (t \in [0, 1] ⟼ F (Y t + Z (1 - t))) (1) = F (Y \cdot 1 + Z \cdot 0)$
265	28	mul01d	$⊢ (φ \land (Y \in B \land Z \in B)) \to Z \cdot 0 = 0$
266	145 265	oveq12d	$⊢ (φ \land (Y \in B \land Z \in B)) \to Y \cdot 1 + Z \cdot 0 = Y + 0$
267	19	addid1d	$⊢ (φ \land (Y \in B \land Z \in B)) \to Y + 0 = Y$
268	266 267	eqtrd	$⊢ (φ \land (Y \in B \land Z \in B)) \to Y \cdot 1 + Z \cdot 0 = Y$
269	268	fveq2d	$⊢ (φ \land (Y \in B \land Z \in B)) \to F (Y \cdot 1 + Z \cdot 0) = F (Y)$
270	264 269	syl5eq	$⊢ (φ \land (Y \in B \land Z \in B)) \to (t \in [0, 1] ⟼ F (Y t + Z (1 - t))) (1) = F (Y)$
271		oveq2	$⊢ t = 0 \to Y t = Y \cdot 0$
272		oveq2	$⊢ t = 0 \to 1 - t = 1 - 0$
273		1m0e1	$⊢ 1 - 0 = 1$
274	272 273	eqtrdi	$⊢ t = 0 \to 1 - t = 1$
275	274	oveq2d	$⊢ t = 0 \to Z (1 - t) = Z \cdot 1$
276	271 275	oveq12d	$⊢ t = 0 \to Y t + Z (1 - t) = Y \cdot 0 + Z \cdot 1$
277	276	fveq2d	$⊢ t = 0 \to F (Y t + Z (1 - t)) = F (Y \cdot 0 + Z \cdot 1)$
278		fvex	$⊢ F (Y \cdot 0 + Z \cdot 1) \in V$
279	277 261 278	fvmpt	$⊢ 0 \in [0, 1] \to (t \in [0, 1] ⟼ F (Y t + Z (1 - t))) (0) = F (Y \cdot 0 + Z \cdot 1)$
280	10 279	ax-mp	$⊢ (t \in [0, 1] ⟼ F (Y t + Z (1 - t))) (0) = F (Y \cdot 0 + Z \cdot 1)$
281	19	mul01d	$⊢ (φ \land (Y \in B \land Z \in B)) \to Y \cdot 0 = 0$
282	28	mulid1d	$⊢ (φ \land (Y \in B \land Z \in B)) \to Z \cdot 1 = Z$
283	281 282	oveq12d	$⊢ (φ \land (Y \in B \land Z \in B)) \to Y \cdot 0 + Z \cdot 1 = 0 + Z$
284	28	addid2d	$⊢ (φ \land (Y \in B \land Z \in B)) \to 0 + Z = Z$
285	283 284	eqtrd	$⊢ (φ \land (Y \in B \land Z \in B)) \to Y \cdot 0 + Z \cdot 1 = Z$
286	285	fveq2d	$⊢ (φ \land (Y \in B \land Z \in B)) \to F (Y \cdot 0 + Z \cdot 1) = F (Z)$
287	280 286	syl5eq	$⊢ (φ \land (Y \in B \land Z \in B)) \to (t \in [0, 1] ⟼ F (Y t + Z (1 - t))) (0) = F (Z)$
288	270 287	oveq12d	$⊢ (φ \land (Y \in B \land Z \in B)) \to (t \in [0, 1] ⟼ F (Y t + Z (1 - t))) (1) - (t \in [0, 1] ⟼ F (Y t + Z (1 - t))) (0) = F (Y) - F (Z)$
289	288	fveq2d	$⊢ (φ \land (Y \in B \land Z \in B)) \to \|(t \in [0, 1] ⟼ F (Y t + Z (1 - t))) (1) - (t \in [0, 1] ⟼ F (Y t + Z (1 - t))) (0)\| = \|F (Y) - F (Z)\|$
290	273	fveq2i	$⊢ \|1 - 0\| = \|1\|$
291		abs1	$⊢ \|1\| = 1$
292	290 291	eqtri	$⊢ \|1 - 0\| = 1$
293	292	oveq2i	$⊢ M \|Y - Z\| \|1 - 0\| = M \|Y - Z\| \cdot 1$
294	205	recnd	$⊢ (φ \land (Y \in B \land Z \in B)) \to M \|Y - Z\| \in ℂ$
295	294	mulid1d	$⊢ (φ \land (Y \in B \land Z \in B)) \to M \|Y - Z\| \cdot 1 = M \|Y - Z\|$
296	293 295	syl5eq	$⊢ (φ \land (Y \in B \land Z \in B)) \to M \|Y - Z\| \|1 - 0\| = M \|Y - Z\|$
297	253 289 296	3brtr3d	$⊢ (φ \land (Y \in B \land Z \in B)) \to \|F (Y) - F (Z)\| \leq M \|Y - Z\|$

Metamath Proof Explorer

Theorem dvlipcn

Proof