Metamath Proof Explorer

Theorem fourierdlem72

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

Ref Expression
Hypotheses fourierdlem72.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
fourierdlem72.xre ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
fourierdlem72.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem72.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
fourierdlem72.v ⊢ ( 𝜑 → 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) )
fourierdlem72.dvcn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ℝ D 𝐹 ) ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℝ ) )
fourierdlem72.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
fourierdlem72.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
fourierdlem72.altb ⊢ ( 𝜑 → 𝐴 < 𝐵 )
fourierdlem72.ab ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( - π [,] π ) )
fourierdlem72.n0 ⊢ ( 𝜑 → ¬ 0 ∈ ( 𝐴 [,] 𝐵 ) )
fourierdlem72.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
fourierdlem72.q ⊢ 𝑄 = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
fourierdlem72.u ⊢ ( 𝜑 → 𝑈 ∈ ( 0 ..^ 𝑀 ) )
fourierdlem72.abss ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( ( 𝑄 ‘ 𝑈 ) (,) ( 𝑄 ‘ ( 𝑈 + 1 ) ) ) )
fourierdlem72.h ⊢ 𝐻 = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) )
fourierdlem72.k ⊢ 𝐾 = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
fourierdlem72.o ⊢ 𝑂 = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) )
Assertion fourierdlem72 ( 𝜑 → ( ℝ D 𝑂 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 fourierdlem72.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2 fourierdlem72.xre ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
3 fourierdlem72.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
4 fourierdlem72.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
5 fourierdlem72.v ⊢ ( 𝜑 → 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) )
6 fourierdlem72.dvcn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ℝ D 𝐹 ) ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℝ ) )
7 fourierdlem72.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
8 fourierdlem72.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
9 fourierdlem72.altb ⊢ ( 𝜑 → 𝐴 < 𝐵 )
10 fourierdlem72.ab ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( - π [,] π ) )
11 fourierdlem72.n0 ⊢ ( 𝜑 → ¬ 0 ∈ ( 𝐴 [,] 𝐵 ) )
12 fourierdlem72.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
13 fourierdlem72.q ⊢ 𝑄 = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
14 fourierdlem72.u ⊢ ( 𝜑 → 𝑈 ∈ ( 0 ..^ 𝑀 ) )
15 fourierdlem72.abss ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( ( 𝑄 ‘ 𝑈 ) (,) ( 𝑄 ‘ ( 𝑈 + 1 ) ) ) )
16 fourierdlem72.h ⊢ 𝐻 = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) )
17 fourierdlem72.k ⊢ 𝐾 = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
18 fourierdlem72.o ⊢ 𝑂 = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) )
19 ovex ⊢ ( 𝐴 (,) 𝐵 ) ∈ V
20 19 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ∈ V )
21 1 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐹 : ℝ ⟶ ℝ )
22 2 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑋 ∈ ℝ )
23 elioore ⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → 𝑠 ∈ ℝ )
24 23 adantl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ℝ )
25 22 24 readdcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝑠 ) ∈ ℝ )
26 21 25 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℝ )
27 12 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐶 ∈ ℝ )
28 26 27 resubcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ∈ ℝ )
29 ioossicc ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
30 29 sseli ⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → 𝑠 ∈ ( 𝐴 [,] 𝐵 ) )
31 30 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑠 ≠ 0 ) → 𝑠 ∈ ( 𝐴 [,] 𝐵 ) )
32 id ⊢ ( 𝑠 ≠ 0 → 𝑠 ≠ 0 )
33 32 necon1bi ⊢ ( ¬ 𝑠 ≠ 0 → 𝑠 = 0 )
34 33 eleq1d ⊢ ( ¬ 𝑠 ≠ 0 → ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↔ 0 ∈ ( 𝐴 [,] 𝐵 ) ) )
35 34 adantl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑠 ≠ 0 ) → ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↔ 0 ∈ ( 𝐴 [,] 𝐵 ) ) )
36 31 35 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑠 ≠ 0 ) → 0 ∈ ( 𝐴 [,] 𝐵 ) )
37 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ¬ 𝑠 ≠ 0 ) → ¬ 0 ∈ ( 𝐴 [,] 𝐵 ) )
38 36 37 condan ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ≠ 0 )
39 28 24 38 redivcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) ∈ ℝ )
40 39 16 fmptd ⊢ ( 𝜑 → 𝐻 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
41 40 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐻 ‘ 𝑠 ) ∈ ℝ )
42 2re ⊢ 2 ∈ ℝ
43 42 a1i ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 2 ∈ ℝ )
44 24 rehalfcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑠 / 2 ) ∈ ℝ )
45 44 resincld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℝ )
46 43 45 remulcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℝ )
47 2cnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 2 ∈ ℂ )
48 24 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ℂ )
49 48 halfcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑠 / 2 ) ∈ ℂ )
50 49 sincld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℂ )
51 2ne0 ⊢ 2 ≠ 0
52 51 a1i ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 2 ≠ 0 )
53 10 sselda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ( - π [,] π ) )
54 fourierdlem44 ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ 𝑠 ≠ 0 ) → ( sin ‘ ( 𝑠 / 2 ) ) ≠ 0 )
55 53 38 54 syl2anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( sin ‘ ( 𝑠 / 2 ) ) ≠ 0 )
56 47 50 52 55 mulne0d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ≠ 0 )
57 24 46 56 redivcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ∈ ℝ )
58 57 17 fmptd ⊢ ( 𝜑 → 𝐾 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
59 58 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐾 ‘ 𝑠 ) ∈ ℝ )
60 40 feqmptd ⊢ ( 𝜑 → 𝐻 = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐻 ‘ 𝑠 ) ) )
61 58 feqmptd ⊢ ( 𝜑 → 𝐾 = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐾 ‘ 𝑠 ) ) )
62 20 41 59 60 61 offval2 ⊢ ( 𝜑 → ( 𝐻 ∘f · 𝐾 ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) ) )
63 18 62 eqtr4id ⊢ ( 𝜑 → 𝑂 = ( 𝐻 ∘f · 𝐾 ) )
64 63 oveq2d ⊢ ( 𝜑 → ( ℝ D 𝑂 ) = ( ℝ D ( 𝐻 ∘f · 𝐾 ) ) )
65 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
66 65 a1i ⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
67 26 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℂ )
68 12 recnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
69 68 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐶 ∈ ℂ )
70 67 69 subcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ∈ ℂ )
71 ioossre ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
72 71 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℝ )
73 72 sselda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ℝ )
74 73 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ℂ )
75 70 74 38 divcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) ∈ ℂ )
76 75 16 fmptd ⊢ ( 𝜑 → 𝐻 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
77 74 halfcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑠 / 2 ) ∈ ℂ )
78 77 sincld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℂ )
79 47 78 mulcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℂ )
80 74 79 56 divcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ∈ ℂ )
81 80 17 fmptd ⊢ ( 𝜑 → 𝐾 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
82 ax-resscn ⊢ ℝ ⊆ ℂ
83 82 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
84 ssid ⊢ ℂ ⊆ ℂ
85 84 a1i ⊢ ( 𝜑 → ℂ ⊆ ℂ )
86 cncfss ⊢ ( ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) ⊆ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
87 83 85 86 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) ⊆ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
88 38 nelrdva ⊢ ( 𝜑 → ¬ 0 ∈ ( 𝐴 (,) 𝐵 ) )
89 1 83 fssd ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ )
90 ssid ⊢ ℝ ⊆ ℝ
91 90 a1i ⊢ ( 𝜑 → ℝ ⊆ ℝ )
92 ioossre ⊢ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ⊆ ℝ
93 92 a1i ⊢ ( 𝜑 → ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ⊆ ℝ )
94 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
95 94 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
96 94 95 dvres ⊢ ( ( ( ℝ ⊆ ℂ ∧ 𝐹 : ℝ ⟶ ℂ ) ∧ ( ℝ ⊆ ℝ ∧ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ⊆ ℝ ) ) → ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) )
97 83 89 91 93 96 syl22anc ⊢ ( 𝜑 → ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) )
98 ioontr ⊢ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) = ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) )
99 98 reseq2i ⊢ ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) )
100 97 99 eqtrdi ⊢ ( 𝜑 → ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) )
101 3 fourierdlem2 ⊢ ( 𝑀 ∈ ℕ → ( 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑉 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ) )
102 4 101 syl ⊢ ( 𝜑 → ( 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑉 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ) )
103 5 102 mpbid ⊢ ( 𝜑 → ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑉 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) )
104 103 simpld ⊢ ( 𝜑 → 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) )
105 elmapi ⊢ ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) → 𝑉 : ( 0 ... 𝑀 ) ⟶ ℝ )
106 104 105 syl ⊢ ( 𝜑 → 𝑉 : ( 0 ... 𝑀 ) ⟶ ℝ )
107 elfzofz ⊢ ( 𝑈 ∈ ( 0 ..^ 𝑀 ) → 𝑈 ∈ ( 0 ... 𝑀 ) )
108 14 107 syl ⊢ ( 𝜑 → 𝑈 ∈ ( 0 ... 𝑀 ) )
109 106 108 ffvelrnd ⊢ ( 𝜑 → ( 𝑉 ‘ 𝑈 ) ∈ ℝ )
110 109 rexrd ⊢ ( 𝜑 → ( 𝑉 ‘ 𝑈 ) ∈ ℝ* )
111 fzofzp1 ⊢ ( 𝑈 ∈ ( 0 ..^ 𝑀 ) → ( 𝑈 + 1 ) ∈ ( 0 ... 𝑀 ) )
112 14 111 syl ⊢ ( 𝜑 → ( 𝑈 + 1 ) ∈ ( 0 ... 𝑀 ) )
113 106 112 ffvelrnd ⊢ ( 𝜑 → ( 𝑉 ‘ ( 𝑈 + 1 ) ) ∈ ℝ )
114 113 rexrd ⊢ ( 𝜑 → ( 𝑉 ‘ ( 𝑈 + 1 ) ) ∈ ℝ* )
115 pire ⊢ π ∈ ℝ
116 115 a1i ⊢ ( 𝜑 → π ∈ ℝ )
117 116 renegcld ⊢ ( 𝜑 → - π ∈ ℝ )
118 117 116 2 3 4 5 108 13 fourierdlem13 ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑈 ) = ( ( 𝑉 ‘ 𝑈 ) − 𝑋 ) ∧ ( 𝑉 ‘ 𝑈 ) = ( 𝑋 + ( 𝑄 ‘ 𝑈 ) ) ) )
119 118 simprd ⊢ ( 𝜑 → ( 𝑉 ‘ 𝑈 ) = ( 𝑋 + ( 𝑄 ‘ 𝑈 ) ) )
120 118 simpld ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑈 ) = ( ( 𝑉 ‘ 𝑈 ) − 𝑋 ) )
121 109 2 resubcld ⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝑈 ) − 𝑋 ) ∈ ℝ )
122 120 121 eqeltrd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑈 ) ∈ ℝ )
123 117 116 2 3 4 5 112 13 fourierdlem13 ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑈 + 1 ) ) = ( ( 𝑉 ‘ ( 𝑈 + 1 ) ) − 𝑋 ) ∧ ( 𝑉 ‘ ( 𝑈 + 1 ) ) = ( 𝑋 + ( 𝑄 ‘ ( 𝑈 + 1 ) ) ) ) )
124 123 simpld ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑈 + 1 ) ) = ( ( 𝑉 ‘ ( 𝑈 + 1 ) ) − 𝑋 ) )
125 113 2 resubcld ⊢ ( 𝜑 → ( ( 𝑉 ‘ ( 𝑈 + 1 ) ) − 𝑋 ) ∈ ℝ )
126 124 125 eqeltrd ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑈 + 1 ) ) ∈ ℝ )
127 122 126 7 8 9 15 fourierdlem10 ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑈 ) ≤ 𝐴 ∧ 𝐵 ≤ ( 𝑄 ‘ ( 𝑈 + 1 ) ) ) )
128 127 simpld ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑈 ) ≤ 𝐴 )
129 122 7 2 128 leadd2dd ⊢ ( 𝜑 → ( 𝑋 + ( 𝑄 ‘ 𝑈 ) ) ≤ ( 𝑋 + 𝐴 ) )
130 119 129 eqbrtrd ⊢ ( 𝜑 → ( 𝑉 ‘ 𝑈 ) ≤ ( 𝑋 + 𝐴 ) )
131 127 simprd ⊢ ( 𝜑 → 𝐵 ≤ ( 𝑄 ‘ ( 𝑈 + 1 ) ) )
132 8 126 2 131 leadd2dd ⊢ ( 𝜑 → ( 𝑋 + 𝐵 ) ≤ ( 𝑋 + ( 𝑄 ‘ ( 𝑈 + 1 ) ) ) )
133 123 simprd ⊢ ( 𝜑 → ( 𝑉 ‘ ( 𝑈 + 1 ) ) = ( 𝑋 + ( 𝑄 ‘ ( 𝑈 + 1 ) ) ) )
134 132 133 breqtrrd ⊢ ( 𝜑 → ( 𝑋 + 𝐵 ) ≤ ( 𝑉 ‘ ( 𝑈 + 1 ) ) )
135 ioossioo ⊢ ( ( ( ( 𝑉 ‘ 𝑈 ) ∈ ℝ* ∧ ( 𝑉 ‘ ( 𝑈 + 1 ) ) ∈ ℝ* ) ∧ ( ( 𝑉 ‘ 𝑈 ) ≤ ( 𝑋 + 𝐴 ) ∧ ( 𝑋 + 𝐵 ) ≤ ( 𝑉 ‘ ( 𝑈 + 1 ) ) ) ) → ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ⊆ ( ( 𝑉 ‘ 𝑈 ) (,) ( 𝑉 ‘ ( 𝑈 + 1 ) ) ) )
136 110 114 130 134 135 syl22anc ⊢ ( 𝜑 → ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ⊆ ( ( 𝑉 ‘ 𝑈 ) (,) ( 𝑉 ‘ ( 𝑈 + 1 ) ) ) )
137 136 resabs1d ⊢ ( 𝜑 → ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑉 ‘ 𝑈 ) (,) ( 𝑉 ‘ ( 𝑈 + 1 ) ) ) ) ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) )
138 137 eqcomd ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) = ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑉 ‘ 𝑈 ) (,) ( 𝑉 ‘ ( 𝑈 + 1 ) ) ) ) ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) )
139 14 ancli ⊢ ( 𝜑 → ( 𝜑 ∧ 𝑈 ∈ ( 0 ..^ 𝑀 ) ) )
140 eleq1 ⊢ ( 𝑖 = 𝑈 → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↔ 𝑈 ∈ ( 0 ..^ 𝑀 ) ) )
141 140 anbi2d ⊢ ( 𝑖 = 𝑈 → ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ↔ ( 𝜑 ∧ 𝑈 ∈ ( 0 ..^ 𝑀 ) ) ) )
142 fveq2 ⊢ ( 𝑖 = 𝑈 → ( 𝑉 ‘ 𝑖 ) = ( 𝑉 ‘ 𝑈 ) )
143 oveq1 ⊢ ( 𝑖 = 𝑈 → ( 𝑖 + 1 ) = ( 𝑈 + 1 ) )
144 143 fveq2d ⊢ ( 𝑖 = 𝑈 → ( 𝑉 ‘ ( 𝑖 + 1 ) ) = ( 𝑉 ‘ ( 𝑈 + 1 ) ) )
145 142 144 oveq12d ⊢ ( 𝑖 = 𝑈 → ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑉 ‘ 𝑈 ) (,) ( 𝑉 ‘ ( 𝑈 + 1 ) ) ) )
146 145 reseq2d ⊢ ( 𝑖 = 𝑈 → ( ( ℝ D 𝐹 ) ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( 𝑉 ‘ 𝑈 ) (,) ( 𝑉 ‘ ( 𝑈 + 1 ) ) ) ) )
147 145 oveq1d ⊢ ( 𝑖 = 𝑈 → ( ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℝ ) = ( ( ( 𝑉 ‘ 𝑈 ) (,) ( 𝑉 ‘ ( 𝑈 + 1 ) ) ) –cn→ ℝ ) )
148 146 147 eleq12d ⊢ ( 𝑖 = 𝑈 → ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℝ ) ↔ ( ( ℝ D 𝐹 ) ↾ ( ( 𝑉 ‘ 𝑈 ) (,) ( 𝑉 ‘ ( 𝑈 + 1 ) ) ) ) ∈ ( ( ( 𝑉 ‘ 𝑈 ) (,) ( 𝑉 ‘ ( 𝑈 + 1 ) ) ) –cn→ ℝ ) ) )
149 141 148 imbi12d ⊢ ( 𝑖 = 𝑈 → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ℝ D 𝐹 ) ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℝ ) ) ↔ ( ( 𝜑 ∧ 𝑈 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ℝ D 𝐹 ) ↾ ( ( 𝑉 ‘ 𝑈 ) (,) ( 𝑉 ‘ ( 𝑈 + 1 ) ) ) ) ∈ ( ( ( 𝑉 ‘ 𝑈 ) (,) ( 𝑉 ‘ ( 𝑈 + 1 ) ) ) –cn→ ℝ ) ) ) )
150 149 6 vtoclg ⊢ ( 𝑈 ∈ ( 0 ..^ 𝑀 ) → ( ( 𝜑 ∧ 𝑈 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ℝ D 𝐹 ) ↾ ( ( 𝑉 ‘ 𝑈 ) (,) ( 𝑉 ‘ ( 𝑈 + 1 ) ) ) ) ∈ ( ( ( 𝑉 ‘ 𝑈 ) (,) ( 𝑉 ‘ ( 𝑈 + 1 ) ) ) –cn→ ℝ ) ) )
151 14 139 150 sylc ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( ( 𝑉 ‘ 𝑈 ) (,) ( 𝑉 ‘ ( 𝑈 + 1 ) ) ) ) ∈ ( ( ( 𝑉 ‘ 𝑈 ) (,) ( 𝑉 ‘ ( 𝑈 + 1 ) ) ) –cn→ ℝ ) )
152 rescncf ⊢ ( ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ⊆ ( ( 𝑉 ‘ 𝑈 ) (,) ( 𝑉 ‘ ( 𝑈 + 1 ) ) ) → ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑉 ‘ 𝑈 ) (,) ( 𝑉 ‘ ( 𝑈 + 1 ) ) ) ) ∈ ( ( ( 𝑉 ‘ 𝑈 ) (,) ( 𝑉 ‘ ( 𝑈 + 1 ) ) ) –cn→ ℝ ) → ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑉 ‘ 𝑈 ) (,) ( 𝑉 ‘ ( 𝑈 + 1 ) ) ) ) ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ∈ ( ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) –cn→ ℝ ) ) )
153 136 151 152 sylc ⊢ ( 𝜑 → ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑉 ‘ 𝑈 ) (,) ( 𝑉 ‘ ( 𝑈 + 1 ) ) ) ) ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ∈ ( ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) –cn→ ℝ ) )
154 138 153 eqeltrd ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ∈ ( ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) –cn→ ℝ ) )
155 100 154 eqeltrd ⊢ ( 𝜑 → ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) ∈ ( ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) –cn→ ℝ ) )
156 1 2 7 8 88 155 12 16 fourierdlem59 ⊢ ( 𝜑 → ( ℝ D 𝐻 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) )
157 87 156 sseldd ⊢ ( 𝜑 → ( ℝ D 𝐻 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
158 iooretop ⊢ ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) )
159 158 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) ) )
160 17 10 88 159 fourierdlem58 ⊢ ( 𝜑 → ( ℝ D 𝐾 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) )
161 87 160 sseldd ⊢ ( 𝜑 → ( ℝ D 𝐾 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
162 66 76 81 157 161 dvmulcncf ⊢ ( 𝜑 → ( ℝ D ( 𝐻 ∘f · 𝐾 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
163 64 162 eqeltrd ⊢ ( 𝜑 → ( ℝ D 𝑂 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )