Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem83 Structured version   Unicode version

Theorem fourierdlem83 31813
Description: The fourier partial sum for  F rewritten as an integral. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem83.f  |-  ( ph  ->  F : RR --> RR )
fourierdlem83.c  |-  C  =  ( -u pi (,) pi )
fourierdlem83.fl1  |-  ( ph  ->  ( F  |`  C )  e.  L^1 )
fourierdlem83.a  |-  A  =  ( n  e.  NN0  |->  ( S. C ( ( F `  x )  x.  ( cos `  (
n  x.  x ) ) )  _d x  /  pi ) )
fourierdlem83.b  |-  B  =  ( n  e.  NN  |->  ( S. C ( ( F `  x )  x.  ( sin `  (
n  x.  x ) ) )  _d x  /  pi ) )
fourierdlem83.x  |-  ( ph  ->  X  e.  RR )
fourierdlem83.s  |-  S  =  ( m  e.  NN  |->  ( ( ( A `
 0 )  / 
2 )  +  sum_ n  e.  ( 1 ... m ) ( ( ( A `  n
)  x.  ( cos `  ( n  x.  X
) ) )  +  ( ( B `  n )  x.  ( sin `  ( n  x.  X ) ) ) ) ) )
fourierdlem83.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 ) ) ) ) ) ) )
fourierdlem83.n  |-  ( ph  ->  N  e.  NN )
Assertion
Ref Expression
fourierdlem83  |-  ( ph  ->  ( S `  N
)  =  S. C
( ( F `  x )  x.  (
( D `  N
) `  ( x  -  X ) ) )  _d x )
Distinct variable groups:    A, m, n    B, m    x, C, n, s    x, D, s    n, F, x   
x, N    m, N, n    N, s    x, X   
m, X, n    X, s    ph, x, n    ph, m    ph, s
Allowed substitution hints:    A( x, s)    B( x, n, s)    C( m)    D( m, n)    S( x, m, n, s)    F( m, s)

Proof of Theorem fourierdlem83
Dummy variables  b 
c  y  k  w  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem83.s . . . 4  |-  S  =  ( m  e.  NN  |->  ( ( ( A `
 0 )  / 
2 )  +  sum_ n  e.  ( 1 ... m ) ( ( ( A `  n
)  x.  ( cos `  ( n  x.  X
) ) )  +  ( ( B `  n )  x.  ( sin `  ( n  x.  X ) ) ) ) ) )
21a1i 11 . . 3  |-  ( ph  ->  S  =  ( m  e.  NN  |->  ( ( ( A `  0
)  /  2 )  +  sum_ n  e.  ( 1 ... m ) ( ( ( A `
 n )  x.  ( cos `  (
n  x.  X ) ) )  +  ( ( B `  n
)  x.  ( sin `  ( n  x.  X
) ) ) ) ) ) )
3 oveq2 6303 . . . . . 6  |-  ( m  =  N  ->  (
1 ... m )  =  ( 1 ... N
) )
43sumeq1d 13503 . . . . 5  |-  ( m  =  N  ->  sum_ n  e.  ( 1 ... m
) ( ( ( A `  n )  x.  ( cos `  (
n  x.  X ) ) )  +  ( ( B `  n
)  x.  ( sin `  ( n  x.  X
) ) ) )  =  sum_ n  e.  ( 1 ... N ) ( ( ( A `
 n )  x.  ( cos `  (
n  x.  X ) ) )  +  ( ( B `  n
)  x.  ( sin `  ( n  x.  X
) ) ) ) )
54oveq2d 6311 . . . 4  |-  ( m  =  N  ->  (
( ( A ` 
0 )  /  2
)  +  sum_ n  e.  ( 1 ... m
) ( ( ( A `  n )  x.  ( cos `  (
n  x.  X ) ) )  +  ( ( B `  n
)  x.  ( sin `  ( n  x.  X
) ) ) ) )  =  ( ( ( A `  0
)  /  2 )  +  sum_ n  e.  ( 1 ... N ) ( ( ( A `
 n )  x.  ( cos `  (
n  x.  X ) ) )  +  ( ( B `  n
)  x.  ( sin `  ( n  x.  X
) ) ) ) ) )
65adantl 466 . . 3  |-  ( (
ph  /\  m  =  N )  ->  (
( ( A ` 
0 )  /  2
)  +  sum_ n  e.  ( 1 ... m
) ( ( ( A `  n )  x.  ( cos `  (
n  x.  X ) ) )  +  ( ( B `  n
)  x.  ( sin `  ( n  x.  X
) ) ) ) )  =  ( ( ( A `  0
)  /  2 )  +  sum_ n  e.  ( 1 ... N ) ( ( ( A `
 n )  x.  ( cos `  (
n  x.  X ) ) )  +  ( ( B `  n
)  x.  ( sin `  ( n  x.  X
) ) ) ) ) )
7 fourierdlem83.n . . 3  |-  ( ph  ->  N  e.  NN )
8 id 22 . . . . . 6  |-  ( ph  ->  ph )
9 0nn0 10822 . . . . . . 7  |-  0  e.  NN0
109a1i 11 . . . . . 6  |-  ( ph  ->  0  e.  NN0 )
119elexi 3128 . . . . . . 7  |-  0  e.  _V
12 eleq1 2539 . . . . . . . . 9  |-  ( n  =  0  ->  (
n  e.  NN0  <->  0  e.  NN0 ) )
1312anbi2d 703 . . . . . . . 8  |-  ( n  =  0  ->  (
( ph  /\  n  e.  NN0 )  <->  ( ph  /\  0  e.  NN0 )
) )
14 fveq2 5872 . . . . . . . . 9  |-  ( n  =  0  ->  ( A `  n )  =  ( A ` 
0 ) )
1514eleq1d 2536 . . . . . . . 8  |-  ( n  =  0  ->  (
( A `  n
)  e.  RR  <->  ( A `  0 )  e.  RR ) )
1613, 15imbi12d 320 . . . . . . 7  |-  ( n  =  0  ->  (
( ( ph  /\  n  e.  NN0 )  -> 
( A `  n
)  e.  RR )  <-> 
( ( ph  /\  0  e.  NN0 )  -> 
( A `  0
)  e.  RR ) ) )
17 fourierdlem83.f . . . . . . . . . 10  |-  ( ph  ->  F : RR --> RR )
18 fourierdlem83.c . . . . . . . . . 10  |-  C  =  ( -u pi (,) pi )
19 fourierdlem83.fl1 . . . . . . . . . 10  |-  ( ph  ->  ( F  |`  C )  e.  L^1 )
20 fourierdlem83.a . . . . . . . . . 10  |-  A  =  ( n  e.  NN0  |->  ( S. C ( ( F `  x )  x.  ( cos `  (
n  x.  x ) ) )  _d x  /  pi ) )
21 fourierdlem83.b . . . . . . . . . 10  |-  B  =  ( n  e.  NN  |->  ( S. C ( ( F `  x )  x.  ( sin `  (
n  x.  x ) ) )  _d x  /  pi ) )
2217, 18, 19, 20, 21fourierdlem22 31752 . . . . . . . . 9  |-  ( ph  ->  ( ( n  e. 
NN0  ->  ( A `  n )  e.  RR )  /\  ( n  e.  NN  ->  ( B `  n )  e.  RR ) ) )
2322simpld 459 . . . . . . . 8  |-  ( ph  ->  ( n  e.  NN0  ->  ( A `  n
)  e.  RR ) )
2423imp 429 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN0 )  ->  ( A `  n )  e.  RR )
2511, 16, 24vtocl 3170 . . . . . 6  |-  ( (
ph  /\  0  e.  NN0 )  ->  ( A `  0 )  e.  RR )
268, 10, 25syl2anc 661 . . . . 5  |-  ( ph  ->  ( A `  0
)  e.  RR )
27 2re 10617 . . . . . 6  |-  2  e.  RR
2827a1i 11 . . . . 5  |-  ( ph  ->  2  e.  RR )
29 2ne0 10640 . . . . . 6  |-  2  =/=  0
3029a1i 11 . . . . 5  |-  ( ph  ->  2  =/=  0 )
3126, 28, 30redivcld 10384 . . . 4  |-  ( ph  ->  ( ( A ` 
0 )  /  2
)  e.  RR )
32 fzfid 12063 . . . . 5  |-  ( ph  ->  ( 1 ... N
)  e.  Fin )
33 eleq1 2539 . . . . . . . . . . . . . 14  |-  ( k  =  n  ->  (
k  e.  NN0  <->  n  e.  NN0 ) )
3433anbi2d 703 . . . . . . . . . . . . 13  |-  ( k  =  n  ->  (
( ph  /\  k  e.  NN0 )  <->  ( ph  /\  n  e.  NN0 )
) )
35 simpl 457 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  =  n  /\  x  e.  C )  ->  k  =  n )
3635oveq1d 6310 . . . . . . . . . . . . . . . . 17  |-  ( ( k  =  n  /\  x  e.  C )  ->  ( k  x.  x
)  =  ( n  x.  x ) )
3736fveq2d 5876 . . . . . . . . . . . . . . . 16  |-  ( ( k  =  n  /\  x  e.  C )  ->  ( cos `  (
k  x.  x ) )  =  ( cos `  ( n  x.  x
) ) )
3837oveq2d 6311 . . . . . . . . . . . . . . 15  |-  ( ( k  =  n  /\  x  e.  C )  ->  ( ( F `  x )  x.  ( cos `  ( k  x.  x ) ) )  =  ( ( F `
 x )  x.  ( cos `  (
n  x.  x ) ) ) )
3938itgeq2dv 22056 . . . . . . . . . . . . . 14  |-  ( k  =  n  ->  S. C ( ( F `
 x )  x.  ( cos `  (
k  x.  x ) ) )  _d x  =  S. C ( ( F `  x
)  x.  ( cos `  ( n  x.  x
) ) )  _d x )
4039eleq1d 2536 . . . . . . . . . . . . 13  |-  ( k  =  n  ->  ( S. C ( ( F `
 x )  x.  ( cos `  (
k  x.  x ) ) )  _d x  e.  RR  <->  S. C
( ( F `  x )  x.  ( cos `  ( n  x.  x ) ) )  _d x  e.  RR ) )
4134, 40imbi12d 320 . . . . . . . . . . . 12  |-  ( k  =  n  ->  (
( ( ph  /\  k  e.  NN0 )  ->  S. C ( ( F `
 x )  x.  ( cos `  (
k  x.  x ) ) )  _d x  e.  RR )  <->  ( ( ph  /\  n  e.  NN0 )  ->  S. C ( ( F `  x
)  x.  ( cos `  ( n  x.  x
) ) )  _d x  e.  RR ) ) )
4217adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN0 )  ->  F : RR
--> RR )
4319adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( F  |`  C )  e.  L^1 )
44 simpr 461 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN0 )  ->  k  e.  NN0 )
4542, 18, 43, 20, 44fourierdlem16 31746 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
( A `  k
)  e.  RR  /\  ( x  e.  C  |->  ( F `  x
) )  e.  L^1 )  /\  S. C
( ( F `  x )  x.  ( cos `  ( k  x.  x ) ) )  _d x  e.  RR ) )
4645simprd 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN0 )  ->  S. C
( ( F `  x )  x.  ( cos `  ( k  x.  x ) ) )  _d x  e.  RR )
4741, 46chvarv 1983 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN0 )  ->  S. C
( ( F `  x )  x.  ( cos `  ( n  x.  x ) ) )  _d x  e.  RR )
48 pire 22718 . . . . . . . . . . . 12  |-  pi  e.  RR
4948a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN0 )  ->  pi  e.  RR )
50 0re 9608 . . . . . . . . . . . . 13  |-  0  e.  RR
51 pipos 22720 . . . . . . . . . . . . 13  |-  0  <  pi
52 ltne 9693 . . . . . . . . . . . . 13  |-  ( ( 0  e.  RR  /\  0  <  pi )  ->  pi  =/=  0 )
5350, 51, 52mp2an 672 . . . . . . . . . . . 12  |-  pi  =/=  0
5453a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN0 )  ->  pi  =/=  0 )
5547, 49, 54redivcld 10384 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  NN0 )  ->  ( S. C ( ( F `
 x )  x.  ( cos `  (
n  x.  x ) ) )  _d x  /  pi )  e.  RR )
5655, 20fmptd 6056 . . . . . . . . 9  |-  ( ph  ->  A : NN0 --> RR )
5756adantr 465 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  A : NN0 --> RR )
58 nnssnn0 10810 . . . . . . . . . . 11  |-  NN  C_  NN0
5958a1i 11 . . . . . . . . . 10  |-  ( n  e.  ( 1 ... N )  ->  NN  C_ 
NN0 )
60 elfznn 11726 . . . . . . . . . 10  |-  ( n  e.  ( 1 ... N )  ->  n  e.  NN )
6159, 60sseldd 3510 . . . . . . . . 9  |-  ( n  e.  ( 1 ... N )  ->  n  e.  NN0 )
6261adantl 466 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  n  e.  NN0 )
6357, 62ffvelrnd 6033 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  ( A `  n )  e.  RR )
6462nn0red 10865 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  n  e.  RR )
65 fourierdlem83.x . . . . . . . . . 10  |-  ( ph  ->  X  e.  RR )
6665adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  X  e.  RR )
6764, 66remulcld 9636 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
n  x.  X )  e.  RR )
6867recoscld 13757 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  ( cos `  ( n  x.  X ) )  e.  RR )
6963, 68remulcld 9636 . . . . . 6  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( A `  n
)  x.  ( cos `  ( n  x.  X
) ) )  e.  RR )
70 eleq1 2539 . . . . . . . . . . . . . 14  |-  ( k  =  n  ->  (
k  e.  NN  <->  n  e.  NN ) )
7170anbi2d 703 . . . . . . . . . . . . 13  |-  ( k  =  n  ->  (
( ph  /\  k  e.  NN )  <->  ( ph  /\  n  e.  NN ) ) )
72 oveq1 6302 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  n  ->  (
k  x.  x )  =  ( n  x.  x ) )
7372fveq2d 5876 . . . . . . . . . . . . . . . . 17  |-  ( k  =  n  ->  ( sin `  ( k  x.  x ) )  =  ( sin `  (
n  x.  x ) ) )
7473oveq2d 6311 . . . . . . . . . . . . . . . 16  |-  ( k  =  n  ->  (
( F `  x
)  x.  ( sin `  ( k  x.  x
) ) )  =  ( ( F `  x )  x.  ( sin `  ( n  x.  x ) ) ) )
7574adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( k  =  n  /\  x  e.  C )  ->  ( ( F `  x )  x.  ( sin `  ( k  x.  x ) ) )  =  ( ( F `
 x )  x.  ( sin `  (
n  x.  x ) ) ) )
7675itgeq2dv 22056 . . . . . . . . . . . . . 14  |-  ( k  =  n  ->  S. C ( ( F `
 x )  x.  ( sin `  (
k  x.  x ) ) )  _d x  =  S. C ( ( F `  x
)  x.  ( sin `  ( n  x.  x
) ) )  _d x )
7776eleq1d 2536 . . . . . . . . . . . . 13  |-  ( k  =  n  ->  ( S. C ( ( F `
 x )  x.  ( sin `  (
k  x.  x ) ) )  _d x  e.  RR  <->  S. C
( ( F `  x )  x.  ( sin `  ( n  x.  x ) ) )  _d x  e.  RR ) )
7871, 77imbi12d 320 . . . . . . . . . . . 12  |-  ( k  =  n  ->  (
( ( ph  /\  k  e.  NN )  ->  S. C ( ( F `  x )  x.  ( sin `  (
k  x.  x ) ) )  _d x  e.  RR )  <->  ( ( ph  /\  n  e.  NN )  ->  S. C ( ( F `  x
)  x.  ( sin `  ( n  x.  x
) ) )  _d x  e.  RR ) ) )
7917adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  F : RR
--> RR )
8019adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  ( F  |`  C )  e.  L^1 )
81 simpr 461 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  NN )
8279, 18, 80, 21, 81fourierdlem21 31751 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( B `  k
)  e.  RR  /\  ( x  e.  C  |->  ( ( F `  x )  x.  ( sin `  ( k  x.  x ) ) ) )  e.  L^1 )  /\  S. C
( ( F `  x )  x.  ( sin `  ( k  x.  x ) ) )  _d x  e.  RR ) )
8382simprd 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  S. C
( ( F `  x )  x.  ( sin `  ( k  x.  x ) ) )  _d x  e.  RR )
8478, 83chvarv 1983 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  S. C
( ( F `  x )  x.  ( sin `  ( n  x.  x ) ) )  _d x  e.  RR )
8548a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  pi  e.  RR )
8653a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  pi  =/=  0 )
8784, 85, 86redivcld 10384 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  NN )  ->  ( S. C ( ( F `
 x )  x.  ( sin `  (
n  x.  x ) ) )  _d x  /  pi )  e.  RR )
8887, 21fmptd 6056 . . . . . . . . 9  |-  ( ph  ->  B : NN --> RR )
8988adantr 465 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  B : NN --> RR )
9060adantl 466 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  n  e.  NN )
9189, 90ffvelrnd 6033 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  ( B `  n )  e.  RR )
9267resincld 13756 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  ( sin `  ( n  x.  X ) )  e.  RR )
9391, 92remulcld 9636 . . . . . 6  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( B `  n
)  x.  ( sin `  ( n  x.  X
) ) )  e.  RR )
9469, 93readdcld 9635 . . . . 5  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( ( A `  n )  x.  ( cos `  ( n  x.  X ) ) )  +  ( ( B `
 n )  x.  ( sin `  (
n  x.  X ) ) ) )  e.  RR )
9532, 94fsumrecl 13536 . . . 4  |-  ( ph  -> 
sum_ n  e.  (
1 ... N ) ( ( ( A `  n )  x.  ( cos `  ( n  x.  X ) ) )  +  ( ( B `
 n )  x.  ( sin `  (
n  x.  X ) ) ) )  e.  RR )
9631, 95readdcld 9635 . . 3  |-  ( ph  ->  ( ( ( A `
 0 )  / 
2 )  +  sum_ n  e.  ( 1 ... N ) ( ( ( A `  n
)  x.  ( cos `  ( n  x.  X
) ) )  +  ( ( B `  n )  x.  ( sin `  ( n  x.  X ) ) ) ) )  e.  RR )
972, 6, 7, 96fvmptd 5962 . 2  |-  ( ph  ->  ( S `  N
)  =  ( ( ( A `  0
)  /  2 )  +  sum_ n  e.  ( 1 ... N ) ( ( ( A `
 n )  x.  ( cos `  (
n  x.  X ) ) )  +  ( ( B `  n
)  x.  ( sin `  ( n  x.  X
) ) ) ) ) )
9820a1i 11 . . . . . . 7  |-  ( ph  ->  A  =  ( n  e.  NN0  |->  ( S. C ( ( F `
 x )  x.  ( cos `  (
n  x.  x ) ) )  _d x  /  pi ) ) )
99 oveq1 6302 . . . . . . . . . . . . 13  |-  ( n  =  0  ->  (
n  x.  x )  =  ( 0  x.  x ) )
10099fveq2d 5876 . . . . . . . . . . . 12  |-  ( n  =  0  ->  ( cos `  ( n  x.  x ) )  =  ( cos `  (
0  x.  x ) ) )
101100oveq2d 6311 . . . . . . . . . . 11  |-  ( n  =  0  ->  (
( F `  x
)  x.  ( cos `  ( n  x.  x
) ) )  =  ( ( F `  x )  x.  ( cos `  ( 0  x.  x ) ) ) )
102101adantr 465 . . . . . . . . . 10  |-  ( ( n  =  0  /\  x  e.  C )  ->  ( ( F `
 x )  x.  ( cos `  (
n  x.  x ) ) )  =  ( ( F `  x
)  x.  ( cos `  ( 0  x.  x
) ) ) )
103102itgeq2dv 22056 . . . . . . . . 9  |-  ( n  =  0  ->  S. C ( ( F `
 x )  x.  ( cos `  (
n  x.  x ) ) )  _d x  =  S. C ( ( F `  x
)  x.  ( cos `  ( 0  x.  x
) ) )  _d x )
104103adantl 466 . . . . . . . 8  |-  ( (
ph  /\  n  = 
0 )  ->  S. C ( ( F `
 x )  x.  ( cos `  (
n  x.  x ) ) )  _d x  =  S. C ( ( F `  x
)  x.  ( cos `  ( 0  x.  x
) ) )  _d x )
105104oveq1d 6310 . . . . . . 7  |-  ( (
ph  /\  n  = 
0 )  ->  ( S. C ( ( F `
 x )  x.  ( cos `  (
n  x.  x ) ) )  _d x  /  pi )  =  ( S. C ( ( F `  x
)  x.  ( cos `  ( 0  x.  x
) ) )  _d x  /  pi ) )
10617, 18, 19, 20, 10fourierdlem16 31746 . . . . . . . . 9  |-  ( ph  ->  ( ( ( A `
 0 )  e.  RR  /\  ( x  e.  C  |->  ( F `
 x ) )  e.  L^1 )  /\  S. C ( ( F `  x
)  x.  ( cos `  ( 0  x.  x
) ) )  _d x  e.  RR ) )
107106simprd 463 . . . . . . . 8  |-  ( ph  ->  S. C ( ( F `  x )  x.  ( cos `  (
0  x.  x ) ) )  _d x  e.  RR )
10848a1i 11 . . . . . . . 8  |-  ( ph  ->  pi  e.  RR )
10953a1i 11 . . . . . . . 8  |-  ( ph  ->  pi  =/=  0 )
110107, 108, 109redivcld 10384 . . . . . . 7  |-  ( ph  ->  ( S. C ( ( F `  x
)  x.  ( cos `  ( 0  x.  x
) ) )  _d x  /  pi )  e.  RR )
11198, 105, 10, 110fvmptd 5962 . . . . . 6  |-  ( ph  ->  ( A `  0
)  =  ( S. C ( ( F `
 x )  x.  ( cos `  (
0  x.  x ) ) )  _d x  /  pi ) )
112 ioosscn 31414 . . . . . . . . . . . . . . . 16  |-  ( -u pi (,) pi )  C_  CC
113112a1i 11 . . . . . . . . . . . . . . 15  |-  ( x  e.  C  ->  ( -u pi (,) pi ) 
C_  CC )
114 id 22 . . . . . . . . . . . . . . . 16  |-  ( x  e.  C  ->  x  e.  C )
115114, 18syl6eleq 2565 . . . . . . . . . . . . . . 15  |-  ( x  e.  C  ->  x  e.  ( -u pi (,) pi ) )
116113, 115sseldd 3510 . . . . . . . . . . . . . 14  |-  ( x  e.  C  ->  x  e.  CC )
117116mul02d 9789 . . . . . . . . . . . . 13  |-  ( x  e.  C  ->  (
0  x.  x )  =  0 )
118117fveq2d 5876 . . . . . . . . . . . 12  |-  ( x  e.  C  ->  ( cos `  ( 0  x.  x ) )  =  ( cos `  0
) )
119 cos0 13763 . . . . . . . . . . . . 13  |-  ( cos `  0 )  =  1
120119a1i 11 . . . . . . . . . . . 12  |-  ( x  e.  C  ->  ( cos `  0 )  =  1 )
121118, 120eqtrd 2508 . . . . . . . . . . 11  |-  ( x  e.  C  ->  ( cos `  ( 0  x.  x ) )  =  1 )
122121oveq2d 6311 . . . . . . . . . 10  |-  ( x  e.  C  ->  (
( F `  x
)  x.  ( cos `  ( 0  x.  x
) ) )  =  ( ( F `  x )  x.  1 ) )
123122adantl 466 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  C )  ->  (
( F `  x
)  x.  ( cos `  ( 0  x.  x
) ) )  =  ( ( F `  x )  x.  1 ) )
124 ax-resscn 9561 . . . . . . . . . . . 12  |-  RR  C_  CC
125124a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  C )  ->  RR  C_  CC )
12617adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  C )  ->  F : RR --> RR )
127 ioossre 11598 . . . . . . . . . . . . . 14  |-  ( -u pi (,) pi )  C_  RR
128127, 115sseldi 3507 . . . . . . . . . . . . 13  |-  ( x  e.  C  ->  x  e.  RR )
129128adantl 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  C )  ->  x  e.  RR )
130126, 129ffvelrnd 6033 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  C )  ->  ( F `  x )  e.  RR )
131125, 130sseldd 3510 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  C )  ->  ( F `  x )  e.  CC )
132131mulid1d 9625 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  C )  ->  (
( F `  x
)  x.  1 )  =  ( F `  x ) )
133123, 132eqtrd 2508 . . . . . . . 8  |-  ( (
ph  /\  x  e.  C )  ->  (
( F `  x
)  x.  ( cos `  ( 0  x.  x
) ) )  =  ( F `  x
) )
134133itgeq2dv 22056 . . . . . . 7  |-  ( ph  ->  S. C ( ( F `  x )  x.  ( cos `  (
0  x.  x ) ) )  _d x  =  S. C ( F `  x )  _d x )
135134oveq1d 6310 . . . . . 6  |-  ( ph  ->  ( S. C ( ( F `  x
)  x.  ( cos `  ( 0  x.  x
) ) )  _d x  /  pi )  =  ( S. C
( F `  x
)  _d x  /  pi ) )
136111, 135eqtrd 2508 . . . . 5  |-  ( ph  ->  ( A `  0
)  =  ( S. C ( F `  x )  _d x  /  pi ) )
137136oveq1d 6310 . . . 4  |-  ( ph  ->  ( ( A ` 
0 )  /  2
)  =  ( ( S. C ( F `
 x )  _d x  /  pi )  /  2 ) )
13817feqmptd 5927 . . . . . . . . 9  |-  ( ph  ->  F  =  ( x  e.  RR  |->  ( F `
 x ) ) )
139138reseq1d 5278 . . . . . . . 8  |-  ( ph  ->  ( F  |`  C )  =  ( ( x  e.  RR  |->  ( F `
 x ) )  |`  C ) )
14048a1i 11 . . . . . . . . . . . . 13  |-  ( x  e.  C  ->  pi  e.  RR )
141140renegcld 9998 . . . . . . . . . . . 12  |-  ( x  e.  C  ->  -u pi  e.  RR )
142 ioossicc 11622 . . . . . . . . . . . . . 14  |-  ( -u pi (,) pi )  C_  ( -u pi [,] pi )
14318, 142eqsstri 3539 . . . . . . . . . . . . 13  |-  C  C_  ( -u pi [,] pi )
144143sseli 3505 . . . . . . . . . . . 12  |-  ( x  e.  C  ->  x  e.  ( -u pi [,] pi ) )
145 eliccre 31427 . . . . . . . . . . . 12  |-  ( (
-u pi  e.  RR  /\  pi  e.  RR  /\  x  e.  ( -u pi [,] pi ) )  ->  x  e.  RR )
146141, 140, 144, 145syl3anc 1228 . . . . . . . . . . 11  |-  ( x  e.  C  ->  x  e.  RR )
147146ssriv 3513 . . . . . . . . . 10  |-  C  C_  RR
148 resmpt 5329 . . . . . . . . . 10  |-  ( C 
C_  RR  ->  ( ( x  e.  RR  |->  ( F `  x ) )  |`  C )  =  ( x  e.  C  |->  ( F `  x ) ) )
149147, 148ax-mp 5 . . . . . . . . 9  |-  ( ( x  e.  RR  |->  ( F `  x ) )  |`  C )  =  ( x  e.  C  |->  ( F `  x ) )
150149a1i 11 . . . . . . . 8  |-  ( ph  ->  ( ( x  e.  RR  |->  ( F `  x ) )  |`  C )  =  ( x  e.  C  |->  ( F `  x ) ) )
151 eqidd 2468 . . . . . . . 8  |-  ( ph  ->  ( x  e.  C  |->  ( F `  x
) )  =  ( x  e.  C  |->  ( F `  x ) ) )
152139, 150, 1513eqtrrd 2513 . . . . . . 7  |-  ( ph  ->  ( x  e.  C  |->  ( F `  x
) )  =  ( F  |`  C )
)
153152, 19eqeltrd 2555 . . . . . 6  |-  ( ph  ->  ( x  e.  C  |->  ( F `  x
) )  e.  L^1 )
154130, 153itgcl 22058 . . . . 5  |-  ( ph  ->  S. C ( F `
 x )  _d x  e.  CC )
155124, 108sseldi 3507 . . . . 5  |-  ( ph  ->  pi  e.  CC )
156124, 28sseldi 3507 . . . . 5  |-  ( ph  ->  2  e.  CC )
157154, 155, 156, 109, 30divdiv32d 10357 . . . 4  |-  ( ph  ->  ( ( S. C
( F `  x
)  _d x  /  pi )  /  2
)  =  ( ( S. C ( F `
 x )  _d x  /  2 )  /  pi ) )
158154, 156, 30divrecd 10335 . . . . . 6  |-  ( ph  ->  ( S. C ( F `  x )  _d x  /  2
)  =  ( S. C ( F `  x )  _d x  x.  ( 1  / 
2 ) ) )
159156, 30reccld 10325 . . . . . . 7  |-  ( ph  ->  ( 1  /  2
)  e.  CC )
160154, 159mulcomd 9629 . . . . . 6  |-  ( ph  ->  ( S. C ( F `  x )  _d x  x.  (
1  /  2 ) )  =  ( ( 1  /  2 )  x.  S. C ( F `  x )  _d x ) )
161159, 130, 153itgmulc2 22108 . . . . . 6  |-  ( ph  ->  ( ( 1  / 
2 )  x.  S. C ( F `  x )  _d x )  =  S. C
( ( 1  / 
2 )  x.  ( F `  x )
)  _d x )
162158, 160, 1613eqtrd 2512 . . . . 5  |-  ( ph  ->  ( S. C ( F `  x )  _d x  /  2
)  =  S. C
( ( 1  / 
2 )  x.  ( F `  x )
)  _d x )
163162oveq1d 6310 . . . 4  |-  ( ph  ->  ( ( S. C
( F `  x
)  _d x  / 
2 )  /  pi )  =  ( S. C ( ( 1  /  2 )  x.  ( F `  x
) )  _d x  /  pi ) )
164137, 157, 1633eqtrd 2512 . . 3  |-  ( ph  ->  ( ( A ` 
0 )  /  2
)  =  ( S. C ( ( 1  /  2 )  x.  ( F `  x
) )  _d x  /  pi ) )
16562, 55syldan 470 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  ( S. C ( ( F `
 x )  x.  ( cos `  (
n  x.  x ) ) )  _d x  /  pi )  e.  RR )
16620fvmpt2 5964 . . . . . . . . . . 11  |-  ( ( n  e.  NN0  /\  ( S. C ( ( F `  x )  x.  ( cos `  (
n  x.  x ) ) )  _d x  /  pi )  e.  RR )  ->  ( A `  n )  =  ( S. C
( ( F `  x )  x.  ( cos `  ( n  x.  x ) ) )  _d x  /  pi ) )
16762, 165, 166syl2anc 661 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  ( A `  n )  =  ( S. C
( ( F `  x )  x.  ( cos `  ( n  x.  x ) ) )  _d x  /  pi ) )
168167oveq1d 6310 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( A `  n
)  x.  ( cos `  ( n  x.  X
) ) )  =  ( ( S. C
( ( F `  x )  x.  ( cos `  ( n  x.  x ) ) )  _d x  /  pi )  x.  ( cos `  ( n  x.  X
) ) ) )
169124, 165sseldi 3507 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  ( S. C ( ( F `
 x )  x.  ( cos `  (
n  x.  x ) ) )  _d x  /  pi )  e.  CC )
170124, 68sseldi 3507 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  ( cos `  ( n  x.  X ) )  e.  CC )
171169, 170mulcomd 9629 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( S. C ( ( F `  x
)  x.  ( cos `  ( n  x.  x
) ) )  _d x  /  pi )  x.  ( cos `  (
n  x.  X ) ) )  =  ( ( cos `  (
n  x.  X ) )  x.  ( S. C ( ( F `
 x )  x.  ( cos `  (
n  x.  x ) ) )  _d x  /  pi ) ) )
17262, 47syldan 470 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  S. C ( ( F `
 x )  x.  ( cos `  (
n  x.  x ) ) )  _d x  e.  RR )
173172recnd 9634 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  S. C ( ( F `
 x )  x.  ( cos `  (
n  x.  x ) ) )  _d x  e.  CC )
174155adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  pi  e.  CC )
17553a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  pi  =/=  0 )
176170, 173, 174, 175divassd 10367 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( ( cos `  (
n  x.  X ) )  x.  S. C
( ( F `  x )  x.  ( cos `  ( n  x.  x ) ) )  _d x )  /  pi )  =  (
( cos `  (
n  x.  X ) )  x.  ( S. C ( ( F `
 x )  x.  ( cos `  (
n  x.  x ) ) )  _d x  /  pi ) ) )
177176eqcomd 2475 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( cos `  (
n  x.  X ) )  x.  ( S. C ( ( F `
 x )  x.  ( cos `  (
n  x.  x ) ) )  _d x  /  pi ) )  =  ( ( ( cos `  ( n  x.  X ) )  x.  S. C ( ( F `  x
)  x.  ( cos `  ( n  x.  x
) ) )  _d x )  /  pi ) )
178126adantlr 714 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN0 )  /\  x  e.  C )  ->  F : RR --> RR )
179128adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN0 )  /\  x  e.  C )  ->  x  e.  RR )
180178, 179ffvelrnd 6033 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN0 )  /\  x  e.  C )  ->  ( F `  x )  e.  RR )
181 nn0re 10816 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  NN0  ->  n  e.  RR )
182181ad2antlr 726 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN0 )  /\  x  e.  C )  ->  n  e.  RR )
183182, 179remulcld 9636 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN0 )  /\  x  e.  C )  ->  (
n  x.  x )  e.  RR )
184183recoscld 13757 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN0 )  /\  x  e.  C )  ->  ( cos `  ( n  x.  x ) )  e.  RR )
185180, 184remulcld 9636 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN0 )  /\  x  e.  C )  ->  (
( F `  x
)  x.  ( cos `  ( n  x.  x
) ) )  e.  RR )
18661, 185sylanl2 651 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( F `  x
)  x.  ( cos `  ( n  x.  x
) ) )  e.  RR )
187 ioombl 21843 . . . . . . . . . . . . . . . . . . . 20  |-  ( -u pi (,) pi )  e. 
dom  vol
18818, 187eqeltri 2551 . . . . . . . . . . . . . . . . . . 19  |-  C  e. 
dom  vol
189188elexi 3128 . . . . . . . . . . . . . . . . . 18  |-  C  e. 
_V
190189a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN0 )  ->  C  e.  _V )
191 eqidd 2468 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN0 )  ->  ( x  e.  C  |->  ( cos `  ( n  x.  x
) ) )  =  ( x  e.  C  |->  ( cos `  (
n  x.  x ) ) ) )
192 eqidd 2468 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN0 )  ->  ( x  e.  C  |->  ( F `
 x ) )  =  ( x  e.  C  |->  ( F `  x ) ) )
193190, 184, 180, 191, 192offval2 6551 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN0 )  ->  ( (
x  e.  C  |->  ( cos `  ( n  x.  x ) ) )  oF  x.  ( x  e.  C  |->  ( F `  x
) ) )  =  ( x  e.  C  |->  ( ( cos `  (
n  x.  x ) )  x.  ( F `
 x ) ) ) )
194124, 184sseldi 3507 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  NN0 )  /\  x  e.  C )  ->  ( cos `  ( n  x.  x ) )  e.  CC )
195131adantlr 714 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  NN0 )  /\  x  e.  C )  ->  ( F `  x )  e.  CC )
196194, 195mulcomd 9629 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN0 )  /\  x  e.  C )  ->  (
( cos `  (
n  x.  x ) )  x.  ( F `
 x ) )  =  ( ( F `
 x )  x.  ( cos `  (
n  x.  x ) ) ) )
197196mpteq2dva 4539 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN0 )  ->  ( x  e.  C  |->  ( ( cos `  ( n  x.  x ) )  x.  ( F `  x ) ) )  =  ( x  e.  C  |->  ( ( F `
 x )  x.  ( cos `  (
n  x.  x ) ) ) ) )
198193, 197eqtr2d 2509 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN0 )  ->  ( x  e.  C  |->  ( ( F `  x )  x.  ( cos `  (
n  x.  x ) ) ) )  =  ( ( x  e.  C  |->  ( cos `  (
n  x.  x ) ) )  oF  x.  ( x  e.  C  |->  ( F `  x ) ) ) )
199188a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN0 )  ->  C  e.  dom  vol )
200 coscn 22707 . . . . . . . . . . . . . . . . . . 19  |-  cos  e.  ( CC -cn-> CC )
201200a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  NN0 )  ->  cos  e.  ( CC -cn-> CC ) )
202147, 124sstri 3518 . . . . . . . . . . . . . . . . . . . . 21  |-  C  C_  CC
203202a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  n  e.  NN0 )  ->  C  C_  CC )
204124, 181sseldi 3507 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  NN0  ->  n  e.  CC )
205204adantl 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  n  e.  NN0 )  ->  n  e.  CC )
206 ssid 3528 . . . . . . . . . . . . . . . . . . . . 21  |-  CC  C_  CC
207206a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  n  e.  NN0 )  ->  CC  C_  CC )
208203, 205, 207constcncfg 31532 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  e.  NN0 )  ->  ( x  e.  C  |->  n )  e.  ( C -cn-> CC ) )
209203, 207idcncfg 31533 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  e.  NN0 )  ->  ( x  e.  C  |->  x )  e.  ( C -cn-> CC ) )
210208, 209mulcncf 21727 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  NN0 )  ->  ( x  e.  C  |->  ( n  x.  x ) )  e.  ( C -cn-> CC ) )
211201, 210cncfmpt1f 21285 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN0 )  ->  ( x  e.  C  |->  ( cos `  ( n  x.  x
) ) )  e.  ( C -cn-> CC ) )
212 cnmbf 21934 . . . . . . . . . . . . . . . . 17  |-  ( ( C  e.  dom  vol  /\  ( x  e.  C  |->  ( cos `  (
n  x.  x ) ) )  e.  ( C -cn-> CC ) )  -> 
( x  e.  C  |->  ( cos `  (
n  x.  x ) ) )  e. MblFn )
213199, 211, 212syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN0 )  ->  ( x  e.  C  |->  ( cos `  ( n  x.  x
) ) )  e. MblFn
)
214153adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN0 )  ->  ( x  e.  C  |->  ( F `
 x ) )  e.  L^1 )
215 1re 9607 . . . . . . . . . . . . . . . . . . 19  |-  1  e.  RR
216215a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  NN0  ->  1  e.  RR )
217 simpl 457 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  e.  NN0  /\  y  e.  dom  ( x  e.  C  |->  ( cos `  ( n  x.  x
) ) ) )  ->  n  e.  NN0 )
218 simpr 461 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( n  e.  NN0  /\  y  e.  dom  ( x  e.  C  |->  ( cos `  ( n  x.  x
) ) ) )  ->  y  e.  dom  ( x  e.  C  |->  ( cos `  (
n  x.  x ) ) ) )
219181adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( n  e.  NN0  /\  x  e.  C )  ->  n  e.  RR )
220128adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( n  e.  NN0  /\  x  e.  C )  ->  x  e.  RR )
221219, 220remulcld 9636 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( n  e.  NN0  /\  x  e.  C )  ->  ( n  x.  x
)  e.  RR )
222221recoscld 13757 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( n  e.  NN0  /\  x  e.  C )  ->  ( cos `  (
n  x.  x ) )  e.  RR )
223222ralrimiva 2881 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  NN0  ->  A. x  e.  C  ( cos `  ( n  x.  x
) )  e.  RR )
224223adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( n  e.  NN0  /\  y  e.  dom  ( x  e.  C  |->  ( cos `  ( n  x.  x
) ) ) )  ->  A. x  e.  C  ( cos `  ( n  x.  x ) )  e.  RR )
225 dmmptg 5510 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( A. x  e.  C  ( cos `  ( n  x.  x ) )  e.  RR  ->  dom  ( x  e.  C  |->  ( cos `  ( n  x.  x
) ) )  =  C )
226224, 225syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( n  e.  NN0  /\  y  e.  dom  ( x  e.  C  |->  ( cos `  ( n  x.  x
) ) ) )  ->  dom  ( x  e.  C  |->  ( cos `  ( n  x.  x
) ) )  =  C )
227218, 226eleqtrd 2557 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  e.  NN0  /\  y  e.  dom  ( x  e.  C  |->  ( cos `  ( n  x.  x
) ) ) )  ->  y  e.  C
)
228 eqidd 2468 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( n  e.  NN0  /\  y  e.  C )  ->  ( x  e.  C  |->  ( cos `  (
n  x.  x ) ) )  =  ( x  e.  C  |->  ( cos `  ( n  x.  x ) ) ) )
229 oveq2 6303 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  y  ->  (
n  x.  x )  =  ( n  x.  y ) )
230229fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  y  ->  ( cos `  ( n  x.  x ) )  =  ( cos `  (
n  x.  y ) ) )
231230adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( n  e.  NN0  /\  y  e.  C )  /\  x  =  y )  ->  ( cos `  ( n  x.  x
) )  =  ( cos `  ( n  x.  y ) ) )
232 simpr 461 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( n  e.  NN0  /\  y  e.  C )  ->  y  e.  C )
233181adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( n  e.  NN0  /\  y  e.  C )  ->  n  e.  RR )
234147, 232sseldi 3507 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( n  e.  NN0  /\  y  e.  C )  ->  y  e.  RR )
235233, 234remulcld 9636 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( n  e.  NN0  /\  y  e.  C )  ->  ( n  x.  y
)  e.  RR )
236235recoscld 13757 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( n  e.  NN0  /\  y  e.  C )  ->  ( cos `  (
n  x.  y ) )  e.  RR )
237228, 231, 232, 236fvmptd 5962 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( n  e.  NN0  /\  y  e.  C )  ->  ( ( x  e.  C  |->  ( cos `  (
n  x.  x ) ) ) `  y
)  =  ( cos `  ( n  x.  y
) ) )
238237fveq2d 5876 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( n  e.  NN0  /\  y  e.  C )  ->  ( abs `  (
( x  e.  C  |->  ( cos `  (
n  x.  x ) ) ) `  y
) )  =  ( abs `  ( cos `  ( n  x.  y
) ) ) )
239 abscosbd 31360 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( n  x.  y )  e.  RR  ->  ( abs `  ( cos `  (
n  x.  y ) ) )  <_  1
)
240235, 239syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( n  e.  NN0  /\  y  e.  C )  ->  ( abs `  ( cos `  ( n  x.  y ) ) )  <_  1 )
241238, 240eqbrtrd 4473 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  e.  NN0  /\  y  e.  C )  ->  ( abs `  (
( x  e.  C  |->  ( cos `  (
n  x.  x ) ) ) `  y
) )  <_  1
)
242217, 227, 241syl2anc 661 . . . . . . . . . . . . . . . . . . 19  |-  ( ( n  e.  NN0  /\  y  e.  dom  ( x  e.  C  |->  ( cos `  ( n  x.  x
) ) ) )  ->  ( abs `  (
( x  e.  C  |->  ( cos `  (
n  x.  x ) ) ) `  y
) )  <_  1
)
243242ralrimiva 2881 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  NN0  ->  A. y  e.  dom  ( x  e.  C  |->  ( cos `  (
n  x.  x ) ) ) ( abs `  ( ( x  e.  C  |->  ( cos `  (
n  x.  x ) ) ) `  y
) )  <_  1
)
244 breq2 4457 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  =  1  ->  (
( abs `  (
( x  e.  C  |->  ( cos `  (
n  x.  x ) ) ) `  y
) )  <_  b  <->  ( abs `  ( ( x  e.  C  |->  ( cos `  ( n  x.  x ) ) ) `  y ) )  <_  1 ) )
245244ralbidv 2906 . . . . . . . . . . . . . . . . . . 19  |-  ( b  =  1  ->  ( A. y  e.  dom  ( x  e.  C  |->  ( cos `  (
n  x.  x ) ) ) ( abs `  ( ( x  e.  C  |->  ( cos `  (
n  x.  x ) ) ) `  y
) )  <_  b  <->  A. y  e.  dom  (
x  e.  C  |->  ( cos `  ( n  x.  x ) ) ) ( abs `  (
( x  e.  C  |->  ( cos `  (
n  x.  x ) ) ) `  y
) )  <_  1
) )
246245rspcev 3219 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1  e.  RR  /\  A. y  e.  dom  (
x  e.  C  |->  ( cos `  ( n  x.  x ) ) ) ( abs `  (
( x  e.  C  |->  ( cos `  (
n  x.  x ) ) ) `  y
) )  <_  1
)  ->  E. b  e.  RR  A. y  e. 
dom  ( x  e.  C  |->  ( cos `  (
n  x.  x ) ) ) ( abs `  ( ( x  e.  C  |->  ( cos `  (
n  x.  x ) ) ) `  y
) )  <_  b
)
247216, 243, 246syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  NN0  ->  E. b  e.  RR  A. y  e. 
dom  ( x  e.  C  |->  ( cos `  (
n  x.  x ) ) ) ( abs `  ( ( x  e.  C  |->  ( cos `  (
n  x.  x ) ) ) `  y
) )  <_  b
)
248247adantl 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN0 )  ->  E. b  e.  RR  A. y  e. 
dom  ( x  e.  C  |->  ( cos `  (
n  x.  x ) ) ) ( abs `  ( ( x  e.  C  |->  ( cos `  (
n  x.  x ) ) ) `  y
) )  <_  b
)
249 bddmulibl 22113 . . . . . . . . . . . . . . . 16  |-  ( ( ( x  e.  C  |->  ( cos `  (
n  x.  x ) ) )  e. MblFn  /\  (
x  e.  C  |->  ( F `  x ) )  e.  L^1 
/\  E. b  e.  RR  A. y  e.  dom  (
x  e.  C  |->  ( cos `  ( n  x.  x ) ) ) ( abs `  (
( x  e.  C  |->  ( cos `  (
n  x.  x ) ) ) `  y
) )  <_  b
)  ->  ( (
x  e.  C  |->  ( cos `  ( n  x.  x ) ) )  oF  x.  ( x  e.  C  |->  ( F `  x
) ) )  e.  L^1 )
250213, 214, 248, 249syl3anc 1228 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN0 )  ->  ( (
x  e.  C  |->  ( cos `  ( n  x.  x ) ) )  oF  x.  ( x  e.  C  |->  ( F `  x
) ) )  e.  L^1 )
251198, 250eqeltrd 2555 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  NN0 )  ->  ( x  e.  C  |->  ( ( F `  x )  x.  ( cos `  (
n  x.  x ) ) ) )  e.  L^1 )
25262, 251syldan 470 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
x  e.  C  |->  ( ( F `  x
)  x.  ( cos `  ( n  x.  x
) ) ) )  e.  L^1 )
253170, 186, 252itgmulc2 22108 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( cos `  (
n  x.  X ) )  x.  S. C
( ( F `  x )  x.  ( cos `  ( n  x.  x ) ) )  _d x )  =  S. C ( ( cos `  ( n  x.  X ) )  x.  ( ( F `
 x )  x.  ( cos `  (
n  x.  x ) ) ) )  _d x )
254170adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  ( cos `  ( n  x.  X ) )  e.  CC )
25561, 195sylanl2 651 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  ( F `  x )  e.  CC )
25661, 194sylanl2 651 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  ( cos `  ( n  x.  x ) )  e.  CC )
257254, 255, 256mul12d 9800 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( cos `  (
n  x.  X ) )  x.  ( ( F `  x )  x.  ( cos `  (
n  x.  x ) ) ) )  =  ( ( F `  x )  x.  (
( cos `  (
n  x.  X ) )  x.  ( cos `  ( n  x.  x
) ) ) ) )
258254, 256mulcomd 9629 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( cos `  (
n  x.  X ) )  x.  ( cos `  ( n  x.  x
) ) )  =  ( ( cos `  (
n  x.  x ) )  x.  ( cos `  ( n  x.  X
) ) ) )
259258oveq2d 6311 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( F `  x
)  x.  ( ( cos `  ( n  x.  X ) )  x.  ( cos `  (
n  x.  x ) ) ) )  =  ( ( F `  x )  x.  (
( cos `  (
n  x.  x ) )  x.  ( cos `  ( n  x.  X
) ) ) ) )
260257, 259eqtrd 2508 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( cos `  (
n  x.  X ) )  x.  ( ( F `  x )  x.  ( cos `  (
n  x.  x ) ) ) )  =  ( ( F `  x )  x.  (
( cos `  (
n  x.  x ) )  x.  ( cos `  ( n  x.  X
) ) ) ) )
261260itgeq2dv 22056 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  S. C ( ( cos `  ( n  x.  X
) )  x.  (
( F `  x
)  x.  ( cos `  ( n  x.  x
) ) ) )  _d x  =  S. C ( ( F `
 x )  x.  ( ( cos `  (
n  x.  x ) )  x.  ( cos `  ( n  x.  X
) ) ) )  _d x )
262253, 261eqtrd 2508 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( cos `  (
n  x.  X ) )  x.  S. C
( ( F `  x )  x.  ( cos `  ( n  x.  x ) ) )  _d x )  =  S. C ( ( F `  x )  x.  ( ( cos `  ( n  x.  x
) )  x.  ( cos `  ( n  x.  X ) ) ) )  _d x )
263262oveq1d 6310 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( ( cos `  (
n  x.  X ) )  x.  S. C
( ( F `  x )  x.  ( cos `  ( n  x.  x ) ) )  _d x )  /  pi )  =  ( S. C ( ( F `
 x )  x.  ( ( cos `  (
n  x.  x ) )  x.  ( cos `  ( n  x.  X
) ) ) )  _d x  /  pi ) )
264177, 263eqtrd 2508 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( cos `  (
n  x.  X ) )  x.  ( S. C ( ( F `
 x )  x.  ( cos `  (
n  x.  x ) ) )  _d x  /  pi ) )  =  ( S. C
( ( F `  x )  x.  (
( cos `  (
n  x.  x ) )  x.  ( cos `  ( n  x.  X
) ) ) )  _d x  /  pi ) )
265168, 171, 2643eqtrd 2512 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( A `  n
)  x.  ( cos `  ( n  x.  X
) ) )  =  ( S. C ( ( F `  x
)  x.  ( ( cos `  ( n  x.  x ) )  x.  ( cos `  (
n  x.  X ) ) ) )  _d x  /  pi ) )
26690, 87syldan 470 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  ( S. C ( ( F `
 x )  x.  ( sin `  (
n  x.  x ) ) )  _d x  /  pi )  e.  RR )
26721fvmpt2 5964 . . . . . . . . . . 11  |-  ( ( n  e.  NN  /\  ( S. C ( ( F `  x )  x.  ( sin `  (
n  x.  x ) ) )  _d x  /  pi )  e.  RR )  ->  ( B `  n )  =  ( S. C
( ( F `  x )  x.  ( sin `  ( n  x.  x ) ) )  _d x  /  pi ) )
26890, 266, 267syl2anc 661 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  ( B `  n )  =  ( S. C
( ( F `  x )  x.  ( sin `  ( n  x.  x ) ) )  _d x  /  pi ) )
269268oveq1d 6310 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( B `  n
)  x.  ( sin `  ( n  x.  X
) ) )  =  ( ( S. C
( ( F `  x )  x.  ( sin `  ( n  x.  x ) ) )  _d x  /  pi )  x.  ( sin `  ( n  x.  X
) ) ) )
270124, 266sseldi 3507 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  ( S. C ( ( F `
 x )  x.  ( sin `  (
n  x.  x ) ) )  _d x  /  pi )  e.  CC )
271124, 92sseldi 3507 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  ( sin `  ( n  x.  X ) )  e.  CC )
272270, 271mulcomd 9629 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( S. C ( ( F `  x
)  x.  ( sin `  ( n  x.  x
) ) )  _d x  /  pi )  x.  ( sin `  (
n  x.  X ) ) )  =  ( ( sin `  (
n  x.  X ) )  x.  ( S. C ( ( F `
 x )  x.  ( sin `  (
n  x.  x ) ) )  _d x  /  pi ) ) )
27390, 84syldan 470 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  S. C ( ( F `
 x )  x.  ( sin `  (
n  x.  x ) ) )  _d x  e.  RR )
274273recnd 9634 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  S. C ( ( F `
 x )  x.  ( sin `  (
n  x.  x ) ) )  _d x  e.  CC )
275271, 274, 174, 175divassd 10367 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( ( sin `  (
n  x.  X ) )  x.  S. C
( ( F `  x )  x.  ( sin `  ( n  x.  x ) ) )  _d x )  /  pi )  =  (
( sin `  (
n  x.  X ) )  x.  ( S. C ( ( F `
 x )  x.  ( sin `  (
n  x.  x ) ) )  _d x  /  pi ) ) )
276275eqcomd 2475 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( sin `  (
n  x.  X ) )  x.  ( S. C ( ( F `
 x )  x.  ( sin `  (
n  x.  x ) ) )  _d x  /  pi ) )  =  ( ( ( sin `  ( n  x.  X ) )  x.  S. C ( ( F `  x
)  x.  ( sin `  ( n  x.  x
) ) )  _d x )  /  pi ) )
277130adantlr 714 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  C )  ->  ( F `  x )  e.  RR )
278 nnre 10555 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  NN  ->  n  e.  RR )
279278adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  e.  NN  /\  x  e.  C )  ->  n  e.  RR )
280128adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  e.  NN  /\  x  e.  C )  ->  x  e.  RR )
281279, 280remulcld 9636 . . . . . . . . . . . . . . . . 17  |-  ( ( n  e.  NN  /\  x  e.  C )  ->  ( n  x.  x
)  e.  RR )
282281resincld 13756 . . . . . . . . . . . . . . . 16  |-  ( ( n  e.  NN  /\  x  e.  C )  ->  ( sin `  (
n  x.  x ) )  e.  RR )
283282adantll 713 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  C )  ->  ( sin `  ( n  x.  x ) )  e.  RR )
284277, 283remulcld 9636 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  C )  ->  (
( F `  x
)  x.  ( sin `  ( n  x.  x
) ) )  e.  RR )
28560, 284sylanl2 651 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( F `  x
)  x.  ( sin `  ( n  x.  x
) ) )  e.  RR )
286189a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN )  ->  C  e. 
_V )
287 eqidd 2468 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN )  ->  ( x  e.  C  |->  ( sin `  ( n  x.  x
) ) )  =  ( x  e.  C  |->  ( sin `  (
n  x.  x ) ) ) )
288 eqidd 2468 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN )  ->  ( x  e.  C  |->  ( F `
 x ) )  =  ( x  e.  C  |->  ( F `  x ) ) )
289286, 283, 277, 287, 288offval2 6551 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( x  e.  C  |->  ( sin `  ( n  x.  x ) ) )  oF  x.  ( x  e.  C  |->  ( F `  x
) ) )  =  ( x  e.  C  |->  ( ( sin `  (
n  x.  x ) )  x.  ( F `
 x ) ) ) )
290124, 283sseldi 3507 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  C )  ->  ( sin `  ( n  x.  x ) )  e.  CC )
291131adantlr 714 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  C )  ->  ( F `  x )  e.  CC )
292290, 291mulcomd 9629 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  C )  ->  (
( sin `  (
n  x.  x ) )  x.  ( F `
 x ) )  =  ( ( F `
 x )  x.  ( sin `  (
n  x.  x ) ) ) )
293292mpteq2dva 4539 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  ( x  e.  C  |->  ( ( sin `  ( n  x.  x ) )  x.  ( F `  x ) ) )  =  ( x  e.  C  |->  ( ( F `
 x )  x.  ( sin `  (
n  x.  x ) ) ) ) )
294289, 293eqtr2d 2509 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  ( x  e.  C  |->  ( ( F `  x )  x.  ( sin `  (
n  x.  x ) ) ) )  =  ( ( x  e.  C  |->  ( sin `  (
n  x.  x ) ) )  oF  x.  ( x  e.  C  |->  ( F `  x ) ) ) )
295188a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN )  ->  C  e. 
dom  vol )
296 sincn 22706 . . . . . . . . . . . . . . . . . . 19  |-  sin  e.  ( CC -cn-> CC )
297296a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  NN )  ->  sin  e.  ( CC -cn-> CC ) )
298202a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  NN  ->  C  C_  CC )
299124, 278sseldi 3507 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  NN  ->  n  e.  CC )
300206a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  NN  ->  CC  C_  CC )
301298, 299, 300constcncfg 31532 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  NN  ->  (
x  e.  C  |->  n )  e.  ( C
-cn-> CC ) )
302298, 300idcncfg 31533 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  NN  ->  (
x  e.  C  |->  x )  e.  ( C
-cn-> CC ) )
303301, 302mulcncf 21727 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  NN  ->  (
x  e.  C  |->  ( n  x.  x ) )  e.  ( C
-cn-> CC ) )
304303adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  NN )  ->  ( x  e.  C  |->  ( n  x.  x ) )  e.  ( C -cn-> CC ) )
305297, 304cncfmpt1f 21285 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN )  ->  ( x  e.  C  |->  ( sin `  ( n  x.  x
) ) )  e.  ( C -cn-> CC ) )
306 cnmbf 21934 . . . . . . . . . . . . . . . . 17  |-  ( ( C  e.  dom  vol  /\  ( x  e.  C  |->  ( sin `  (
n  x.  x ) ) )  e.  ( C -cn-> CC ) )  -> 
( x  e.  C  |->  ( sin `  (
n  x.  x ) ) )  e. MblFn )
307295, 305, 306syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  ( x  e.  C  |->  ( sin `  ( n  x.  x
) ) )  e. MblFn
)
308153adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  ( x  e.  C  |->  ( F `
 x ) )  e.  L^1 )
309215a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  NN  ->  1  e.  RR )
310 simpl 457 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  e.  NN  /\  y  e.  dom  ( x  e.  C  |->  ( sin `  ( n  x.  x
) ) ) )  ->  n  e.  NN )
311 simpr 461 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( n  e.  NN  /\  y  e.  dom  ( x  e.  C  |->  ( sin `  ( n  x.  x
) ) ) )  ->  y  e.  dom  ( x  e.  C  |->  ( sin `  (
n  x.  x ) ) ) )
312282ralrimiva 2881 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  NN  ->  A. x  e.  C  ( sin `  ( n  x.  x
) )  e.  RR )
313 dmmptg 5510 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( A. x  e.  C  ( sin `  ( n  x.  x ) )  e.  RR  ->  dom  ( x  e.  C  |->  ( sin `  ( n  x.  x
) ) )  =  C )
314312, 313syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  NN  ->  dom  ( x  e.  C  |->  ( sin `  (
n  x.  x ) ) )  =  C )
315314adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( n  e.  NN  /\  y  e.  dom  ( x  e.  C  |->  ( sin `  ( n  x.  x
) ) ) )  ->  dom  ( x  e.  C  |->  ( sin `  ( n  x.  x
) ) )  =  C )
316311, 315eleqtrd 2557 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  e.  NN  /\  y  e.  dom  ( x  e.  C  |->  ( sin `  ( n  x.  x
) ) ) )  ->  y  e.  C
)
317 eqidd 2468 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( n  e.  NN  /\  y  e.  C )  ->  ( x  e.  C  |->  ( sin `  (
n  x.  x ) ) )  =  ( x  e.  C  |->  ( sin `  ( n  x.  x ) ) ) )
318229fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  y  ->  ( sin `  ( n  x.  x ) )  =  ( sin `  (
n  x.  y ) ) )
319318adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( n  e.  NN  /\  y  e.  C )  /\  x  =  y )  ->  ( sin `  ( n  x.  x
) )  =  ( sin `  ( n  x.  y ) ) )
320 simpr 461 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( n  e.  NN  /\  y  e.  C )  ->  y  e.  C )
321278adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( n  e.  NN  /\  y  e.  C )  ->  n  e.  RR )
322147, 320sseldi 3507 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( n  e.  NN  /\  y  e.  C )  ->  y  e.  RR )
323321, 322remulcld 9636 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( n  e.  NN  /\  y  e.  C )  ->  ( n  x.  y
)  e.  RR )
324323resincld 13756 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( n  e.  NN  /\  y  e.  C )  ->  ( sin `  (
n  x.  y ) )  e.  RR )
325317, 319, 320, 324fvmptd 5962 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( n  e.  NN  /\  y  e.  C )  ->  ( ( x  e.  C  |->  ( sin `  (
n  x.  x ) ) ) `  y
)  =  ( sin `  ( n  x.  y
) ) )
326325fveq2d 5876 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( n  e.  NN  /\  y  e.  C )  ->  ( abs `  (
( x  e.  C  |->  ( sin `  (
n  x.  x ) ) ) `  y
) )  =  ( abs `  ( sin `  ( n  x.  y
) ) ) )
327 abssinbd 31390 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( n  x.  y )  e.  RR  ->  ( abs `  ( sin `  (
n  x.  y ) ) )  <_  1
)
328323, 327syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( n  e.  NN  /\  y  e.  C )  ->  ( abs `  ( sin `  ( n  x.  y ) ) )  <_  1 )
329326, 328eqbrtrd 4473 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  e.  NN  /\  y  e.  C )  ->  ( abs `  (
( x  e.  C  |->  ( sin `  (
n  x.  x ) ) ) `  y
) )  <_  1
)
330310, 316, 329syl2anc 661 . . . . . . . . . . . . . . . . . . 19  |-  ( ( n  e.  NN  /\  y  e.  dom  ( x  e.  C  |->  ( sin `  ( n  x.  x
) ) ) )  ->  ( abs `  (
( x  e.  C  |->  ( sin `  (
n  x.  x ) ) ) `  y
) )  <_  1
)
331330ralrimiva 2881 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  NN  ->  A. y  e.  dom  ( x  e.  C  |->  ( sin `  (
n  x.  x ) ) ) ( abs `  ( ( x  e.  C  |->  ( sin `  (
n  x.  x ) ) ) `  y
) )  <_  1
)
332 breq2 4457 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  =  1  ->  (
( abs `  (
( x  e.  C  |->  ( sin `  (
n  x.  x ) ) ) `  y
) )  <_  b  <->  ( abs `  ( ( x  e.  C  |->  ( sin `  ( n  x.  x ) ) ) `  y ) )  <_  1 ) )
333332ralbidv 2906 . . . . . . . . . . . . . . . . . . 19  |-  ( b  =  1  ->  ( A. y  e.  dom  ( x  e.  C  |->  ( sin `  (
n  x.  x ) ) ) ( abs `  ( ( x  e.  C  |->  ( sin `  (
n  x.  x ) ) ) `  y
) )  <_  b  <->  A. y  e.  dom  (
x  e.  C  |->  ( sin `  ( n  x.  x ) ) ) ( abs `  (
( x  e.  C  |->  ( sin `  (
n  x.  x ) ) ) `  y
) )  <_  1
) )
334333rspcev 3219 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1  e.  RR  /\  A. y  e.  dom  (
x  e.  C  |->  ( sin `  ( n  x.  x ) ) ) ( abs `  (
( x  e.  C  |->  ( sin `  (
n  x.  x ) ) ) `  y
) )  <_  1
)  ->  E. b  e.  RR  A. y  e. 
dom  ( x  e.  C  |->  ( sin `  (
n  x.  x ) ) ) ( abs `  ( ( x  e.  C  |->  ( sin `  (
n  x.  x ) ) ) `  y
) )  <_  b
)
335309, 331, 334syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  NN  ->  E. b  e.  RR  A. y  e. 
dom  ( x  e.  C  |->  ( sin `  (
n  x.  x ) ) ) ( abs `  ( ( x  e.  C  |->  ( sin `  (
n  x.  x ) ) ) `  y
) )  <_  b
)
336335adantl 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  E. b  e.  RR  A. y  e. 
dom  ( x  e.  C  |->  ( sin `  (
n  x.  x ) ) ) ( abs `  ( ( x  e.  C  |->  ( sin `  (
n  x.  x ) ) ) `  y
) )  <_  b
)
337 bddmulibl 22113 . . . . . . . . . . . . . . . 16  |-  ( ( ( x  e.  C  |->  ( sin `  (
n  x.  x ) ) )  e. MblFn  /\  (
x  e.  C  |->  ( F `  x ) )  e.  L^1 
/\  E. b  e.  RR  A. y  e.  dom  (
x  e.  C  |->  ( sin `  ( n  x.  x ) ) ) ( abs `  (
( x  e.  C  |->  ( sin `  (
n  x.  x ) ) ) `  y
) )  <_  b
)  ->  ( (
x  e.  C  |->  ( sin `  ( n  x.  x ) ) )  oF  x.  ( x  e.  C  |->  ( F `  x
) ) )  e.  L^1 )
338307, 308, 336, 337syl3anc 1228 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( x  e.  C  |->  ( sin `  ( n  x.  x ) ) )  oF  x.  ( x  e.  C  |->  ( F `  x
) ) )  e.  L^1 )
339294, 338eqeltrd 2555 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  NN )  ->  ( x  e.  C  |->  ( ( F `  x )  x.  ( sin `  (
n  x.  x ) ) ) )  e.  L^1 )
34090, 339syldan 470 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
x  e.  C  |->  ( ( F `  x
)  x.  ( sin `  ( n  x.  x
) ) ) )  e.  L^1 )
341271, 285, 340itgmulc2 22108 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( sin `  (
n  x.  X ) )  x.  S. C
( ( F `  x )  x.  ( sin `  ( n  x.  x ) ) )  _d x )  =  S. C ( ( sin `  ( n  x.  X ) )  x.  ( ( F `
 x )  x.  ( sin `  (
n  x.  x ) ) ) )  _d x )
342271adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  ( sin `  ( n  x.  X ) )  e.  CC )
34360, 290sylanl2 651 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  ( sin `  ( n  x.  x ) )  e.  CC )
344342, 255, 343mul12d 9800 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( sin `  (
n  x.  X ) )  x.  ( ( F `  x )  x.  ( sin `  (
n  x.  x ) ) ) )  =  ( ( F `  x )  x.  (
( sin `  (
n  x.  X ) )  x.  ( sin `  ( n  x.  x
) ) ) ) )
345342, 343mulcomd 9629 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( sin `  (
n  x.  X ) )  x.  ( sin `  ( n  x.  x
) ) )  =  ( ( sin `  (
n  x.  x ) )  x.  ( sin `  ( n  x.  X
) ) ) )
346345oveq2d 6311 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( F `  x
)  x.  ( ( sin `  ( n  x.  X ) )  x.  ( sin `  (
n  x.  x ) ) ) )  =  ( ( F `  x )  x.  (
( sin `  (
n  x.  x ) )  x.  ( sin `  ( n  x.  X
) ) ) ) )
347344, 346eqtrd 2508 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( sin `  (
n  x.  X ) )  x.  ( ( F `  x )  x.  ( sin `  (
n  x.  x ) ) ) )  =  ( ( F `  x )  x.  (
( sin `  (
n  x.  x ) )  x.  ( sin `  ( n  x.  X
) ) ) ) )
348347itgeq2dv 22056 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  S. C ( ( sin `  ( n  x.  X
) )  x.  (
( F `  x
)  x.  ( sin `  ( n  x.  x
) ) ) )  _d x  =  S. C ( ( F `
 x )  x.  ( ( sin `  (
n  x.  x ) )  x.  ( sin `  ( n  x.  X
) ) ) )  _d x )
349341, 348eqtrd 2508 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( sin `  (
n  x.  X ) )  x.  S. C
( ( F `  x )  x.  ( sin `  ( n  x.  x ) ) )  _d x )  =  S. C ( ( F `  x )  x.  ( ( sin `  ( n  x.  x
) )  x.  ( sin `  ( n  x.  X ) ) ) )  _d x )
350349oveq1d 6310 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( ( sin `  (
n  x.  X ) )  x.  S. C
( ( F `  x )  x.  ( sin `  ( n  x.  x ) ) )  _d x )  /  pi )  =  ( S. C ( ( F `
 x )  x.  ( ( sin `  (
n  x.  x ) )  x.  ( sin `  ( n  x.  X
) ) ) )  _d x  /  pi ) )
351276, 350eqtrd 2508 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( sin `  (
n  x.  X ) )  x.  ( S. C ( ( F `
 x )  x.  ( sin `  (
n  x.  x ) ) )  _d x  /  pi ) )  =  ( S. C
( ( F `  x )  x.  (
( sin `  (
n  x.  x ) )  x.  ( sin `  ( n  x.  X
) ) ) )  _d x  /  pi ) )
352269, 272, 3513eqtrd 2512 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( B `  n
)  x.  ( sin `  ( n  x.  X
) ) )  =  ( S. C ( ( F `  x
)  x.  ( ( sin `  ( n  x.  x ) )  x.  ( sin `  (
n  x.  X ) ) ) )  _d x  /  pi ) )
353265, 352oveq12d 6313 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( ( A `  n )  x.  ( cos `  ( n  x.  X ) ) )  +  ( ( B `
 n )  x.  ( sin `  (
n  x.  X ) ) ) )  =  ( ( S. C
( ( F `  x )  x.  (
( cos `  (
n  x.  x ) )  x.  ( cos `  ( n  x.  X
) ) ) )  _d x  /  pi )  +  ( S. C ( ( F `
 x )  x.  ( ( sin `  (
n  x.  x ) )  x.  ( sin `  ( n  x.  X
) ) ) )  _d x  /  pi ) ) )
35461, 180sylanl2 651 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  ( F `  x )  e.  RR )
35562, 222sylan 471 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  ( cos `  ( n  x.  x ) )  e.  RR )
35668adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  ( cos `  ( n  x.  X ) )  e.  RR )
357355, 356remulcld 9636 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( cos `  (
n  x.  x ) )  x.  ( cos `  ( n  x.  X
) ) )  e.  RR )
358354, 357remulcld 9636 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( F `  x
)  x.  ( ( cos `  ( n  x.  x ) )  x.  ( cos `  (
n  x.  X ) ) ) )  e.  RR )
359255, 256, 254mul13d 31361 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( F `  x
)  x.  ( ( cos `  ( n  x.  x ) )  x.  ( cos `  (
n  x.  X ) ) ) )  =  ( ( cos `  (
n  x.  X ) )  x.  ( ( cos `  ( n  x.  x ) )  x.  ( F `  x ) ) ) )
360256, 255mulcomd 9629 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( cos `  (
n  x.  x ) )  x.  ( F `
 x ) )  =  ( ( F `
 x )  x.  ( cos `  (
n  x.  x ) ) ) )
361360oveq2d 6311 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( cos `  (
n  x.  X ) )  x.  ( ( cos `  ( n  x.  x ) )  x.  ( F `  x ) ) )  =  ( ( cos `  ( n  x.  X
) )  x.  (
( F `  x
)  x.  ( cos `  ( n  x.  x
) ) ) ) )
362359, 361eqtrd 2508 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( F `  x
)  x.  ( ( cos `  ( n  x.  x ) )  x.  ( cos `  (
n  x.  X ) ) ) )  =  ( ( cos `  (
n  x.  X ) )  x.  ( ( F `  x )  x.  ( cos `  (
n  x.  x ) ) ) ) )
363362mpteq2dva 4539 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
x  e.  C  |->  ( ( F `  x
)  x.  ( ( cos `  ( n  x.  x ) )  x.  ( cos `  (
n  x.  X ) ) ) ) )  =  ( x  e.  C  |->  ( ( cos `  ( n  x.  X
) )  x.  (
( F `  x
)  x.  ( cos `  ( n  x.  x
) ) ) ) ) )
364170, 186, 252iblmulc2 22105 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
x  e.  C  |->  ( ( cos `  (
n  x.  X ) )  x.  ( ( F `  x )  x.  ( cos `  (
n  x.  x ) ) ) ) )  e.  L^1 )
365363, 364eqeltrd 2555 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
x  e.  C  |->  ( ( F `  x
)  x.  ( ( cos `  ( n  x.  x ) )  x.  ( cos `  (
n  x.  X ) ) ) ) )  e.  L^1 )
366358, 365itgcl 22058 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  S. C ( ( F `
 x )  x.  ( ( cos `  (
n  x.  x ) )  x.  ( cos `  ( n  x.  X
) ) ) )  _d x  e.  CC )
36790, 282sylan 471 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  ( sin `  ( n  x.  x ) )  e.  RR )
36892adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  ( sin `  ( n  x.  X ) )  e.  RR )
369367, 368remulcld 9636 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( sin `  (
n  x.  x ) )  x.  ( sin `  ( n  x.  X
) ) )  e.  RR )
370354, 369remulcld 9636 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( F `  x
)  x.  ( ( sin `  ( n  x.  x ) )  x.  ( sin `  (
n  x.  X ) ) ) )  e.  RR )
371255, 343, 342mul13d 31361 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( F `  x
)  x.  ( ( sin `  ( n  x.  x ) )  x.  ( sin `  (
n  x.  X ) ) ) )  =  ( ( sin `  (
n  x.  X ) )  x.  ( ( sin `  ( n  x.  x ) )  x.  ( F `  x ) ) ) )
372343, 255mulcomd 9629 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( sin `  (
n  x.  x ) )  x.  ( F `
 x ) )  =  ( ( F `
 x )  x.  ( sin `  (
n  x.  x ) ) ) )
373372oveq2d 6311 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( sin `  (
n  x.  X ) )  x.  ( ( sin `  ( n  x.  x ) )  x.  ( F `  x ) ) )  =  ( ( sin `  ( n  x.  X
) )  x.  (
( F `  x
)  x.  ( sin `  ( n  x.  x
) ) ) ) )
374371, 373eqtrd 2508 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( F `  x
)  x.  ( ( sin `  ( n  x.  x ) )  x.  ( sin `  (
n  x.  X ) ) ) )  =  ( ( sin `  (
n  x.  X ) )  x.  ( ( F `  x )  x.  ( sin `  (
n  x.  x ) ) ) ) )
375374mpteq2dva 4539 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
x  e.  C  |->  ( ( F `  x
)  x.  ( ( sin `  ( n  x.  x ) )  x.  ( sin `  (
n  x.  X ) ) ) ) )  =  ( x  e.  C  |->  ( ( sin `  ( n  x.  X
) )  x.  (
( F `  x
)  x.  ( sin `  ( n  x.  x
) ) ) ) ) )
376271, 285, 340iblmulc2 22105 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
x  e.  C  |->  ( ( sin `  (
n  x.  X ) )  x.  ( ( F `  x )  x.  ( sin `  (
n  x.  x ) ) ) ) )  e.  L^1 )
377375, 376eqeltrd 2555 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
x  e.  C  |->  ( ( F `  x
)  x.  ( ( sin `  ( n  x.  x ) )  x.  ( sin `  (
n  x.  X ) ) ) ) )  e.  L^1 )
378370, 377itgcl 22058 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  S. C ( ( F `
 x )  x.  ( ( sin `  (
n  x.  x ) )  x.  ( sin `  ( n  x.  X
) ) ) )  _d x  e.  CC )
379366, 378, 174, 175divdird 10370 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( S. C ( ( F `  x
)  x.  ( ( cos `  ( n  x.  x ) )  x.  ( cos `  (
n  x.  X ) ) ) )  _d x  +  S. C
( ( F `  x )  x.  (
( sin `  (
n  x.  x ) )  x.  ( sin `  ( n  x.  X
) ) ) )  _d x )  /  pi )  =  (
( S. C ( ( F `  x
)  x.  ( ( cos `  ( n  x.  x ) )  x.  ( cos `  (
n  x.  X ) ) ) )  _d x  /  pi )  +  ( S. C
( ( F `  x )  x.  (
( sin `  (
n  x.  x ) )  x.  ( sin `  ( n  x.  X
) ) ) )  _d x  /  pi ) ) )
380379eqcomd 2475 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( S. C ( ( F `  x
)  x.  ( ( cos `  ( n  x.  x ) )  x.  ( cos `  (
n  x.  X ) ) ) )  _d x  /  pi )  +  ( S. C
( ( F `  x )  x.  (
( sin `  (
n  x.  x ) )  x.  ( sin `  ( n  x.  X
) ) ) )  _d x  /  pi ) )  =  ( ( S. C ( ( F `  x
)  x.  ( ( cos `  ( n  x.  x ) )  x.  ( cos `  (
n  x.  X ) ) ) )  _d x  +  S. C
( ( F `  x )  x.  (
( sin `  (
n  x.  x ) )  x.  ( sin `  ( n  x.  X
) ) ) )  _d x )  /  pi ) )
381 eqidd 2468 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  S. C ( ( F `
 x )  x.  ( cos `  (
n  x.  ( x  -  X ) ) ) )  _d x  =  S. C ( ( F `  x
)  x.  ( cos `  ( n  x.  (
x  -  X ) ) ) )  _d x )
38261, 204syl 16 . . . . . . . . . . . . . . . 16  |-  ( n  e.  ( 1 ... N )  ->  n  e.  CC )
383382ad2antlr 726 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  n  e.  CC )
384116adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  x  e.  CC )
385124, 65sseldi 3507 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  X  e.  CC )
386385ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  X  e.  CC )
387383, 384, 386subdid 10024 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
n  x.  ( x  -  X ) )  =  ( ( n  x.  x )  -  ( n  x.  X
) ) )
388387fveq2d 5876 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  ( cos `  ( n  x.  ( x  -  X
) ) )  =  ( cos `  (
( n  x.  x
)  -  ( n  x.  X ) ) ) )
389383, 384mulcld 9628 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
n  x.  x )  e.  CC )
390383, 386mulcld 9628 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
n  x.  X )  e.  CC )
391 cossub 13782 . . . . . . . . . . . . . 14  |-  ( ( ( n  x.  x
)  e.  CC  /\  ( n  x.  X
)  e.  CC )  ->  ( cos `  (
( n  x.  x
)  -  ( n  x.  X ) ) )  =  ( ( ( cos `  (
n  x.  x ) )  x.  ( cos `  ( n  x.  X
) ) )  +  ( ( sin `  (
n  x.  x ) )  x.  ( sin `  ( n  x.  X
) ) ) ) )
392389, 390, 391syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  ( cos `  ( ( n  x.  x )  -  ( n  x.  X
) ) )  =  ( ( ( cos `  ( n  x.  x
) )  x.  ( cos `  ( n  x.  X ) ) )  +  ( ( sin `  ( n  x.  x
) )  x.  ( sin `  ( n  x.  X ) ) ) ) )
393388, 392eqtrd 2508 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  ( cos `  ( n  x.  ( x  -  X
) ) )  =  ( ( ( cos `  ( n  x.  x
) )  x.  ( cos `  ( n  x.  X ) ) )  +  ( ( sin `  ( n  x.  x
) )  x.  ( sin `  ( n  x.  X ) ) ) ) )
394393oveq2d 6311 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( F `  x
)  x.  ( cos `  ( n  x.  (
x  -  X ) ) ) )  =  ( ( F `  x )  x.  (
( ( cos `  (
n  x.  x ) )  x.  ( cos `  ( n  x.  X
) ) )  +  ( ( sin `  (
n  x.  x ) )  x.  ( sin `  ( n  x.  X
) ) ) ) ) )
395124, 357sseldi 3507 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( cos `  (
n  x.  x ) )  x.  ( cos `  ( n  x.  X
) ) )  e.  CC )
396124, 369sseldi 3507 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( sin `  (
n  x.  x ) )  x.  ( sin `  ( n  x.  X
) ) )  e.  CC )
397255, 395, 396adddid 9632 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( F `  x
)  x.  ( ( ( cos `  (
n  x.  x ) )  x.  ( cos `  ( n  x.  X
) ) )  +  ( ( sin `  (
n  x.  x ) )  x.  ( sin `  ( n  x.  X
) ) ) ) )  =  ( ( ( F `  x
)  x.  ( ( cos `  ( n  x.  x ) )  x.  ( cos `  (
n  x.  X ) ) ) )  +  ( ( F `  x )  x.  (
( sin `  (
n  x.  x ) )  x.  ( sin `  ( n  x.  X
) ) ) ) ) )
398394, 397eqtrd 2508 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( F `  x
)  x.  ( cos `  ( n  x.  (
x  -  X ) ) ) )  =  ( ( ( F `
 x )  x.  ( ( cos `  (
n  x.  x ) )  x.  ( cos `  ( n  x.  X
) ) ) )  +  ( ( F `
 x )  x.  ( ( sin `  (
n  x.  x ) )  x.  ( sin `  ( n  x.  X
) ) ) ) ) )
399398itgeq2dv 22056 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  S. C ( ( F `
 x )  x.  ( cos `  (
n  x.  ( x  -  X ) ) ) )  _d x  =  S. C ( ( ( F `  x )  x.  (
( cos `  (
n  x.  x ) )  x.  ( cos `  ( n  x.  X
) ) ) )  +  ( ( F `
 x )  x.  ( ( sin `  (
n  x.  x ) )  x.  ( sin `  ( n  x.  X
) ) ) ) )  _d x )
400358, 365, 370, 377itgadd 22099 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  S. C ( ( ( F `  x )  x.  ( ( cos `  ( n  x.  x
) )  x.  ( cos `  ( n  x.  X ) ) ) )  +  ( ( F `  x )  x.  ( ( sin `  ( n  x.  x
) )  x.  ( sin `  ( n  x.  X ) ) ) ) )  _d x  =  ( S. C
( ( F `  x )  x.  (
( cos `  (
n  x.  x ) )  x.  ( cos `  ( n  x.  X
) ) ) )  _d x  +  S. C ( ( F `
 x )  x.  ( ( sin `  (
n  x.  x ) )  x.  ( sin `  ( n  x.  X
) ) ) )  _d x ) )
401381, 399, 4003eqtrrd 2513 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  ( S. C ( ( F `
 x )  x.  ( ( cos `  (
n  x.  x ) )  x.  ( cos `  ( n  x.  X
) ) ) )  _d x  +  S. C ( ( F `
 x )  x.  ( ( sin `  (
n  x.  x ) )  x.  ( sin `  ( n  x.  X
) ) ) )  _d x )  =  S. C ( ( F `  x )  x.  ( cos `  (
n  x.  (