Metamath Proof Explorer


Theorem fourierdlem59

Description: The derivative of H is continuous on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem59.f ( 𝜑𝐹 : ℝ ⟶ ℝ )
fourierdlem59.x ( 𝜑𝑋 ∈ ℝ )
fourierdlem59.a ( 𝜑𝐴 ∈ ℝ )
fourierdlem59.b ( 𝜑𝐵 ∈ ℝ )
fourierdlem59.n0 ( 𝜑 → ¬ 0 ∈ ( 𝐴 (,) 𝐵 ) )
fourierdlem59.fdv ( 𝜑 → ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ∈ ( ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) –cn→ ℝ ) )
fourierdlem59.c ( 𝜑𝐶 ∈ ℝ )
fourierdlem59.h 𝐻 = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) )
Assertion fourierdlem59 ( 𝜑 → ( ℝ D 𝐻 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) )

Proof

Step Hyp Ref Expression
1 fourierdlem59.f ( 𝜑𝐹 : ℝ ⟶ ℝ )
2 fourierdlem59.x ( 𝜑𝑋 ∈ ℝ )
3 fourierdlem59.a ( 𝜑𝐴 ∈ ℝ )
4 fourierdlem59.b ( 𝜑𝐵 ∈ ℝ )
5 fourierdlem59.n0 ( 𝜑 → ¬ 0 ∈ ( 𝐴 (,) 𝐵 ) )
6 fourierdlem59.fdv ( 𝜑 → ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ∈ ( ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) –cn→ ℝ ) )
7 fourierdlem59.c ( 𝜑𝐶 ∈ ℝ )
8 fourierdlem59.h 𝐻 = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) )
9 1 adantr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐹 : ℝ ⟶ ℝ )
10 2 adantr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑋 ∈ ℝ )
11 elioore ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → 𝑠 ∈ ℝ )
12 11 adantl ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ℝ )
13 10 12 readdcld ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝑠 ) ∈ ℝ )
14 9 13 ffvelrnd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℝ )
15 7 adantr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐶 ∈ ℝ )
16 14 15 resubcld ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ∈ ℝ )
17 eqcom ( 𝑠 = 0 ↔ 0 = 𝑠 )
18 17 biimpi ( 𝑠 = 0 → 0 = 𝑠 )
19 18 adantl ( ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝑠 = 0 ) → 0 = 𝑠 )
20 simpl ( ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝑠 = 0 ) → 𝑠 ∈ ( 𝐴 (,) 𝐵 ) )
21 19 20 eqeltrd ( ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝑠 = 0 ) → 0 ∈ ( 𝐴 (,) 𝐵 ) )
22 21 adantll ( ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑠 = 0 ) → 0 ∈ ( 𝐴 (,) 𝐵 ) )
23 5 ad2antrr ( ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑠 = 0 ) → ¬ 0 ∈ ( 𝐴 (,) 𝐵 ) )
24 22 23 pm2.65da ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ 𝑠 = 0 )
25 24 neqned ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ≠ 0 )
26 16 12 25 redivcld ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) ∈ ℝ )
27 26 8 fmptd ( 𝜑𝐻 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
28 ioossre ( 𝐴 (,) 𝐵 ) ⊆ ℝ
29 28 a1i ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℝ )
30 dvfre ( ( 𝐻 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℝ ) → ( ℝ D 𝐻 ) : dom ( ℝ D 𝐻 ) ⟶ ℝ )
31 27 29 30 syl2anc ( 𝜑 → ( ℝ D 𝐻 ) : dom ( ℝ D 𝐻 ) ⟶ ℝ )
32 ovex ( 𝐴 (,) 𝐵 ) ∈ V
33 32 a1i ( 𝜑 → ( 𝐴 (,) 𝐵 ) ∈ V )
34 eqidd ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) )
35 eqidd ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑠 ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑠 ) )
36 33 16 12 34 35 offval2 ( 𝜑 → ( ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ∘f / ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑠 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) ) )
37 8 36 eqtr4id ( 𝜑𝐻 = ( ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ∘f / ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑠 ) ) )
38 37 oveq2d ( 𝜑 → ( ℝ D 𝐻 ) = ( ℝ D ( ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ∘f / ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑠 ) ) ) )
39 reelprrecn ℝ ∈ { ℝ , ℂ }
40 39 a1i ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
41 16 recnd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ∈ ℂ )
42 eqid ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) )
43 41 42 fmptd ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
44 12 recnd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ℂ )
45 eldifsn ( 𝑠 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) )
46 44 25 45 sylanbrc ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ( ℂ ∖ { 0 } ) )
47 eqid ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑠 ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑠 )
48 46 47 fmptd ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑠 ) : ( 𝐴 (,) 𝐵 ) ⟶ ( ℂ ∖ { 0 } ) )
49 eqidd ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) )
50 eqidd ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐶 ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐶 ) )
51 33 14 15 49 50 offval2 ( 𝜑 → ( ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ∘f − ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐶 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) )
52 51 eqcomd ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) = ( ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ∘f − ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐶 ) ) )
53 52 oveq2d ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) = ( ℝ D ( ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ∘f − ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐶 ) ) ) )
54 14 recnd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℂ )
55 eqid ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) )
56 54 55 fmptd ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
57 15 recnd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐶 ∈ ℂ )
58 eqid ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐶 ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐶 )
59 57 58 fmptd ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐶 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
60 eqid ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) = ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) )
61 cncff ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ∈ ( ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) –cn→ ℝ ) → ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) : ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ⟶ ℝ )
62 6 61 syl ( 𝜑 → ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) : ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ⟶ ℝ )
63 1 2 3 4 60 62 fourierdlem28 ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ) )
64 ioosscn ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ⊆ ℂ
65 64 a1i ( 𝜑 → ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ⊆ ℂ )
66 ax-resscn ℝ ⊆ ℂ
67 66 a1i ( 𝜑 → ℝ ⊆ ℂ )
68 62 67 fssd ( 𝜑 → ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) : ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ⟶ ℂ )
69 ssid ℂ ⊆ ℂ
70 69 a1i ( 𝜑 → ℂ ⊆ ℂ )
71 cncffvrn ( ( ℂ ⊆ ℂ ∧ ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ∈ ( ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) –cn→ ℝ ) ) → ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ∈ ( ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) –cn→ ℂ ) ↔ ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) : ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ⟶ ℂ ) )
72 70 6 71 syl2anc ( 𝜑 → ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ∈ ( ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) –cn→ ℂ ) ↔ ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) : ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ⟶ ℂ ) )
73 68 72 mpbird ( 𝜑 → ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ∈ ( ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) –cn→ ℂ ) )
74 ioosscn ( 𝐴 (,) 𝐵 ) ⊆ ℂ
75 74 a1i ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℂ )
76 2 recnd ( 𝜑𝑋 ∈ ℂ )
77 2 3 readdcld ( 𝜑 → ( 𝑋 + 𝐴 ) ∈ ℝ )
78 77 rexrd ( 𝜑 → ( 𝑋 + 𝐴 ) ∈ ℝ* )
79 78 adantr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝐴 ) ∈ ℝ* )
80 2 4 readdcld ( 𝜑 → ( 𝑋 + 𝐵 ) ∈ ℝ )
81 80 rexrd ( 𝜑 → ( 𝑋 + 𝐵 ) ∈ ℝ* )
82 81 adantr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝐵 ) ∈ ℝ* )
83 3 adantr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 ∈ ℝ )
84 83 rexrd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 ∈ ℝ* )
85 4 rexrd ( 𝜑𝐵 ∈ ℝ* )
86 85 adantr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐵 ∈ ℝ* )
87 simpr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ( 𝐴 (,) 𝐵 ) )
88 ioogtlb ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 < 𝑠 )
89 84 86 87 88 syl3anc ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 < 𝑠 )
90 83 12 10 89 ltadd2dd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝐴 ) < ( 𝑋 + 𝑠 ) )
91 4 adantr ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐵 ∈ ℝ )
92 iooltub ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 < 𝐵 )
93 84 86 87 92 syl3anc ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 < 𝐵 )
94 12 91 10 93 ltadd2dd ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝑠 ) < ( 𝑋 + 𝐵 ) )
95 79 82 13 90 94 eliood ( ( 𝜑𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝑠 ) ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) )
96 65 73 75 76 95 fourierdlem23 ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
97 63 96 eqeltrd ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
98 iooretop ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) )
99 eqid ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
100 99 tgioo2 ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
101 98 100 eleqtri ( 𝐴 (,) 𝐵 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
102 101 a1i ( 𝜑 → ( 𝐴 (,) 𝐵 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
103 7 recnd ( 𝜑𝐶 ∈ ℂ )
104 40 102 103 dvmptconst ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐶 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 0 ) )
105 0cnd ( 𝜑 → 0 ∈ ℂ )
106 75 105 70 constcncfg ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 0 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
107 104 106 eqeltrd ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐶 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
108 40 56 59 97 107 dvsubcncf ( 𝜑 → ( ℝ D ( ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ∘f − ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐶 ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
109 53 108 eqeltrd ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
110 40 102 dvmptidg ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑠 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) )
111 1cnd ( 𝜑 → 1 ∈ ℂ )
112 75 111 70 constcncfg ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
113 110 112 eqeltrd ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑠 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
114 40 43 48 109 113 dvdivcncf ( 𝜑 → ( ℝ D ( ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ∘f / ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑠 ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
115 38 114 eqeltrd ( 𝜑 → ( ℝ D 𝐻 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
116 cncff ( ( ℝ D 𝐻 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) → ( ℝ D 𝐻 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
117 fdm ( ( ℝ D 𝐻 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ → dom ( ℝ D 𝐻 ) = ( 𝐴 (,) 𝐵 ) )
118 115 116 117 3syl ( 𝜑 → dom ( ℝ D 𝐻 ) = ( 𝐴 (,) 𝐵 ) )
119 118 feq2d ( 𝜑 → ( ( ℝ D 𝐻 ) : dom ( ℝ D 𝐻 ) ⟶ ℝ ↔ ( ℝ D 𝐻 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ) )
120 31 119 mpbid ( 𝜑 → ( ℝ D 𝐻 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
121 cncffvrn ( ( ℝ ⊆ ℂ ∧ ( ℝ D 𝐻 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) ) → ( ( ℝ D 𝐻 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) ↔ ( ℝ D 𝐻 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ) )
122 67 115 121 syl2anc ( 𝜑 → ( ( ℝ D 𝐻 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) ↔ ( ℝ D 𝐻 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ) )
123 120 122 mpbird ( 𝜑 → ( ℝ D 𝐻 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) )