Metamath Proof Explorer

Theorem fourierdlem66

Description: Value of the G function when the argument is not zero. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem66.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
fourierdlem66.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
fourierdlem66.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
fourierdlem66.w ⊢ ( 𝜑 → 𝑊 ∈ ℝ )
fourierdlem66.d ⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
fourierdlem66.h ⊢ 𝐻 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) )
fourierdlem66.k ⊢ 𝐾 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
fourierdlem66.u ⊢ 𝑈 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) )
fourierdlem66.s ⊢ 𝑆 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) )
fourierdlem66.g ⊢ 𝐺 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) )
fourierdlem66.a ⊢ 𝐴 = ( ( - π [,] π ) ∖ { 0 } )
Assertion fourierdlem66 ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑠 ) = ( π · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem66.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2 fourierdlem66.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
3 fourierdlem66.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
4 fourierdlem66.w ⊢ ( 𝜑 → 𝑊 ∈ ℝ )
5 fourierdlem66.d ⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
6 fourierdlem66.h ⊢ 𝐻 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) )
7 fourierdlem66.k ⊢ 𝐾 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
8 fourierdlem66.u ⊢ 𝑈 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) )
9 fourierdlem66.s ⊢ 𝑆 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) )
10 fourierdlem66.g ⊢ 𝐺 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) )
11 fourierdlem66.a ⊢ 𝐴 = ( ( - π [,] π ) ∖ { 0 } )
12 11 eqimssi ⊢ 𝐴 ⊆ ( ( - π [,] π ) ∖ { 0 } )
13 difss ⊢ ( ( - π [,] π ) ∖ { 0 } ) ⊆ ( - π [,] π )
14 12 13 sstri ⊢ 𝐴 ⊆ ( - π [,] π )
15 14 a1i ⊢ ( 𝜑 → 𝐴 ⊆ ( - π [,] π ) )
16 15 sselda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ ( - π [,] π ) )
17 16 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ ( - π [,] π ) )
18 1 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐹 : ℝ ⟶ ℝ )
19 2 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑋 ∈ ℝ )
20 3 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑌 ∈ ℝ )
21 4 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑊 ∈ ℝ )
22 18 19 20 21 6 7 8 fourierdlem55 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑈 : ( - π [,] π ) ⟶ ℝ )
23 22 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → 𝑈 : ( - π [,] π ) ⟶ ℝ )
24 23 17 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝑈 ‘ 𝑠 ) ∈ ℝ )
25 nnre ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ )
26 9 fourierdlem5 ⊢ ( 𝑛 ∈ ℝ → 𝑆 : ( - π [,] π ) ⟶ ℝ )
27 25 26 syl ⊢ ( 𝑛 ∈ ℕ → 𝑆 : ( - π [,] π ) ⟶ ℝ )
28 27 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → 𝑆 : ( - π [,] π ) ⟶ ℝ )
29 28 17 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝑆 ‘ 𝑠 ) ∈ ℝ )
30 24 29 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) ∈ ℝ )
31 10 fvmpt2 ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) ∈ ℝ ) → ( 𝐺 ‘ 𝑠 ) = ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) )
32 17 30 31 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑠 ) = ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) )
33 1 2 3 4 6 fourierdlem9 ⊢ ( 𝜑 → 𝐻 : ( - π [,] π ) ⟶ ℝ )
34 33 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝐻 : ( - π [,] π ) ⟶ ℝ )
35 34 16 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑠 ) ∈ ℝ )
36 7 fourierdlem43 ⊢ 𝐾 : ( - π [,] π ) ⟶ ℝ
37 36 a1i ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝐾 : ( - π [,] π ) ⟶ ℝ )
38 37 16 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝐾 ‘ 𝑠 ) ∈ ℝ )
39 35 38 remulcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) ∈ ℝ )
40 8 fvmpt2 ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) ∈ ℝ ) → ( 𝑈 ‘ 𝑠 ) = ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) )
41 16 39 40 syl2anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝑈 ‘ 𝑠 ) = ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) )
42 0red ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 0 ∈ ℝ )
43 1 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝐹 : ℝ ⟶ ℝ )
44 2 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑋 ∈ ℝ )
45 pire ⊢ π ∈ ℝ
46 45 renegcli ⊢ - π ∈ ℝ
47 iccssre ⊢ ( ( - π ∈ ℝ ∧ π ∈ ℝ ) → ( - π [,] π ) ⊆ ℝ )
48 46 45 47 mp2an ⊢ ( - π [,] π ) ⊆ ℝ
49 14 sseli ⊢ ( 𝑠 ∈ 𝐴 → 𝑠 ∈ ( - π [,] π ) )
50 48 49 sseldi ⊢ ( 𝑠 ∈ 𝐴 → 𝑠 ∈ ℝ )
51 50 adantl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ ℝ )
52 44 51 readdcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝑋 + 𝑠 ) ∈ ℝ )
53 43 52 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℝ )
54 3 4 ifcld ⊢ ( 𝜑 → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ∈ ℝ )
55 54 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ∈ ℝ )
56 53 55 resubcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ∈ ℝ )
57 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ 𝐴 )
58 12 57 sseldi ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) )
59 58 eldifbd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ¬ 𝑠 ∈ { 0 } )
60 velsn ⊢ ( 𝑠 ∈ { 0 } ↔ 𝑠 = 0 )
61 59 60 sylnib ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ¬ 𝑠 = 0 )
62 61 neqned ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ≠ 0 )
63 56 51 62 redivcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ∈ ℝ )
64 42 63 ifcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ∈ ℝ )
65 6 fvmpt2 ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ∈ ℝ ) → ( 𝐻 ‘ 𝑠 ) = if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) )
66 16 64 65 syl2anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑠 ) = if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) )
67 61 iffalsed ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) = ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) )
68 66 67 eqtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑠 ) = ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) )
69 1red ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 1 ∈ ℝ )
70 2re ⊢ 2 ∈ ℝ
71 70 a1i ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 2 ∈ ℝ )
72 51 rehalfcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝑠 / 2 ) ∈ ℝ )
73 72 resincld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℝ )
74 71 73 remulcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℝ )
75 2cnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 2 ∈ ℂ )
76 73 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℂ )
77 2ne0 ⊢ 2 ≠ 0
78 77 a1i ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 2 ≠ 0 )
79 fourierdlem44 ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ 𝑠 ≠ 0 ) → ( sin ‘ ( 𝑠 / 2 ) ) ≠ 0 )
80 16 62 79 syl2anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( sin ‘ ( 𝑠 / 2 ) ) ≠ 0 )
81 75 76 78 80 mulne0d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ≠ 0 )
82 51 74 81 redivcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ∈ ℝ )
83 69 82 ifcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ∈ ℝ )
84 7 fvmpt2 ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ∈ ℝ ) → ( 𝐾 ‘ 𝑠 ) = if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
85 16 83 84 syl2anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝐾 ‘ 𝑠 ) = if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
86 61 iffalsed ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
87 85 86 eqtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝐾 ‘ 𝑠 ) = ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
88 68 87 oveq12d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝐻 ‘ 𝑠 ) · ( 𝐾 ‘ 𝑠 ) ) = ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) · ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
89 56 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ∈ ℂ )
90 51 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ ℂ )
91 75 76 mulcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℂ )
92 89 90 91 62 81 dmdcan2d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) · ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
93 41 88 92 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝑈 ‘ 𝑠 ) = ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
94 93 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝑈 ‘ 𝑠 ) = ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
95 25 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → 𝑛 ∈ ℝ )
96 1red ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → 1 ∈ ℝ )
97 96 rehalfcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( 1 / 2 ) ∈ ℝ )
98 95 97 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝑛 + ( 1 / 2 ) ) ∈ ℝ )
99 50 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ ℝ )
100 98 99 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ∈ ℝ )
101 100 resincld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) ∈ ℝ )
102 9 fvmpt2 ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) ∈ ℝ ) → ( 𝑆 ‘ 𝑠 ) = ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) )
103 17 101 102 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝑆 ‘ 𝑠 ) = ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) )
104 94 103 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝑈 ‘ 𝑠 ) · ( 𝑆 ‘ 𝑠 ) ) = ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) · ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) ) )
105 89 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ∈ ℂ )
106 91 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℂ )
107 101 recnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) ∈ ℂ )
108 81 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ≠ 0 )
109 105 106 107 108 div32d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) · ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) ) = ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
110 25 adantr ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → 𝑛 ∈ ℝ )
111 halfre ⊢ ( 1 / 2 ) ∈ ℝ
112 111 a1i ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → ( 1 / 2 ) ∈ ℝ )
113 110 112 readdcld ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → ( 𝑛 + ( 1 / 2 ) ) ∈ ℝ )
114 50 adantl ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ ℝ )
115 113 114 remulcld ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ∈ ℝ )
116 115 resincld ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) ∈ ℝ )
117 116 recnd ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) ∈ ℂ )
118 70 a1i ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → 2 ∈ ℝ )
119 114 rehalfcld ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → ( 𝑠 / 2 ) ∈ ℝ )
120 119 resincld ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℝ )
121 118 120 remulcld ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℝ )
122 121 recnd ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℂ )
123 picn ⊢ π ∈ ℂ
124 123 a1i ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → π ∈ ℂ )
125 2cnd ⊢ ( 𝑠 ∈ 𝐴 → 2 ∈ ℂ )
126 rehalfcl ⊢ ( 𝑠 ∈ ℝ → ( 𝑠 / 2 ) ∈ ℝ )
127 resincl ⊢ ( ( 𝑠 / 2 ) ∈ ℝ → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℝ )
128 50 126 127 3syl ⊢ ( 𝑠 ∈ 𝐴 → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℝ )
129 128 recnd ⊢ ( 𝑠 ∈ 𝐴 → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℂ )
130 77 a1i ⊢ ( 𝑠 ∈ 𝐴 → 2 ≠ 0 )
131 eldifsni ⊢ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) → 𝑠 ≠ 0 )
132 131 11 eleq2s ⊢ ( 𝑠 ∈ 𝐴 → 𝑠 ≠ 0 )
133 49 132 79 syl2anc ⊢ ( 𝑠 ∈ 𝐴 → ( sin ‘ ( 𝑠 / 2 ) ) ≠ 0 )
134 125 129 130 133 mulne0d ⊢ ( 𝑠 ∈ 𝐴 → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ≠ 0 )
135 134 adantl ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ≠ 0 )
136 0re ⊢ 0 ∈ ℝ
137 pipos ⊢ 0 < π
138 136 137 gtneii ⊢ π ≠ 0
139 138 a1i ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → π ≠ 0 )
140 117 122 124 135 139 divdiv1d ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → ( ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) / π ) = ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) · π ) ) )
141 2cnd ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → 2 ∈ ℂ )
142 129 adantl ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℂ )
143 141 142 124 mulassd ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) · π ) = ( 2 · ( ( sin ‘ ( 𝑠 / 2 ) ) · π ) ) )
144 143 oveq2d ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) · π ) ) = ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( 2 · ( ( sin ‘ ( 𝑠 / 2 ) ) · π ) ) ) )
145 142 124 mulcomd ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → ( ( sin ‘ ( 𝑠 / 2 ) ) · π ) = ( π · ( sin ‘ ( 𝑠 / 2 ) ) ) )
146 145 oveq2d ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → ( 2 · ( ( sin ‘ ( 𝑠 / 2 ) ) · π ) ) = ( 2 · ( π · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
147 141 124 142 mulassd ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) = ( 2 · ( π · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
148 146 147 eqtr4d ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → ( 2 · ( ( sin ‘ ( 𝑠 / 2 ) ) · π ) ) = ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) )
149 148 oveq2d ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( 2 · ( ( sin ‘ ( 𝑠 / 2 ) ) · π ) ) ) = ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
150 140 144 149 3eqtrd ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → ( ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) / π ) = ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
151 150 oveq2d ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → ( π · ( ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) / π ) ) = ( π · ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
152 116 121 135 redivcld ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ∈ ℝ )
153 152 recnd ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ∈ ℂ )
154 153 124 139 divcan2d ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → ( π · ( ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) / π ) ) = ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
155 5 dirkerval2 ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ ℝ ) → ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) = if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
156 50 155 sylan2 ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) = if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
157 fourierdlem24 ⊢ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) → ( 𝑠 mod ( 2 · π ) ) ≠ 0 )
158 157 11 eleq2s ⊢ ( 𝑠 ∈ 𝐴 → ( 𝑠 mod ( 2 · π ) ) ≠ 0 )
159 158 neneqd ⊢ ( 𝑠 ∈ 𝐴 → ¬ ( 𝑠 mod ( 2 · π ) ) = 0 )
160 159 adantl ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → ¬ ( 𝑠 mod ( 2 · π ) ) = 0 )
161 160 iffalsed ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
162 156 161 eqtr2d ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) )
163 162 oveq2d ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → ( π · ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( π · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) )
164 151 154 163 3eqtr3d ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( π · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) )
165 164 oveq2d ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( π · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) )
166 165 adantll ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( π · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) )
167 123 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → π ∈ ℂ )
168 5 dirkerre ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ ℝ ) → ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ∈ ℝ )
169 50 168 sylan2 ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ∈ ℝ )
170 169 recnd ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ∈ ℂ )
171 170 adantll ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ∈ ℂ )
172 105 167 171 mul12d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( π · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) = ( π · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) )
173 109 166 172 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) · ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) ) = ( π · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) )
174 32 104 173 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑠 ) = ( π · ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) · ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑠 ) ) ) )