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 
|- ( ph -> F : RR --> RR )
fourierdlem66.x 
|- ( ph -> X e. RR )
fourierdlem66.y 
|- ( ph -> Y e. RR )
fourierdlem66.w 
|- ( ph -> W e. RR )
fourierdlem66.d 
|- D = ( n e. NN |-> ( s e. RR |-> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) )
fourierdlem66.h 
|- H = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
fourierdlem66.k 
|- K = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
fourierdlem66.u 
|- U = ( s e. ( -u _pi [,] _pi ) |-> ( ( H ` s ) x. ( K ` s ) ) )
fourierdlem66.s 
|- S = ( s e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) )
fourierdlem66.g 
|- G = ( s e. ( -u _pi [,] _pi ) |-> ( ( U ` s ) x. ( S ` s ) ) )
fourierdlem66.a 
|- A = ( ( -u _pi [,] _pi ) \ { 0 } )
Assertion fourierdlem66 
|- ( ( ( ph /\ n e. NN ) /\ s e. A ) -> ( G ` s ) = ( _pi x. ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) ) )

Proof

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