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 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 cncfcdm ⊢ ( ( ℂ ⊆ ℂ ∧ ( ℝ 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 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
100 98 99 eleqtri ⊢ ( 𝐴 (,) 𝐵 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
101 100 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
102 7 recnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
103 40 101 102 dvmptconst ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐶 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 0 ) )
104 0cnd ⊢ ( 𝜑 → 0 ∈ ℂ )
105 75 104 70 constcncfg ⊢ ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 0 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
106 103 105 eqeltrd ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐶 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
107 40 56 59 97 106 dvsubcncf ⊢ ( 𝜑 → ( ℝ D ( ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ∘f − ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐶 ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
108 53 107 eqeltrd ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
109 40 101 dvmptidg ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑠 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) )
110 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
111 75 110 70 constcncfg ⊢ ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
112 109 111 eqeltrd ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑠 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
113 40 43 48 108 112 dvdivcncf ⊢ ( 𝜑 → ( ℝ D ( ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ∘f / ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑠 ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
114 38 113 eqeltrd ⊢ ( 𝜑 → ( ℝ D 𝐻 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
115 cncff ⊢ ( ( ℝ D 𝐻 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) → ( ℝ D 𝐻 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
116 fdm ⊢ ( ( ℝ D 𝐻 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ → dom ( ℝ D 𝐻 ) = ( 𝐴 (,) 𝐵 ) )
117 114 115 116 3syl ⊢ ( 𝜑 → dom ( ℝ D 𝐻 ) = ( 𝐴 (,) 𝐵 ) )
118 117 feq2d ⊢ ( 𝜑 → ( ( ℝ D 𝐻 ) : dom ( ℝ D 𝐻 ) ⟶ ℝ ↔ ( ℝ D 𝐻 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ) )
119 31 118 mpbid ⊢ ( 𝜑 → ( ℝ D 𝐻 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
120 cncfcdm ⊢ ( ( ℝ ⊆ ℂ ∧ ( ℝ D 𝐻 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) ) → ( ( ℝ D 𝐻 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) ↔ ( ℝ D 𝐻 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ) )
121 67 114 120 syl2anc ⊢ ( 𝜑 → ( ( ℝ D 𝐻 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) ↔ ( ℝ D 𝐻 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ) )
122 119 121 mpbird ⊢ ( 𝜑 → ( ℝ D 𝐻 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) )