Metamath Proof Explorer

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 cncffvrn ⊢ ( ( 𝐵 ⊆ ℂ ∧ ( 𝑡 ∈ ( 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 syl5eq ⊢ ( 𝜑 → 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 ffvelrnd ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑡 ∈ ( 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 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
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 mulid1d ⊢ ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑌 · 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 ffvelrn ⊢ ( ( ( ℂ 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 addid1d ⊢ ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑌 + 0 ) = 𝑌 )
268 266 267 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑌 · 1 ) + ( 𝑍 · 0 ) ) = 𝑌 )
269 268 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( ( 𝑌 · 1 ) + ( 𝑍 · 0 ) ) ) = ( 𝐹 ‘ 𝑌 ) )
270 264 269 syl5eq ⊢ ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑡 ∈ ( 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 mulid1d ⊢ ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑍 · 1 ) = 𝑍 )
283 281 282 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑌 · 0 ) + ( 𝑍 · 1 ) ) = ( 0 + 𝑍 ) )
284 28 addid2d ⊢ ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 0 + 𝑍 ) = 𝑍 )
285 283 284 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑌 · 0 ) + ( 𝑍 · 1 ) ) = 𝑍 )
286 285 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( ( 𝑌 · 0 ) + ( 𝑍 · 1 ) ) ) = ( 𝐹 ‘ 𝑍 ) )
287 280 286 syl5eq ⊢ ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑡 ∈ ( 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 mulid1d ⊢ ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑀 · ( abs ‘ ( 𝑌 − 𝑍 ) ) ) · 1 ) = ( 𝑀 · ( abs ‘ ( 𝑌 − 𝑍 ) ) ) )
296 293 295 syl5eq ⊢ ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑀 · ( abs ‘ ( 𝑌 − 𝑍 ) ) ) · ( abs ‘ ( 1 − 0 ) ) ) = ( 𝑀 · ( abs ‘ ( 𝑌 − 𝑍 ) ) ) )
297 253 289 296 3brtr3d ⊢ ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑍 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑌 − 𝑍 ) ) ) )