Theorem 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	⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
	dvlipcn.f	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
	dvlipcn.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	dvlipcn.r	⊢ ( 𝜑 → 𝑅 ∈ ℝ* )
	dvlipcn.b	⊢ 𝐵 = ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑅 )
	dvlipcn.d	⊢ ( 𝜑 → 𝐵 ⊆ dom ( ℂ D 𝐹 ) )
	dvlipcn.m	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
	dvlipcn.l	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( abs ‘ ( ( ℂ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑀 )
Assertion	dvlipcn	⊢ ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑍 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑌 − 𝑍 ) ) ) )

Proof

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