Metamath Proof Explorer

Theorem fourierdlem95

Description: Algebraic manipulation of integrals, used by other lemmas. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem95.f 
|- ( ph -> F : RR --> RR )
fourierdlem95.xre 
|- ( ph -> X e. RR )
fourierdlem95.p 
|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( -u _pi + X ) /\ ( p ` m ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
fourierdlem95.m 
|- ( ph -> M e. NN )
fourierdlem95.v 
|- ( ph -> V e. ( P ` M ) )
fourierdlem95.x 
|- ( ph -> X e. ran V )
fourierdlem95.fcn 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem95.r 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( V ` i ) ) )
fourierdlem95.l 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( V ` ( i + 1 ) ) ) )
fourierdlem95.h 
|- H = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
fourierdlem95.k 
|- K = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
fourierdlem95.u 
|- U = ( s e. ( -u _pi [,] _pi ) |-> ( ( H ` s ) x. ( K ` s ) ) )
fourierdlem95.s 
|- S = ( s e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) )
fourierdlem95.g 
|- G = ( s e. ( -u _pi [,] _pi ) |-> ( ( U ` s ) x. ( S ` s ) ) )
fourierdlem95.i 
|- I = ( RR _D F )
fourierdlem95.ifn 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( I |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR )
fourierdlem95.b 
|- ( ph -> B e. ( ( I |` ( -oo (,) X ) ) limCC X ) )
fourierdlem95.c 
|- ( ph -> C e. ( ( I |` ( X (,) +oo ) ) limCC X ) )
fourierdlem95.y 
|- ( ph -> Y e. ( ( F |` ( X (,) +oo ) ) limCC X ) )
fourierdlem95.w 
|- ( ph -> W e. ( ( F |` ( -oo (,) X ) ) limCC X ) )
fourierdlem95.admvol 
|- ( ph -> A e. dom vol )
fourierdlem95.ass 
|- ( ph -> A C_ ( ( -u _pi [,] _pi ) \ { 0 } ) )
fourierlemenplusacver2eqitgdirker.e 
|- E = ( n e. NN |-> ( S. A ( G ` s ) _d s / _pi ) )
fourierdlem95.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 ) ) ) ) ) ) )
fourierdlem95.o 
|- ( ph -> O e. RR )
fourierdlem95.ifeqo 
|- ( ( ph /\ s e. A ) -> if ( 0 < s , Y , W ) = O )
fourierdlem95.itgdirker 
|- ( ( ph /\ n e. NN ) -> S. A ( ( D ` n ) ` s ) _d s = ( 1 / 2 ) )
Assertion fourierdlem95 
|- ( ( ph /\ n e. NN ) -> ( ( E ` n ) + ( O / 2 ) ) = S. A ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s )

Proof

Step Hyp Ref Expression
1 fourierdlem95.f 
 |-  ( ph -> F : RR --> RR )
2 fourierdlem95.xre 
 |-  ( ph -> X e. RR )
3 fourierdlem95.p 
 |-  P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( -u _pi + X ) /\ ( p ` m ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
4 fourierdlem95.m 
 |-  ( ph -> M e. NN )
5 fourierdlem95.v 
 |-  ( ph -> V e. ( P ` M ) )
6 fourierdlem95.x 
 |-  ( ph -> X e. ran V )
7 fourierdlem95.fcn 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) )
8 fourierdlem95.r 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( V ` i ) ) )
9 fourierdlem95.l 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( V ` ( i + 1 ) ) ) )
10 fourierdlem95.h 
 |-  H = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
11 fourierdlem95.k 
 |-  K = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
12 fourierdlem95.u 
 |-  U = ( s e. ( -u _pi [,] _pi ) |-> ( ( H ` s ) x. ( K ` s ) ) )
13 fourierdlem95.s 
 |-  S = ( s e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) )
14 fourierdlem95.g 
 |-  G = ( s e. ( -u _pi [,] _pi ) |-> ( ( U ` s ) x. ( S ` s ) ) )
15 fourierdlem95.i 
 |-  I = ( RR _D F )
16 fourierdlem95.ifn 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( I |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR )
17 fourierdlem95.b 
 |-  ( ph -> B e. ( ( I |` ( -oo (,) X ) ) limCC X ) )
18 fourierdlem95.c 
 |-  ( ph -> C e. ( ( I |` ( X (,) +oo ) ) limCC X ) )
19 fourierdlem95.y 
 |-  ( ph -> Y e. ( ( F |` ( X (,) +oo ) ) limCC X ) )
20 fourierdlem95.w 
 |-  ( ph -> W e. ( ( F |` ( -oo (,) X ) ) limCC X ) )
21 fourierdlem95.admvol 
 |-  ( ph -> A e. dom vol )
22 fourierdlem95.ass 
 |-  ( ph -> A C_ ( ( -u _pi [,] _pi ) \ { 0 } ) )
23 fourierlemenplusacver2eqitgdirker.e 
 |-  E = ( n e. NN |-> ( S. A ( G ` s ) _d s / _pi ) )
24 fourierdlem95.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 ) ) ) ) ) ) )
25 fourierdlem95.o 
 |-  ( ph -> O e. RR )
26 fourierdlem95.ifeqo 
 |-  ( ( ph /\ s e. A ) -> if ( 0 < s , Y , W ) = O )
27 fourierdlem95.itgdirker 
 |-  ( ( ph /\ n e. NN ) -> S. A ( ( D ` n ) ` s ) _d s = ( 1 / 2 ) )
28 simpr 
 |-  ( ( ph /\ n e. NN ) -> n e. NN )
29 22 difss2d 
 |-  ( ph -> A C_ ( -u _pi [,] _pi ) )
30 29 adantr 
 |-  ( ( ph /\ n e. NN ) -> A C_ ( -u _pi [,] _pi ) )
31 30 sselda 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> s e. ( -u _pi [,] _pi ) )
32 1 adantr 
 |-  ( ( ph /\ n e. NN ) -> F : RR --> RR )
33 2 adantr 
 |-  ( ( ph /\ n e. NN ) -> X e. RR )
34 ioossre 
 |-  ( X (,) +oo ) C_ RR
35 34 a1i 
 |-  ( ph -> ( X (,) +oo ) C_ RR )
36 1 35 fssresd 
 |-  ( ph -> ( F |` ( X (,) +oo ) ) : ( X (,) +oo ) --> RR )
37 ioosscn 
 |-  ( X (,) +oo ) C_ CC
38 37 a1i 
 |-  ( ph -> ( X (,) +oo ) C_ CC )
39 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
40 pnfxr 
 |-  +oo e. RR*
41 40 a1i 
 |-  ( ph -> +oo e. RR* )
42 2 ltpnfd 
 |-  ( ph -> X < +oo )
43 39 41 2 42 lptioo1cn 
 |-  ( ph -> X e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( X (,) +oo ) ) )
44 36 38 43 19 limcrecl 
 |-  ( ph -> Y e. RR )
45 44 adantr 
 |-  ( ( ph /\ n e. NN ) -> Y e. RR )
46 ioossre 
 |-  ( -oo (,) X ) C_ RR
47 46 a1i 
 |-  ( ph -> ( -oo (,) X ) C_ RR )
48 1 47 fssresd 
 |-  ( ph -> ( F |` ( -oo (,) X ) ) : ( -oo (,) X ) --> RR )
49 ioosscn 
 |-  ( -oo (,) X ) C_ CC
50 49 a1i 
 |-  ( ph -> ( -oo (,) X ) C_ CC )
51 mnfxr 
 |-  -oo e. RR*
52 51 a1i 
 |-  ( ph -> -oo e. RR* )
53 2 mnfltd 
 |-  ( ph -> -oo < X )
54 39 52 2 53 lptioo2cn 
 |-  ( ph -> X e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( -oo (,) X ) ) )
55 48 50 54 20 limcrecl 
 |-  ( ph -> W e. RR )
56 55 adantr 
 |-  ( ( ph /\ n e. NN ) -> W e. RR )
57 28 nnred 
 |-  ( ( ph /\ n e. NN ) -> n e. RR )
58 32 33 45 56 10 11 12 57 13 14 fourierdlem67 
 |-  ( ( ph /\ n e. NN ) -> G : ( -u _pi [,] _pi ) --> RR )
59 58 ffvelrnda 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( G ` s ) e. RR )
60 31 59 syldan 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> ( G ` s ) e. RR )
61 21 adantr 
 |-  ( ( ph /\ n e. NN ) -> A e. dom vol )
62 58 feqmptd 
 |-  ( ( ph /\ n e. NN ) -> G = ( s e. ( -u _pi [,] _pi ) |-> ( G ` s ) ) )
63 6 adantr 
 |-  ( ( ph /\ n e. NN ) -> X e. ran V )
64 19 adantr 
 |-  ( ( ph /\ n e. NN ) -> Y e. ( ( F |` ( X (,) +oo ) ) limCC X ) )
65 20 adantr 
 |-  ( ( ph /\ n e. NN ) -> W e. ( ( F |` ( -oo (,) X ) ) limCC X ) )
66 4 adantr 
 |-  ( ( ph /\ n e. NN ) -> M e. NN )
67 5 adantr 
 |-  ( ( ph /\ n e. NN ) -> V e. ( P ` M ) )
68 7 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) )
69 8 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( V ` i ) ) )
70 9 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( V ` ( i + 1 ) ) ) )
71 fveq2 
 |-  ( j = i -> ( V ` j ) = ( V ` i ) )
72 71 oveq1d 
 |-  ( j = i -> ( ( V ` j ) - X ) = ( ( V ` i ) - X ) )
73 72 cbvmptv 
 |-  ( j e. ( 0 ... M ) |-> ( ( V ` j ) - X ) ) = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) )
74 eqid 
 |-  ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = -u _pi /\ ( p ` m ) = _pi ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = -u _pi /\ ( p ` m ) = _pi ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
75 16 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( I |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR )
76 17 adantr 
 |-  ( ( ph /\ n e. NN ) -> B e. ( ( I |` ( -oo (,) X ) ) limCC X ) )
77 18 adantr 
 |-  ( ( ph /\ n e. NN ) -> C e. ( ( I |` ( X (,) +oo ) ) limCC X ) )
78 3 32 63 64 65 10 11 12 57 13 14 66 67 68 69 70 73 74 15 75 76 77 fourierdlem88 
 |-  ( ( ph /\ n e. NN ) -> G e. L^1 )
79 62 78 eqeltrrd 
 |-  ( ( ph /\ n e. NN ) -> ( s e. ( -u _pi [,] _pi ) |-> ( G ` s ) ) e. L^1 )
80 30 61 59 79 iblss 
 |-  ( ( ph /\ n e. NN ) -> ( s e. A |-> ( G ` s ) ) e. L^1 )
81 60 80 itgrecl 
 |-  ( ( ph /\ n e. NN ) -> S. A ( G ` s ) _d s e. RR )
82 pire 
 |-  _pi e. RR
83 82 a1i 
 |-  ( ( ph /\ n e. NN ) -> _pi e. RR )
84 pipos 
 |-  0 < _pi
85 82 84 gt0ne0ii 
 |-  _pi =/= 0
86 85 a1i 
 |-  ( ( ph /\ n e. NN ) -> _pi =/= 0 )
87 81 83 86 redivcld 
 |-  ( ( ph /\ n e. NN ) -> ( S. A ( G ` s ) _d s / _pi ) e. RR )
88 23 fvmpt2 
 |-  ( ( n e. NN /\ ( S. A ( G ` s ) _d s / _pi ) e. RR ) -> ( E ` n ) = ( S. A ( G ` s ) _d s / _pi ) )
89 28 87 88 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> ( E ` n ) = ( S. A ( G ` s ) _d s / _pi ) )
90 25 recnd 
 |-  ( ph -> O e. CC )
91 2cnd 
 |-  ( ph -> 2 e. CC )
92 2ne0 
 |-  2 =/= 0
93 92 a1i 
 |-  ( ph -> 2 =/= 0 )
94 90 91 93 divrecd 
 |-  ( ph -> ( O / 2 ) = ( O x. ( 1 / 2 ) ) )
95 94 adantr 
 |-  ( ( ph /\ n e. NN ) -> ( O / 2 ) = ( O x. ( 1 / 2 ) ) )
96 27 eqcomd 
 |-  ( ( ph /\ n e. NN ) -> ( 1 / 2 ) = S. A ( ( D ` n ) ` s ) _d s )
97 96 oveq2d 
 |-  ( ( ph /\ n e. NN ) -> ( O x. ( 1 / 2 ) ) = ( O x. S. A ( ( D ` n ) ` s ) _d s ) )
98 95 97 eqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( O / 2 ) = ( O x. S. A ( ( D ` n ) ` s ) _d s ) )
99 89 98 oveq12d 
 |-  ( ( ph /\ n e. NN ) -> ( ( E ` n ) + ( O / 2 ) ) = ( ( S. A ( G ` s ) _d s / _pi ) + ( O x. S. A ( ( D ` n ) ` s ) _d s ) ) )
100 22 sselda 
 |-  ( ( ph /\ s e. A ) -> s e. ( ( -u _pi [,] _pi ) \ { 0 } ) )
101 100 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> s e. ( ( -u _pi [,] _pi ) \ { 0 } ) )
102 eqid 
 |-  ( ( -u _pi [,] _pi ) \ { 0 } ) = ( ( -u _pi [,] _pi ) \ { 0 } )
103 1 2 44 55 24 10 11 12 13 14 102 fourierdlem66 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u _pi [,] _pi ) \ { 0 } ) ) -> ( G ` s ) = ( _pi x. ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) ) )
104 101 103 syldan 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> ( G ` s ) = ( _pi x. ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) ) )
105 104 itgeq2dv 
 |-  ( ( ph /\ n e. NN ) -> S. A ( G ` s ) _d s = S. A ( _pi x. ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) ) _d s )
106 105 oveq1d 
 |-  ( ( ph /\ n e. NN ) -> ( S. A ( G ` s ) _d s / _pi ) = ( S. A ( _pi x. ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) ) _d s / _pi ) )
107 83 recnd 
 |-  ( ( ph /\ n e. NN ) -> _pi e. CC )
108 1 adantr 
 |-  ( ( ph /\ s e. A ) -> F : RR --> RR )
109 2 adantr 
 |-  ( ( ph /\ s e. A ) -> X e. RR )
110 difss 
 |-  ( ( -u _pi [,] _pi ) \ { 0 } ) C_ ( -u _pi [,] _pi )
111 82 renegcli 
 |-  -u _pi e. RR
112 iccssre 
 |-  ( ( -u _pi e. RR /\ _pi e. RR ) -> ( -u _pi [,] _pi ) C_ RR )
113 111 82 112 mp2an 
 |-  ( -u _pi [,] _pi ) C_ RR
114 110 113 sstri 
 |-  ( ( -u _pi [,] _pi ) \ { 0 } ) C_ RR
115 114 100 sseldi 
 |-  ( ( ph /\ s e. A ) -> s e. RR )
116 109 115 readdcld 
 |-  ( ( ph /\ s e. A ) -> ( X + s ) e. RR )
117 108 116 ffvelrnd 
 |-  ( ( ph /\ s e. A ) -> ( F ` ( X + s ) ) e. RR )
118 44 55 ifcld 
 |-  ( ph -> if ( 0 < s , Y , W ) e. RR )
119 118 adantr 
 |-  ( ( ph /\ s e. A ) -> if ( 0 < s , Y , W ) e. RR )
120 117 119 resubcld 
 |-  ( ( ph /\ s e. A ) -> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) e. RR )
121 120 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) e. RR )
122 28 adantr 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> n e. NN )
123 115 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> s e. RR )
124 24 dirkerre 
 |-  ( ( n e. NN /\ s e. RR ) -> ( ( D ` n ) ` s ) e. RR )
125 122 123 124 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> ( ( D ` n ) ` s ) e. RR )
126 121 125 remulcld 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) e. RR )
127 104 eqcomd 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> ( _pi x. ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) ) = ( G ` s ) )
128 127 oveq1d 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> ( ( _pi x. ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) ) / _pi ) = ( ( G ` s ) / _pi ) )
129 picn 
 |-  _pi e. CC
130 129 a1i 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> _pi e. CC )
131 126 recnd 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) e. CC )
132 85 a1i 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> _pi =/= 0 )
133 130 131 130 132 div23d 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> ( ( _pi x. ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) ) / _pi ) = ( ( _pi / _pi ) x. ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) ) )
134 60 recnd 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> ( G ` s ) e. CC )
135 134 130 132 divrec2d 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> ( ( G ` s ) / _pi ) = ( ( 1 / _pi ) x. ( G ` s ) ) )
136 128 133 135 3eqtr3rd 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> ( ( 1 / _pi ) x. ( G ` s ) ) = ( ( _pi / _pi ) x. ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) ) )
137 129 85 dividi 
 |-  ( _pi / _pi ) = 1
138 137 a1i 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> ( _pi / _pi ) = 1 )
139 138 oveq1d 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> ( ( _pi / _pi ) x. ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) ) = ( 1 x. ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) ) )
140 131 mulid2d 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> ( 1 x. ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) ) = ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) )
141 136 139 140 3eqtrrd 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) = ( ( 1 / _pi ) x. ( G ` s ) ) )
142 141 mpteq2dva 
 |-  ( ( ph /\ n e. NN ) -> ( s e. A |-> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) ) = ( s e. A |-> ( ( 1 / _pi ) x. ( G ` s ) ) ) )
143 107 86 reccld 
 |-  ( ( ph /\ n e. NN ) -> ( 1 / _pi ) e. CC )
144 143 60 80 iblmulc2 
 |-  ( ( ph /\ n e. NN ) -> ( s e. A |-> ( ( 1 / _pi ) x. ( G ` s ) ) ) e. L^1 )
145 142 144 eqeltrd 
 |-  ( ( ph /\ n e. NN ) -> ( s e. A |-> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) ) e. L^1 )
146 107 126 145 itgmulc2 
 |-  ( ( ph /\ n e. NN ) -> ( _pi x. S. A ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) _d s ) = S. A ( _pi x. ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) ) _d s )
147 146 eqcomd 
 |-  ( ( ph /\ n e. NN ) -> S. A ( _pi x. ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) ) _d s = ( _pi x. S. A ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) _d s ) )
148 147 oveq1d 
 |-  ( ( ph /\ n e. NN ) -> ( S. A ( _pi x. ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) ) _d s / _pi ) = ( ( _pi x. S. A ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) _d s ) / _pi ) )
149 126 145 itgcl 
 |-  ( ( ph /\ n e. NN ) -> S. A ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) _d s e. CC )
150 149 107 86 divcan3d 
 |-  ( ( ph /\ n e. NN ) -> ( ( _pi x. S. A ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) _d s ) / _pi ) = S. A ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) _d s )
151 106 148 150 3eqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( S. A ( G ` s ) _d s / _pi ) = S. A ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) _d s )
152 90 adantr 
 |-  ( ( ph /\ n e. NN ) -> O e. CC )
153 113 sseli 
 |-  ( s e. ( -u _pi [,] _pi ) -> s e. RR )
154 153 124 sylan2 
 |-  ( ( n e. NN /\ s e. ( -u _pi [,] _pi ) ) -> ( ( D ` n ) ` s ) e. RR )
155 154 adantll 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( ( D ` n ) ` s ) e. RR )
156 111 a1i 
 |-  ( ( ph /\ n e. NN ) -> -u _pi e. RR )
157 ax-resscn 
 |-  RR C_ CC
158 157 a1i 
 |-  ( n e. NN -> RR C_ CC )
159 ssid 
 |-  CC C_ CC
160 cncfss 
 |-  ( ( RR C_ CC /\ CC C_ CC ) -> ( ( -u _pi [,] _pi ) -cn-> RR ) C_ ( ( -u _pi [,] _pi ) -cn-> CC ) )
161 158 159 160 sylancl 
 |-  ( n e. NN -> ( ( -u _pi [,] _pi ) -cn-> RR ) C_ ( ( -u _pi [,] _pi ) -cn-> CC ) )
162 eqid 
 |-  ( s e. RR |-> ( ( D ` n ) ` s ) ) = ( s e. RR |-> ( ( D ` n ) ` s ) )
163 24 dirkerf 
 |-  ( n e. NN -> ( D ` n ) : RR --> RR )
164 163 feqmptd 
 |-  ( n e. NN -> ( D ` n ) = ( s e. RR |-> ( ( D ` n ) ` s ) ) )
165 24 dirkercncf 
 |-  ( n e. NN -> ( D ` n ) e. ( RR -cn-> RR ) )
166 164 165 eqeltrrd 
 |-  ( n e. NN -> ( s e. RR |-> ( ( D ` n ) ` s ) ) e. ( RR -cn-> RR ) )
167 113 a1i 
 |-  ( n e. NN -> ( -u _pi [,] _pi ) C_ RR )
168 ssid 
 |-  RR C_ RR
169 168 a1i 
 |-  ( n e. NN -> RR C_ RR )
170 162 166 167 169 154 cncfmptssg 
 |-  ( n e. NN -> ( s e. ( -u _pi [,] _pi ) |-> ( ( D ` n ) ` s ) ) e. ( ( -u _pi [,] _pi ) -cn-> RR ) )
171 161 170 sseldd 
 |-  ( n e. NN -> ( s e. ( -u _pi [,] _pi ) |-> ( ( D ` n ) ` s ) ) e. ( ( -u _pi [,] _pi ) -cn-> CC ) )
172 171 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( s e. ( -u _pi [,] _pi ) |-> ( ( D ` n ) ` s ) ) e. ( ( -u _pi [,] _pi ) -cn-> CC ) )
173 cniccibl 
 |-  ( ( -u _pi e. RR /\ _pi e. RR /\ ( s e. ( -u _pi [,] _pi ) |-> ( ( D ` n ) ` s ) ) e. ( ( -u _pi [,] _pi ) -cn-> CC ) ) -> ( s e. ( -u _pi [,] _pi ) |-> ( ( D ` n ) ` s ) ) e. L^1 )
174 156 83 172 173 syl3anc 
 |-  ( ( ph /\ n e. NN ) -> ( s e. ( -u _pi [,] _pi ) |-> ( ( D ` n ) ` s ) ) e. L^1 )
175 30 61 155 174 iblss 
 |-  ( ( ph /\ n e. NN ) -> ( s e. A |-> ( ( D ` n ) ` s ) ) e. L^1 )
176 152 125 175 itgmulc2 
 |-  ( ( ph /\ n e. NN ) -> ( O x. S. A ( ( D ` n ) ` s ) _d s ) = S. A ( O x. ( ( D ` n ) ` s ) ) _d s )
177 151 176 oveq12d 
 |-  ( ( ph /\ n e. NN ) -> ( ( S. A ( G ` s ) _d s / _pi ) + ( O x. S. A ( ( D ` n ) ` s ) _d s ) ) = ( S. A ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) _d s + S. A ( O x. ( ( D ` n ) ` s ) ) _d s ) )
178 25 ad2antrr 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> O e. RR )
179 178 125 remulcld 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> ( O x. ( ( D ` n ) ` s ) ) e. RR )
180 152 125 175 iblmulc2 
 |-  ( ( ph /\ n e. NN ) -> ( s e. A |-> ( O x. ( ( D ` n ) ` s ) ) ) e. L^1 )
181 126 145 179 180 itgadd 
 |-  ( ( ph /\ n e. NN ) -> S. A ( ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) + ( O x. ( ( D ` n ) ` s ) ) ) _d s = ( S. A ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) _d s + S. A ( O x. ( ( D ` n ) ` s ) ) _d s ) )
182 26 eqcomd 
 |-  ( ( ph /\ s e. A ) -> O = if ( 0 < s , Y , W ) )
183 182 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> O = if ( 0 < s , Y , W ) )
184 183 oveq1d 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> ( O x. ( ( D ` n ) ` s ) ) = ( if ( 0 < s , Y , W ) x. ( ( D ` n ) ` s ) ) )
185 184 oveq2d 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> ( ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) + ( O x. ( ( D ` n ) ` s ) ) ) = ( ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) + ( if ( 0 < s , Y , W ) x. ( ( D ` n ) ` s ) ) ) )
186 117 recnd 
 |-  ( ( ph /\ s e. A ) -> ( F ` ( X + s ) ) e. CC )
187 186 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> ( F ` ( X + s ) ) e. CC )
188 119 recnd 
 |-  ( ( ph /\ s e. A ) -> if ( 0 < s , Y , W ) e. CC )
189 188 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> if ( 0 < s , Y , W ) e. CC )
190 125 recnd 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> ( ( D ` n ) ` s ) e. CC )
191 187 189 190 subdird 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) = ( ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) - ( if ( 0 < s , Y , W ) x. ( ( D ` n ) ` s ) ) ) )
192 191 oveq1d 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> ( ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) + ( if ( 0 < s , Y , W ) x. ( ( D ` n ) ` s ) ) ) = ( ( ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) - ( if ( 0 < s , Y , W ) x. ( ( D ` n ) ` s ) ) ) + ( if ( 0 < s , Y , W ) x. ( ( D ` n ) ` s ) ) ) )
193 187 190 mulcld 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) e. CC )
194 189 190 mulcld 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> ( if ( 0 < s , Y , W ) x. ( ( D ` n ) ` s ) ) e. CC )
195 193 194 npcand 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> ( ( ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) - ( if ( 0 < s , Y , W ) x. ( ( D ` n ) ` s ) ) ) + ( if ( 0 < s , Y , W ) x. ( ( D ` n ) ` s ) ) ) = ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) )
196 185 192 195 3eqtrd 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. A ) -> ( ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) + ( O x. ( ( D ` n ) ` s ) ) ) = ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) )
197 196 itgeq2dv 
 |-  ( ( ph /\ n e. NN ) -> S. A ( ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) + ( O x. ( ( D ` n ) ` s ) ) ) _d s = S. A ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s )
198 181 197 eqtr3d 
 |-  ( ( ph /\ n e. NN ) -> ( S. A ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( ( D ` n ) ` s ) ) _d s + S. A ( O x. ( ( D ` n ) ` s ) ) _d s ) = S. A ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s )
199 99 177 198 3eqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( ( E ` n ) + ( O / 2 ) ) = S. A ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s )