Metamath Proof Explorer

Theorem fourierdlem85

Description: Limit of the function G at the lower bounds of the partition intervals. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem85.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem85.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
fourierdlem85.x ⊢ ( 𝜑 → 𝑋 ∈ ran 𝑉 )
fourierdlem85.y ⊢ ( 𝜑 → 𝑌 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) )
fourierdlem85.w ⊢ ( 𝜑 → 𝑊 ∈ ℝ )
fourierdlem85.h ⊢ 𝐻 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) )
fourierdlem85.k ⊢ 𝐾 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
fourierdlem85.u ⊢ 𝑈 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) )
fourierdlem85.n ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
fourierdlem85.s ⊢ 𝑆 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) )
fourierdlem85.g ⊢ 𝐺 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) )
fourierdlem85.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
fourierdlem85.v ⊢ ( 𝜑 → 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) )
fourierdlem85.r ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ 𝑖 ) ) )
fourierdlem85.q ⊢ 𝑄 = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
fourierdlem85.o ⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑚 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem85.i ⊢ 𝐼 = ( ℝ D 𝐹 )
fourierdlem85.ifn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐼 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
fourierdlem85.e ⊢ ( 𝜑 → 𝐸 ∈ ( ( 𝐼 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) )
fourierdlem85.a ⊢ 𝐴 = ( ( if ( ( 𝑉 ‘ 𝑖 ) = 𝑋 , 𝐸 , ( ( 𝑅 − if ( ( 𝑉 ‘ 𝑖 ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ 𝑖 ) ) ) · ( 𝐾 ‘ ( 𝑄 ‘ 𝑖 ) ) ) · ( 𝑆 ‘ ( 𝑄 ‘ 𝑖 ) ) )
Assertion fourierdlem85 ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐴 ∈ ( ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem85.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
2 fourierdlem85.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
3 fourierdlem85.x ⊢ ( 𝜑 → 𝑋 ∈ ran 𝑉 )
4 fourierdlem85.y ⊢ ( 𝜑 → 𝑌 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) )
5 fourierdlem85.w ⊢ ( 𝜑 → 𝑊 ∈ ℝ )
6 fourierdlem85.h ⊢ 𝐻 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) )
7 fourierdlem85.k ⊢ 𝐾 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
8 fourierdlem85.u ⊢ 𝑈 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) )
9 fourierdlem85.n ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
10 fourierdlem85.s ⊢ 𝑆 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) )
11 fourierdlem85.g ⊢ 𝐺 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) )
12 fourierdlem85.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
13 fourierdlem85.v ⊢ ( 𝜑 → 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) )
14 fourierdlem85.r ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ 𝑖 ) ) )
15 fourierdlem85.q ⊢ 𝑄 = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
16 fourierdlem85.o ⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑚 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
17 fourierdlem85.i ⊢ 𝐼 = ( ℝ D 𝐹 )
18 fourierdlem85.ifn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐼 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
19 fourierdlem85.e ⊢ ( 𝜑 → 𝐸 ∈ ( ( 𝐼 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) )
20 fourierdlem85.a ⊢ 𝐴 = ( ( if ( ( 𝑉 ‘ 𝑖 ) = 𝑋 , 𝐸 , ( ( 𝑅 − if ( ( 𝑉 ‘ 𝑖 ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ 𝑖 ) ) ) · ( 𝐾 ‘ ( 𝑄 ‘ 𝑖 ) ) ) · ( 𝑆 ‘ ( 𝑄 ‘ 𝑖 ) ) )
21 eqid ⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑈 ‘ 𝑠 ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑈 ‘ 𝑠 ) )
22 eqid ⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑆 ‘ 𝑠 ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑆 ‘ 𝑠 ) )
23 eqid ⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) )
24 pire ⊢ π ∈ ℝ
25 24 renegcli ⊢ - π ∈ ℝ
26 25 rexri ⊢ - π ∈ ℝ*
27 26 a1i ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → - π ∈ ℝ* )
28 24 rexri ⊢ π ∈ ℝ*
29 28 a1i ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → π ∈ ℝ* )
30 24 a1i ⊢ ( 𝜑 → π ∈ ℝ )
31 30 renegcld ⊢ ( 𝜑 → - π ∈ ℝ )
32 1 fourierdlem2 ⊢ ( 𝑀 ∈ ℕ → ( 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑉 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ) )
33 12 32 syl ⊢ ( 𝜑 → ( 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑉 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ) )
34 13 33 mpbid ⊢ ( 𝜑 → ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑉 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) )
35 34 simpld ⊢ ( 𝜑 → 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) )
36 elmapi ⊢ ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) → 𝑉 : ( 0 ... 𝑀 ) ⟶ ℝ )
37 frn ⊢ ( 𝑉 : ( 0 ... 𝑀 ) ⟶ ℝ → ran 𝑉 ⊆ ℝ )
38 35 36 37 3syl ⊢ ( 𝜑 → ran 𝑉 ⊆ ℝ )
39 38 3 sseldd ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
40 31 30 39 1 16 12 13 15 fourierdlem14 ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑂 ‘ 𝑀 ) )
41 16 12 40 fourierdlem15 ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( - π [,] π ) )
42 41 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( - π [,] π ) )
43 42 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( - π [,] π ) )
44 simplr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
45 27 29 43 44 fourierdlem8 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑄 ‘ 𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( - π [,] π ) )
46 ioossicc ⊢ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
47 46 sseli ⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
48 47 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
49 45 48 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ( - π [,] π ) )
50 ioossre ⊢ ( 𝑋 (,) +∞ ) ⊆ ℝ
51 50 a1i ⊢ ( 𝜑 → ( 𝑋 (,) +∞ ) ⊆ ℝ )
52 2 51 fssresd ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) : ( 𝑋 (,) +∞ ) ⟶ ℝ )
53 ax-resscn ⊢ ℝ ⊆ ℂ
54 51 53 sstrdi ⊢ ( 𝜑 → ( 𝑋 (,) +∞ ) ⊆ ℂ )
55 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
56 pnfxr ⊢ +∞ ∈ ℝ*
57 56 a1i ⊢ ( 𝜑 → +∞ ∈ ℝ* )
58 39 ltpnfd ⊢ ( 𝜑 → 𝑋 < +∞ )
59 55 57 39 58 lptioo1cn ⊢ ( 𝜑 → 𝑋 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑋 (,) +∞ ) ) )
60 52 54 59 4 limcrecl ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
61 2 39 60 5 6 fourierdlem9 ⊢ ( 𝜑 → 𝐻 : ( - π [,] π ) ⟶ ℝ )
62 53 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
63 61 62 fssd ⊢ ( 𝜑 → 𝐻 : ( - π [,] π ) ⟶ ℂ )
64 63 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝐻 : ( - π [,] π ) ⟶ ℂ )
65 64 49 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐻 ‘ 𝑠 ) ∈ ℂ )
66 7 fourierdlem43 ⊢ 𝐾 : ( - π [,] π ) ⟶ ℝ
67 66 a1i ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝐾 : ( - π [,] π ) ⟶ ℝ )
68 67 49 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐾 ‘ 𝑠 ) ∈ ℝ )
69 68 recnd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐾 ‘ 𝑠 ) ∈ ℂ )
70 65 69 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) ∈ ℂ )
71 8 fvmpt2 ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) ∈ ℂ ) → ( 𝑈 ‘ 𝑠 ) = ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) )
72 49 70 71 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑈 ‘ 𝑠 ) = ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) )
73 72 70 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑈 ‘ 𝑠 ) ∈ ℂ )
74 9 10 fourierdlem18 ⊢ ( 𝜑 → 𝑆 ∈ ( ( - π [,] π ) –cn→ ℝ ) )
75 cncff ⊢ ( 𝑆 ∈ ( ( - π [,] π ) –cn→ ℝ ) → 𝑆 : ( - π [,] π ) ⟶ ℝ )
76 74 75 syl ⊢ ( 𝜑 → 𝑆 : ( - π [,] π ) ⟶ ℝ )
77 76 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑆 : ( - π [,] π ) ⟶ ℝ )
78 77 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑆 : ( - π [,] π ) ⟶ ℝ )
79 78 49 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑆 ‘ 𝑠 ) ∈ ℝ )
80 79 recnd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑆 ‘ 𝑠 ) ∈ ℂ )
81 eqid ⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐻 ‘ 𝑠 ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐻 ‘ 𝑠 ) )
82 eqid ⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐾 ‘ 𝑠 ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐾 ‘ 𝑠 ) )
83 eqid ⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) )
84 eqid ⊢ if ( ( 𝑉 ‘ 𝑖 ) = 𝑋 , 𝐸 , ( ( 𝑅 − if ( ( 𝑉 ‘ 𝑖 ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ 𝑖 ) ) ) = if ( ( 𝑉 ‘ 𝑖 ) = 𝑋 , 𝐸 , ( ( 𝑅 − if ( ( 𝑉 ‘ 𝑖 ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ 𝑖 ) ) )
85 39 1 2 3 4 5 6 12 13 14 15 16 17 18 19 84 fourierdlem75 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → if ( ( 𝑉 ‘ 𝑖 ) = 𝑋 , 𝐸 , ( ( 𝑅 − if ( ( 𝑉 ‘ 𝑖 ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ 𝑖 ) ) ) ∈ ( ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
86 61 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐻 : ( - π [,] π ) ⟶ ℝ )
87 26 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → - π ∈ ℝ* )
88 28 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → π ∈ ℝ* )
89 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
90 87 88 42 89 fourierdlem8 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( - π [,] π ) )
91 46 90 sstrid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( - π [,] π ) )
92 86 91 feqresmpt ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐻 ‘ 𝑠 ) ) )
93 92 oveq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) = ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐻 ‘ 𝑠 ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
94 85 93 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → if ( ( 𝑉 ‘ 𝑖 ) = 𝑋 , 𝐸 , ( ( 𝑅 − if ( ( 𝑉 ‘ 𝑖 ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ 𝑖 ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐻 ‘ 𝑠 ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
95 limcresi ⊢ ( 𝐾 limℂ ( 𝑄 ‘ 𝑖 ) ) ⊆ ( ( 𝐾 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) )
96 ssid ⊢ ℂ ⊆ ℂ
97 cncfss ⊢ ( ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( - π [,] π ) –cn→ ℝ ) ⊆ ( ( - π [,] π ) –cn→ ℂ ) )
98 53 96 97 mp2an ⊢ ( ( - π [,] π ) –cn→ ℝ ) ⊆ ( ( - π [,] π ) –cn→ ℂ )
99 7 fourierdlem62 ⊢ 𝐾 ∈ ( ( - π [,] π ) –cn→ ℝ )
100 98 99 sselii ⊢ 𝐾 ∈ ( ( - π [,] π ) –cn→ ℂ )
101 100 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐾 ∈ ( ( - π [,] π ) –cn→ ℂ ) )
102 elfzofz ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
103 102 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
104 42 103 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ( - π [,] π ) )
105 101 104 cnlimci ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐾 ‘ ( 𝑄 ‘ 𝑖 ) ) ∈ ( 𝐾 limℂ ( 𝑄 ‘ 𝑖 ) ) )
106 95 105 sselid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐾 ‘ ( 𝑄 ‘ 𝑖 ) ) ∈ ( ( 𝐾 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
107 cncff ⊢ ( 𝐾 ∈ ( ( - π [,] π ) –cn→ ℂ ) → 𝐾 : ( - π [,] π ) ⟶ ℂ )
108 100 107 mp1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐾 : ( - π [,] π ) ⟶ ℂ )
109 108 91 feqresmpt ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐾 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐾 ‘ 𝑠 ) ) )
110 109 oveq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐾 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) = ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐾 ‘ 𝑠 ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
111 106 110 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐾 ‘ ( 𝑄 ‘ 𝑖 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐾 ‘ 𝑠 ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
112 81 82 83 65 69 94 111 mullimc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( if ( ( 𝑉 ‘ 𝑖 ) = 𝑋 , 𝐸 , ( ( 𝑅 − if ( ( 𝑉 ‘ 𝑖 ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ 𝑖 ) ) ) · ( 𝐾 ‘ ( 𝑄 ‘ 𝑖 ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
113 72 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑈 ‘ 𝑠 ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) ) )
114 113 oveq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑈 ‘ 𝑠 ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) = ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
115 112 114 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( if ( ( 𝑉 ‘ 𝑖 ) = 𝑋 , 𝐸 , ( ( 𝑅 − if ( ( 𝑉 ‘ 𝑖 ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ 𝑖 ) ) ) · ( 𝐾 ‘ ( 𝑄 ‘ 𝑖 ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑈 ‘ 𝑠 ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
116 limcresi ⊢ ( 𝑆 limℂ ( 𝑄 ‘ 𝑖 ) ) ⊆ ( ( 𝑆 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) )
117 74 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑆 ∈ ( ( - π [,] π ) –cn→ ℝ ) )
118 117 104 cnlimci ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑆 ‘ ( 𝑄 ‘ 𝑖 ) ) ∈ ( 𝑆 limℂ ( 𝑄 ‘ 𝑖 ) ) )
119 116 118 sselid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑆 ‘ ( 𝑄 ‘ 𝑖 ) ) ∈ ( ( 𝑆 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
120 77 91 feqresmpt ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑆 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑆 ‘ 𝑠 ) ) )
121 120 oveq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑆 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) = ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑆 ‘ 𝑠 ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
122 119 121 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑆 ‘ ( 𝑄 ‘ 𝑖 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑆 ‘ 𝑠 ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
123 21 22 23 73 80 115 122 mullimc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( if ( ( 𝑉 ‘ 𝑖 ) = 𝑋 , 𝐸 , ( ( 𝑅 − if ( ( 𝑉 ‘ 𝑖 ) < 𝑋 , 𝑊 , 𝑌 ) ) / ( 𝑄 ‘ 𝑖 ) ) ) · ( 𝐾 ‘ ( 𝑄 ‘ 𝑖 ) ) ) · ( 𝑆 ‘ ( 𝑄 ‘ 𝑖 ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
124 20 123 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐴 ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
125 11 reseq1i ⊢ ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
126 91 resmptd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) ) )
127 125 126 eqtr2id ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) ) = ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
128 127 oveq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) = ( ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
129 124 128 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐴 ∈ ( ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )