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

Theorem fourierdlem83 32214
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 6278 . . . . . 6  |-  ( m  =  N  ->  (
1 ... m )  =  ( 1 ... N
) )
43sumeq1d 13608 . . . . 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 6286 . . . 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 464 . . 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 10806 . . . . . . 7  |-  0  e.  NN0
109a1i 11 . . . . . 6  |-  ( ph  ->  0  e.  NN0 )
119elexi 3116 . . . . . . 7  |-  0  e.  _V
12 eleq1 2526 . . . . . . . . 9  |-  ( n  =  0  ->  (
n  e.  NN0  <->  0  e.  NN0 ) )
1312anbi2d 701 . . . . . . . 8  |-  ( n  =  0  ->  (
( ph  /\  n  e.  NN0 )  <->  ( ph  /\  0  e.  NN0 )
) )
14 fveq2 5848 . . . . . . . . 9  |-  ( n  =  0  ->  ( A `  n )  =  ( A ` 
0 ) )
1514eleq1d 2523 . . . . . . . 8  |-  ( n  =  0  ->  (
( A `  n
)  e.  RR  <->  ( A `  0 )  e.  RR ) )
1613, 15imbi12d 318 . . . . . . 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 32153 . . . . . . . . 9  |-  ( ph  ->  ( ( n  e. 
NN0  ->  ( A `  n )  e.  RR )  /\  ( n  e.  NN  ->  ( B `  n )  e.  RR ) ) )
2322simpld 457 . . . . . . . 8  |-  ( ph  ->  ( n  e.  NN0  ->  ( A `  n
)  e.  RR ) )
2423imp 427 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN0 )  ->  ( A `  n )  e.  RR )
2511, 16, 24vtocl 3158 . . . . . 6  |-  ( (
ph  /\  0  e.  NN0 )  ->  ( A `  0 )  e.  RR )
268, 10, 25syl2anc 659 . . . . 5  |-  ( ph  ->  ( A `  0
)  e.  RR )
2726rehalfcld 10781 . . . 4  |-  ( ph  ->  ( ( A ` 
0 )  /  2
)  e.  RR )
28 fzfid 12068 . . . . 5  |-  ( ph  ->  ( 1 ... N
)  e.  Fin )
29 eleq1 2526 . . . . . . . . . . . . . 14  |-  ( k  =  n  ->  (
k  e.  NN0  <->  n  e.  NN0 ) )
3029anbi2d 701 . . . . . . . . . . . . 13  |-  ( k  =  n  ->  (
( ph  /\  k  e.  NN0 )  <->  ( ph  /\  n  e.  NN0 )
) )
31 simpl 455 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  =  n  /\  x  e.  C )  ->  k  =  n )
3231oveq1d 6285 . . . . . . . . . . . . . . . . 17  |-  ( ( k  =  n  /\  x  e.  C )  ->  ( k  x.  x
)  =  ( n  x.  x ) )
3332fveq2d 5852 . . . . . . . . . . . . . . . 16  |-  ( ( k  =  n  /\  x  e.  C )  ->  ( cos `  (
k  x.  x ) )  =  ( cos `  ( n  x.  x
) ) )
3433oveq2d 6286 . . . . . . . . . . . . . . 15  |-  ( ( k  =  n  /\  x  e.  C )  ->  ( ( F `  x )  x.  ( cos `  ( k  x.  x ) ) )  =  ( ( F `
 x )  x.  ( cos `  (
n  x.  x ) ) ) )
3534itgeq2dv 22357 . . . . . . . . . . . . . 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 )
3635eleq1d 2523 . . . . . . . . . . . . 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 ) )
3730, 36imbi12d 318 . . . . . . . . . . . 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 ) ) )
3817adantr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN0 )  ->  F : RR
--> RR )
3919adantr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( F  |`  C )  e.  L^1 )
40 simpr 459 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN0 )  ->  k  e.  NN0 )
4138, 18, 39, 20, 40fourierdlem16 32147 . . . . . . . . . . . . 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 ) )
4241simprd 461 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN0 )  ->  S. C
( ( F `  x )  x.  ( cos `  ( k  x.  x ) ) )  _d x  e.  RR )
4337, 42chvarv 2019 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN0 )  ->  S. C
( ( F `  x )  x.  ( cos `  ( n  x.  x ) ) )  _d x  e.  RR )
44 pire 23020 . . . . . . . . . . . 12  |-  pi  e.  RR
4544a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN0 )  ->  pi  e.  RR )
46 0re 9585 . . . . . . . . . . . . 13  |-  0  e.  RR
47 pipos 23022 . . . . . . . . . . . . 13  |-  0  <  pi
4846, 47gtneii 9685 . . . . . . . . . . . 12  |-  pi  =/=  0
4948a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN0 )  ->  pi  =/=  0 )
5043, 45, 49redivcld 10368 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  NN0 )  ->  ( S. C ( ( F `
 x )  x.  ( cos `  (
n  x.  x ) ) )  _d x  /  pi )  e.  RR )
5150, 20fmptd 6031 . . . . . . . . 9  |-  ( ph  ->  A : NN0 --> RR )
5251adantr 463 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  A : NN0 --> RR )
53 elfznn 11717 . . . . . . . . . 10  |-  ( n  e.  ( 1 ... N )  ->  n  e.  NN )
5453nnnn0d 10848 . . . . . . . . 9  |-  ( n  e.  ( 1 ... N )  ->  n  e.  NN0 )
5554adantl 464 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  n  e.  NN0 )
5652, 55ffvelrnd 6008 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  ( A `  n )  e.  RR )
5755nn0red 10849 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  n  e.  RR )
58 fourierdlem83.x . . . . . . . . . 10  |-  ( ph  ->  X  e.  RR )
5958adantr 463 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  X  e.  RR )
6057, 59remulcld 9613 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
n  x.  X )  e.  RR )
6160recoscld 13964 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  ( cos `  ( n  x.  X ) )  e.  RR )
6256, 61remulcld 9613 . . . . . 6  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( A `  n
)  x.  ( cos `  ( n  x.  X
) ) )  e.  RR )
63 eleq1 2526 . . . . . . . . . . . . . 14  |-  ( k  =  n  ->  (
k  e.  NN  <->  n  e.  NN ) )
6463anbi2d 701 . . . . . . . . . . . . 13  |-  ( k  =  n  ->  (
( ph  /\  k  e.  NN )  <->  ( ph  /\  n  e.  NN ) ) )
65 oveq1 6277 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  n  ->  (
k  x.  x )  =  ( n  x.  x ) )
6665fveq2d 5852 . . . . . . . . . . . . . . . . 17  |-  ( k  =  n  ->  ( sin `  ( k  x.  x ) )  =  ( sin `  (
n  x.  x ) ) )
6766oveq2d 6286 . . . . . . . . . . . . . . . 16  |-  ( k  =  n  ->  (
( F `  x
)  x.  ( sin `  ( k  x.  x
) ) )  =  ( ( F `  x )  x.  ( sin `  ( n  x.  x ) ) ) )
6867adantr 463 . . . . . . . . . . . . . . 15  |-  ( ( k  =  n  /\  x  e.  C )  ->  ( ( F `  x )  x.  ( sin `  ( k  x.  x ) ) )  =  ( ( F `
 x )  x.  ( sin `  (
n  x.  x ) ) ) )
6968itgeq2dv 22357 . . . . . . . . . . . . . 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 )
7069eleq1d 2523 . . . . . . . . . . . . 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 ) )
7164, 70imbi12d 318 . . . . . . . . . . . 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 ) ) )
7217adantr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  F : RR
--> RR )
7319adantr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  ( F  |`  C )  e.  L^1 )
74 simpr 459 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  NN )
7572, 18, 73, 21, 74fourierdlem21 32152 . . . . . . . . . . . . 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 ) )
7675simprd 461 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  S. C
( ( F `  x )  x.  ( sin `  ( k  x.  x ) ) )  _d x  e.  RR )
7771, 76chvarv 2019 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  S. C
( ( F `  x )  x.  ( sin `  ( n  x.  x ) ) )  _d x  e.  RR )
7844a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  pi  e.  RR )
7948a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  pi  =/=  0 )
8077, 78, 79redivcld 10368 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  NN )  ->  ( S. C ( ( F `
 x )  x.  ( sin `  (
n  x.  x ) ) )  _d x  /  pi )  e.  RR )
8180, 21fmptd 6031 . . . . . . . . 9  |-  ( ph  ->  B : NN --> RR )
8281adantr 463 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  B : NN --> RR )
8353adantl 464 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  n  e.  NN )
8482, 83ffvelrnd 6008 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  ( B `  n )  e.  RR )
8560resincld 13963 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  ( sin `  ( n  x.  X ) )  e.  RR )
8684, 85remulcld 9613 . . . . . 6  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( B `  n
)  x.  ( sin `  ( n  x.  X
) ) )  e.  RR )
8762, 86readdcld 9612 . . . . 5  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( ( A `  n )  x.  ( cos `  ( n  x.  X ) ) )  +  ( ( B `
 n )  x.  ( sin `  (
n  x.  X ) ) ) )  e.  RR )
8828, 87fsumrecl 13641 . . . 4  |-  ( ph  -> 
sum_ n  e.  (
1 ... N ) ( ( ( A `  n )  x.  ( cos `  ( n  x.  X ) ) )  +  ( ( B `
 n )  x.  ( sin `  (
n  x.  X ) ) ) )  e.  RR )
8927, 88readdcld 9612 . . 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 )
902, 6, 7, 89fvmptd 5936 . 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
) ) ) ) ) )
9120a1i 11 . . . . . . 7  |-  ( ph  ->  A  =  ( n  e.  NN0  |->  ( S. C ( ( F `
 x )  x.  ( cos `  (
n  x.  x ) ) )  _d x  /  pi ) ) )
92 oveq1 6277 . . . . . . . . . . . . 13  |-  ( n  =  0  ->  (
n  x.  x )  =  ( 0  x.  x ) )
9392fveq2d 5852 . . . . . . . . . . . 12  |-  ( n  =  0  ->  ( cos `  ( n  x.  x ) )  =  ( cos `  (
0  x.  x ) ) )
9493oveq2d 6286 . . . . . . . . . . 11  |-  ( n  =  0  ->  (
( F `  x
)  x.  ( cos `  ( n  x.  x
) ) )  =  ( ( F `  x )  x.  ( cos `  ( 0  x.  x ) ) ) )
9594adantr 463 . . . . . . . . . 10  |-  ( ( n  =  0  /\  x  e.  C )  ->  ( ( F `
 x )  x.  ( cos `  (
n  x.  x ) ) )  =  ( ( F `  x
)  x.  ( cos `  ( 0  x.  x
) ) ) )
9695itgeq2dv 22357 . . . . . . . . 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 )
9796adantl 464 . . . . . . . 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 )
9897oveq1d 6285 . . . . . . 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 ) )
9917, 18, 19, 20, 10fourierdlem16 32147 . . . . . . . . 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 ) )
10099simprd 461 . . . . . . . 8  |-  ( ph  ->  S. C ( ( F `  x )  x.  ( cos `  (
0  x.  x ) ) )  _d x  e.  RR )
10144a1i 11 . . . . . . . 8  |-  ( ph  ->  pi  e.  RR )
10248a1i 11 . . . . . . . 8  |-  ( ph  ->  pi  =/=  0 )
103100, 101, 102redivcld 10368 . . . . . . 7  |-  ( ph  ->  ( S. C ( ( F `  x
)  x.  ( cos `  ( 0  x.  x
) ) )  _d x  /  pi )  e.  RR )
10491, 98, 10, 103fvmptd 5936 . . . . . 6  |-  ( ph  ->  ( A `  0
)  =  ( S. C ( ( F `
 x )  x.  ( cos `  (
0  x.  x ) ) )  _d x  /  pi ) )
105 ioosscn 31769 . . . . . . . . . . . . . . 15  |-  ( -u pi (,) pi )  C_  CC
106 id 22 . . . . . . . . . . . . . . . 16  |-  ( x  e.  C  ->  x  e.  C )
107106, 18syl6eleq 2552 . . . . . . . . . . . . . . 15  |-  ( x  e.  C  ->  x  e.  ( -u pi (,) pi ) )
108105, 107sseldi 3487 . . . . . . . . . . . . . 14  |-  ( x  e.  C  ->  x  e.  CC )
109108mul02d 9767 . . . . . . . . . . . . 13  |-  ( x  e.  C  ->  (
0  x.  x )  =  0 )
110109fveq2d 5852 . . . . . . . . . . . 12  |-  ( x  e.  C  ->  ( cos `  ( 0  x.  x ) )  =  ( cos `  0
) )
111 cos0 13970 . . . . . . . . . . . 12  |-  ( cos `  0 )  =  1
112110, 111syl6eq 2511 . . . . . . . . . . 11  |-  ( x  e.  C  ->  ( cos `  ( 0  x.  x ) )  =  1 )
113112oveq2d 6286 . . . . . . . . . 10  |-  ( x  e.  C  ->  (
( F `  x
)  x.  ( cos `  ( 0  x.  x
) ) )  =  ( ( F `  x )  x.  1 ) )
114113adantl 464 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  C )  ->  (
( F `  x
)  x.  ( cos `  ( 0  x.  x
) ) )  =  ( ( F `  x )  x.  1 ) )
11517adantr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  C )  ->  F : RR --> RR )
116 ioossre 11589 . . . . . . . . . . . . . 14  |-  ( -u pi (,) pi )  C_  RR
117116, 107sseldi 3487 . . . . . . . . . . . . 13  |-  ( x  e.  C  ->  x  e.  RR )
118117adantl 464 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  C )  ->  x  e.  RR )
119115, 118ffvelrnd 6008 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  C )  ->  ( F `  x )  e.  RR )
120119recnd 9611 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  C )  ->  ( F `  x )  e.  CC )
121120mulid1d 9602 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  C )  ->  (
( F `  x
)  x.  1 )  =  ( F `  x ) )
122114, 121eqtrd 2495 . . . . . . . 8  |-  ( (
ph  /\  x  e.  C )  ->  (
( F `  x
)  x.  ( cos `  ( 0  x.  x
) ) )  =  ( F `  x
) )
123122itgeq2dv 22357 . . . . . . 7  |-  ( ph  ->  S. C ( ( F `  x )  x.  ( cos `  (
0  x.  x ) ) )  _d x  =  S. C ( F `  x )  _d x )
124123oveq1d 6285 . . . . . 6  |-  ( ph  ->  ( S. C ( ( F `  x
)  x.  ( cos `  ( 0  x.  x
) ) )  _d x  /  pi )  =  ( S. C
( F `  x
)  _d x  /  pi ) )
125104, 124eqtrd 2495 . . . . 5  |-  ( ph  ->  ( A `  0
)  =  ( S. C ( F `  x )  _d x  /  pi ) )
126125oveq1d 6285 . . . 4  |-  ( ph  ->  ( ( A ` 
0 )  /  2
)  =  ( ( S. C ( F `
 x )  _d x  /  pi )  /  2 ) )
12717feqmptd 5901 . . . . . . . . 9  |-  ( ph  ->  F  =  ( x  e.  RR  |->  ( F `
 x ) ) )
128127reseq1d 5261 . . . . . . . 8  |-  ( ph  ->  ( F  |`  C )  =  ( ( x  e.  RR  |->  ( F `
 x ) )  |`  C ) )
12944a1i 11 . . . . . . . . . . . 12  |-  ( x  e.  C  ->  pi  e.  RR )
130129renegcld 9982 . . . . . . . . . . 11  |-  ( x  e.  C  ->  -u pi  e.  RR )
131 ioossicc 11613 . . . . . . . . . . . . 13  |-  ( -u pi (,) pi )  C_  ( -u pi [,] pi )
13218, 131eqsstri 3519 . . . . . . . . . . . 12  |-  C  C_  ( -u pi [,] pi )
133132sseli 3485 . . . . . . . . . . 11  |-  ( x  e.  C  ->  x  e.  ( -u pi [,] pi ) )
134 eliccre 31782 . . . . . . . . . . 11  |-  ( (
-u pi  e.  RR  /\  pi  e.  RR  /\  x  e.  ( -u pi [,] pi ) )  ->  x  e.  RR )
135130, 129, 133, 134syl3anc 1226 . . . . . . . . . 10  |-  ( x  e.  C  ->  x  e.  RR )
136135ssriv 3493 . . . . . . . . 9  |-  C  C_  RR
137 resmpt 5311 . . . . . . . . 9  |-  ( C 
C_  RR  ->  ( ( x  e.  RR  |->  ( F `  x ) )  |`  C )  =  ( x  e.  C  |->  ( F `  x ) ) )
138136, 137mp1i 12 . . . . . . . 8  |-  ( ph  ->  ( ( x  e.  RR  |->  ( F `  x ) )  |`  C )  =  ( x  e.  C  |->  ( F `  x ) ) )
139128, 138eqtr2d 2496 . . . . . . 7  |-  ( ph  ->  ( x  e.  C  |->  ( F `  x
) )  =  ( F  |`  C )
)
140139, 19eqeltrd 2542 . . . . . 6  |-  ( ph  ->  ( x  e.  C  |->  ( F `  x
) )  e.  L^1 )
141119, 140itgcl 22359 . . . . 5  |-  ( ph  ->  S. C ( F `
 x )  _d x  e.  CC )
142101recnd 9611 . . . . 5  |-  ( ph  ->  pi  e.  CC )
143 2cnd 10604 . . . . 5  |-  ( ph  ->  2  e.  CC )
144 2ne0 10624 . . . . . 6  |-  2  =/=  0
145144a1i 11 . . . . 5  |-  ( ph  ->  2  =/=  0 )
146141, 142, 143, 102, 145divdiv32d 10341 . . . 4  |-  ( ph  ->  ( ( S. C
( F `  x
)  _d x  /  pi )  /  2
)  =  ( ( S. C ( F `
 x )  _d x  /  2 )  /  pi ) )
147141, 143, 145divrecd 10319 . . . . . 6  |-  ( ph  ->  ( S. C ( F `  x )  _d x  /  2
)  =  ( S. C ( F `  x )  _d x  x.  ( 1  / 
2 ) ) )
148143, 145reccld 10309 . . . . . . 7  |-  ( ph  ->  ( 1  /  2
)  e.  CC )
149141, 148mulcomd 9606 . . . . . 6  |-  ( ph  ->  ( S. C ( F `  x )  _d x  x.  (
1  /  2 ) )  =  ( ( 1  /  2 )  x.  S. C ( F `  x )  _d x ) )
150148, 119, 140itgmulc2 22409 . . . . . 6  |-  ( ph  ->  ( ( 1  / 
2 )  x.  S. C ( F `  x )  _d x )  =  S. C
( ( 1  / 
2 )  x.  ( F `  x )
)  _d x )
151147, 149, 1503eqtrd 2499 . . . . 5  |-  ( ph  ->  ( S. C ( F `  x )  _d x  /  2
)  =  S. C
( ( 1  / 
2 )  x.  ( F `  x )
)  _d x )
152151oveq1d 6285 . . . 4  |-  ( ph  ->  ( ( S. C
( F `  x
)  _d x  / 
2 )  /  pi )  =  ( S. C ( ( 1  /  2 )  x.  ( F `  x
) )  _d x  /  pi ) )
153126, 146, 1523eqtrd 2499 . . 3  |-  ( ph  ->  ( ( A ` 
0 )  /  2
)  =  ( S. C ( ( 1  /  2 )  x.  ( F `  x
) )  _d x  /  pi ) )
15455, 50syldan 468 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  ( S. C ( ( F `
 x )  x.  ( cos `  (
n  x.  x ) ) )  _d x  /  pi )  e.  RR )
15520fvmpt2 5939 . . . . . . . . . 10  |-  ( ( 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 ) )
15655, 154, 155syl2anc 659 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  ( A `  n )  =  ( S. C
( ( F `  x )  x.  ( cos `  ( n  x.  x ) ) )  _d x  /  pi ) )
157156oveq1d 6285 . . . . . . . 8  |-  ( (
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
) ) ) )
158154recnd 9611 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  ( S. C ( ( F `
 x )  x.  ( cos `  (
n  x.  x ) ) )  _d x  /  pi )  e.  CC )
15961recnd 9611 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  ( cos `  ( n  x.  X ) )  e.  CC )
160158, 159mulcomd 9606 . . . . . . . 8  |-  ( (
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 ) ) )
16155, 43syldan 468 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  S. C ( ( F `
 x )  x.  ( cos `  (
n  x.  x ) ) )  _d x  e.  RR )
162161recnd 9611 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  S. C ( ( F `
 x )  x.  ( cos `  (
n  x.  x ) ) )  _d x  e.  CC )
163142adantr 463 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  pi  e.  CC )
16448a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  pi  =/=  0 )
165159, 162, 163, 164divassd 10351 . . . . . . . . 9  |-  ( (
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 ) ) )
16617ad2antrr 723 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN0 )  /\  x  e.  C )  ->  F : RR --> RR )
167117adantl 464 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN0 )  /\  x  e.  C )  ->  x  e.  RR )
168166, 167ffvelrnd 6008 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN0 )  /\  x  e.  C )  ->  ( F `  x )  e.  RR )
169 nn0re 10800 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  NN0  ->  n  e.  RR )
170169ad2antlr 724 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN0 )  /\  x  e.  C )  ->  n  e.  RR )
171170, 167remulcld 9613 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN0 )  /\  x  e.  C )  ->  (
n  x.  x )  e.  RR )
172171recoscld 13964 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN0 )  /\  x  e.  C )  ->  ( cos `  ( n  x.  x ) )  e.  RR )
173168, 172remulcld 9613 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN0 )  /\  x  e.  C )  ->  (
( F `  x
)  x.  ( cos `  ( n  x.  x
) ) )  e.  RR )
17454, 173sylanl2 649 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( F `  x
)  x.  ( cos `  ( n  x.  x
) ) )  e.  RR )
175 ioombl 22144 . . . . . . . . . . . . . . . . . . 19  |-  ( -u pi (,) pi )  e. 
dom  vol
17618, 175eqeltri 2538 . . . . . . . . . . . . . . . . . 18  |-  C  e. 
dom  vol
177176elexi 3116 . . . . . . . . . . . . . . . . 17  |-  C  e. 
_V
178177a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN0 )  ->  C  e.  _V )
179 eqidd 2455 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN0 )  ->  ( x  e.  C  |->  ( cos `  ( n  x.  x
) ) )  =  ( x  e.  C  |->  ( cos `  (
n  x.  x ) ) ) )
180 eqidd 2455 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN0 )  ->  ( x  e.  C  |->  ( F `
 x ) )  =  ( x  e.  C  |->  ( F `  x ) ) )
181178, 172, 168, 179, 180offval2 6529 . . . . . . . . . . . . . . 15  |-  ( (
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 ) ) ) )
182172recnd 9611 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN0 )  /\  x  e.  C )  ->  ( cos `  ( n  x.  x ) )  e.  CC )
183120adantlr 712 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN0 )  /\  x  e.  C )  ->  ( F `  x )  e.  CC )
184182, 183mulcomd 9606 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN0 )  /\  x  e.  C )  ->  (
( cos `  (
n  x.  x ) )  x.  ( F `
 x ) )  =  ( ( F `
 x )  x.  ( cos `  (
n  x.  x ) ) ) )
185184mpteq2dva 4525 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN0 )  ->  ( x  e.  C  |->  ( ( cos `  ( n  x.  x ) )  x.  ( F `  x ) ) )  =  ( x  e.  C  |->  ( ( F `
 x )  x.  ( cos `  (
n  x.  x ) ) ) ) )
186181, 185eqtr2d 2496 . . . . . . . . . . . . . 14  |-  ( (
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 ) ) ) )
187 coscn 23009 . . . . . . . . . . . . . . . . . 18  |-  cos  e.  ( CC -cn-> CC )
188187a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN0 )  ->  cos  e.  ( CC -cn-> CC ) )
189 ax-resscn 9538 . . . . . . . . . . . . . . . . . . . . 21  |-  RR  C_  CC
190136, 189sstri 3498 . . . . . . . . . . . . . . . . . . . 20  |-  C  C_  CC
191190a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  e.  NN0 )  ->  C  C_  CC )
192169recnd 9611 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  NN0  ->  n  e.  CC )
193192adantl 464 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  e.  NN0 )  ->  n  e.  CC )
194 ssid 3508 . . . . . . . . . . . . . . . . . . . 20  |-  CC  C_  CC
195194a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  e.  NN0 )  ->  CC  C_  CC )
196191, 193, 195constcncfg 31915 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  NN0 )  ->  ( x  e.  C  |->  n )  e.  ( C -cn-> CC ) )
197191, 195idcncfg 31916 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  NN0 )  ->  ( x  e.  C  |->  x )  e.  ( C -cn-> CC ) )
198196, 197mulcncf 22028 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN0 )  ->  ( x  e.  C  |->  ( n  x.  x ) )  e.  ( C -cn-> CC ) )
199188, 198cncfmpt1f 21586 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN0 )  ->  ( x  e.  C  |->  ( cos `  ( n  x.  x
) ) )  e.  ( C -cn-> CC ) )
200 cnmbf 22235 . . . . . . . . . . . . . . . 16  |-  ( ( C  e.  dom  vol  /\  ( x  e.  C  |->  ( cos `  (
n  x.  x ) ) )  e.  ( C -cn-> CC ) )  -> 
( x  e.  C  |->  ( cos `  (
n  x.  x ) ) )  e. MblFn )
201176, 199, 200sylancr 661 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN0 )  ->  ( x  e.  C  |->  ( cos `  ( n  x.  x
) ) )  e. MblFn
)
202140adantr 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN0 )  ->  ( x  e.  C  |->  ( F `
 x ) )  e.  L^1 )
203 1re 9584 . . . . . . . . . . . . . . . . 17  |-  1  e.  RR
204 simpr 459 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  e.  NN0  /\  y  e.  dom  ( x  e.  C  |->  ( cos `  ( n  x.  x
) ) ) )  ->  y  e.  dom  ( x  e.  C  |->  ( cos `  (
n  x.  x ) ) ) )
205169adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( n  e.  NN0  /\  x  e.  C )  ->  n  e.  RR )
206117adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( n  e.  NN0  /\  x  e.  C )  ->  x  e.  RR )
207205, 206remulcld 9613 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( n  e.  NN0  /\  x  e.  C )  ->  ( n  x.  x
)  e.  RR )
208207recoscld 13964 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( n  e.  NN0  /\  x  e.  C )  ->  ( cos `  (
n  x.  x ) )  e.  RR )
209208ralrimiva 2868 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  NN0  ->  A. x  e.  C  ( cos `  ( n  x.  x
) )  e.  RR )
210209adantr 463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( n  e.  NN0  /\  y  e.  dom  ( x  e.  C  |->  ( cos `  ( n  x.  x
) ) ) )  ->  A. x  e.  C  ( cos `  ( n  x.  x ) )  e.  RR )
211 dmmptg 5487 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. x  e.  C  ( cos `  ( n  x.  x ) )  e.  RR  ->  dom  ( x  e.  C  |->  ( cos `  ( n  x.  x
) ) )  =  C )
212210, 211syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  e.  NN0  /\  y  e.  dom  ( x  e.  C  |->  ( cos `  ( n  x.  x
) ) ) )  ->  dom  ( x  e.  C  |->  ( cos `  ( n  x.  x
) ) )  =  C )
213204, 212eleqtrd 2544 . . . . . . . . . . . . . . . . . . 19  |-  ( ( n  e.  NN0  /\  y  e.  dom  ( x  e.  C  |->  ( cos `  ( n  x.  x
) ) ) )  ->  y  e.  C
)
214 eqidd 2455 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( n  e.  NN0  /\  y  e.  C )  ->  ( x  e.  C  |->  ( cos `  (
n  x.  x ) ) )  =  ( x  e.  C  |->  ( cos `  ( n  x.  x ) ) ) )
215 oveq2 6278 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  y  ->  (
n  x.  x )  =  ( n  x.  y ) )
216215fveq2d 5852 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  y  ->  ( cos `  ( n  x.  x ) )  =  ( cos `  (
n  x.  y ) ) )
217216adantl 464 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( n  e.  NN0  /\  y  e.  C )  /\  x  =  y )  ->  ( cos `  ( n  x.  x
) )  =  ( cos `  ( n  x.  y ) ) )
218 simpr 459 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( n  e.  NN0  /\  y  e.  C )  ->  y  e.  C )
219169adantr 463 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( n  e.  NN0  /\  y  e.  C )  ->  n  e.  RR )
220136, 218sseldi 3487 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( n  e.  NN0  /\  y  e.  C )  ->  y  e.  RR )
221219, 220remulcld 9613 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( n  e.  NN0  /\  y  e.  C )  ->  ( n  x.  y
)  e.  RR )
222221recoscld 13964 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( n  e.  NN0  /\  y  e.  C )  ->  ( cos `  (
n  x.  y ) )  e.  RR )
223214, 217, 218, 222fvmptd 5936 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( n  e.  NN0  /\  y  e.  C )  ->  ( ( x  e.  C  |->  ( cos `  (
n  x.  x ) ) ) `  y
)  =  ( cos `  ( n  x.  y
) ) )
224223fveq2d 5852 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  e.  NN0  /\  y  e.  C )  ->  ( abs `  (
( x  e.  C  |->  ( cos `  (
n  x.  x ) ) ) `  y
) )  =  ( abs `  ( cos `  ( n  x.  y
) ) ) )
225 abscosbd 31703 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( n  x.  y )  e.  RR  ->  ( abs `  ( cos `  (
n  x.  y ) ) )  <_  1
)
226221, 225syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  e.  NN0  /\  y  e.  C )  ->  ( abs `  ( cos `  ( n  x.  y ) ) )  <_  1 )
227224, 226eqbrtrd 4459 . . . . . . . . . . . . . . . . . . 19  |-  ( ( n  e.  NN0  /\  y  e.  C )  ->  ( abs `  (
( x  e.  C  |->  ( cos `  (
n  x.  x ) ) ) `  y
) )  <_  1
)
228213, 227syldan 468 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  e.  NN0  /\  y  e.  dom  ( x  e.  C  |->  ( cos `  ( n  x.  x
) ) ) )  ->  ( abs `  (
( x  e.  C  |->  ( cos `  (
n  x.  x ) ) ) `  y
) )  <_  1
)
229228ralrimiva 2868 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  NN0  ->  A. y  e.  dom  ( x  e.  C  |->  ( cos `  (
n  x.  x ) ) ) ( abs `  ( ( x  e.  C  |->  ( cos `  (
n  x.  x ) ) ) `  y
) )  <_  1
)
230 breq2 4443 . . . . . . . . . . . . . . . . . . 19  |-  ( b  =  1  ->  (
( abs `  (
( x  e.  C  |->  ( cos `  (
n  x.  x ) ) ) `  y
) )  <_  b  <->  ( abs `  ( ( x  e.  C  |->  ( cos `  ( n  x.  x ) ) ) `  y ) )  <_  1 ) )
231230ralbidv 2893 . . . . . . . . . . . . . . . . . 18  |-  ( 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
) )
232231rspcev 3207 . . . . . . . . . . . . . . . . 17  |-  ( ( 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
)
233203, 229, 232sylancr 661 . . . . . . . . . . . . . . . 16  |-  ( 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
)
234233adantl 464 . . . . . . . . . . . . . . 15  |-  ( (
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
)
235 bddmulibl 22414 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 )
236201, 202, 234, 235syl3anc 1226 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  NN0 )  ->  ( (
x  e.  C  |->  ( cos `  ( n  x.  x ) ) )  oF  x.  ( x  e.  C  |->  ( F `  x
) ) )  e.  L^1 )
237186, 236eqeltrd 2542 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  NN0 )  ->  ( x  e.  C  |->  ( ( F `  x )  x.  ( cos `  (
n  x.  x ) ) ) )  e.  L^1 )
23855, 237syldan 468 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
x  e.  C  |->  ( ( F `  x
)  x.  ( cos `  ( n  x.  x
) ) ) )  e.  L^1 )
239159, 174, 238itgmulc2 22409 . . . . . . . . . . 11  |-  ( (
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 )
240159adantr 463 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  ( cos `  ( n  x.  X ) )  e.  CC )
241120adantlr 712 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  ( F `  x )  e.  CC )
24254, 182sylanl2 649 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  ( cos `  ( n  x.  x ) )  e.  CC )
243240, 241, 242mul12d 9778 . . . . . . . . . . . . 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
) ) ) ) )
244240, 242mulcomd 9606 . . . . . . . . . . . . . 14  |-  ( ( ( 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
) ) ) )
245244oveq2d 6286 . . . . . . . . . . . . 13  |-  ( ( ( 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
) ) ) ) )
246243, 245eqtrd 2495 . . . . . . . . . . . 12  |-  ( ( ( 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
) ) ) ) )
247246itgeq2dv 22357 . . . . . . . . . . 11  |-  ( (
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 )
248239, 247eqtrd 2495 . . . . . . . . . 10  |-  ( (
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 )
249248oveq1d 6285 . . . . . . . . 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 ) )
250165, 249eqtr3d 2497 . . . . . . . 8  |-  ( (
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 ) )
251157, 160, 2503eqtrd 2499 . . . . . . 7  |-  ( (
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 ) )
25283, 80syldan 468 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  ( S. C ( ( F `
 x )  x.  ( sin `  (
n  x.  x ) ) )  _d x  /  pi )  e.  RR )
25321fvmpt2 5939 . . . . . . . . . 10  |-  ( ( 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 ) )
25483, 252, 253syl2anc 659 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  ( B `  n )  =  ( S. C
( ( F `  x )  x.  ( sin `  ( n  x.  x ) ) )  _d x  /  pi ) )
255254oveq1d 6285 . . . . . . . 8  |-  ( (
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
) ) ) )
256252recnd 9611 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  ( S. C ( ( F `
 x )  x.  ( sin `  (
n  x.  x ) ) )  _d x  /  pi )  e.  CC )
25785recnd 9611 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  ( sin `  ( n  x.  X ) )  e.  CC )
258256, 257mulcomd 9606 . . . . . . . 8  |-  ( (
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 ) ) )
25983, 77syldan 468 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  S. C ( ( F `
 x )  x.  ( sin `  (
n  x.  x ) ) )  _d x  e.  RR )
260259recnd 9611 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  S. C ( ( F `
 x )  x.  ( sin `  (
n  x.  x ) ) )  _d x  e.  CC )
261257, 260, 163, 164divassd 10351 . . . . . . . . 9  |-  ( (
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 ) ) )
262119adantlr 712 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  C )  ->  ( F `  x )  e.  RR )
263 nnre 10538 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  NN  ->  n  e.  RR )
264263adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( ( n  e.  NN  /\  x  e.  C )  ->  n  e.  RR )
265117adantl 464 . . . . . . . . . . . . . . . . 17  |-  ( ( n  e.  NN  /\  x  e.  C )  ->  x  e.  RR )
266264, 265remulcld 9613 . . . . . . . . . . . . . . . 16  |-  ( ( n  e.  NN  /\  x  e.  C )  ->  ( n  x.  x
)  e.  RR )
267266resincld 13963 . . . . . . . . . . . . . . 15  |-  ( ( n  e.  NN  /\  x  e.  C )  ->  ( sin `  (
n  x.  x ) )  e.  RR )
268267adantll 711 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  C )  ->  ( sin `  ( n  x.  x ) )  e.  RR )
269262, 268remulcld 9613 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  C )  ->  (
( F `  x
)  x.  ( sin `  ( n  x.  x
) ) )  e.  RR )
27053, 269sylanl2 649 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( F `  x
)  x.  ( sin `  ( n  x.  x
) ) )  e.  RR )
271177a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  C  e. 
_V )
272 eqidd 2455 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  ( x  e.  C  |->  ( sin `  ( n  x.  x
) ) )  =  ( x  e.  C  |->  ( sin `  (
n  x.  x ) ) ) )
273 eqidd 2455 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  ( x  e.  C  |->  ( F `
 x ) )  =  ( x  e.  C  |->  ( F `  x ) ) )
274271, 268, 262, 272, 273offval2 6529 . . . . . . . . . . . . . . 15  |-  ( (
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 ) ) ) )
275268recnd 9611 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  C )  ->  ( sin `  ( n  x.  x ) )  e.  CC )
276120adantlr 712 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  C )  ->  ( F `  x )  e.  CC )
277275, 276mulcomd 9606 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  C )  ->  (
( sin `  (
n  x.  x ) )  x.  ( F `
 x ) )  =  ( ( F `
 x )  x.  ( sin `  (
n  x.  x ) ) ) )
278277mpteq2dva 4525 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  ( x  e.  C  |->  ( ( sin `  ( n  x.  x ) )  x.  ( F `  x ) ) )  =  ( x  e.  C  |->  ( ( F `
 x )  x.  ( sin `  (
n  x.  x ) ) ) ) )
279274, 278eqtr2d 2496 . . . . . . . . . . . . . 14  |-  ( (
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 ) ) ) )
280 sincn 23008 . . . . . . . . . . . . . . . . . 18  |-  sin  e.  ( CC -cn-> CC )
281280a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN )  ->  sin  e.  ( CC -cn-> CC ) )
282190a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  NN  ->  C  C_  CC )
283263recnd 9611 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  NN  ->  n  e.  CC )
284194a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  NN  ->  CC  C_  CC )
285282, 283, 284constcncfg 31915 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  NN  ->  (
x  e.  C  |->  n )  e.  ( C
-cn-> CC ) )
286282, 284idcncfg 31916 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  NN  ->  (
x  e.  C  |->  x )  e.  ( C
-cn-> CC ) )
287285, 286mulcncf 22028 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  NN  ->  (
x  e.  C  |->  ( n  x.  x ) )  e.  ( C
-cn-> CC ) )
288287adantl 464 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN )  ->  ( x  e.  C  |->  ( n  x.  x ) )  e.  ( C -cn-> CC ) )
289281, 288cncfmpt1f 21586 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  ( x  e.  C  |->  ( sin `  ( n  x.  x
) ) )  e.  ( C -cn-> CC ) )
290 cnmbf 22235 . . . . . . . . . . . . . . . 16  |-  ( ( C  e.  dom  vol  /\  ( x  e.  C  |->  ( sin `  (
n  x.  x ) ) )  e.  ( C -cn-> CC ) )  -> 
( x  e.  C  |->  ( sin `  (
n  x.  x ) ) )  e. MblFn )
291176, 289, 290sylancr 661 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  ( x  e.  C  |->  ( sin `  ( n  x.  x
) ) )  e. MblFn
)
292140adantr 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  ( x  e.  C  |->  ( F `
 x ) )  e.  L^1 )
293 simpr 459 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  e.  NN  /\  y  e.  dom  ( x  e.  C  |->  ( sin `  ( n  x.  x
) ) ) )  ->  y  e.  dom  ( x  e.  C  |->  ( sin `  (
n  x.  x ) ) ) )
294267ralrimiva 2868 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  NN  ->  A. x  e.  C  ( sin `  ( n  x.  x
) )  e.  RR )
295 dmmptg 5487 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( A. x  e.  C  ( sin `  ( n  x.  x ) )  e.  RR  ->  dom  ( x  e.  C  |->  ( sin `  ( n  x.  x
) ) )  =  C )
296294, 295syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  NN  ->  dom  ( x  e.  C  |->  ( sin `  (
n  x.  x ) ) )  =  C )
297296adantr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  e.  NN  /\  y  e.  dom  ( x  e.  C  |->  ( sin `  ( n  x.  x
) ) ) )  ->  dom  ( x  e.  C  |->  ( sin `  ( n  x.  x
) ) )  =  C )
298293, 297eleqtrd 2544 . . . . . . . . . . . . . . . . . . 19  |-  ( ( n  e.  NN  /\  y  e.  dom  ( x  e.  C  |->  ( sin `  ( n  x.  x
) ) ) )  ->  y  e.  C
)
299 eqidd 2455 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( n  e.  NN  /\  y  e.  C )  ->  ( x  e.  C  |->  ( sin `  (
n  x.  x ) ) )  =  ( x  e.  C  |->  ( sin `  ( n  x.  x ) ) ) )
300215fveq2d 5852 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  y  ->  ( sin `  ( n  x.  x ) )  =  ( sin `  (
n  x.  y ) ) )
301300adantl 464 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( n  e.  NN  /\  y  e.  C )  /\  x  =  y )  ->  ( sin `  ( n  x.  x
) )  =  ( sin `  ( n  x.  y ) ) )
302 simpr 459 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( n  e.  NN  /\  y  e.  C )  ->  y  e.  C )
303263adantr 463 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( n  e.  NN  /\  y  e.  C )  ->  n  e.  RR )
304136, 302sseldi 3487 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( n  e.  NN  /\  y  e.  C )  ->  y  e.  RR )
305303, 304remulcld 9613 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( n  e.  NN  /\  y  e.  C )  ->  ( n  x.  y
)  e.  RR )
306305resincld 13963 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( n  e.  NN  /\  y  e.  C )  ->  ( sin `  (
n  x.  y ) )  e.  RR )
307299, 301, 302, 306fvmptd 5936 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( n  e.  NN  /\  y  e.  C )  ->  ( ( x  e.  C  |->  ( sin `  (
n  x.  x ) ) ) `  y
)  =  ( sin `  ( n  x.  y
) ) )
308307fveq2d 5852 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  e.  NN  /\  y  e.  C )  ->  ( abs `  (
( x  e.  C  |->  ( sin `  (
n  x.  x ) ) ) `  y
) )  =  ( abs `  ( sin `  ( n  x.  y
) ) ) )
309 abssinbd 31732 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( n  x.  y )  e.  RR  ->  ( abs `  ( sin `  (
n  x.  y ) ) )  <_  1
)
310305, 309syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  e.  NN  /\  y  e.  C )  ->  ( abs `  ( sin `  ( n  x.  y ) ) )  <_  1 )
311308, 310eqbrtrd 4459 . . . . . . . . . . . . . . . . . . 19  |-  ( ( n  e.  NN  /\  y  e.  C )  ->  ( abs `  (
( x  e.  C  |->  ( sin `  (
n  x.  x ) ) ) `  y
) )  <_  1
)
312298, 311syldan 468 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  e.  NN  /\  y  e.  dom  ( x  e.  C  |->  ( sin `  ( n  x.  x
) ) ) )  ->  ( abs `  (
( x  e.  C  |->  ( sin `  (
n  x.  x ) ) ) `  y
) )  <_  1
)
313312ralrimiva 2868 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  NN  ->  A. y  e.  dom  ( x  e.  C  |->  ( sin `  (
n  x.  x ) ) ) ( abs `  ( ( x  e.  C  |->  ( sin `  (
n  x.  x ) ) ) `  y
) )  <_  1
)
314 breq2 4443 . . . . . . . . . . . . . . . . . . 19  |-  ( b  =  1  ->  (
( abs `  (
( x  e.  C  |->  ( sin `  (
n  x.  x ) ) ) `  y
) )  <_  b  <->  ( abs `  ( ( x  e.  C  |->  ( sin `  ( n  x.  x ) ) ) `  y ) )  <_  1 ) )
315314ralbidv 2893 . . . . . . . . . . . . . . . . . 18  |-  ( 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
) )
316315rspcev 3207 . . . . . . . . . . . . . . . . 17  |-  ( ( 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
)
317203, 313, 316sylancr 661 . . . . . . . . . . . . . . . 16  |-  ( 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
)
318317adantl 464 . . . . . . . . . . . . . . 15  |-  ( (
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
)
319 bddmulibl 22414 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 )
320291, 292, 318, 319syl3anc 1226 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( x  e.  C  |->  ( sin `  ( n  x.  x ) ) )  oF  x.  ( x  e.  C  |->  ( F `  x
) ) )  e.  L^1 )
321279, 320eqeltrd 2542 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  NN )  ->  ( x  e.  C  |->  ( ( F `  x )  x.  ( sin `  (
n  x.  x ) ) ) )  e.  L^1 )
32283, 321syldan 468 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
x  e.  C  |->  ( ( F `  x
)  x.  ( sin `  ( n  x.  x
) ) ) )  e.  L^1 )
323257, 270, 322itgmulc2 22409 . . . . . . . . . . 11  |-  ( (
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 )
324257adantr 463 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  ( sin `  ( n  x.  X ) )  e.  CC )
32553, 275sylanl2 649 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  ( sin `  ( n  x.  x ) )  e.  CC )
326324, 241, 325mul12d 9778 . . . . . . . . . . . . 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
) ) ) ) )
327324, 325mulcomd 9606 . . . . . . . . . . . . . 14  |-  ( ( ( 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
) ) ) )
328327oveq2d 6286 . . . . . . . . . . . . 13  |-  ( ( ( 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
) ) ) ) )
329326, 328eqtrd 2495 . . . . . . . . . . . 12  |-  ( ( ( 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
) ) ) ) )
330329itgeq2dv 22357 . . . . . . . . . . 11  |-  ( (
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 )
331323, 330eqtrd 2495 . . . . . . . . . 10  |-  ( (
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 )
332331oveq1d 6285 . . . . . . . . 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 ) )
333261, 332eqtr3d 2497 . . . . . . . 8  |-  ( (
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 ) )
334255, 258, 3333eqtrd 2499 . . . . . . 7  |-  ( (
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 ) )
335251, 334oveq12d 6288 . . . . . 6  |-  ( (
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 ) ) )
33654, 168sylanl2 649 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  ( F `  x )  e.  RR )
33755, 208sylan 469 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  ( cos `  ( n  x.  x ) )  e.  RR )
33861adantr 463 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  ( cos `  ( n  x.  X ) )  e.  RR )
339337, 338remulcld 9613 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( cos `  (
n  x.  x ) )  x.  ( cos `  ( n  x.  X
) ) )  e.  RR )
340336, 339remulcld 9613 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( F `  x
)  x.  ( ( cos `  ( n  x.  x ) )  x.  ( cos `  (
n  x.  X ) ) ) )  e.  RR )
341241, 242, 240mul13d 31704 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) ) )
342242, 241mulcomd 9606 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( cos `  (
n  x.  x ) )  x.  ( F `
 x ) )  =  ( ( F `
 x )  x.  ( cos `  (
n  x.  x ) ) ) )
343342oveq2d 6286 . . . . . . . . . . 11  |-  ( ( ( 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
) ) ) ) )
344341, 343eqtrd 2495 . . . . . . . . . 10  |-  ( ( ( 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 ) ) ) ) )
345344mpteq2dva 4525 . . . . . . . . 9  |-  ( (
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
) ) ) ) ) )
346159, 174, 238iblmulc2 22406 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
x  e.  C  |->  ( ( cos `  (
n  x.  X ) )  x.  ( ( F `  x )  x.  ( cos `  (
n  x.  x ) ) ) ) )  e.  L^1 )
347345, 346eqeltrd 2542 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
x  e.  C  |->  ( ( F `  x
)  x.  ( ( cos `  ( n  x.  x ) )  x.  ( cos `  (
n  x.  X ) ) ) ) )  e.  L^1 )
348340, 347itgcl 22359 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  S. C ( ( F `
 x )  x.  ( ( cos `  (
n  x.  x ) )  x.  ( cos `  ( n  x.  X
) ) ) )  _d x  e.  CC )
34983, 267sylan 469 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  ( sin `  ( n  x.  x ) )  e.  RR )
35085adantr 463 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  ( sin `  ( n  x.  X ) )  e.  RR )
351349, 350remulcld 9613 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( sin `  (
n  x.  x ) )  x.  ( sin `  ( n  x.  X
) ) )  e.  RR )
352336, 351remulcld 9613 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( F `  x
)  x.  ( ( sin `  ( n  x.  x ) )  x.  ( sin `  (
n  x.  X ) ) ) )  e.  RR )
353241, 325, 324mul13d 31704 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) ) )
354325, 241mulcomd 9606 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( sin `  (
n  x.  x ) )  x.  ( F `
 x ) )  =  ( ( F `
 x )  x.  ( sin `  (
n  x.  x ) ) ) )
355354oveq2d 6286 . . . . . . . . . . 11  |-  ( ( ( 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
) ) ) ) )
356353, 355eqtrd 2495 . . . . . . . . . 10  |-  ( ( ( 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 ) ) ) ) )
357356mpteq2dva 4525 . . . . . . . . 9  |-  ( (
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
) ) ) ) ) )
358257, 270, 322iblmulc2 22406 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
x  e.  C  |->  ( ( sin `  (
n  x.  X ) )  x.  ( ( F `  x )  x.  ( sin `  (
n  x.  x ) ) ) ) )  e.  L^1 )
359357, 358eqeltrd 2542 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
x  e.  C  |->  ( ( F `  x
)  x.  ( ( sin `  ( n  x.  x ) )  x.  ( sin `  (
n  x.  X ) ) ) ) )  e.  L^1 )
360352, 359itgcl 22359 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  S. C ( ( F `
 x )  x.  ( ( sin `  (
n  x.  x ) )  x.  ( sin `  ( n  x.  X
) ) ) )  _d x  e.  CC )
361348, 360, 163, 164divdird 10354 . . . . . 6  |-  ( (
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 ) ) )
36253nncnd 10547 . . . . . . . . . . . . . . 15  |-  ( n  e.  ( 1 ... N )  ->  n  e.  CC )
363362ad2antlr 724 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  n  e.  CC )
364108adantl 464 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  x  e.  CC )
36558recnd 9611 . . . . . . . . . . . . . . 15  |-  ( ph  ->  X  e.  CC )
366365ad2antrr 723 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  X  e.  CC )
367363, 364, 366subdid 10008 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
n  x.  ( x  -  X ) )  =  ( ( n  x.  x )  -  ( n  x.  X
) ) )
368367fveq2d 5852 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  ( cos `  ( n  x.  ( x  -  X
) ) )  =  ( cos `  (
( n  x.  x
)  -  ( n  x.  X ) ) ) )
369363, 364mulcld 9605 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
n  x.  x )  e.  CC )
370363, 366mulcld 9605 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
n  x.  X )  e.  CC )
371 cossub 13989 . . . . . . . . . . . . 13  |-  ( ( ( 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
) ) ) ) )
372369, 370, 371syl2anc 659 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) ) ) )
373368, 372eqtrd 2495 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) ) ) )
374373oveq2d 6286 . . . . . . . . . 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
) ) )  +  ( ( sin `  (
n  x.  x ) )  x.  ( sin `  ( n  x.  X
) ) ) ) ) )
375339recnd 9611 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( cos `  (
n  x.  x ) )  x.  ( cos `  ( n  x.  X
) ) )  e.  CC )
376351recnd 9611 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( sin `  (
n  x.  x ) )  x.  ( sin `  ( n  x.  X
) ) )  e.  CC )
377241, 375, 376adddid 9609 . . . . . . . . . 10  |-  ( ( ( 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
) ) ) ) ) )
378374, 377eqtrd 2495 . . . . . . . . 9  |-  ( ( ( 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
) ) ) ) ) )
379378itgeq2dv 22357 . . . . . . . 8  |-  ( (
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 )
380340, 347, 352, 359itgadd 22400 . . . . . . . 8  |-  ( (
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 ) )
381379, 380eqtr2d 2496 . . . . . . 7  |-  ( (
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.  ( x  -  X ) ) ) )  _d x )
382381oveq1d 6285 . . . . . 6  |-  ( (
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 ) ) ) )  _d x  /  pi ) )
383335, 361, 3823eqtr2d 2501 . . . . 5  |-  ( (
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 ) ) ) )  _d x  /  pi ) )
384383sumeq2dv 13610 . . . 4  |-  ( ph  -> 
sum_ n  e.  (
1 ... N ) ( ( ( A `  n )  x.  ( cos `  ( n  x.  X ) ) )  +  ( ( B `
 n )  x.  ( sin `  (
n  x.  X ) ) ) )  = 
sum_ n  e.  (
1 ... N ) ( S. C ( ( F `  x )  x.  ( cos `  (
n  x.  ( x  -  X ) ) ) )  _d x  /  pi ) )
38557adantr 463 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  n  e.  RR )
386117adantl 464 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  x  e.  RR )
38758ad2antrr 723 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  X  e.  RR )
388386, 387resubcld 9983 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
x  -  X )  e.  RR )
389385, 388remulcld 9613 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
n  x.  ( x  -  X ) )  e.  RR )
390389recoscld 13964 . . . . . . 7  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  ( cos `  ( n  x.  ( x  -  X
) ) )  e.  RR )
391336, 390remulcld 9613 . . . . . 6  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )  ->  (
( F `  x
)  x.  ( cos `  ( n  x.  (
x  -  X ) ) ) )  e.  RR )
392177a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  C  e.  _V )
393 eqidd 2455 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
x  e.  C  |->  ( cos `  ( n  x.  ( x  -  X ) ) ) )  =  ( x  e.  C  |->  ( cos `  ( n  x.  (
x  -  X ) ) ) ) )
394 eqidd 2455 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
x  e.  C  |->  ( F `  x ) )  =  ( x  e.  C  |->  ( F `
 x ) ) )
395392, 390, 336, 393, 394offval2 6529 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( x  e.  C  |->  ( cos `  (
n  x.  ( x  -  X ) ) ) )  oF  x.  ( x  e.  C  |->  ( F `  x ) ) )  =  ( x  e.  C  |->  ( ( cos `  ( n  x.  (
x  -  X ) ) )  x.  ( F `  x )
) ) )
396390recnd 9611 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  x  e.  C )