dvlipcn - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dvlipcn		Structured version Visualization version GIF version

Theorem dvlipcn 26314

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

**Hypotheses**
Ref	Expression
dvlipcn.x	⊢ (𝜑 → 𝑋 ⊆ ℂ)
dvlipcn.f	⊢ (𝜑 → 𝐹:𝑋⟶ℂ)
dvlipcn.a	⊢ (𝜑 → 𝐴 ∈ ℂ)
dvlipcn.r	⊢ (𝜑 → 𝑅 ∈ ℝ^*)
dvlipcn.b	⊢ 𝐵 = (𝐴(ball‘(abs ∘ − ))𝑅)
dvlipcn.d	⊢ (𝜑 → 𝐵 ⊆ dom (ℂ D 𝐹))
dvlipcn.m	⊢ (𝜑 → 𝑀 ∈ ℝ)
dvlipcn.l	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (abs‘((ℂ D 𝐹)‘𝑥)) ≤ 𝑀)

**Assertion**
Ref	Expression
dvlipcn	⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))

Distinct variable groups: 𝑥,𝐵 𝑥,𝐹 𝑥,𝑀 𝜑,𝑥 Allowed substitution hints: 𝐴(𝑥) 𝑅(𝑥) 𝑋(𝑥) 𝑌(𝑥) 𝑍(𝑥)

Proof of Theorem dvlipcn Dummy variables 𝑡 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		1elunit 13601	. . 3 ⊢ 1 ∈ (0[,]1)
2		0elunit 13600	. . 3 ⊢ 0 ∈ (0[,]1)
3		0red 11311	. . . 4 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 0 ∈ ℝ)
4		1red 11309	. . . 4 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 1 ∈ ℝ)
5		dvlipcn.d	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ⊆ dom (ℂ D 𝐹))
6		ssidd 3954	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ℂ ⊆ ℂ)
7		dvlipcn.f	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)
8		dvlipcn.x	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋 ⊆ ℂ)
9	6, 7, 8	dvbss 26221	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom (ℂ D 𝐹) ⊆ 𝑋)
10	5, 9	sstrd 3941	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ⊆ 𝑋)
11	10, 8	sstrd 3941	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ⊆ ℂ)
12	11	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐵 ⊆ ℂ)
13		simprl 783	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ 𝐵)
14	12, 13	sseldd 3932	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ ℂ)
15	14	adantr 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑌 ∈ ℂ)
16		unitssre 13630	. . . . . . . . . . 11 ⊢ (0[,]1) ⊆ ℝ
17		ax-resscn 11257	. . . . . . . . . . 11 ⊢ ℝ ⊆ ℂ
18	16, 17	sstri 3940	. . . . . . . . . 10 ⊢ (0[,]1) ⊆ ℂ
19		simpr 490	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑡 ∈ (0[,]1))
20	18, 19	sselid 3929	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑡 ∈ ℂ)
21	15, 20	mulcomd 11330	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → (𝑌 · 𝑡) = (𝑡 · 𝑌))
22		simprr 785	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ 𝐵)
23	12, 22	sseldd 3932	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ ℂ)
24	23	adantr 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑍 ∈ ℂ)
25		iirev 25250	. . . . . . . . . . 11 ⊢ (𝑡 ∈ (0[,]1) → (1 − 𝑡) ∈ (0[,]1))
26	25	adantl 487	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → (1 − 𝑡) ∈ (0[,]1))
27	18, 26	sselid 3929	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → (1 − 𝑡) ∈ ℂ)
28	24, 27	mulcomd 11330	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → (𝑍 · (1 − 𝑡)) = ((1 − 𝑡) · 𝑍))
29	21, 28	oveq12d 7438	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) = ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑍)))
30		dvlipcn.a	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ ℂ)
31	30	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝐴 ∈ ℂ)
32		dvlipcn.r	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ ℝ^*)
33	32	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑅 ∈ ℝ^*)
34	13	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑌 ∈ 𝐵)
35	22	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑍 ∈ 𝐵)
36		dvlipcn.b	. . . . . . . . 9 ⊢ 𝐵 = (𝐴(ball‘(abs ∘ − ))𝑅)
37	36	blcvx 25117	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ 𝑡 ∈ (0[,]1))) → ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑍)) ∈ 𝐵)
38	31, 33, 34, 35, 19, 37	syl23anc 1404	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑍)) ∈ 𝐵)
39	29, 38	eqeltrd 2861	. . . . . 6 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) ∈ 𝐵)
40		eqidd 2762	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) = (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))
41	7, 10	fssresd 6749	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 ↾ 𝐵):𝐵⟶ℂ)
42	41	feqmptd 6953	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ↾ 𝐵) = (𝑧 ∈ 𝐵 ↦ ((𝐹 ↾ 𝐵)‘𝑧)))
43		fvres 6904	. . . . . . . . 9 ⊢ (𝑧 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝑧) = (𝐹‘𝑧))
44	43	mpteq2ia 5200	. . . . . . . 8 ⊢ (𝑧 ∈ 𝐵 ↦ ((𝐹 ↾ 𝐵)‘𝑧)) = (𝑧 ∈ 𝐵 ↦ (𝐹‘𝑧))
45	42, 44	eqtrdi 2812	. . . . . . 7 ⊢ (𝜑 → (𝐹 ↾ 𝐵) = (𝑧 ∈ 𝐵 ↦ (𝐹‘𝑧)))
46	45	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝐹 ↾ 𝐵) = (𝑧 ∈ 𝐵 ↦ (𝐹‘𝑧)))
47		fveq2 6885	. . . . . 6 ⊢ (𝑧 = ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) → (𝐹‘𝑧) = (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))
48	39, 40, 46, 47	fmptco 7130	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝐹 ↾ 𝐵) ∘ (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) = (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))
49	39	fmpttd 7115	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))):(0[,]1)⟶𝐵)
50		eqid 2761	. . . . . . . . 9 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
51	50	addcn 25185	. . . . . . . . . 10 ⊢ + ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld))
52	51	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → + ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld)))
53		ssid 3953	. . . . . . . . . . . 12 ⊢ ℂ ⊆ ℂ
54		cncfmptc 25233	. . . . . . . . . . . 12 ⊢ ((𝑌 ∈ ℂ ∧ (0[,]1) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (0[,]1) ↦ 𝑌) ∈ ((0[,]1)–cn→ℂ))
55	18, 53, 54	mp3an23 1482	. . . . . . . . . . 11 ⊢ (𝑌 ∈ ℂ → (𝑡 ∈ (0[,]1) ↦ 𝑌) ∈ ((0[,]1)–cn→ℂ))
56	14, 55	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ 𝑌) ∈ ((0[,]1)–cn→ℂ))
57		cncfmptid 25234	. . . . . . . . . . . 12 ⊢ (((0[,]1) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (0[,]1) ↦ 𝑡) ∈ ((0[,]1)–cn→ℂ))
58	18, 53, 57	mp2an 705	. . . . . . . . . . 11 ⊢ (𝑡 ∈ (0[,]1) ↦ 𝑡) ∈ ((0[,]1)–cn→ℂ)
59	58	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ 𝑡) ∈ ((0[,]1)–cn→ℂ))
60	56, 59	mulcncf 25767	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ (𝑌 · 𝑡)) ∈ ((0[,]1)–cn→ℂ))
61		cncfmptc 25233	. . . . . . . . . . . 12 ⊢ ((𝑍 ∈ ℂ ∧ (0[,]1) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (0[,]1) ↦ 𝑍) ∈ ((0[,]1)–cn→ℂ))
62	18, 53, 61	mp3an23 1482	. . . . . . . . . . 11 ⊢ (𝑍 ∈ ℂ → (𝑡 ∈ (0[,]1) ↦ 𝑍) ∈ ((0[,]1)–cn→ℂ))
63	23, 62	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ 𝑍) ∈ ((0[,]1)–cn→ℂ))
64	50	subcn 25186	. . . . . . . . . . . 12 ⊢ − ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld))
65	64	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → − ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld)))
66		ax-1cn 11258	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
67		cncfmptc 25233	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℂ ∧ (0[,]1) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (0[,]1) ↦ 1) ∈ ((0[,]1)–cn→ℂ))
68	66, 18, 53, 67	mp3an 1490	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ (0[,]1) ↦ 1) ∈ ((0[,]1)–cn→ℂ)
69	68	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ 1) ∈ ((0[,]1)–cn→ℂ))
70	50, 65, 69, 59	cncfmpt2f 25236	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ (1 − 𝑡)) ∈ ((0[,]1)–cn→ℂ))
71	63, 70	mulcncf 25767	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ (𝑍 · (1 − 𝑡))) ∈ ((0[,]1)–cn→ℂ))
72	50, 52, 60, 71	cncfmpt2f 25236	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ((0[,]1)–cn→ℂ))
73		cncfcdm 25219	. . . . . . . 8 ⊢ ((𝐵 ⊆ ℂ ∧ (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ((0[,]1)–cn→ℂ)) → ((𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ((0[,]1)–cn→𝐵) ↔ (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))):(0[,]1)⟶𝐵))
74	12, 72, 73	syl2anc 596	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ((0[,]1)–cn→𝐵) ↔ (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))):(0[,]1)⟶𝐵))
75	49, 74	mpbird 260	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ((0[,]1)–cn→𝐵))
76		ssidd 3954	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ℂ ⊆ ℂ)
77	41	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝐹 ↾ 𝐵):𝐵⟶ℂ)
78	50	cnfldtopon 25101	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
79	78	toponrestid 23239	. . . . . . . . . . . . 13 ⊢ (TopOpen‘ℂ_fld) = ((TopOpen‘ℂ_fld) ↾_t ℂ)
80	50, 79	dvres 26231	. . . . . . . . . . . 12 ⊢ (((ℂ ⊆ ℂ ∧ 𝐹:𝑋⟶ℂ) ∧ (𝑋 ⊆ ℂ ∧ 𝐵 ⊆ ℂ)) → (ℂ D (𝐹 ↾ 𝐵)) = ((ℂ D 𝐹) ↾ ((int‘(TopOpen‘ℂ_fld))‘𝐵)))
81	6, 7, 8, 11, 80	syl22anc 852	. . . . . . . . . . 11 ⊢ (𝜑 → (ℂ D (𝐹 ↾ 𝐵)) = ((ℂ D 𝐹) ↾ ((int‘(TopOpen‘ℂ_fld))‘𝐵)))
82	50	cnfldtop 25102	. . . . . . . . . . . . 13 ⊢ (TopOpen‘ℂ_fld) ∈ Top
83		cnxmet 25091	. . . . . . . . . . . . . . 15 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
84	50	cnfldtopn 25100	. . . . . . . . . . . . . . . 16 ⊢ (TopOpen‘ℂ_fld) = (MetOpen‘(abs ∘ − ))
85	84	blopn 24819	. . . . . . . . . . . . . . 15 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℝ^*) → (𝐴(ball‘(abs ∘ − ))𝑅) ∈ (TopOpen‘ℂ_fld))
86	83, 30, 32, 85	mp3an2i 1495	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴(ball‘(abs ∘ − ))𝑅) ∈ (TopOpen‘ℂ_fld))
87	36, 86	eqeltrid 2865	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ (TopOpen‘ℂ_fld))
88		isopn3i 23400	. . . . . . . . . . . . 13 ⊢ (((TopOpen‘ℂ_fld) ∈ Top ∧ 𝐵 ∈ (TopOpen‘ℂ_fld)) → ((int‘(TopOpen‘ℂ_fld))‘𝐵) = 𝐵)
89	82, 87, 88	sylancr 599	. . . . . . . . . . . 12 ⊢ (𝜑 → ((int‘(TopOpen‘ℂ_fld))‘𝐵) = 𝐵)
90	89	reseq2d 5970	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℂ D 𝐹) ↾ ((int‘(TopOpen‘ℂ_fld))‘𝐵)) = ((ℂ D 𝐹) ↾ 𝐵))
91	81, 90	eqtrd 2796	. . . . . . . . . 10 ⊢ (𝜑 → (ℂ D (𝐹 ↾ 𝐵)) = ((ℂ D 𝐹) ↾ 𝐵))
92	91	dmeqd 5887	. . . . . . . . 9 ⊢ (𝜑 → dom (ℂ D (𝐹 ↾ 𝐵)) = dom ((ℂ D 𝐹) ↾ 𝐵))
93		dmres 6003	. . . . . . . . . 10 ⊢ dom ((ℂ D 𝐹) ↾ 𝐵) = (𝐵 ∩ dom (ℂ D 𝐹))
94		dfss2 3917	. . . . . . . . . . 11 ⊢ (𝐵 ⊆ dom (ℂ D 𝐹) ↔ (𝐵 ∩ dom (ℂ D 𝐹)) = 𝐵)
95	5, 94	sylib 221	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 ∩ dom (ℂ D 𝐹)) = 𝐵)
96	93, 95	eqtrid 2808	. . . . . . . . 9 ⊢ (𝜑 → dom ((ℂ D 𝐹) ↾ 𝐵) = 𝐵)
97	92, 96	eqtrd 2796	. . . . . . . 8 ⊢ (𝜑 → dom (ℂ D (𝐹 ↾ 𝐵)) = 𝐵)
98	97	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → dom (ℂ D (𝐹 ↾ 𝐵)) = 𝐵)
99		dvcn 26241	. . . . . . 7 ⊢ (((ℂ ⊆ ℂ ∧ (𝐹 ↾ 𝐵):𝐵⟶ℂ ∧ 𝐵 ⊆ ℂ) ∧ dom (ℂ D (𝐹 ↾ 𝐵)) = 𝐵) → (𝐹 ↾ 𝐵) ∈ (𝐵–cn→ℂ))
100	76, 77, 12, 98, 99	syl31anc 1400	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝐹 ↾ 𝐵) ∈ (𝐵–cn→ℂ))
101	75, 100	cncfco 25228	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝐹 ↾ 𝐵) ∘ (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) ∈ ((0[,]1)–cn→ℂ))
102	48, 101	eqeltrrd 2862	. . . 4 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) ∈ ((0[,]1)–cn→ℂ))
103	17	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ℝ ⊆ ℂ)
104	16	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (0[,]1) ⊆ ℝ)
105	7	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝐹:𝑋⟶ℂ)
106	10	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝐵 ⊆ 𝑋)
107	106, 39	sseldd 3932	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) ∈ 𝑋)
108	105, 107	ffvelcdmd 7085	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0[,]1)) → (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ℂ)
109		tgioo4 25124	. . . . . . . 8 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
110		1re 11308	. . . . . . . . 9 ⊢ 1 ∈ ℝ
111		iccntr 25141	. . . . . . . . 9 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(0[,]1)) = (0(,)1))
112	3, 110, 111	sylancl 598	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((int‘(topGen‘ran (,)))‘(0[,]1)) = (0(,)1))
113	103, 104, 108, 109, 50, 112	dvmptntr 26291	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))) = (ℝ D (𝑡 ∈ (0(,)1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))))
114		reelprrecn 11292	. . . . . . . . 9 ⊢ ℝ ∈ {ℝ, ℂ}
115	114	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ℝ ∈ {ℝ, ℂ})
116		cnelprrecn 11293	. . . . . . . . 9 ⊢ ℂ ∈ {ℝ, ℂ}
117	116	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ℂ ∈ {ℝ, ℂ})
118		ioossicc 13564	. . . . . . . . . 10 ⊢ (0(,)1) ⊆ (0[,]1)
119	118	sseli 3927	. . . . . . . . 9 ⊢ (𝑡 ∈ (0(,)1) → 𝑡 ∈ (0[,]1))
120	119, 39	sylan2 605	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) ∈ 𝐵)
121	14, 23	subcld 11669	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 − 𝑍) ∈ ℂ)
122	121	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (𝑌 − 𝑍) ∈ ℂ)
123	10	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐵 ⊆ 𝑋)
124	123	sselda 3931	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝑋)
125	7	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐹:𝑋⟶ℂ)
126	125	ffvelcdmda 7084	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ ℂ)
127	124, 126	syldan 603	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑧 ∈ 𝐵) → (𝐹‘𝑧) ∈ ℂ)
128		fvexd 6900	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑧 ∈ 𝐵) → ((ℂ D 𝐹)‘𝑧) ∈ V)
129	14	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 𝑌 ∈ ℂ)
130	119, 20	sylan2 605	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℂ)
131	129, 130	mulcld 11329	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (𝑌 · 𝑡) ∈ ℂ)
132		1red 11309	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 1 ∈ ℝ)
133		simpr 490	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
134	133	recnd 11337	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℂ)
135		1red 11309	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ ℝ) → 1 ∈ ℝ)
136	115	dvmptid 26277	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ ℝ ↦ 𝑡)) = (𝑡 ∈ ℝ ↦ 1))
137		ioossre 13538	. . . . . . . . . . . . . 14 ⊢ (0(,)1) ⊆ ℝ
138	137	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (0(,)1) ⊆ ℝ)
139		iooretop 25084	. . . . . . . . . . . . . 14 ⊢ (0(,)1) ∈ (topGen‘ran (,))
140	139	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (0(,)1) ∈ (topGen‘ran (,)))
141	115, 134, 135, 136, 138, 109, 50, 140	dvmptres 26283	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ 𝑡)) = (𝑡 ∈ (0(,)1) ↦ 1))
142	115, 130, 132, 141, 14	dvmptcmul 26284	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (𝑌 · 𝑡))) = (𝑡 ∈ (0(,)1) ↦ (𝑌 · 1)))
143	14	mulridd 11326	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 · 1) = 𝑌)
144	143	mpteq2dv 5199	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0(,)1) ↦ (𝑌 · 1)) = (𝑡 ∈ (0(,)1) ↦ 𝑌))
145	142, 144	eqtrd 2796	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (𝑌 · 𝑡))) = (𝑡 ∈ (0(,)1) ↦ 𝑌))
146	23	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 𝑍 ∈ ℂ)
147	119, 27	sylan2 605	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈ ℂ)
148	146, 147	mulcld 11329	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (𝑍 · (1 − 𝑡)) ∈ ℂ)
149		negex 11555	. . . . . . . . . . 11 ⊢ -𝑍 ∈ V
150	149	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → -𝑍 ∈ V)
151		negex 11555	. . . . . . . . . . . . 13 ⊢ -1 ∈ V
152	151	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → -1 ∈ V)
153		1cnd 11302	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 1 ∈ ℂ)
154		0red 11311	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 0 ∈ ℝ)
155		1cnd 11302	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ ℝ) → 1 ∈ ℂ)
156		0red 11311	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ ℝ) → 0 ∈ ℝ)
157		1cnd 11302	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 1 ∈ ℂ)
158	115, 157	dvmptc 26278	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ ℝ ↦ 1)) = (𝑡 ∈ ℝ ↦ 0))
159	115, 155, 156, 158, 138, 109, 50, 140	dvmptres 26283	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ 1)) = (𝑡 ∈ (0(,)1) ↦ 0))
160	115, 153, 154, 159, 130, 132, 141	dvmptsub 26287	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (1 − 𝑡))) = (𝑡 ∈ (0(,)1) ↦ (0 − 1)))
161		df-neg 11544	. . . . . . . . . . . . . 14 ⊢ -1 = (0 − 1)
162	161	mpteq2i 5201	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ (0(,)1) ↦ -1) = (𝑡 ∈ (0(,)1) ↦ (0 − 1))
163	160, 162	eqtr4di 2814	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (1 − 𝑡))) = (𝑡 ∈ (0(,)1) ↦ -1))
164	115, 147, 152, 163, 23	dvmptcmul 26284	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (𝑍 · (1 − 𝑡)))) = (𝑡 ∈ (0(,)1) ↦ (𝑍 · -1)))
165		neg1cn 12305	. . . . . . . . . . . . . 14 ⊢ -1 ∈ ℂ
166		mulcom 11286	. . . . . . . . . . . . . 14 ⊢ ((𝑍 ∈ ℂ ∧ -1 ∈ ℂ) → (𝑍 · -1) = (-1 · 𝑍))
167	23, 165, 166	sylancl 598	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑍 · -1) = (-1 · 𝑍))
168	23	mulm1d 11768	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (-1 · 𝑍) = -𝑍)
169	167, 168	eqtrd 2796	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑍 · -1) = -𝑍)
170	169	mpteq2dv 5199	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0(,)1) ↦ (𝑍 · -1)) = (𝑡 ∈ (0(,)1) ↦ -𝑍))
171	164, 170	eqtrd 2796	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (𝑍 · (1 − 𝑡)))) = (𝑡 ∈ (0(,)1) ↦ -𝑍))
172	115, 131, 129, 145, 148, 150, 171	dvmptadd 26280	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) = (𝑡 ∈ (0(,)1) ↦ (𝑌 + -𝑍)))
173	14, 23	negsubd 11675	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 + -𝑍) = (𝑌 − 𝑍))
174	173	mpteq2dv 5199	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑡 ∈ (0(,)1) ↦ (𝑌 + -𝑍)) = (𝑡 ∈ (0(,)1) ↦ (𝑌 − 𝑍)))
175	172, 174	eqtrd 2796	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) = (𝑡 ∈ (0(,)1) ↦ (𝑌 − 𝑍)))
176	8	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ⊆ ℂ)
177	76, 125, 176, 12, 80	syl22anc 852	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℂ D (𝐹 ↾ 𝐵)) = ((ℂ D 𝐹) ↾ ((int‘(TopOpen‘ℂ_fld))‘𝐵)))
178	89	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((int‘(TopOpen‘ℂ_fld))‘𝐵) = 𝐵)
179	178	reseq2d 5970	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((ℂ D 𝐹) ↾ ((int‘(TopOpen‘ℂ_fld))‘𝐵)) = ((ℂ D 𝐹) ↾ 𝐵))
180	177, 179	eqtrd 2796	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℂ D (𝐹 ↾ 𝐵)) = ((ℂ D 𝐹) ↾ 𝐵))
181	46	oveq2d 7436	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℂ D (𝐹 ↾ 𝐵)) = (ℂ D (𝑧 ∈ 𝐵 ↦ (𝐹‘𝑧))))
182		dvfcn 26228	. . . . . . . . . . . . 13 ⊢ (ℂ D (𝐹 ↾ 𝐵)):dom (ℂ D (𝐹 ↾ 𝐵))⟶ℂ
183	98	feq2d 6693	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((ℂ D (𝐹 ↾ 𝐵)):dom (ℂ D (𝐹 ↾ 𝐵))⟶ℂ ↔ (ℂ D (𝐹 ↾ 𝐵)):𝐵⟶ℂ))
184	182, 183	mpbii 236	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℂ D (𝐹 ↾ 𝐵)):𝐵⟶ℂ)
185	180	feq1d 6691	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((ℂ D (𝐹 ↾ 𝐵)):𝐵⟶ℂ ↔ ((ℂ D 𝐹) ↾ 𝐵):𝐵⟶ℂ))
186	184, 185	mpbid 235	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((ℂ D 𝐹) ↾ 𝐵):𝐵⟶ℂ)
187	186	feqmptd 6953	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((ℂ D 𝐹) ↾ 𝐵) = (𝑧 ∈ 𝐵 ↦ (((ℂ D 𝐹) ↾ 𝐵)‘𝑧)))
188		fvres 6904	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐵 → (((ℂ D 𝐹) ↾ 𝐵)‘𝑧) = ((ℂ D 𝐹)‘𝑧))
189	188	mpteq2ia 5200	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝐵 ↦ (((ℂ D 𝐹) ↾ 𝐵)‘𝑧)) = (𝑧 ∈ 𝐵 ↦ ((ℂ D 𝐹)‘𝑧))
190	187, 189	eqtrdi 2812	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((ℂ D 𝐹) ↾ 𝐵) = (𝑧 ∈ 𝐵 ↦ ((ℂ D 𝐹)‘𝑧)))
191	180, 181, 190	3eqtr3d 2804	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℂ D (𝑧 ∈ 𝐵 ↦ (𝐹‘𝑧))) = (𝑧 ∈ 𝐵 ↦ ((ℂ D 𝐹)‘𝑧)))
192		fveq2 6885	. . . . . . . 8 ⊢ (𝑧 = ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) → ((ℂ D 𝐹)‘𝑧) = ((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))
193	115, 117, 120, 122, 127, 128, 175, 191, 47, 192	dvmptco 26292	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))) = (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍))))
194	113, 193	eqtrd 2796	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))) = (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍))))
195	194	dmeqd 5887	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → dom (ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))) = dom (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍))))
196		ovex 7453	. . . . . . 7 ⊢ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)) ∈ V
197	196	rgenw 3081	. . . . . 6 ⊢ ∀𝑡 ∈ (0(,)1)(((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)) ∈ V
198		dmmptg 6243	. . . . . 6 ⊢ (∀𝑡 ∈ (0(,)1)(((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)) ∈ V → dom (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍))) = (0(,)1))
199	197, 198	mp1i 14	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → dom (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍))) = (0(,)1))
200	195, 199	eqtrd 2796	. . . 4 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → dom (ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))) = (0(,)1))
201		dvlipcn.m	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℝ)
202	201	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑀 ∈ ℝ)
203	121	abscld 15606	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (abs‘(𝑌 − 𝑍)) ∈ ℝ)
204	202, 203	remulcld 11339	. . . 4 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑀 · (abs‘(𝑌 − 𝑍))) ∈ ℝ)
205	194	fveq1d 6887	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡) = ((𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)))‘𝑡))
206		eqid 2761	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍))) = (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)))
207	206	fvmpt2 7005	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ (0(,)1) ∧ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)) ∈ V) → ((𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)))‘𝑡) = (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)))
208	196, 207	mpan2 704	. . . . . . . . . . 11 ⊢ (𝑡 ∈ (0(,)1) → ((𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)))‘𝑡) = (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)))
209	205, 208	sylan9eq 2816	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → ((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡) = (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍)))
210	209	fveq2d 6889	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) = (abs‘(((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍))))
211		dvfcn 26228	. . . . . . . . . . 11 ⊢ (ℂ D 𝐹):dom (ℂ D 𝐹)⟶ℂ
212	5	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 𝐵 ⊆ dom (ℂ D 𝐹))
213	212, 120	sseldd 3932	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) ∈ dom (ℂ D 𝐹))
214		ffvelcdm 7081	. . . . . . . . . . 11 ⊢ (((ℂ D 𝐹):dom (ℂ D 𝐹)⟶ℂ ∧ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) ∈ dom (ℂ D 𝐹)) → ((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ℂ)
215	211, 213, 214	sylancr 599	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → ((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ℂ)
216	215, 122	absmuld 15624	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘(((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌 − 𝑍))) = ((abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) · (abs‘(𝑌 − 𝑍))))
217	210, 216	eqtrd 2796	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) = ((abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) · (abs‘(𝑌 − 𝑍))))
218	215	abscld 15606	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) ∈ ℝ)
219	201	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 𝑀 ∈ ℝ)
220	122	abscld 15606	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘(𝑌 − 𝑍)) ∈ ℝ)
221	122	absge0d 15614	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 0 ≤ (abs‘(𝑌 − 𝑍)))
222		2fveq3 6890	. . . . . . . . . . 11 ⊢ (𝑦 = ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) → (abs‘((ℂ D 𝐹)‘𝑦)) = (abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))
223	222	breq1d 5113	. . . . . . . . . 10 ⊢ (𝑦 = ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) → ((abs‘((ℂ D 𝐹)‘𝑦)) ≤ 𝑀 ↔ (abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) ≤ 𝑀))
224		dvlipcn.l	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (abs‘((ℂ D 𝐹)‘𝑥)) ≤ 𝑀)
225	224	ralrimiva 3155	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (abs‘((ℂ D 𝐹)‘𝑥)) ≤ 𝑀)
226		2fveq3 6890	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (abs‘((ℂ D 𝐹)‘𝑥)) = (abs‘((ℂ D 𝐹)‘𝑦)))
227	226	breq1d 5113	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → ((abs‘((ℂ D 𝐹)‘𝑥)) ≤ 𝑀 ↔ (abs‘((ℂ D 𝐹)‘𝑦)) ≤ 𝑀))
228	227	cbvralvw 3241	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝐵 (abs‘((ℂ D 𝐹)‘𝑥)) ≤ 𝑀 ↔ ∀𝑦 ∈ 𝐵 (abs‘((ℂ D 𝐹)‘𝑦)) ≤ 𝑀)
229	225, 228	sylib 221	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑦 ∈ 𝐵 (abs‘((ℂ D 𝐹)‘𝑦)) ≤ 𝑀)
230	229	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → ∀𝑦 ∈ 𝐵 (abs‘((ℂ D 𝐹)‘𝑦)) ≤ 𝑀)
231	223, 230, 120	rspcdva 3578	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) ≤ 𝑀)
232	218, 219, 220, 221, 231	lemul1ad 12256	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → ((abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) · (abs‘(𝑌 − 𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
233	217, 232	eqbrtrd 5127	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
234	233	ralrimiva 3155	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ∀𝑡 ∈ (0(,)1)(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
235		nfv 1947	. . . . . . 7 ⊢ Ⅎ𝑧(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍)))
236		nfcv 2923	. . . . . . . . 9 ⊢ Ⅎ𝑡abs
237		nfcv 2923	. . . . . . . . . . 11 ⊢ Ⅎ𝑡ℝ
238		nfcv 2923	. . . . . . . . . . 11 ⊢ Ⅎ𝑡 D
239		nfmpt1 5204	. . . . . . . . . . 11 ⊢ Ⅎ𝑡(𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))
240	237, 238, 239	nfov 7450	. . . . . . . . . 10 ⊢ Ⅎ𝑡(ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))
241		nfcv 2923	. . . . . . . . . 10 ⊢ Ⅎ𝑡𝑧
242	240, 241	nffv 6895	. . . . . . . . 9 ⊢ Ⅎ𝑡((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)
243	236, 242	nffv 6895	. . . . . . . 8 ⊢ Ⅎ𝑡(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧))
244		nfcv 2923	. . . . . . . 8 ⊢ Ⅎ𝑡 ≤
245		nfcv 2923	. . . . . . . 8 ⊢ Ⅎ𝑡(𝑀 · (abs‘(𝑌 − 𝑍)))
246	243, 244, 245	nfbr 5152	. . . . . . 7 ⊢ Ⅎ𝑡(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍)))
247		2fveq3 6890	. . . . . . . 8 ⊢ (𝑡 = 𝑧 → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) = (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)))
248	247	breq1d 5113	. . . . . . 7 ⊢ (𝑡 = 𝑧 → ((abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))) ↔ (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍)))))
249	235, 246, 248	cbvralw 3305	. . . . . 6 ⊢ (∀𝑡 ∈ (0(,)1)(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))) ↔ ∀𝑧 ∈ (0(,)1)(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
250	234, 249	sylib 221	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ∀𝑧 ∈ (0(,)1)(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
251	250	r19.21bi 3255	. . . 4 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑧 ∈ (0(,)1)) → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
252	3, 4, 102, 200, 204, 251	dvlip 26313	. . 3 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (1 ∈ (0[,]1) ∧ 0 ∈ (0[,]1))) → (abs‘(((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘0))) ≤ ((𝑀 · (abs‘(𝑌 − 𝑍))) · (abs‘(1 − 0))))
253	1, 2, 252	mpanr12 718	. 2 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (abs‘(((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘0))) ≤ ((𝑀 · (abs‘(𝑌 − 𝑍))) · (abs‘(1 − 0))))
254		oveq2 7428	. . . . . . . . 9 ⊢ (𝑡 = 1 → (𝑌 · 𝑡) = (𝑌 · 1))
255		oveq2 7428	. . . . . . . . . . 11 ⊢ (𝑡 = 1 → (1 − 𝑡) = (1 − 1))
256		1m1e0 12415	. . . . . . . . . . 11 ⊢ (1 − 1) = 0
257	255, 256	eqtrdi 2812	. . . . . . . . . 10 ⊢ (𝑡 = 1 → (1 − 𝑡) = 0)
258	257	oveq2d 7436	. . . . . . . . 9 ⊢ (𝑡 = 1 → (𝑍 · (1 − 𝑡)) = (𝑍 · 0))
259	254, 258	oveq12d 7438	. . . . . . . 8 ⊢ (𝑡 = 1 → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) = ((𝑌 · 1) + (𝑍 · 0)))
260	259	fveq2d 6889	. . . . . . 7 ⊢ (𝑡 = 1 → (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) = (𝐹‘((𝑌 · 1) + (𝑍 · 0))))
261		eqid 2761	. . . . . . 7 ⊢ (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) = (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))
262		fvex 6898	. . . . . . 7 ⊢ (𝐹‘((𝑌 · 1) + (𝑍 · 0))) ∈ V
263	260, 261, 262	fvmpt 6993	. . . . . 6 ⊢ (1 ∈ (0[,]1) → ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘1) = (𝐹‘((𝑌 · 1) + (𝑍 · 0))))
264	1, 263	ax-mp 5	. . . . 5 ⊢ ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘1) = (𝐹‘((𝑌 · 1) + (𝑍 · 0)))
265	23	mul01d 11509	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑍 · 0) = 0)
266	143, 265	oveq12d 7438	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑌 · 1) + (𝑍 · 0)) = (𝑌 + 0))
267	14	addridd 11510	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 + 0) = 𝑌)
268	266, 267	eqtrd 2796	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑌 · 1) + (𝑍 · 0)) = 𝑌)
269	268	fveq2d 6889	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝐹‘((𝑌 · 1) + (𝑍 · 0))) = (𝐹‘𝑌))
270	264, 269	eqtrid 2808	. . . 4 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘1) = (𝐹‘𝑌))
271		oveq2 7428	. . . . . . . . 9 ⊢ (𝑡 = 0 → (𝑌 · 𝑡) = (𝑌 · 0))
272		oveq2 7428	. . . . . . . . . . 11 ⊢ (𝑡 = 0 → (1 − 𝑡) = (1 − 0))
273		1m0e1 12462	. . . . . . . . . . 11 ⊢ (1 − 0) = 1
274	272, 273	eqtrdi 2812	. . . . . . . . . 10 ⊢ (𝑡 = 0 → (1 − 𝑡) = 1)
275	274	oveq2d 7436	. . . . . . . . 9 ⊢ (𝑡 = 0 → (𝑍 · (1 − 𝑡)) = (𝑍 · 1))
276	271, 275	oveq12d 7438	. . . . . . . 8 ⊢ (𝑡 = 0 → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) = ((𝑌 · 0) + (𝑍 · 1)))
277	276	fveq2d 6889	. . . . . . 7 ⊢ (𝑡 = 0 → (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) = (𝐹‘((𝑌 · 0) + (𝑍 · 1))))
278		fvex 6898	. . . . . . 7 ⊢ (𝐹‘((𝑌 · 0) + (𝑍 · 1))) ∈ V
279	277, 261, 278	fvmpt 6993	. . . . . 6 ⊢ (0 ∈ (0[,]1) → ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘0) = (𝐹‘((𝑌 · 0) + (𝑍 · 1))))
280	2, 279	ax-mp 5	. . . . 5 ⊢ ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘0) = (𝐹‘((𝑌 · 0) + (𝑍 · 1)))
281	14	mul01d 11509	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 · 0) = 0)
282	23	mulridd 11326	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑍 · 1) = 𝑍)
283	281, 282	oveq12d 7438	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑌 · 0) + (𝑍 · 1)) = (0 + 𝑍))
284	23	addlidd 11511	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (0 + 𝑍) = 𝑍)
285	283, 284	eqtrd 2796	. . . . . 6 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑌 · 0) + (𝑍 · 1)) = 𝑍)
286	285	fveq2d 6889	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝐹‘((𝑌 · 0) + (𝑍 · 1))) = (𝐹‘𝑍))
287	280, 286	eqtrid 2808	. . . 4 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘0) = (𝐹‘𝑍))
288	270, 287	oveq12d 7438	. . 3 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘0)) = ((𝐹‘𝑌) − (𝐹‘𝑍)))
289	288	fveq2d 6889	. 2 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (abs‘(((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘0))) = (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))))
290	273	fveq2i 6888	. . . . 5 ⊢ (abs‘(1 − 0)) = (abs‘1)
291		abs1 15464	. . . . 5 ⊢ (abs‘1) = 1
292	290, 291	eqtri 2784	. . . 4 ⊢ (abs‘(1 − 0)) = 1
293	292	oveq2i 7431	. . 3 ⊢ ((𝑀 · (abs‘(𝑌 − 𝑍))) · (abs‘(1 − 0))) = ((𝑀 · (abs‘(𝑌 − 𝑍))) · 1)
294	204	recnd 11337	. . . 4 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑀 · (abs‘(𝑌 − 𝑍))) ∈ ℂ)
295	294	mulridd 11326	. . 3 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑀 · (abs‘(𝑌 − 𝑍))) · 1) = (𝑀 · (abs‘(𝑌 − 𝑍))))
296	293, 295	eqtrid 2808	. 2 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑀 · (abs‘(𝑌 − 𝑍))) · (abs‘(1 − 0))) = (𝑀 · (abs‘(𝑌 − 𝑍))))
297	253, 289, 296	3brtr3d 5136	1 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ∀wral 3077 Vcvv 3451 ∩ cin 3898 ⊆ wss 3899 {cpr 4586 class class class wbr 5103 ↦ cmpt 5186 dom cdm 5651 ran crn 5652 ↾ cres 5653 ∘ ccom 5655 ⟶wf 6534 ‘cfv 6538 (class class class)co 7420 ℂcc 11198 ℝcr 11199 0cc0 11200 1c1 11201 + caddc 11203 · cmul 11205 ℝ^*cxr 11342 ≤ cle 11344 − cmin 11541 -cneg 11542 (,)cioo 13476 [,]cicc 13479 abscabs 15401 TopOpenctopn 17592 topGenctg 17608 ∞Metcxmet 21663 ballcbl 21665 ℂ_fldccnfld 21678 Topctop 23211 intcnt 23335 Cn ccn 23542 ×_t ctx 23879 –cn→ccncf 25197 D cdv 26183

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 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7751 ax-cnex 11256 ax-resscn 11257 ax-1cn 11258 ax-icn 11259 ax-addcl 11260 ax-addrcl 11261 ax-mulcl 11262 ax-mulrcl 11263 ax-mulcom 11264 ax-addass 11265 ax-mulass 11266 ax-distr 11267 ax-i2m1 11268 ax-1ne0 11269 ax-1rid 11270 ax-rnegex 11271 ax-rrecex 11272 ax-cnre 11273 ax-pre-lttri 11274 ax-pre-lttrn 11275 ax-pre-ltadd 11276 ax-pre-mulgt0 11277 ax-pre-sup 11278 ax-addf 11279

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 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-of 7693 df-om 7878 df-1st 8001 df-2nd 8002 df-supp 8178 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418 df-1o 8476 df-2o 8477 df-er 8717 df-map 8849 df-pm 8850 df-ixp 8926 df-en 8974 df-dom 8975 df-sdom 8976 df-fin 8977 df-fsupp 9354 df-fi 9403 df-sup 9434 df-inf 9435 df-oi 9504 df-card 10020 df-pnf 11345 df-mnf 11346 df-xr 11347 df-ltxr 11348 df-le 11349 df-sub 11543 df-neg 11544 df-div 11974 df-nn 12336 df-2 12405 df-3 12406 df-4 12407 df-5 12408 df-6 12409 df-7 12410 df-8 12411 df-9 12412 df-n0 12607 df-z 12694 df-dec 12815 df-uz 12966 df-q 13076 df-rp 13121 df-xneg 13241 df-xadd 13242 df-xmul 13243 df-ioo 13480 df-ico 13482 df-icc 13483 df-fz 13640 df-fzo 13789 df-seq 14145 df-exp 14205 df-hash 14475 df-cj 15266 df-re 15267 df-im 15268 df-sqrt 15402 df-abs 15403 df-struct 17325 df-sets 17342 df-slot 17360 df-ndx 17372 df-base 17388 df-ress 17409 df-plusg 17441 df-mulr 17442 df-starv 17443 df-sca 17444 df-vsca 17445 df-ip 17446 df-tset 17447 df-ple 17448 df-ds 17450 df-unif 17451 df-hom 17452 df-cco 17453 df-rest 17593 df-topn 17594 df-0g 17612 df-gsum 17613 df-topgen 17614 df-pt 17615 df-prds 17618 df-xrs 17674 df-qtop 17679 df-imas 17680 df-xps 17682 df-mre 17756 df-mrc 17757 df-acs 17759 df-mgm 18816 df-sgrp 18908 df-mnd 18924 df-submnd 18979 df-mulg 19278 df-cntz 19531 df-cmn 19996 df-psmet 21670 df-xmet 21671 df-met 21672 df-bl 21673 df-mopn 21674 df-fbas 21675 df-fg 21676 df-cnfld 21679 df-top 23212 df-topon 23229 df-topsp 23251 df-bases 23264 df-cld 23337 df-ntr 23338 df-cls 23339 df-nei 23416 df-lp 23454 df-perf 23455 df-cn 23545 df-cnp 23546 df-haus 23633 df-cmp 23705 df-tx 23881 df-hmeo 24074 df-fil 24165 df-fm 24257 df-flim 24258 df-flf 24259 df-xms 24639 df-ms 24640 df-tms 24641 df-cncf 25199 df-limc 26186 df-dv 26187

This theorem is used by: dvlip2 26315 dv11cn 26321

W3C validator