Metamath Proof Explorer

Theorem dirkeritg

Description: The definite integral of the Dirichlet Kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dirkeritg.d 
|- D = ( n e. NN |-> ( x e. RR |-> if ( ( x mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. x ) ) / ( ( 2 x. _pi ) x. ( sin ` ( x / 2 ) ) ) ) ) ) )
dirkeritg.n 
|- ( ph -> N e. NN )
dirkeritg.f 
|- F = ( D ` N )
dirkeritg.a 
|- ( ph -> A e. RR )
dirkeritg.b 
|- ( ph -> B e. RR )
dirkeritg.aleb 
|- ( ph -> A <_ B )
dirkeritg.g 
|- G = ( x e. ( A [,] B ) |-> ( ( ( x / 2 ) + sum_ k e. ( 1 ... N ) ( ( sin ` ( k x. x ) ) / k ) ) / _pi ) )
Assertion dirkeritg 
|- ( ph -> S. ( A (,) B ) ( F ` x ) _d x = ( ( G ` B ) - ( G ` A ) ) )

Proof

Step Hyp Ref Expression
1 dirkeritg.d 
 |-  D = ( n e. NN |-> ( x e. RR |-> if ( ( x mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. x ) ) / ( ( 2 x. _pi ) x. ( sin ` ( x / 2 ) ) ) ) ) ) )
2 dirkeritg.n 
 |-  ( ph -> N e. NN )
3 dirkeritg.f 
 |-  F = ( D ` N )
4 dirkeritg.a 
 |-  ( ph -> A e. RR )
5 dirkeritg.b 
 |-  ( ph -> B e. RR )
6 dirkeritg.aleb 
 |-  ( ph -> A <_ B )
7 dirkeritg.g 
 |-  G = ( x e. ( A [,] B ) |-> ( ( ( x / 2 ) + sum_ k e. ( 1 ... N ) ( ( sin ` ( k x. x ) ) / k ) ) / _pi ) )
8 fveq2 
 |-  ( x = s -> ( F ` x ) = ( F ` s ) )
9 8 cbvitgv 
 |-  S. ( A (,) B ) ( F ` x ) _d x = S. ( A (,) B ) ( F ` s ) _d s
10 9 a1i 
 |-  ( ph -> S. ( A (,) B ) ( F ` x ) _d x = S. ( A (,) B ) ( F ` s ) _d s )
11 elioore 
 |-  ( s e. ( A (,) B ) -> s e. RR )
12 11 adantl 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> s e. RR )
13 halfre 
 |-  ( 1 / 2 ) e. RR
14 13 a1i 
 |-  ( s e. RR -> ( 1 / 2 ) e. RR )
15 fzfid 
 |-  ( s e. RR -> ( 1 ... N ) e. Fin )
16 elfzelz 
 |-  ( k e. ( 1 ... N ) -> k e. ZZ )
17 16 zred 
 |-  ( k e. ( 1 ... N ) -> k e. RR )
18 17 adantl 
 |-  ( ( s e. RR /\ k e. ( 1 ... N ) ) -> k e. RR )
19 simpl 
 |-  ( ( s e. RR /\ k e. ( 1 ... N ) ) -> s e. RR )
20 18 19 remulcld 
 |-  ( ( s e. RR /\ k e. ( 1 ... N ) ) -> ( k x. s ) e. RR )
21 20 recoscld 
 |-  ( ( s e. RR /\ k e. ( 1 ... N ) ) -> ( cos ` ( k x. s ) ) e. RR )
22 15 21 fsumrecl 
 |-  ( s e. RR -> sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) e. RR )
23 14 22 readdcld 
 |-  ( s e. RR -> ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) e. RR )
24 pire 
 |-  _pi e. RR
25 24 a1i 
 |-  ( s e. RR -> _pi e. RR )
26 pipos 
 |-  0 < _pi
27 24 26 gt0ne0ii 
 |-  _pi =/= 0
28 27 a1i 
 |-  ( s e. RR -> _pi =/= 0 )
29 23 25 28 redivcld 
 |-  ( s e. RR -> ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) e. RR )
30 12 29 syl 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) e. RR )
31 eqid 
 |-  ( s e. RR |-> ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) ) = ( s e. RR |-> ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) )
32 31 fvmpt2 
 |-  ( ( s e. RR /\ ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) e. RR ) -> ( ( s e. RR |-> ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) ) ` s ) = ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) )
33 12 30 32 syl2anc 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( s e. RR |-> ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) ) ` s ) = ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) )
34 oveq1 
 |-  ( x = s -> ( x mod ( 2 x. _pi ) ) = ( s mod ( 2 x. _pi ) ) )
35 34 eqeq1d 
 |-  ( x = s -> ( ( x mod ( 2 x. _pi ) ) = 0 <-> ( s mod ( 2 x. _pi ) ) = 0 ) )
36 oveq2 
 |-  ( x = s -> ( ( n + ( 1 / 2 ) ) x. x ) = ( ( n + ( 1 / 2 ) ) x. s ) )
37 36 fveq2d 
 |-  ( x = s -> ( sin ` ( ( n + ( 1 / 2 ) ) x. x ) ) = ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) )
38 oveq1 
 |-  ( x = s -> ( x / 2 ) = ( s / 2 ) )
39 38 fveq2d 
 |-  ( x = s -> ( sin ` ( x / 2 ) ) = ( sin ` ( s / 2 ) ) )
40 39 oveq2d 
 |-  ( x = s -> ( ( 2 x. _pi ) x. ( sin ` ( x / 2 ) ) ) = ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) )
41 37 40 oveq12d 
 |-  ( x = s -> ( ( sin ` ( ( n + ( 1 / 2 ) ) x. x ) ) / ( ( 2 x. _pi ) x. ( sin ` ( x / 2 ) ) ) ) = ( ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) )
42 35 41 ifbieq2d 
 |-  ( x = s -> if ( ( x mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. x ) ) / ( ( 2 x. _pi ) x. ( sin ` ( x / 2 ) ) ) ) ) = 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 ) ) ) ) ) )
43 42 cbvmptv 
 |-  ( x e. RR |-> if ( ( x mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. x ) ) / ( ( 2 x. _pi ) x. ( sin ` ( x / 2 ) ) ) ) ) ) = ( 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 ) ) ) ) ) )
44 43 mpteq2i 
 |-  ( n e. NN |-> ( x e. RR |-> if ( ( x mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. x ) ) / ( ( 2 x. _pi ) x. ( sin ` ( x / 2 ) ) ) ) ) ) ) = ( 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 ) ) ) ) ) ) )
45 1 44 eqtri 
 |-  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 ) ) ) ) ) ) )
46 45 2 3 31 dirkertrigeq 
 |-  ( ph -> F = ( s e. RR |-> ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) ) )
47 46 fveq1d 
 |-  ( ph -> ( F ` s ) = ( ( s e. RR |-> ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) ) ` s ) )
48 47 adantr 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( F ` s ) = ( ( s e. RR |-> ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) ) ` s ) )
49 oveq2 
 |-  ( x = s -> ( k x. x ) = ( k x. s ) )
50 49 fveq2d 
 |-  ( x = s -> ( sin ` ( k x. x ) ) = ( sin ` ( k x. s ) ) )
51 50 oveq1d 
 |-  ( x = s -> ( ( sin ` ( k x. x ) ) / k ) = ( ( sin ` ( k x. s ) ) / k ) )
52 51 sumeq2sdv 
 |-  ( x = s -> sum_ k e. ( 1 ... N ) ( ( sin ` ( k x. x ) ) / k ) = sum_ k e. ( 1 ... N ) ( ( sin ` ( k x. s ) ) / k ) )
53 38 52 oveq12d 
 |-  ( x = s -> ( ( x / 2 ) + sum_ k e. ( 1 ... N ) ( ( sin ` ( k x. x ) ) / k ) ) = ( ( s / 2 ) + sum_ k e. ( 1 ... N ) ( ( sin ` ( k x. s ) ) / k ) ) )
54 53 oveq1d 
 |-  ( x = s -> ( ( ( x / 2 ) + sum_ k e. ( 1 ... N ) ( ( sin ` ( k x. x ) ) / k ) ) / _pi ) = ( ( ( s / 2 ) + sum_ k e. ( 1 ... N ) ( ( sin ` ( k x. s ) ) / k ) ) / _pi ) )
55 54 cbvmptv 
 |-  ( x e. ( A [,] B ) |-> ( ( ( x / 2 ) + sum_ k e. ( 1 ... N ) ( ( sin ` ( k x. x ) ) / k ) ) / _pi ) ) = ( s e. ( A [,] B ) |-> ( ( ( s / 2 ) + sum_ k e. ( 1 ... N ) ( ( sin ` ( k x. s ) ) / k ) ) / _pi ) )
56 7 55 eqtri 
 |-  G = ( s e. ( A [,] B ) |-> ( ( ( s / 2 ) + sum_ k e. ( 1 ... N ) ( ( sin ` ( k x. s ) ) / k ) ) / _pi ) )
57 56 oveq2i 
 |-  ( RR _D G ) = ( RR _D ( s e. ( A [,] B ) |-> ( ( ( s / 2 ) + sum_ k e. ( 1 ... N ) ( ( sin ` ( k x. s ) ) / k ) ) / _pi ) ) )
58 reelprrecn 
 |-  RR e. { RR , CC }
59 58 a1i 
 |-  ( ph -> RR e. { RR , CC } )
60 recn 
 |-  ( s e. RR -> s e. CC )
61 60 halfcld 
 |-  ( s e. RR -> ( s / 2 ) e. CC )
62 16 zcnd 
 |-  ( k e. ( 1 ... N ) -> k e. CC )
63 62 adantl 
 |-  ( ( s e. RR /\ k e. ( 1 ... N ) ) -> k e. CC )
64 60 adantr 
 |-  ( ( s e. RR /\ k e. ( 1 ... N ) ) -> s e. CC )
65 63 64 mulcld 
 |-  ( ( s e. RR /\ k e. ( 1 ... N ) ) -> ( k x. s ) e. CC )
66 65 sincld 
 |-  ( ( s e. RR /\ k e. ( 1 ... N ) ) -> ( sin ` ( k x. s ) ) e. CC )
67 0red 
 |-  ( k e. ( 1 ... N ) -> 0 e. RR )
68 1red 
 |-  ( k e. ( 1 ... N ) -> 1 e. RR )
69 0lt1 
 |-  0 < 1
70 69 a1i 
 |-  ( k e. ( 1 ... N ) -> 0 < 1 )
71 elfzle1 
 |-  ( k e. ( 1 ... N ) -> 1 <_ k )
72 67 68 17 70 71 ltletrd 
 |-  ( k e. ( 1 ... N ) -> 0 < k )
73 72 gt0ne0d 
 |-  ( k e. ( 1 ... N ) -> k =/= 0 )
74 73 adantl 
 |-  ( ( s e. RR /\ k e. ( 1 ... N ) ) -> k =/= 0 )
75 66 63 74 divcld 
 |-  ( ( s e. RR /\ k e. ( 1 ... N ) ) -> ( ( sin ` ( k x. s ) ) / k ) e. CC )
76 15 75 fsumcl 
 |-  ( s e. RR -> sum_ k e. ( 1 ... N ) ( ( sin ` ( k x. s ) ) / k ) e. CC )
77 61 76 addcld 
 |-  ( s e. RR -> ( ( s / 2 ) + sum_ k e. ( 1 ... N ) ( ( sin ` ( k x. s ) ) / k ) ) e. CC )
78 picn 
 |-  _pi e. CC
79 78 a1i 
 |-  ( s e. RR -> _pi e. CC )
80 77 79 28 divcld 
 |-  ( s e. RR -> ( ( ( s / 2 ) + sum_ k e. ( 1 ... N ) ( ( sin ` ( k x. s ) ) / k ) ) / _pi ) e. CC )
81 80 adantl 
 |-  ( ( ph /\ s e. RR ) -> ( ( ( s / 2 ) + sum_ k e. ( 1 ... N ) ( ( sin ` ( k x. s ) ) / k ) ) / _pi ) e. CC )
82 29 adantl 
 |-  ( ( ph /\ s e. RR ) -> ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) e. RR )
83 77 adantl 
 |-  ( ( ph /\ s e. RR ) -> ( ( s / 2 ) + sum_ k e. ( 1 ... N ) ( ( sin ` ( k x. s ) ) / k ) ) e. CC )
84 23 adantl 
 |-  ( ( ph /\ s e. RR ) -> ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) e. RR )
85 61 adantl 
 |-  ( ( ph /\ s e. RR ) -> ( s / 2 ) e. CC )
86 13 a1i 
 |-  ( ( ph /\ s e. RR ) -> ( 1 / 2 ) e. RR )
87 60 adantl 
 |-  ( ( ph /\ s e. RR ) -> s e. CC )
88 1red 
 |-  ( ( ph /\ s e. RR ) -> 1 e. RR )
89 59 dvmptid 
 |-  ( ph -> ( RR _D ( s e. RR |-> s ) ) = ( s e. RR |-> 1 ) )
90 2cnd 
 |-  ( ph -> 2 e. CC )
91 2ne0 
 |-  2 =/= 0
92 91 a1i 
 |-  ( ph -> 2 =/= 0 )
93 59 87 88 89 90 92 dvmptdivc 
 |-  ( ph -> ( RR _D ( s e. RR |-> ( s / 2 ) ) ) = ( s e. RR |-> ( 1 / 2 ) ) )
94 76 adantl 
 |-  ( ( ph /\ s e. RR ) -> sum_ k e. ( 1 ... N ) ( ( sin ` ( k x. s ) ) / k ) e. CC )
95 22 adantl 
 |-  ( ( ph /\ s e. RR ) -> sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) e. RR )
96 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
97 96 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
98 reopn 
 |-  RR e. ( topGen ` ran (,) )
99 98 a1i 
 |-  ( ph -> RR e. ( topGen ` ran (,) ) )
100 fzfid 
 |-  ( ph -> ( 1 ... N ) e. Fin )
101 75 ancoms 
 |-  ( ( k e. ( 1 ... N ) /\ s e. RR ) -> ( ( sin ` ( k x. s ) ) / k ) e. CC )
102 101 3adant1 
 |-  ( ( ph /\ k e. ( 1 ... N ) /\ s e. RR ) -> ( ( sin ` ( k x. s ) ) / k ) e. CC )
103 21 ancoms 
 |-  ( ( k e. ( 1 ... N ) /\ s e. RR ) -> ( cos ` ( k x. s ) ) e. RR )
104 103 recnd 
 |-  ( ( k e. ( 1 ... N ) /\ s e. RR ) -> ( cos ` ( k x. s ) ) e. CC )
105 104 3adant1 
 |-  ( ( ph /\ k e. ( 1 ... N ) /\ s e. RR ) -> ( cos ` ( k x. s ) ) e. CC )
106 58 a1i 
 |-  ( k e. ( 1 ... N ) -> RR e. { RR , CC } )
107 66 ancoms 
 |-  ( ( k e. ( 1 ... N ) /\ s e. RR ) -> ( sin ` ( k x. s ) ) e. CC )
108 62 adantr 
 |-  ( ( k e. ( 1 ... N ) /\ s e. CC ) -> k e. CC )
109 simpr 
 |-  ( ( k e. ( 1 ... N ) /\ s e. CC ) -> s e. CC )
110 108 109 mulcld 
 |-  ( ( k e. ( 1 ... N ) /\ s e. CC ) -> ( k x. s ) e. CC )
111 110 coscld 
 |-  ( ( k e. ( 1 ... N ) /\ s e. CC ) -> ( cos ` ( k x. s ) ) e. CC )
112 108 111 mulcld 
 |-  ( ( k e. ( 1 ... N ) /\ s e. CC ) -> ( k x. ( cos ` ( k x. s ) ) ) e. CC )
113 60 112 sylan2 
 |-  ( ( k e. ( 1 ... N ) /\ s e. RR ) -> ( k x. ( cos ` ( k x. s ) ) ) e. CC )
114 ax-resscn 
 |-  RR C_ CC
115 resmpt 
 |-  ( RR C_ CC -> ( ( s e. CC |-> ( sin ` ( k x. s ) ) ) |` RR ) = ( s e. RR |-> ( sin ` ( k x. s ) ) ) )
116 114 115 mp1i 
 |-  ( k e. ( 1 ... N ) -> ( ( s e. CC |-> ( sin ` ( k x. s ) ) ) |` RR ) = ( s e. RR |-> ( sin ` ( k x. s ) ) ) )
117 116 eqcomd 
 |-  ( k e. ( 1 ... N ) -> ( s e. RR |-> ( sin ` ( k x. s ) ) ) = ( ( s e. CC |-> ( sin ` ( k x. s ) ) ) |` RR ) )
118 117 oveq2d 
 |-  ( k e. ( 1 ... N ) -> ( RR _D ( s e. RR |-> ( sin ` ( k x. s ) ) ) ) = ( RR _D ( ( s e. CC |-> ( sin ` ( k x. s ) ) ) |` RR ) ) )
119 110 sincld 
 |-  ( ( k e. ( 1 ... N ) /\ s e. CC ) -> ( sin ` ( k x. s ) ) e. CC )
120 119 fmpttd 
 |-  ( k e. ( 1 ... N ) -> ( s e. CC |-> ( sin ` ( k x. s ) ) ) : CC --> CC )
121 112 ralrimiva 
 |-  ( k e. ( 1 ... N ) -> A. s e. CC ( k x. ( cos ` ( k x. s ) ) ) e. CC )
122 dmmptg 
 |-  ( A. s e. CC ( k x. ( cos ` ( k x. s ) ) ) e. CC -> dom ( s e. CC |-> ( k x. ( cos ` ( k x. s ) ) ) ) = CC )
123 121 122 syl 
 |-  ( k e. ( 1 ... N ) -> dom ( s e. CC |-> ( k x. ( cos ` ( k x. s ) ) ) ) = CC )
124 114 123 sseqtrrid 
 |-  ( k e. ( 1 ... N ) -> RR C_ dom ( s e. CC |-> ( k x. ( cos ` ( k x. s ) ) ) ) )
125 dvsinax 
 |-  ( k e. CC -> ( CC _D ( s e. CC |-> ( sin ` ( k x. s ) ) ) ) = ( s e. CC |-> ( k x. ( cos ` ( k x. s ) ) ) ) )
126 62 125 syl 
 |-  ( k e. ( 1 ... N ) -> ( CC _D ( s e. CC |-> ( sin ` ( k x. s ) ) ) ) = ( s e. CC |-> ( k x. ( cos ` ( k x. s ) ) ) ) )
127 126 dmeqd 
 |-  ( k e. ( 1 ... N ) -> dom ( CC _D ( s e. CC |-> ( sin ` ( k x. s ) ) ) ) = dom ( s e. CC |-> ( k x. ( cos ` ( k x. s ) ) ) ) )
128 124 127 sseqtrrd 
 |-  ( k e. ( 1 ... N ) -> RR C_ dom ( CC _D ( s e. CC |-> ( sin ` ( k x. s ) ) ) ) )
129 dvcnre 
 |-  ( ( ( s e. CC |-> ( sin ` ( k x. s ) ) ) : CC --> CC /\ RR C_ dom ( CC _D ( s e. CC |-> ( sin ` ( k x. s ) ) ) ) ) -> ( RR _D ( ( s e. CC |-> ( sin ` ( k x. s ) ) ) |` RR ) ) = ( ( CC _D ( s e. CC |-> ( sin ` ( k x. s ) ) ) ) |` RR ) )
130 120 128 129 syl2anc 
 |-  ( k e. ( 1 ... N ) -> ( RR _D ( ( s e. CC |-> ( sin ` ( k x. s ) ) ) |` RR ) ) = ( ( CC _D ( s e. CC |-> ( sin ` ( k x. s ) ) ) ) |` RR ) )
131 126 reseq1d 
 |-  ( k e. ( 1 ... N ) -> ( ( CC _D ( s e. CC |-> ( sin ` ( k x. s ) ) ) ) |` RR ) = ( ( s e. CC |-> ( k x. ( cos ` ( k x. s ) ) ) ) |` RR ) )
132 resmpt 
 |-  ( RR C_ CC -> ( ( s e. CC |-> ( k x. ( cos ` ( k x. s ) ) ) ) |` RR ) = ( s e. RR |-> ( k x. ( cos ` ( k x. s ) ) ) ) )
133 114 132 ax-mp 
 |-  ( ( s e. CC |-> ( k x. ( cos ` ( k x. s ) ) ) ) |` RR ) = ( s e. RR |-> ( k x. ( cos ` ( k x. s ) ) ) )
134 131 133 eqtrdi 
 |-  ( k e. ( 1 ... N ) -> ( ( CC _D ( s e. CC |-> ( sin ` ( k x. s ) ) ) ) |` RR ) = ( s e. RR |-> ( k x. ( cos ` ( k x. s ) ) ) ) )
135 118 130 134 3eqtrd 
 |-  ( k e. ( 1 ... N ) -> ( RR _D ( s e. RR |-> ( sin ` ( k x. s ) ) ) ) = ( s e. RR |-> ( k x. ( cos ` ( k x. s ) ) ) ) )
136 106 107 113 135 62 73 dvmptdivc 
 |-  ( k e. ( 1 ... N ) -> ( RR _D ( s e. RR |-> ( ( sin ` ( k x. s ) ) / k ) ) ) = ( s e. RR |-> ( ( k x. ( cos ` ( k x. s ) ) ) / k ) ) )
137 62 adantr 
 |-  ( ( k e. ( 1 ... N ) /\ s e. RR ) -> k e. CC )
138 73 adantr 
 |-  ( ( k e. ( 1 ... N ) /\ s e. RR ) -> k =/= 0 )
139 104 137 138 divcan3d 
 |-  ( ( k e. ( 1 ... N ) /\ s e. RR ) -> ( ( k x. ( cos ` ( k x. s ) ) ) / k ) = ( cos ` ( k x. s ) ) )
140 139 mpteq2dva 
 |-  ( k e. ( 1 ... N ) -> ( s e. RR |-> ( ( k x. ( cos ` ( k x. s ) ) ) / k ) ) = ( s e. RR |-> ( cos ` ( k x. s ) ) ) )
141 136 140 eqtrd 
 |-  ( k e. ( 1 ... N ) -> ( RR _D ( s e. RR |-> ( ( sin ` ( k x. s ) ) / k ) ) ) = ( s e. RR |-> ( cos ` ( k x. s ) ) ) )
142 141 adantl 
 |-  ( ( ph /\ k e. ( 1 ... N ) ) -> ( RR _D ( s e. RR |-> ( ( sin ` ( k x. s ) ) / k ) ) ) = ( s e. RR |-> ( cos ` ( k x. s ) ) ) )
143 97 96 59 99 100 102 105 142 dvmptfsum 
 |-  ( ph -> ( RR _D ( s e. RR |-> sum_ k e. ( 1 ... N ) ( ( sin ` ( k x. s ) ) / k ) ) ) = ( s e. RR |-> sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) )
144 59 85 86 93 94 95 143 dvmptadd 
 |-  ( ph -> ( RR _D ( s e. RR |-> ( ( s / 2 ) + sum_ k e. ( 1 ... N ) ( ( sin ` ( k x. s ) ) / k ) ) ) ) = ( s e. RR |-> ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) ) )
145 78 a1i 
 |-  ( ph -> _pi e. CC )
146 27 a1i 
 |-  ( ph -> _pi =/= 0 )
147 59 83 84 144 145 146 dvmptdivc 
 |-  ( ph -> ( RR _D ( s e. RR |-> ( ( ( s / 2 ) + sum_ k e. ( 1 ... N ) ( ( sin ` ( k x. s ) ) / k ) ) / _pi ) ) ) = ( s e. RR |-> ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) ) )
148 4 5 iccssred 
 |-  ( ph -> ( A [,] B ) C_ RR )
149 iccntr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
150 4 5 149 syl2anc 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
151 59 81 82 147 148 97 96 150 dvmptres2 
 |-  ( ph -> ( RR _D ( s e. ( A [,] B ) |-> ( ( ( s / 2 ) + sum_ k e. ( 1 ... N ) ( ( sin ` ( k x. s ) ) / k ) ) / _pi ) ) ) = ( s e. ( A (,) B ) |-> ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) ) )
152 57 151 eqtrid 
 |-  ( ph -> ( RR _D G ) = ( s e. ( A (,) B ) |-> ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) ) )
153 152 30 fvmpt2d 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( RR _D G ) ` s ) = ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) )
154 33 48 153 3eqtr4d 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( F ` s ) = ( ( RR _D G ) ` s ) )
155 154 itgeq2dv 
 |-  ( ph -> S. ( A (,) B ) ( F ` s ) _d s = S. ( A (,) B ) ( ( RR _D G ) ` s ) _d s )
156 ioosscn 
 |-  ( A (,) B ) C_ CC
157 156 a1i 
 |-  ( ph -> ( A (,) B ) C_ CC )
158 halfcn 
 |-  ( 1 / 2 ) e. CC
159 158 a1i 
 |-  ( ph -> ( 1 / 2 ) e. CC )
160 ssid 
 |-  CC C_ CC
161 160 a1i 
 |-  ( ph -> CC C_ CC )
162 157 159 161 constcncfg 
 |-  ( ph -> ( s e. ( A (,) B ) |-> ( 1 / 2 ) ) e. ( ( A (,) B ) -cn-> CC ) )
163 eqid 
 |-  ( s e. CC |-> ( cos ` ( k x. s ) ) ) = ( s e. CC |-> ( cos ` ( k x. s ) ) )
164 coscn 
 |-  cos e. ( CC -cn-> CC )
165 164 a1i 
 |-  ( k e. ( 1 ... N ) -> cos e. ( CC -cn-> CC ) )
166 eqid 
 |-  ( s e. CC |-> ( k x. s ) ) = ( s e. CC |-> ( k x. s ) )
167 166 mulc1cncf 
 |-  ( k e. CC -> ( s e. CC |-> ( k x. s ) ) e. ( CC -cn-> CC ) )
168 62 167 syl 
 |-  ( k e. ( 1 ... N ) -> ( s e. CC |-> ( k x. s ) ) e. ( CC -cn-> CC ) )
169 165 168 cncfmpt1f 
 |-  ( k e. ( 1 ... N ) -> ( s e. CC |-> ( cos ` ( k x. s ) ) ) e. ( CC -cn-> CC ) )
170 156 a1i 
 |-  ( k e. ( 1 ... N ) -> ( A (,) B ) C_ CC )
171 160 a1i 
 |-  ( k e. ( 1 ... N ) -> CC C_ CC )
172 11 104 sylan2 
 |-  ( ( k e. ( 1 ... N ) /\ s e. ( A (,) B ) ) -> ( cos ` ( k x. s ) ) e. CC )
173 163 169 170 171 172 cncfmptssg 
 |-  ( k e. ( 1 ... N ) -> ( s e. ( A (,) B ) |-> ( cos ` ( k x. s ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
174 173 adantl 
 |-  ( ( ph /\ k e. ( 1 ... N ) ) -> ( s e. ( A (,) B ) |-> ( cos ` ( k x. s ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
175 157 100 174 fsumcncf 
 |-  ( ph -> ( s e. ( A (,) B ) |-> sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
176 162 175 addcncf 
 |-  ( ph -> ( s e. ( A (,) B ) |-> ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
177 eqid 
 |-  ( s e. CC |-> _pi ) = ( s e. CC |-> _pi )
178 cncfmptc 
 |-  ( ( _pi e. CC /\ CC C_ CC /\ CC C_ CC ) -> ( s e. CC |-> _pi ) e. ( CC -cn-> CC ) )
179 78 160 160 178 mp3an 
 |-  ( s e. CC |-> _pi ) e. ( CC -cn-> CC )
180 179 a1i 
 |-  ( ph -> ( s e. CC |-> _pi ) e. ( CC -cn-> CC ) )
181 difssd 
 |-  ( ph -> ( CC \ { 0 } ) C_ CC )
182 eldifsn 
 |-  ( _pi e. ( CC \ { 0 } ) <-> ( _pi e. CC /\ _pi =/= 0 ) )
183 78 27 182 mpbir2an 
 |-  _pi e. ( CC \ { 0 } )
184 183 a1i 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> _pi e. ( CC \ { 0 } ) )
185 177 180 157 181 184 cncfmptssg 
 |-  ( ph -> ( s e. ( A (,) B ) |-> _pi ) e. ( ( A (,) B ) -cn-> ( CC \ { 0 } ) ) )
186 176 185 divcncf 
 |-  ( ph -> ( s e. ( A (,) B ) |-> ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) ) e. ( ( A (,) B ) -cn-> CC ) )
187 152 186 eqeltrd 
 |-  ( ph -> ( RR _D G ) e. ( ( A (,) B ) -cn-> CC ) )
188 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
189 188 a1i 
 |-  ( ph -> ( A (,) B ) C_ ( A [,] B ) )
190 ioombl 
 |-  ( A (,) B ) e. dom vol
191 190 a1i 
 |-  ( ph -> ( A (,) B ) e. dom vol )
192 13 a1i 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> ( 1 / 2 ) e. RR )
193 fzfid 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> ( 1 ... N ) e. Fin )
194 17 adantl 
 |-  ( ( ( ph /\ s e. ( A [,] B ) ) /\ k e. ( 1 ... N ) ) -> k e. RR )
195 148 sselda 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> s e. RR )
196 195 adantr 
 |-  ( ( ( ph /\ s e. ( A [,] B ) ) /\ k e. ( 1 ... N ) ) -> s e. RR )
197 194 196 remulcld 
 |-  ( ( ( ph /\ s e. ( A [,] B ) ) /\ k e. ( 1 ... N ) ) -> ( k x. s ) e. RR )
198 197 recoscld 
 |-  ( ( ( ph /\ s e. ( A [,] B ) ) /\ k e. ( 1 ... N ) ) -> ( cos ` ( k x. s ) ) e. RR )
199 193 198 fsumrecl 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) e. RR )
200 192 199 readdcld 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) e. RR )
201 24 a1i 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> _pi e. RR )
202 27 a1i 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> _pi =/= 0 )
203 200 201 202 redivcld 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) e. RR )
204 148 114 sstrdi 
 |-  ( ph -> ( A [,] B ) C_ CC )
205 204 159 161 constcncfg 
 |-  ( ph -> ( s e. ( A [,] B ) |-> ( 1 / 2 ) ) e. ( ( A [,] B ) -cn-> CC ) )
206 eqid 
 |-  ( s e. CC |-> sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) = ( s e. CC |-> sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) )
207 169 adantl 
 |-  ( ( ph /\ k e. ( 1 ... N ) ) -> ( s e. CC |-> ( cos ` ( k x. s ) ) ) e. ( CC -cn-> CC ) )
208 161 100 207 fsumcncf 
 |-  ( ph -> ( s e. CC |-> sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) e. ( CC -cn-> CC ) )
209 199 recnd 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) e. CC )
210 206 208 204 161 209 cncfmptssg 
 |-  ( ph -> ( s e. ( A [,] B ) |-> sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
211 205 210 addcncf 
 |-  ( ph -> ( s e. ( A [,] B ) |-> ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
212 183 a1i 
 |-  ( ph -> _pi e. ( CC \ { 0 } ) )
213 204 212 181 constcncfg 
 |-  ( ph -> ( s e. ( A [,] B ) |-> _pi ) e. ( ( A [,] B ) -cn-> ( CC \ { 0 } ) ) )
214 211 213 divcncf 
 |-  ( ph -> ( s e. ( A [,] B ) |-> ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) ) e. ( ( A [,] B ) -cn-> CC ) )
215 cniccibl 
 |-  ( ( A e. RR /\ B e. RR /\ ( s e. ( A [,] B ) |-> ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) ) e. ( ( A [,] B ) -cn-> CC ) ) -> ( s e. ( A [,] B ) |-> ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) ) e. L^1 )
216 4 5 214 215 syl3anc 
 |-  ( ph -> ( s e. ( A [,] B ) |-> ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) ) e. L^1 )
217 189 191 203 216 iblss 
 |-  ( ph -> ( s e. ( A (,) B ) |-> ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) ) e. L^1 )
218 152 217 eqeltrd 
 |-  ( ph -> ( RR _D G ) e. L^1 )
219 204 161 idcncfg 
 |-  ( ph -> ( s e. ( A [,] B ) |-> s ) e. ( ( A [,] B ) -cn-> CC ) )
220 2cn 
 |-  2 e. CC
221 eldifsn 
 |-  ( 2 e. ( CC \ { 0 } ) <-> ( 2 e. CC /\ 2 =/= 0 ) )
222 220 91 221 mpbir2an 
 |-  2 e. ( CC \ { 0 } )
223 222 a1i 
 |-  ( ph -> 2 e. ( CC \ { 0 } ) )
224 204 223 181 constcncfg 
 |-  ( ph -> ( s e. ( A [,] B ) |-> 2 ) e. ( ( A [,] B ) -cn-> ( CC \ { 0 } ) ) )
225 219 224 divcncf 
 |-  ( ph -> ( s e. ( A [,] B ) |-> ( s / 2 ) ) e. ( ( A [,] B ) -cn-> CC ) )
226 eqid 
 |-  ( s e. CC |-> ( sin ` ( k x. s ) ) ) = ( s e. CC |-> ( sin ` ( k x. s ) ) )
227 sincn 
 |-  sin e. ( CC -cn-> CC )
228 227 a1i 
 |-  ( k e. ( 1 ... N ) -> sin e. ( CC -cn-> CC ) )
229 228 168 cncfmpt1f 
 |-  ( k e. ( 1 ... N ) -> ( s e. CC |-> ( sin ` ( k x. s ) ) ) e. ( CC -cn-> CC ) )
230 229 adantl 
 |-  ( ( ph /\ k e. ( 1 ... N ) ) -> ( s e. CC |-> ( sin ` ( k x. s ) ) ) e. ( CC -cn-> CC ) )
231 204 adantr 
 |-  ( ( ph /\ k e. ( 1 ... N ) ) -> ( A [,] B ) C_ CC )
232 160 a1i 
 |-  ( ( ph /\ k e. ( 1 ... N ) ) -> CC C_ CC )
233 62 ad2antlr 
 |-  ( ( ( ph /\ k e. ( 1 ... N ) ) /\ s e. ( A [,] B ) ) -> k e. CC )
234 195 recnd 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> s e. CC )
235 234 adantlr 
 |-  ( ( ( ph /\ k e. ( 1 ... N ) ) /\ s e. ( A [,] B ) ) -> s e. CC )
236 233 235 mulcld 
 |-  ( ( ( ph /\ k e. ( 1 ... N ) ) /\ s e. ( A [,] B ) ) -> ( k x. s ) e. CC )
237 236 sincld 
 |-  ( ( ( ph /\ k e. ( 1 ... N ) ) /\ s e. ( A [,] B ) ) -> ( sin ` ( k x. s ) ) e. CC )
238 226 230 231 232 237 cncfmptssg 
 |-  ( ( ph /\ k e. ( 1 ... N ) ) -> ( s e. ( A [,] B ) |-> ( sin ` ( k x. s ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
239 eldifsn 
 |-  ( k e. ( CC \ { 0 } ) <-> ( k e. CC /\ k =/= 0 ) )
240 62 73 239 sylanbrc 
 |-  ( k e. ( 1 ... N ) -> k e. ( CC \ { 0 } ) )
241 240 adantl 
 |-  ( ( ph /\ k e. ( 1 ... N ) ) -> k e. ( CC \ { 0 } ) )
242 difssd 
 |-  ( ( ph /\ k e. ( 1 ... N ) ) -> ( CC \ { 0 } ) C_ CC )
243 231 241 242 constcncfg 
 |-  ( ( ph /\ k e. ( 1 ... N ) ) -> ( s e. ( A [,] B ) |-> k ) e. ( ( A [,] B ) -cn-> ( CC \ { 0 } ) ) )
244 238 243 divcncf 
 |-  ( ( ph /\ k e. ( 1 ... N ) ) -> ( s e. ( A [,] B ) |-> ( ( sin ` ( k x. s ) ) / k ) ) e. ( ( A [,] B ) -cn-> CC ) )
245 204 100 244 fsumcncf 
 |-  ( ph -> ( s e. ( A [,] B ) |-> sum_ k e. ( 1 ... N ) ( ( sin ` ( k x. s ) ) / k ) ) e. ( ( A [,] B ) -cn-> CC ) )
246 225 245 addcncf 
 |-  ( ph -> ( s e. ( A [,] B ) |-> ( ( s / 2 ) + sum_ k e. ( 1 ... N ) ( ( sin ` ( k x. s ) ) / k ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
247 246 213 divcncf 
 |-  ( ph -> ( s e. ( A [,] B ) |-> ( ( ( s / 2 ) + sum_ k e. ( 1 ... N ) ( ( sin ` ( k x. s ) ) / k ) ) / _pi ) ) e. ( ( A [,] B ) -cn-> CC ) )
248 56 247 eqeltrid 
 |-  ( ph -> G e. ( ( A [,] B ) -cn-> CC ) )
249 4 5 6 187 218 248 ftc2 
 |-  ( ph -> S. ( A (,) B ) ( ( RR _D G ) ` s ) _d s = ( ( G ` B ) - ( G ` A ) ) )
250 10 155 249 3eqtrd 
 |-  ( ph -> S. ( A (,) B ) ( F ` x ) _d x = ( ( G ` B ) - ( G ` A ) ) )