This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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