Metamath Proof Explorer

Theorem fourierdlem83

Description: The fourier partial sum for F rewritten as an integral. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses 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 fourierdlem83 
|- ( ph -> ( S ` N ) = S. C ( ( F ` x ) x. ( ( D ` N ) ` ( x - X ) ) ) _d x )

Proof

Step Hyp Ref Expression
1 fourierdlem83.f 
 |-  ( ph -> F : RR --> RR )
2 fourierdlem83.c 
 |-  C = ( -u _pi (,) _pi )
3 fourierdlem83.fl1 
 |-  ( ph -> ( F |` C ) e. L^1 )
4 fourierdlem83.a 
 |-  A = ( n e. NN0 |-> ( S. C ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) )
5 fourierdlem83.b 
 |-  B = ( n e. NN |-> ( S. C ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) )
6 fourierdlem83.x 
 |-  ( ph -> X e. RR )
7 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 ) ) ) ) ) )
8 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 ) ) ) ) ) ) )
9 fourierdlem83.n 
 |-  ( ph -> N e. NN )
10 7 a1i 
 |-  ( 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 ) ) ) ) ) ) )
11 oveq2 
 |-  ( m = N -> ( 1 ... m ) = ( 1 ... N ) )
12 11 sumeq1d 
 |-  ( 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 ) ) ) ) )
13 12 oveq2d 
 |-  ( 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 ) ) ) ) ) )
14 13 adantl 
 |-  ( ( 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 ) ) ) ) ) )
15 id 
 |-  ( ph -> ph )
16 0nn0 
 |-  0 e. NN0
17 16 a1i 
 |-  ( ph -> 0 e. NN0 )
18 16 elexi 
 |-  0 e. _V
19 eleq1 
 |-  ( n = 0 -> ( n e. NN0 <-> 0 e. NN0 ) )
20 19 anbi2d 
 |-  ( n = 0 -> ( ( ph /\ n e. NN0 ) <-> ( ph /\ 0 e. NN0 ) ) )
21 fveq2 
 |-  ( n = 0 -> ( A ` n ) = ( A ` 0 ) )
22 21 eleq1d 
 |-  ( n = 0 -> ( ( A ` n ) e. RR <-> ( A ` 0 ) e. RR ) )
23 20 22 imbi12d 
 |-  ( n = 0 -> ( ( ( ph /\ n e. NN0 ) -> ( A ` n ) e. RR ) <-> ( ( ph /\ 0 e. NN0 ) -> ( A ` 0 ) e. RR ) ) )
24 1 2 3 4 5 fourierdlem22 
 |-  ( ph -> ( ( n e. NN0 -> ( A ` n ) e. RR ) /\ ( n e. NN -> ( B ` n ) e. RR ) ) )
25 24 simpld 
 |-  ( ph -> ( n e. NN0 -> ( A ` n ) e. RR ) )
26 25 imp 
 |-  ( ( ph /\ n e. NN0 ) -> ( A ` n ) e. RR )
27 18 23 26 vtocl 
 |-  ( ( ph /\ 0 e. NN0 ) -> ( A ` 0 ) e. RR )
28 15 17 27 syl2anc 
 |-  ( ph -> ( A ` 0 ) e. RR )
29 28 rehalfcld 
 |-  ( ph -> ( ( A ` 0 ) / 2 ) e. RR )
30 fzfid 
 |-  ( ph -> ( 1 ... N ) e. Fin )
31 eleq1 
 |-  ( k = n -> ( k e. NN0 <-> n e. NN0 ) )
32 31 anbi2d 
 |-  ( k = n -> ( ( ph /\ k e. NN0 ) <-> ( ph /\ n e. NN0 ) ) )
33 simpl 
 |-  ( ( k = n /\ x e. C ) -> k = n )
34 33 oveq1d 
 |-  ( ( k = n /\ x e. C ) -> ( k x. x ) = ( n x. x ) )
35 34 fveq2d 
 |-  ( ( k = n /\ x e. C ) -> ( cos ` ( k x. x ) ) = ( cos ` ( n x. x ) ) )
36 35 oveq2d 
 |-  ( ( k = n /\ x e. C ) -> ( ( F ` x ) x. ( cos ` ( k x. x ) ) ) = ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) )
37 36 itgeq2dv 
 |-  ( k = n -> S. C ( ( F ` x ) x. ( cos ` ( k x. x ) ) ) _d x = S. C ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x )
38 37 eleq1d 
 |-  ( 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 ) )
39 32 38 imbi12d 
 |-  ( 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 ) ) )
40 1 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> F : RR --> RR )
41 3 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> ( F |` C ) e. L^1 )
42 simpr 
 |-  ( ( ph /\ k e. NN0 ) -> k e. NN0 )
43 40 2 41 4 42 fourierdlem16 
 |-  ( ( 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 ) )
44 43 simprd 
 |-  ( ( ph /\ k e. NN0 ) -> S. C ( ( F ` x ) x. ( cos ` ( k x. x ) ) ) _d x e. RR )
45 39 44 chvarvv 
 |-  ( ( ph /\ n e. NN0 ) -> S. C ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x e. RR )
46 pire 
 |-  _pi e. RR
47 46 a1i 
 |-  ( ( ph /\ n e. NN0 ) -> _pi e. RR )
48 0re 
 |-  0 e. RR
49 pipos 
 |-  0 < _pi
50 48 49 gtneii 
 |-  _pi =/= 0
51 50 a1i 
 |-  ( ( ph /\ n e. NN0 ) -> _pi =/= 0 )
52 45 47 51 redivcld 
 |-  ( ( ph /\ n e. NN0 ) -> ( S. C ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) e. RR )
53 52 4 fmptd 
 |-  ( ph -> A : NN0 --> RR )
54 53 adantr 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> A : NN0 --> RR )
55 elfznn 
 |-  ( n e. ( 1 ... N ) -> n e. NN )
56 55 nnnn0d 
 |-  ( n e. ( 1 ... N ) -> n e. NN0 )
57 56 adantl 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> n e. NN0 )
58 54 57 ffvelrnd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( A ` n ) e. RR )
59 57 nn0red 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> n e. RR )
60 6 adantr 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> X e. RR )
61 59 60 remulcld 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( n x. X ) e. RR )
62 61 recoscld 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( cos ` ( n x. X ) ) e. RR )
63 58 62 remulcld 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) e. RR )
64 eleq1 
 |-  ( k = n -> ( k e. NN <-> n e. NN ) )
65 64 anbi2d 
 |-  ( k = n -> ( ( ph /\ k e. NN ) <-> ( ph /\ n e. NN ) ) )
66 oveq1 
 |-  ( k = n -> ( k x. x ) = ( n x. x ) )
67 66 fveq2d 
 |-  ( k = n -> ( sin ` ( k x. x ) ) = ( sin ` ( n x. x ) ) )
68 67 oveq2d 
 |-  ( k = n -> ( ( F ` x ) x. ( sin ` ( k x. x ) ) ) = ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) )
69 68 adantr 
 |-  ( ( k = n /\ x e. C ) -> ( ( F ` x ) x. ( sin ` ( k x. x ) ) ) = ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) )
70 69 itgeq2dv 
 |-  ( k = n -> S. C ( ( F ` x ) x. ( sin ` ( k x. x ) ) ) _d x = S. C ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x )
71 70 eleq1d 
 |-  ( 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 ) )
72 65 71 imbi12d 
 |-  ( 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 ) ) )
73 1 adantr 
 |-  ( ( ph /\ k e. NN ) -> F : RR --> RR )
74 3 adantr 
 |-  ( ( ph /\ k e. NN ) -> ( F |` C ) e. L^1 )
75 simpr 
 |-  ( ( ph /\ k e. NN ) -> k e. NN )
76 73 2 74 5 75 fourierdlem21 
 |-  ( ( 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 ) )
77 76 simprd 
 |-  ( ( ph /\ k e. NN ) -> S. C ( ( F ` x ) x. ( sin ` ( k x. x ) ) ) _d x e. RR )
78 72 77 chvarvv 
 |-  ( ( ph /\ n e. NN ) -> S. C ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x e. RR )
79 46 a1i 
 |-  ( ( ph /\ n e. NN ) -> _pi e. RR )
80 50 a1i 
 |-  ( ( ph /\ n e. NN ) -> _pi =/= 0 )
81 78 79 80 redivcld 
 |-  ( ( ph /\ n e. NN ) -> ( S. C ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) e. RR )
82 81 5 fmptd 
 |-  ( ph -> B : NN --> RR )
83 82 adantr 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> B : NN --> RR )
84 55 adantl 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> n e. NN )
85 83 84 ffvelrnd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( B ` n ) e. RR )
86 61 resincld 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( sin ` ( n x. X ) ) e. RR )
87 85 86 remulcld 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) e. RR )
88 63 87 readdcld 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) e. RR )
89 30 88 fsumrecl 
 |-  ( ph -> sum_ n e. ( 1 ... N ) ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) e. RR )
90 29 89 readdcld 
 |-  ( 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 )
91 10 14 9 90 fvmptd 
 |-  ( 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 ) ) ) ) ) )
92 4 a1i 
 |-  ( ph -> A = ( n e. NN0 |-> ( S. C ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) ) )
93 oveq1 
 |-  ( n = 0 -> ( n x. x ) = ( 0 x. x ) )
94 93 fveq2d 
 |-  ( n = 0 -> ( cos ` ( n x. x ) ) = ( cos ` ( 0 x. x ) ) )
95 94 oveq2d 
 |-  ( n = 0 -> ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) = ( ( F ` x ) x. ( cos ` ( 0 x. x ) ) ) )
96 95 adantr 
 |-  ( ( n = 0 /\ x e. C ) -> ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) = ( ( F ` x ) x. ( cos ` ( 0 x. x ) ) ) )
97 96 itgeq2dv 
 |-  ( n = 0 -> S. C ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x = S. C ( ( F ` x ) x. ( cos ` ( 0 x. x ) ) ) _d x )
98 97 adantl 
 |-  ( ( 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 )
99 98 oveq1d 
 |-  ( ( 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 ) )
100 1 2 3 4 17 fourierdlem16 
 |-  ( 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 ) )
101 100 simprd 
 |-  ( ph -> S. C ( ( F ` x ) x. ( cos ` ( 0 x. x ) ) ) _d x e. RR )
102 46 a1i 
 |-  ( ph -> _pi e. RR )
103 50 a1i 
 |-  ( ph -> _pi =/= 0 )
104 101 102 103 redivcld 
 |-  ( ph -> ( S. C ( ( F ` x ) x. ( cos ` ( 0 x. x ) ) ) _d x / _pi ) e. RR )
105 92 99 17 104 fvmptd 
 |-  ( ph -> ( A ` 0 ) = ( S. C ( ( F ` x ) x. ( cos ` ( 0 x. x ) ) ) _d x / _pi ) )
106 ioosscn 
 |-  ( -u _pi (,) _pi ) C_ CC
107 id 
 |-  ( x e. C -> x e. C )
108 107 2 eleqtrdi 
 |-  ( x e. C -> x e. ( -u _pi (,) _pi ) )
109 106 108 sselid 
 |-  ( x e. C -> x e. CC )
110 109 mul02d 
 |-  ( x e. C -> ( 0 x. x ) = 0 )
111 110 fveq2d 
 |-  ( x e. C -> ( cos ` ( 0 x. x ) ) = ( cos ` 0 ) )
112 cos0 
 |-  ( cos ` 0 ) = 1
113 111 112 eqtrdi 
 |-  ( x e. C -> ( cos ` ( 0 x. x ) ) = 1 )
114 113 oveq2d 
 |-  ( x e. C -> ( ( F ` x ) x. ( cos ` ( 0 x. x ) ) ) = ( ( F ` x ) x. 1 ) )
115 114 adantl 
 |-  ( ( ph /\ x e. C ) -> ( ( F ` x ) x. ( cos ` ( 0 x. x ) ) ) = ( ( F ` x ) x. 1 ) )
116 1 adantr 
 |-  ( ( ph /\ x e. C ) -> F : RR --> RR )
117 ioossre 
 |-  ( -u _pi (,) _pi ) C_ RR
118 117 108 sselid 
 |-  ( x e. C -> x e. RR )
119 118 adantl 
 |-  ( ( ph /\ x e. C ) -> x e. RR )
120 116 119 ffvelrnd 
 |-  ( ( ph /\ x e. C ) -> ( F ` x ) e. RR )
121 120 recnd 
 |-  ( ( ph /\ x e. C ) -> ( F ` x ) e. CC )
122 121 mulid1d 
 |-  ( ( ph /\ x e. C ) -> ( ( F ` x ) x. 1 ) = ( F ` x ) )
123 115 122 eqtrd 
 |-  ( ( ph /\ x e. C ) -> ( ( F ` x ) x. ( cos ` ( 0 x. x ) ) ) = ( F ` x ) )
124 123 itgeq2dv 
 |-  ( ph -> S. C ( ( F ` x ) x. ( cos ` ( 0 x. x ) ) ) _d x = S. C ( F ` x ) _d x )
125 124 oveq1d 
 |-  ( ph -> ( S. C ( ( F ` x ) x. ( cos ` ( 0 x. x ) ) ) _d x / _pi ) = ( S. C ( F ` x ) _d x / _pi ) )
126 105 125 eqtrd 
 |-  ( ph -> ( A ` 0 ) = ( S. C ( F ` x ) _d x / _pi ) )
127 126 oveq1d 
 |-  ( ph -> ( ( A ` 0 ) / 2 ) = ( ( S. C ( F ` x ) _d x / _pi ) / 2 ) )
128 1 feqmptd 
 |-  ( ph -> F = ( x e. RR |-> ( F ` x ) ) )
129 128 reseq1d 
 |-  ( ph -> ( F |` C ) = ( ( x e. RR |-> ( F ` x ) ) |` C ) )
130 46 a1i 
 |-  ( x e. C -> _pi e. RR )
131 130 renegcld 
 |-  ( x e. C -> -u _pi e. RR )
132 ioossicc 
 |-  ( -u _pi (,) _pi ) C_ ( -u _pi [,] _pi )
133 2 132 eqsstri 
 |-  C C_ ( -u _pi [,] _pi )
134 133 sseli 
 |-  ( x e. C -> x e. ( -u _pi [,] _pi ) )
135 eliccre 
 |-  ( ( -u _pi e. RR /\ _pi e. RR /\ x e. ( -u _pi [,] _pi ) ) -> x e. RR )
136 131 130 134 135 syl3anc 
 |-  ( x e. C -> x e. RR )
137 136 ssriv 
 |-  C C_ RR
138 resmpt 
 |-  ( C C_ RR -> ( ( x e. RR |-> ( F ` x ) ) |` C ) = ( x e. C |-> ( F ` x ) ) )
139 137 138 mp1i 
 |-  ( ph -> ( ( x e. RR |-> ( F ` x ) ) |` C ) = ( x e. C |-> ( F ` x ) ) )
140 129 139 eqtr2d 
 |-  ( ph -> ( x e. C |-> ( F ` x ) ) = ( F |` C ) )
141 140 3 eqeltrd 
 |-  ( ph -> ( x e. C |-> ( F ` x ) ) e. L^1 )
142 120 141 itgcl 
 |-  ( ph -> S. C ( F ` x ) _d x e. CC )
143 102 recnd 
 |-  ( ph -> _pi e. CC )
144 2cnd 
 |-  ( ph -> 2 e. CC )
145 2ne0 
 |-  2 =/= 0
146 145 a1i 
 |-  ( ph -> 2 =/= 0 )
147 142 143 144 103 146 divdiv32d 
 |-  ( ph -> ( ( S. C ( F ` x ) _d x / _pi ) / 2 ) = ( ( S. C ( F ` x ) _d x / 2 ) / _pi ) )
148 142 144 146 divrecd 
 |-  ( ph -> ( S. C ( F ` x ) _d x / 2 ) = ( S. C ( F ` x ) _d x x. ( 1 / 2 ) ) )
149 144 146 reccld 
 |-  ( ph -> ( 1 / 2 ) e. CC )
150 142 149 mulcomd 
 |-  ( ph -> ( S. C ( F ` x ) _d x x. ( 1 / 2 ) ) = ( ( 1 / 2 ) x. S. C ( F ` x ) _d x ) )
151 149 120 141 itgmulc2 
 |-  ( ph -> ( ( 1 / 2 ) x. S. C ( F ` x ) _d x ) = S. C ( ( 1 / 2 ) x. ( F ` x ) ) _d x )
152 148 150 151 3eqtrd 
 |-  ( ph -> ( S. C ( F ` x ) _d x / 2 ) = S. C ( ( 1 / 2 ) x. ( F ` x ) ) _d x )
153 152 oveq1d 
 |-  ( ph -> ( ( S. C ( F ` x ) _d x / 2 ) / _pi ) = ( S. C ( ( 1 / 2 ) x. ( F ` x ) ) _d x / _pi ) )
154 127 147 153 3eqtrd 
 |-  ( ph -> ( ( A ` 0 ) / 2 ) = ( S. C ( ( 1 / 2 ) x. ( F ` x ) ) _d x / _pi ) )
155 57 52 syldan 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( S. C ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) e. RR )
156 4 fvmpt2 
 |-  ( ( 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 ) )
157 57 155 156 syl2anc 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( A ` n ) = ( S. C ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) )
158 157 oveq1d 
 |-  ( ( 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 ) ) ) )
159 155 recnd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( S. C ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) e. CC )
160 62 recnd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( cos ` ( n x. X ) ) e. CC )
161 159 160 mulcomd 
 |-  ( ( 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 ) ) )
162 57 45 syldan 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> S. C ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x e. RR )
163 162 recnd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> S. C ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x e. CC )
164 143 adantr 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> _pi e. CC )
165 50 a1i 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> _pi =/= 0 )
166 160 163 164 165 divassd 
 |-  ( ( 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 ) ) )
167 1 ad2antrr 
 |-  ( ( ( ph /\ n e. NN0 ) /\ x e. C ) -> F : RR --> RR )
168 118 adantl 
 |-  ( ( ( ph /\ n e. NN0 ) /\ x e. C ) -> x e. RR )
169 167 168 ffvelrnd 
 |-  ( ( ( ph /\ n e. NN0 ) /\ x e. C ) -> ( F ` x ) e. RR )
170 nn0re 
 |-  ( n e. NN0 -> n e. RR )
171 170 ad2antlr 
 |-  ( ( ( ph /\ n e. NN0 ) /\ x e. C ) -> n e. RR )
172 171 168 remulcld 
 |-  ( ( ( ph /\ n e. NN0 ) /\ x e. C ) -> ( n x. x ) e. RR )
173 172 recoscld 
 |-  ( ( ( ph /\ n e. NN0 ) /\ x e. C ) -> ( cos ` ( n x. x ) ) e. RR )
174 169 173 remulcld 
 |-  ( ( ( ph /\ n e. NN0 ) /\ x e. C ) -> ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) e. RR )
175 56 174 sylanl2 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) e. RR )
176 ioombl 
 |-  ( -u _pi (,) _pi ) e. dom vol
177 2 176 eqeltri 
 |-  C e. dom vol
178 177 elexi 
 |-  C e. _V
179 178 a1i 
 |-  ( ( ph /\ n e. NN0 ) -> C e. _V )
180 eqidd 
 |-  ( ( ph /\ n e. NN0 ) -> ( x e. C |-> ( cos ` ( n x. x ) ) ) = ( x e. C |-> ( cos ` ( n x. x ) ) ) )
181 eqidd 
 |-  ( ( ph /\ n e. NN0 ) -> ( x e. C |-> ( F ` x ) ) = ( x e. C |-> ( F ` x ) ) )
182 179 173 169 180 181 offval2 
 |-  ( ( 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 ) ) ) )
183 173 recnd 
 |-  ( ( ( ph /\ n e. NN0 ) /\ x e. C ) -> ( cos ` ( n x. x ) ) e. CC )
184 121 adantlr 
 |-  ( ( ( ph /\ n e. NN0 ) /\ x e. C ) -> ( F ` x ) e. CC )
185 183 184 mulcomd 
 |-  ( ( ( ph /\ n e. NN0 ) /\ x e. C ) -> ( ( cos ` ( n x. x ) ) x. ( F ` x ) ) = ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) )
186 185 mpteq2dva 
 |-  ( ( ph /\ n e. NN0 ) -> ( x e. C |-> ( ( cos ` ( n x. x ) ) x. ( F ` x ) ) ) = ( x e. C |-> ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) ) )
187 182 186 eqtr2d 
 |-  ( ( 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 ) ) ) )
188 coscn 
 |-  cos e. ( CC -cn-> CC )
189 188 a1i 
 |-  ( ( ph /\ n e. NN0 ) -> cos e. ( CC -cn-> CC ) )
190 ax-resscn 
 |-  RR C_ CC
191 137 190 sstri 
 |-  C C_ CC
192 191 a1i 
 |-  ( ( ph /\ n e. NN0 ) -> C C_ CC )
193 170 recnd 
 |-  ( n e. NN0 -> n e. CC )
194 193 adantl 
 |-  ( ( ph /\ n e. NN0 ) -> n e. CC )
195 ssid 
 |-  CC C_ CC
196 195 a1i 
 |-  ( ( ph /\ n e. NN0 ) -> CC C_ CC )
197 192 194 196 constcncfg 
 |-  ( ( ph /\ n e. NN0 ) -> ( x e. C |-> n ) e. ( C -cn-> CC ) )
198 192 196 idcncfg 
 |-  ( ( ph /\ n e. NN0 ) -> ( x e. C |-> x ) e. ( C -cn-> CC ) )
199 197 198 mulcncf 
 |-  ( ( ph /\ n e. NN0 ) -> ( x e. C |-> ( n x. x ) ) e. ( C -cn-> CC ) )
200 189 199 cncfmpt1f 
 |-  ( ( ph /\ n e. NN0 ) -> ( x e. C |-> ( cos ` ( n x. x ) ) ) e. ( C -cn-> CC ) )
201 cnmbf 
 |-  ( ( C e. dom vol /\ ( x e. C |-> ( cos ` ( n x. x ) ) ) e. ( C -cn-> CC ) ) -> ( x e. C |-> ( cos ` ( n x. x ) ) ) e. MblFn )
202 177 200 201 sylancr 
 |-  ( ( ph /\ n e. NN0 ) -> ( x e. C |-> ( cos ` ( n x. x ) ) ) e. MblFn )
203 141 adantr 
 |-  ( ( ph /\ n e. NN0 ) -> ( x e. C |-> ( F ` x ) ) e. L^1 )
204 1re 
 |-  1 e. RR
205 simpr 
 |-  ( ( n e. NN0 /\ y e. dom ( x e. C |-> ( cos ` ( n x. x ) ) ) ) -> y e. dom ( x e. C |-> ( cos ` ( n x. x ) ) ) )
206 170 adantr 
 |-  ( ( n e. NN0 /\ x e. C ) -> n e. RR )
207 118 adantl 
 |-  ( ( n e. NN0 /\ x e. C ) -> x e. RR )
208 206 207 remulcld 
 |-  ( ( n e. NN0 /\ x e. C ) -> ( n x. x ) e. RR )
209 208 recoscld 
 |-  ( ( n e. NN0 /\ x e. C ) -> ( cos ` ( n x. x ) ) e. RR )
210 209 ralrimiva 
 |-  ( n e. NN0 -> A. x e. C ( cos ` ( n x. x ) ) e. RR )
211 210 adantr 
 |-  ( ( n e. NN0 /\ y e. dom ( x e. C |-> ( cos ` ( n x. x ) ) ) ) -> A. x e. C ( cos ` ( n x. x ) ) e. RR )
212 dmmptg 
 |-  ( A. x e. C ( cos ` ( n x. x ) ) e. RR -> dom ( x e. C |-> ( cos ` ( n x. x ) ) ) = C )
213 211 212 syl 
 |-  ( ( n e. NN0 /\ y e. dom ( x e. C |-> ( cos ` ( n x. x ) ) ) ) -> dom ( x e. C |-> ( cos ` ( n x. x ) ) ) = C )
214 205 213 eleqtrd 
 |-  ( ( n e. NN0 /\ y e. dom ( x e. C |-> ( cos ` ( n x. x ) ) ) ) -> y e. C )
215 eqidd 
 |-  ( ( n e. NN0 /\ y e. C ) -> ( x e. C |-> ( cos ` ( n x. x ) ) ) = ( x e. C |-> ( cos ` ( n x. x ) ) ) )
216 oveq2 
 |-  ( x = y -> ( n x. x ) = ( n x. y ) )
217 216 fveq2d 
 |-  ( x = y -> ( cos ` ( n x. x ) ) = ( cos ` ( n x. y ) ) )
218 217 adantl 
 |-  ( ( ( n e. NN0 /\ y e. C ) /\ x = y ) -> ( cos ` ( n x. x ) ) = ( cos ` ( n x. y ) ) )
219 simpr 
 |-  ( ( n e. NN0 /\ y e. C ) -> y e. C )
220 170 adantr 
 |-  ( ( n e. NN0 /\ y e. C ) -> n e. RR )
221 137 219 sselid 
 |-  ( ( n e. NN0 /\ y e. C ) -> y e. RR )
222 220 221 remulcld 
 |-  ( ( n e. NN0 /\ y e. C ) -> ( n x. y ) e. RR )
223 222 recoscld 
 |-  ( ( n e. NN0 /\ y e. C ) -> ( cos ` ( n x. y ) ) e. RR )
224 215 218 219 223 fvmptd 
 |-  ( ( n e. NN0 /\ y e. C ) -> ( ( x e. C |-> ( cos ` ( n x. x ) ) ) ` y ) = ( cos ` ( n x. y ) ) )
225 224 fveq2d 
 |-  ( ( n e. NN0 /\ y e. C ) -> ( abs ` ( ( x e. C |-> ( cos ` ( n x. x ) ) ) ` y ) ) = ( abs ` ( cos ` ( n x. y ) ) ) )
226 abscosbd 
 |-  ( ( n x. y ) e. RR -> ( abs ` ( cos ` ( n x. y ) ) ) <_ 1 )
227 222 226 syl 
 |-  ( ( n e. NN0 /\ y e. C ) -> ( abs ` ( cos ` ( n x. y ) ) ) <_ 1 )
228 225 227 eqbrtrd 
 |-  ( ( n e. NN0 /\ y e. C ) -> ( abs ` ( ( x e. C |-> ( cos ` ( n x. x ) ) ) ` y ) ) <_ 1 )
229 214 228 syldan 
 |-  ( ( n e. NN0 /\ y e. dom ( x e. C |-> ( cos ` ( n x. x ) ) ) ) -> ( abs ` ( ( x e. C |-> ( cos ` ( n x. x ) ) ) ` y ) ) <_ 1 )
230 229 ralrimiva 
 |-  ( n e. NN0 -> A. y e. dom ( x e. C |-> ( cos ` ( n x. x ) ) ) ( abs ` ( ( x e. C |-> ( cos ` ( n x. x ) ) ) ` y ) ) <_ 1 )
231 breq2 
 |-  ( b = 1 -> ( ( abs ` ( ( x e. C |-> ( cos ` ( n x. x ) ) ) ` y ) ) <_ b <-> ( abs ` ( ( x e. C |-> ( cos ` ( n x. x ) ) ) ` y ) ) <_ 1 ) )
232 231 ralbidv 
 |-  ( 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 ) )
233 232 rspcev 
 |-  ( ( 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 )
234 204 230 233 sylancr 
 |-  ( 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 234 adantl 
 |-  ( ( 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 )
236 bddmulibl 
 |-  ( ( ( 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 )
237 202 203 235 236 syl3anc 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( x e. C |-> ( cos ` ( n x. x ) ) ) oF x. ( x e. C |-> ( F ` x ) ) ) e. L^1 )
238 187 237 eqeltrd 
 |-  ( ( ph /\ n e. NN0 ) -> ( x e. C |-> ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) ) e. L^1 )
239 57 238 syldan 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( x e. C |-> ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) ) e. L^1 )
240 160 175 239 itgmulc2 
 |-  ( ( 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 )
241 160 adantr 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> ( cos ` ( n x. X ) ) e. CC )
242 121 adantlr 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> ( F ` x ) e. CC )
243 56 183 sylanl2 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> ( cos ` ( n x. x ) ) e. CC )
244 241 242 243 mul12d 
 |-  ( ( ( 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 ) ) ) ) )
245 241 243 mulcomd 
 |-  ( ( ( 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 ) ) ) )
246 245 oveq2d 
 |-  ( ( ( 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 ) ) ) ) )
247 244 246 eqtrd 
 |-  ( ( ( 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 ) ) ) ) )
248 247 itgeq2dv 
 |-  ( ( 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 )
249 240 248 eqtrd 
 |-  ( ( 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 )
250 249 oveq1d 
 |-  ( ( 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 ) )
251 166 250 eqtr3d 
 |-  ( ( 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 ) )
252 158 161 251 3eqtrd 
 |-  ( ( 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 ) )
253 84 81 syldan 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( S. C ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) e. RR )
254 5 fvmpt2 
 |-  ( ( 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 ) )
255 84 253 254 syl2anc 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( B ` n ) = ( S. C ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) )
256 255 oveq1d 
 |-  ( ( 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 ) ) ) )
257 253 recnd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( S. C ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) e. CC )
258 86 recnd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( sin ` ( n x. X ) ) e. CC )
259 257 258 mulcomd 
 |-  ( ( 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 ) ) )
260 84 78 syldan 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> S. C ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x e. RR )
261 260 recnd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> S. C ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x e. CC )
262 258 261 164 165 divassd 
 |-  ( ( 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 ) ) )
263 120 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. C ) -> ( F ` x ) e. RR )
264 nnre 
 |-  ( n e. NN -> n e. RR )
265 264 adantr 
 |-  ( ( n e. NN /\ x e. C ) -> n e. RR )
266 118 adantl 
 |-  ( ( n e. NN /\ x e. C ) -> x e. RR )
267 265 266 remulcld 
 |-  ( ( n e. NN /\ x e. C ) -> ( n x. x ) e. RR )
268 267 resincld 
 |-  ( ( n e. NN /\ x e. C ) -> ( sin ` ( n x. x ) ) e. RR )
269 268 adantll 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. C ) -> ( sin ` ( n x. x ) ) e. RR )
270 263 269 remulcld 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. C ) -> ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) e. RR )
271 55 270 sylanl2 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) e. RR )
272 178 a1i 
 |-  ( ( ph /\ n e. NN ) -> C e. _V )
273 eqidd 
 |-  ( ( ph /\ n e. NN ) -> ( x e. C |-> ( sin ` ( n x. x ) ) ) = ( x e. C |-> ( sin ` ( n x. x ) ) ) )
274 eqidd 
 |-  ( ( ph /\ n e. NN ) -> ( x e. C |-> ( F ` x ) ) = ( x e. C |-> ( F ` x ) ) )
275 272 269 263 273 274 offval2 
 |-  ( ( 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 ) ) ) )
276 269 recnd 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. C ) -> ( sin ` ( n x. x ) ) e. CC )
277 121 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. C ) -> ( F ` x ) e. CC )
278 276 277 mulcomd 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. C ) -> ( ( sin ` ( n x. x ) ) x. ( F ` x ) ) = ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) )
279 278 mpteq2dva 
 |-  ( ( ph /\ n e. NN ) -> ( x e. C |-> ( ( sin ` ( n x. x ) ) x. ( F ` x ) ) ) = ( x e. C |-> ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) ) )
280 275 279 eqtr2d 
 |-  ( ( 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 ) ) ) )
281 sincn 
 |-  sin e. ( CC -cn-> CC )
282 281 a1i 
 |-  ( ( ph /\ n e. NN ) -> sin e. ( CC -cn-> CC ) )
283 191 a1i 
 |-  ( n e. NN -> C C_ CC )
284 264 recnd 
 |-  ( n e. NN -> n e. CC )
285 195 a1i 
 |-  ( n e. NN -> CC C_ CC )
286 283 284 285 constcncfg 
 |-  ( n e. NN -> ( x e. C |-> n ) e. ( C -cn-> CC ) )
287 283 285 idcncfg 
 |-  ( n e. NN -> ( x e. C |-> x ) e. ( C -cn-> CC ) )
288 286 287 mulcncf 
 |-  ( n e. NN -> ( x e. C |-> ( n x. x ) ) e. ( C -cn-> CC ) )
289 288 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( x e. C |-> ( n x. x ) ) e. ( C -cn-> CC ) )
290 282 289 cncfmpt1f 
 |-  ( ( ph /\ n e. NN ) -> ( x e. C |-> ( sin ` ( n x. x ) ) ) e. ( C -cn-> CC ) )
291 cnmbf 
 |-  ( ( C e. dom vol /\ ( x e. C |-> ( sin ` ( n x. x ) ) ) e. ( C -cn-> CC ) ) -> ( x e. C |-> ( sin ` ( n x. x ) ) ) e. MblFn )
292 177 290 291 sylancr 
 |-  ( ( ph /\ n e. NN ) -> ( x e. C |-> ( sin ` ( n x. x ) ) ) e. MblFn )
293 141 adantr 
 |-  ( ( ph /\ n e. NN ) -> ( x e. C |-> ( F ` x ) ) e. L^1 )
294 simpr 
 |-  ( ( n e. NN /\ y e. dom ( x e. C |-> ( sin ` ( n x. x ) ) ) ) -> y e. dom ( x e. C |-> ( sin ` ( n x. x ) ) ) )
295 268 ralrimiva 
 |-  ( n e. NN -> A. x e. C ( sin ` ( n x. x ) ) e. RR )
296 dmmptg 
 |-  ( A. x e. C ( sin ` ( n x. x ) ) e. RR -> dom ( x e. C |-> ( sin ` ( n x. x ) ) ) = C )
297 295 296 syl 
 |-  ( n e. NN -> dom ( x e. C |-> ( sin ` ( n x. x ) ) ) = C )
298 297 adantr 
 |-  ( ( n e. NN /\ y e. dom ( x e. C |-> ( sin ` ( n x. x ) ) ) ) -> dom ( x e. C |-> ( sin ` ( n x. x ) ) ) = C )
299 294 298 eleqtrd 
 |-  ( ( n e. NN /\ y e. dom ( x e. C |-> ( sin ` ( n x. x ) ) ) ) -> y e. C )
300 eqidd 
 |-  ( ( n e. NN /\ y e. C ) -> ( x e. C |-> ( sin ` ( n x. x ) ) ) = ( x e. C |-> ( sin ` ( n x. x ) ) ) )
301 216 fveq2d 
 |-  ( x = y -> ( sin ` ( n x. x ) ) = ( sin ` ( n x. y ) ) )
302 301 adantl 
 |-  ( ( ( n e. NN /\ y e. C ) /\ x = y ) -> ( sin ` ( n x. x ) ) = ( sin ` ( n x. y ) ) )
303 simpr 
 |-  ( ( n e. NN /\ y e. C ) -> y e. C )
304 264 adantr 
 |-  ( ( n e. NN /\ y e. C ) -> n e. RR )
305 137 303 sselid 
 |-  ( ( n e. NN /\ y e. C ) -> y e. RR )
306 304 305 remulcld 
 |-  ( ( n e. NN /\ y e. C ) -> ( n x. y ) e. RR )
307 306 resincld 
 |-  ( ( n e. NN /\ y e. C ) -> ( sin ` ( n x. y ) ) e. RR )
308 300 302 303 307 fvmptd 
 |-  ( ( n e. NN /\ y e. C ) -> ( ( x e. C |-> ( sin ` ( n x. x ) ) ) ` y ) = ( sin ` ( n x. y ) ) )
309 308 fveq2d 
 |-  ( ( n e. NN /\ y e. C ) -> ( abs ` ( ( x e. C |-> ( sin ` ( n x. x ) ) ) ` y ) ) = ( abs ` ( sin ` ( n x. y ) ) ) )
310 abssinbd 
 |-  ( ( n x. y ) e. RR -> ( abs ` ( sin ` ( n x. y ) ) ) <_ 1 )
311 306 310 syl 
 |-  ( ( n e. NN /\ y e. C ) -> ( abs ` ( sin ` ( n x. y ) ) ) <_ 1 )
312 309 311 eqbrtrd 
 |-  ( ( n e. NN /\ y e. C ) -> ( abs ` ( ( x e. C |-> ( sin ` ( n x. x ) ) ) ` y ) ) <_ 1 )
313 299 312 syldan 
 |-  ( ( n e. NN /\ y e. dom ( x e. C |-> ( sin ` ( n x. x ) ) ) ) -> ( abs ` ( ( x e. C |-> ( sin ` ( n x. x ) ) ) ` y ) ) <_ 1 )
314 313 ralrimiva 
 |-  ( n e. NN -> A. y e. dom ( x e. C |-> ( sin ` ( n x. x ) ) ) ( abs ` ( ( x e. C |-> ( sin ` ( n x. x ) ) ) ` y ) ) <_ 1 )
315 breq2 
 |-  ( b = 1 -> ( ( abs ` ( ( x e. C |-> ( sin ` ( n x. x ) ) ) ` y ) ) <_ b <-> ( abs ` ( ( x e. C |-> ( sin ` ( n x. x ) ) ) ` y ) ) <_ 1 ) )
316 315 ralbidv 
 |-  ( 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 ) )
317 316 rspcev 
 |-  ( ( 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 )
318 204 314 317 sylancr 
 |-  ( 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 318 adantl 
 |-  ( ( 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 )
320 bddmulibl 
 |-  ( ( ( 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 )
321 292 293 319 320 syl3anc 
 |-  ( ( ph /\ n e. NN ) -> ( ( x e. C |-> ( sin ` ( n x. x ) ) ) oF x. ( x e. C |-> ( F ` x ) ) ) e. L^1 )
322 280 321 eqeltrd 
 |-  ( ( ph /\ n e. NN ) -> ( x e. C |-> ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) ) e. L^1 )
323 84 322 syldan 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( x e. C |-> ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) ) e. L^1 )
324 258 271 323 itgmulc2 
 |-  ( ( 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 )
325 258 adantr 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> ( sin ` ( n x. X ) ) e. CC )
326 55 276 sylanl2 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> ( sin ` ( n x. x ) ) e. CC )
327 325 242 326 mul12d 
 |-  ( ( ( 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 ) ) ) ) )
328 325 326 mulcomd 
 |-  ( ( ( 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 ) ) ) )
329 328 oveq2d 
 |-  ( ( ( 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 ) ) ) ) )
330 327 329 eqtrd 
 |-  ( ( ( 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 ) ) ) ) )
331 330 itgeq2dv 
 |-  ( ( 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 )
332 324 331 eqtrd 
 |-  ( ( 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 )
333 332 oveq1d 
 |-  ( ( 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 ) )
334 262 333 eqtr3d 
 |-  ( ( 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 ) )
335 256 259 334 3eqtrd 
 |-  ( ( 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 ) )
336 252 335 oveq12d 
 |-  ( ( 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 ) ) )
337 56 169 sylanl2 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> ( F ` x ) e. RR )
338 57 209 sylan 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> ( cos ` ( n x. x ) ) e. RR )
339 62 adantr 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> ( cos ` ( n x. X ) ) e. RR )
340 338 339 remulcld 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> ( ( cos ` ( n x. x ) ) x. ( cos ` ( n x. X ) ) ) e. RR )
341 337 340 remulcld 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> ( ( F ` x ) x. ( ( cos ` ( n x. x ) ) x. ( cos ` ( n x. X ) ) ) ) e. RR )
342 242 243 241 mul13d 
 |-  ( ( ( 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 ) ) ) )
343 243 242 mulcomd 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> ( ( cos ` ( n x. x ) ) x. ( F ` x ) ) = ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) )
344 343 oveq2d 
 |-  ( ( ( 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 ) ) ) ) )
345 342 344 eqtrd 
 |-  ( ( ( 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 ) ) ) ) )
346 345 mpteq2dva 
 |-  ( ( 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 ) ) ) ) ) )
347 160 175 239 iblmulc2 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( x e. C |-> ( ( cos ` ( n x. X ) ) x. ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) ) ) e. L^1 )
348 346 347 eqeltrd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( x e. C |-> ( ( F ` x ) x. ( ( cos ` ( n x. x ) ) x. ( cos ` ( n x. X ) ) ) ) ) e. L^1 )
349 341 348 itgcl 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> S. C ( ( F ` x ) x. ( ( cos ` ( n x. x ) ) x. ( cos ` ( n x. X ) ) ) ) _d x e. CC )
350 84 268 sylan 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> ( sin ` ( n x. x ) ) e. RR )
351 86 adantr 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> ( sin ` ( n x. X ) ) e. RR )
352 350 351 remulcld 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> ( ( sin ` ( n x. x ) ) x. ( sin ` ( n x. X ) ) ) e. RR )
353 337 352 remulcld 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> ( ( F ` x ) x. ( ( sin ` ( n x. x ) ) x. ( sin ` ( n x. X ) ) ) ) e. RR )
354 242 326 325 mul13d 
 |-  ( ( ( 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 ) ) ) )
355 326 242 mulcomd 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> ( ( sin ` ( n x. x ) ) x. ( F ` x ) ) = ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) )
356 355 oveq2d 
 |-  ( ( ( 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 ) ) ) ) )
357 354 356 eqtrd 
 |-  ( ( ( 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 ) ) ) ) )
358 357 mpteq2dva 
 |-  ( ( 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 ) ) ) ) ) )
359 258 271 323 iblmulc2 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( x e. C |-> ( ( sin ` ( n x. X ) ) x. ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) ) ) e. L^1 )
360 358 359 eqeltrd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( x e. C |-> ( ( F ` x ) x. ( ( sin ` ( n x. x ) ) x. ( sin ` ( n x. X ) ) ) ) ) e. L^1 )
361 353 360 itgcl 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> S. C ( ( F ` x ) x. ( ( sin ` ( n x. x ) ) x. ( sin ` ( n x. X ) ) ) ) _d x e. CC )
362 349 361 164 165 divdird 
 |-  ( ( 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 ) ) )
363 55 nncnd 
 |-  ( n e. ( 1 ... N ) -> n e. CC )
364 363 ad2antlr 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> n e. CC )
365 109 adantl 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> x e. CC )
366 6 recnd 
 |-  ( ph -> X e. CC )
367 366 ad2antrr 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> X e. CC )
368 364 365 367 subdid 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> ( n x. ( x - X ) ) = ( ( n x. x ) - ( n x. X ) ) )
369 368 fveq2d 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> ( cos ` ( n x. ( x - X ) ) ) = ( cos ` ( ( n x. x ) - ( n x. X ) ) ) )
370 364 365 mulcld 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> ( n x. x ) e. CC )
371 364 367 mulcld 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> ( n x. X ) e. CC )
372 cossub 
 |-  ( ( ( 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 ) ) ) ) )
373 370 371 372 syl2anc 
 |-  ( ( ( 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 ) ) ) ) )
374 369 373 eqtrd 
 |-  ( ( ( 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 ) ) ) ) )
375 374 oveq2d 
 |-  ( ( ( 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 ) ) ) ) ) )
376 340 recnd 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> ( ( cos ` ( n x. x ) ) x. ( cos ` ( n x. X ) ) ) e. CC )
377 352 recnd 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> ( ( sin ` ( n x. x ) ) x. ( sin ` ( n x. X ) ) ) e. CC )
378 242 376 377 adddid 
 |-  ( ( ( 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 ) ) ) ) ) )
379 375 378 eqtrd 
 |-  ( ( ( 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 ) ) ) ) ) )
380 379 itgeq2dv 
 |-  ( ( 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 )
381 341 348 353 360 itgadd 
 |-  ( ( 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 ) )
382 380 381 eqtr2d 
 |-  ( ( 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 )
383 382 oveq1d 
 |-  ( ( 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 ) )
384 336 362 383 3eqtr2d 
 |-  ( ( 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 ) )
385 384 sumeq2dv 
 |-  ( 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 ) )
386 59 adantr 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> n e. RR )
387 118 adantl 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> x e. RR )
388 6 ad2antrr 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> X e. RR )
389 387 388 resubcld 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> ( x - X ) e. RR )
390 386 389 remulcld 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> ( n x. ( x - X ) ) e. RR )
391 390 recoscld 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> ( cos ` ( n x. ( x - X ) ) ) e. RR )
392 337 391 remulcld 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) e. RR )
393 178 a1i 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> C e. _V )
394 eqidd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) = ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) )
395 eqidd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( x e. C |-> ( F ` x ) ) = ( x e. C |-> ( F ` x ) ) )
396 393 391 337 394 395 offval2 
 |-  ( ( 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 ) ) ) )
397 391 recnd 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> ( cos ` ( n x. ( x - X ) ) ) e. CC )
398 397 242 mulcomd 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) -> ( ( cos ` ( n x. ( x - X ) ) ) x. ( F ` x ) ) = ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) )
399 398 mpteq2dva 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( x e. C |-> ( ( cos ` ( n x. ( x - X ) ) ) x. ( F ` x ) ) ) = ( x e. C |-> ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) ) )
400 396 399 eqtr2d 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( x e. C |-> ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) ) = ( ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) oF x. ( x e. C |-> ( F ` x ) ) ) )
401 188 a1i 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> cos e. ( CC -cn-> CC ) )
402 84 286 syl 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( x e. C |-> n ) e. ( C -cn-> CC ) )
403 84 287 syl 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( x e. C |-> x ) e. ( C -cn-> CC ) )
404 191 a1i 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> C C_ CC )
405 366 adantr 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> X e. CC )
406 195 a1i 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> CC C_ CC )
407 404 405 406 constcncfg 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( x e. C |-> X ) e. ( C -cn-> CC ) )
408 403 407 subcncf 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( x e. C |-> ( x - X ) ) e. ( C -cn-> CC ) )
409 402 408 mulcncf 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( x e. C |-> ( n x. ( x - X ) ) ) e. ( C -cn-> CC ) )
410 401 409 cncfmpt1f 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) e. ( C -cn-> CC ) )
411 cnmbf 
 |-  ( ( C e. dom vol /\ ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) e. ( C -cn-> CC ) ) -> ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) e. MblFn )
412 177 410 411 sylancr 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) e. MblFn )
413 141 adantr 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( x e. C |-> ( F ` x ) ) e. L^1 )
414 simpr 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ y e. dom ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) ) -> y e. dom ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) )
415 391 ralrimiva 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> A. x e. C ( cos ` ( n x. ( x - X ) ) ) e. RR )
416 dmmptg 
 |-  ( A. x e. C ( cos ` ( n x. ( x - X ) ) ) e. RR -> dom ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) = C )
417 415 416 syl 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> dom ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) = C )
418 417 adantr 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ y e. dom ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) ) -> dom ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) = C )
419 414 418 eleqtrd 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ y e. dom ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) ) -> y e. C )
420 eqidd 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ y e. C ) -> ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) = ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) )
421 oveq1 
 |-  ( x = y -> ( x - X ) = ( y - X ) )
422 421 oveq2d 
 |-  ( x = y -> ( n x. ( x - X ) ) = ( n x. ( y - X ) ) )
423 422 fveq2d 
 |-  ( x = y -> ( cos ` ( n x. ( x - X ) ) ) = ( cos ` ( n x. ( y - X ) ) ) )
424 423 adantl 
 |-  ( ( ( ( ph /\ n e. ( 1 ... N ) ) /\ y e. C ) /\ x = y ) -> ( cos ` ( n x. ( x - X ) ) ) = ( cos ` ( n x. ( y - X ) ) ) )
425 simpr 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ y e. C ) -> y e. C )
426 59 adantr 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ y e. C ) -> n e. RR )
427 57 221 sylan 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ y e. C ) -> y e. RR )
428 6 ad2antrr 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ y e. C ) -> X e. RR )
429 427 428 resubcld 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ y e. C ) -> ( y - X ) e. RR )
430 426 429 remulcld 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ y e. C ) -> ( n x. ( y - X ) ) e. RR )
431 430 recoscld 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ y e. C ) -> ( cos ` ( n x. ( y - X ) ) ) e. RR )
432 420 424 425 431 fvmptd 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ y e. C ) -> ( ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) ` y ) = ( cos ` ( n x. ( y - X ) ) ) )
433 432 fveq2d 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ y e. C ) -> ( abs ` ( ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) ` y ) ) = ( abs ` ( cos ` ( n x. ( y - X ) ) ) ) )
434 abscosbd 
 |-  ( ( n x. ( y - X ) ) e. RR -> ( abs ` ( cos ` ( n x. ( y - X ) ) ) ) <_ 1 )
435 430 434 syl 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ y e. C ) -> ( abs ` ( cos ` ( n x. ( y - X ) ) ) ) <_ 1 )
436 433 435 eqbrtrd 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ y e. C ) -> ( abs ` ( ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) ` y ) ) <_ 1 )
437 419 436 syldan 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ y e. dom ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) ) -> ( abs ` ( ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) ` y ) ) <_ 1 )
438 437 ralrimiva 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> A. y e. dom ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) ( abs ` ( ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) ` y ) ) <_ 1 )
439 breq2 
 |-  ( b = 1 -> ( ( abs ` ( ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) ` y ) ) <_ b <-> ( abs ` ( ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) ` y ) ) <_ 1 ) )
440 439 ralbidv 
 |-  ( b = 1 -> ( A. y e. dom ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) ( abs ` ( ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) ` y ) ) <_ b <-> A. y e. dom ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) ( abs ` ( ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) ` y ) ) <_ 1 ) )
441 440 rspcev 
 |-  ( ( 1 e. RR /\ A. y e. dom ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) ( abs ` ( ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) ` y ) ) <_ 1 ) -> E. b e. RR A. y e. dom ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) ( abs ` ( ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) ` y ) ) <_ b )
442 204 438 441 sylancr 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> E. b e. RR A. y e. dom ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) ( abs ` ( ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) ` y ) ) <_ b )
443 bddmulibl 
 |-  ( ( ( x e. C |-> ( cos ` ( n x. ( 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 - X ) ) ) ) ( abs ` ( ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) ` y ) ) <_ b ) -> ( ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) oF x. ( x e. C |-> ( F ` x ) ) ) e. L^1 )
444 412 413 442 443 syl3anc 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( x e. C |-> ( cos ` ( n x. ( x - X ) ) ) ) oF x. ( x e. C |-> ( F ` x ) ) ) e. L^1 )
445 400 444 eqeltrd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( x e. C |-> ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) ) e. L^1 )
446 392 445 itgcl 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> S. C ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) _d x e. CC )
447 30 143 446 103 fsumdivc 
 |-  ( ph -> ( sum_ n e. ( 1 ... N ) S. C ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) _d x / _pi ) = sum_ n e. ( 1 ... N ) ( S. C ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) _d x / _pi ) )
448 177 a1i 
 |-  ( ph -> C e. dom vol )
449 anass 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) <-> ( ph /\ ( n e. ( 1 ... N ) /\ x e. C ) ) )
450 ancom 
 |-  ( ( n e. ( 1 ... N ) /\ x e. C ) <-> ( x e. C /\ n e. ( 1 ... N ) ) )
451 450 anbi2i 
 |-  ( ( ph /\ ( n e. ( 1 ... N ) /\ x e. C ) ) <-> ( ph /\ ( x e. C /\ n e. ( 1 ... N ) ) ) )
452 449 451 bitri 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ x e. C ) <-> ( ph /\ ( x e. C /\ n e. ( 1 ... N ) ) ) )
453 452 392 sylbir 
 |-  ( ( ph /\ ( x e. C /\ n e. ( 1 ... N ) ) ) -> ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) e. RR )
454 448 30 453 445 itgfsum 
 |-  ( ph -> ( ( x e. C |-> sum_ n e. ( 1 ... N ) ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) ) e. L^1 /\ S. C sum_ n e. ( 1 ... N ) ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) _d x = sum_ n e. ( 1 ... N ) S. C ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) _d x ) )
455 454 simprd 
 |-  ( ph -> S. C sum_ n e. ( 1 ... N ) ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) _d x = sum_ n e. ( 1 ... N ) S. C ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) _d x )
456 455 eqcomd 
 |-  ( ph -> sum_ n e. ( 1 ... N ) S. C ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) _d x = S. C sum_ n e. ( 1 ... N ) ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) _d x )
457 456 oveq1d 
 |-  ( ph -> ( sum_ n e. ( 1 ... N ) S. C ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) _d x / _pi ) = ( S. C sum_ n e. ( 1 ... N ) ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) _d x / _pi ) )
458 385 447 457 3eqtr2d 
 |-  ( ph -> sum_ n e. ( 1 ... N ) ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) = ( S. C sum_ n e. ( 1 ... N ) ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) _d x / _pi ) )
459 154 458 oveq12d 
 |-  ( ph -> ( ( ( A ` 0 ) / 2 ) + sum_ n e. ( 1 ... N ) ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( ( S. C ( ( 1 / 2 ) x. ( F ` x ) ) _d x / _pi ) + ( S. C sum_ n e. ( 1 ... N ) ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) _d x / _pi ) ) )
460 9 adantr 
 |-  ( ( ph /\ x e. C ) -> N e. NN )
461 eqid 
 |-  ( D ` N ) = ( D ` N )
462 eqid 
 |-  ( s e. RR |-> ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. s ) ) ) / _pi ) ) = ( s e. RR |-> ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. s ) ) ) / _pi ) )
463 8 460 461 462 dirkertrigeq 
 |-  ( ( ph /\ x e. C ) -> ( D ` N ) = ( s e. RR |-> ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. s ) ) ) / _pi ) ) )
464 oveq2 
 |-  ( s = ( x - X ) -> ( n x. s ) = ( n x. ( x - X ) ) )
465 464 fveq2d 
 |-  ( s = ( x - X ) -> ( cos ` ( n x. s ) ) = ( cos ` ( n x. ( x - X ) ) ) )
466 465 sumeq2sdv 
 |-  ( s = ( x - X ) -> sum_ n e. ( 1 ... N ) ( cos ` ( n x. s ) ) = sum_ n e. ( 1 ... N ) ( cos ` ( n x. ( x - X ) ) ) )
467 466 oveq2d 
 |-  ( s = ( x - X ) -> ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. s ) ) ) = ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. ( x - X ) ) ) ) )
468 467 oveq1d 
 |-  ( s = ( x - X ) -> ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. s ) ) ) / _pi ) = ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. ( x - X ) ) ) ) / _pi ) )
469 468 adantl 
 |-  ( ( ( ph /\ x e. C ) /\ s = ( x - X ) ) -> ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. s ) ) ) / _pi ) = ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. ( x - X ) ) ) ) / _pi ) )
470 6 adantr 
 |-  ( ( ph /\ x e. C ) -> X e. RR )
471 119 470 resubcld 
 |-  ( ( ph /\ x e. C ) -> ( x - X ) e. RR )
472 halfre 
 |-  ( 1 / 2 ) e. RR
473 472 a1i 
 |-  ( ( ph /\ x e. C ) -> ( 1 / 2 ) e. RR )
474 fzfid 
 |-  ( ( ph /\ x e. C ) -> ( 1 ... N ) e. Fin )
475 391 an32s 
 |-  ( ( ( ph /\ x e. C ) /\ n e. ( 1 ... N ) ) -> ( cos ` ( n x. ( x - X ) ) ) e. RR )
476 474 475 fsumrecl 
 |-  ( ( ph /\ x e. C ) -> sum_ n e. ( 1 ... N ) ( cos ` ( n x. ( x - X ) ) ) e. RR )
477 473 476 readdcld 
 |-  ( ( ph /\ x e. C ) -> ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. ( x - X ) ) ) ) e. RR )
478 46 a1i 
 |-  ( ( ph /\ x e. C ) -> _pi e. RR )
479 50 a1i 
 |-  ( ( ph /\ x e. C ) -> _pi =/= 0 )
480 477 478 479 redivcld 
 |-  ( ( ph /\ x e. C ) -> ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. ( x - X ) ) ) ) / _pi ) e. RR )
481 463 469 471 480 fvmptd 
 |-  ( ( ph /\ x e. C ) -> ( ( D ` N ) ` ( x - X ) ) = ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. ( x - X ) ) ) ) / _pi ) )
482 481 480 eqeltrd 
 |-  ( ( ph /\ x e. C ) -> ( ( D ` N ) ` ( x - X ) ) e. RR )
483 120 482 remulcld 
 |-  ( ( ph /\ x e. C ) -> ( ( F ` x ) x. ( ( D ` N ) ` ( x - X ) ) ) e. RR )
484 178 a1i 
 |-  ( ph -> C e. _V )
485 eqidd 
 |-  ( ph -> ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) = ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) )
486 eqidd 
 |-  ( ph -> ( x e. C |-> ( F ` x ) ) = ( x e. C |-> ( F ` x ) ) )
487 484 482 120 485 486 offval2 
 |-  ( ph -> ( ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) oF x. ( x e. C |-> ( F ` x ) ) ) = ( x e. C |-> ( ( ( D ` N ) ` ( x - X ) ) x. ( F ` x ) ) ) )
488 482 recnd 
 |-  ( ( ph /\ x e. C ) -> ( ( D ` N ) ` ( x - X ) ) e. CC )
489 488 121 mulcomd 
 |-  ( ( ph /\ x e. C ) -> ( ( ( D ` N ) ` ( x - X ) ) x. ( F ` x ) ) = ( ( F ` x ) x. ( ( D ` N ) ` ( x - X ) ) ) )
490 489 mpteq2dva 
 |-  ( ph -> ( x e. C |-> ( ( ( D ` N ) ` ( x - X ) ) x. ( F ` x ) ) ) = ( x e. C |-> ( ( F ` x ) x. ( ( D ` N ) ` ( x - X ) ) ) ) )
491 487 490 eqtr2d 
 |-  ( ph -> ( x e. C |-> ( ( F ` x ) x. ( ( D ` N ) ` ( x - X ) ) ) ) = ( ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) oF x. ( x e. C |-> ( F ` x ) ) ) )
492 eqid 
 |-  ( x e. ( -u _pi [,] _pi ) |-> ( ( D ` N ) ` ( x - X ) ) ) = ( x e. ( -u _pi [,] _pi ) |-> ( ( D ` N ) ` ( x - X ) ) )
493 eqid 
 |-  ( x e. RR |-> ( ( D ` N ) ` ( x - X ) ) ) = ( x e. RR |-> ( ( D ` N ) ` ( x - X ) ) )
494 195 a1i 
 |-  ( ph -> CC C_ CC )
495 cncfss 
 |-  ( ( RR C_ CC /\ CC C_ CC ) -> ( RR -cn-> RR ) C_ ( RR -cn-> CC ) )
496 190 494 495 sylancr 
 |-  ( ph -> ( RR -cn-> RR ) C_ ( RR -cn-> CC ) )
497 simpr 
 |-  ( ( ph /\ x e. RR ) -> x e. RR )
498 6 adantr 
 |-  ( ( ph /\ x e. RR ) -> X e. RR )
499 497 498 resubcld 
 |-  ( ( ph /\ x e. RR ) -> ( x - X ) e. RR )
500 eqid 
 |-  ( x e. RR |-> ( x - X ) ) = ( x e. RR |-> ( x - X ) )
501 499 500 fmptd 
 |-  ( ph -> ( x e. RR |-> ( x - X ) ) : RR --> RR )
502 190 a1i 
 |-  ( ph -> RR C_ CC )
503 502 494 idcncfg 
 |-  ( ph -> ( x e. RR |-> x ) e. ( RR -cn-> CC ) )
504 502 366 494 constcncfg 
 |-  ( ph -> ( x e. RR |-> X ) e. ( RR -cn-> CC ) )
505 503 504 subcncf 
 |-  ( ph -> ( x e. RR |-> ( x - X ) ) e. ( RR -cn-> CC ) )
506 cncffvrn 
 |-  ( ( RR C_ CC /\ ( x e. RR |-> ( x - X ) ) e. ( RR -cn-> CC ) ) -> ( ( x e. RR |-> ( x - X ) ) e. ( RR -cn-> RR ) <-> ( x e. RR |-> ( x - X ) ) : RR --> RR ) )
507 190 505 506 sylancr 
 |-  ( ph -> ( ( x e. RR |-> ( x - X ) ) e. ( RR -cn-> RR ) <-> ( x e. RR |-> ( x - X ) ) : RR --> RR ) )
508 501 507 mpbird 
 |-  ( ph -> ( x e. RR |-> ( x - X ) ) e. ( RR -cn-> RR ) )
509 8 dirkercncf 
 |-  ( N e. NN -> ( D ` N ) e. ( RR -cn-> RR ) )
510 9 509 syl 
 |-  ( ph -> ( D ` N ) e. ( RR -cn-> RR ) )
511 508 510 cncfcompt 
 |-  ( ph -> ( x e. RR |-> ( ( D ` N ) ` ( x - X ) ) ) e. ( RR -cn-> RR ) )
512 496 511 sseldd 
 |-  ( ph -> ( x e. RR |-> ( ( D ` N ) ` ( x - X ) ) ) e. ( RR -cn-> CC ) )
513 46 renegcli 
 |-  -u _pi e. RR
514 iccssre 
 |-  ( ( -u _pi e. RR /\ _pi e. RR ) -> ( -u _pi [,] _pi ) C_ RR )
515 513 46 514 mp2an 
 |-  ( -u _pi [,] _pi ) C_ RR
516 515 a1i 
 |-  ( ph -> ( -u _pi [,] _pi ) C_ RR )
517 8 dirkerf 
 |-  ( N e. NN -> ( D ` N ) : RR --> RR )
518 9 517 syl 
 |-  ( ph -> ( D ` N ) : RR --> RR )
519 518 adantr 
 |-  ( ( ph /\ x e. ( -u _pi [,] _pi ) ) -> ( D ` N ) : RR --> RR )
520 516 sselda 
 |-  ( ( ph /\ x e. ( -u _pi [,] _pi ) ) -> x e. RR )
521 6 adantr 
 |-  ( ( ph /\ x e. ( -u _pi [,] _pi ) ) -> X e. RR )
522 520 521 resubcld 
 |-  ( ( ph /\ x e. ( -u _pi [,] _pi ) ) -> ( x - X ) e. RR )
523 519 522 ffvelrnd 
 |-  ( ( ph /\ x e. ( -u _pi [,] _pi ) ) -> ( ( D ` N ) ` ( x - X ) ) e. RR )
524 523 recnd 
 |-  ( ( ph /\ x e. ( -u _pi [,] _pi ) ) -> ( ( D ` N ) ` ( x - X ) ) e. CC )
525 493 512 516 494 524 cncfmptssg 
 |-  ( ph -> ( x e. ( -u _pi [,] _pi ) |-> ( ( D ` N ) ` ( x - X ) ) ) e. ( ( -u _pi [,] _pi ) -cn-> CC ) )
526 133 a1i 
 |-  ( ph -> C C_ ( -u _pi [,] _pi ) )
527 492 525 526 494 488 cncfmptssg 
 |-  ( ph -> ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) e. ( C -cn-> CC ) )
528 cnmbf 
 |-  ( ( C e. dom vol /\ ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) e. ( C -cn-> CC ) ) -> ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) e. MblFn )
529 177 527 528 sylancr 
 |-  ( ph -> ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) e. MblFn )
530 513 a1i 
 |-  ( ph -> -u _pi e. RR )
531 0red 
 |-  ( ph -> 0 e. RR )
532 negpilt0 
 |-  -u _pi < 0
533 532 a1i 
 |-  ( ph -> -u _pi < 0 )
534 49 a1i 
 |-  ( ph -> 0 < _pi )
535 530 531 102 533 534 lttrd 
 |-  ( ph -> -u _pi < _pi )
536 530 102 535 ltled 
 |-  ( ph -> -u _pi <_ _pi )
537 493 512 516 502 523 cncfmptssg 
 |-  ( ph -> ( x e. ( -u _pi [,] _pi ) |-> ( ( D ` N ) ` ( x - X ) ) ) e. ( ( -u _pi [,] _pi ) -cn-> RR ) )
538 530 102 536 537 evthiccabs 
 |-  ( ph -> ( E. c e. ( -u _pi [,] _pi ) A. y e. ( -u _pi [,] _pi ) ( abs ` ( ( x e. ( -u _pi [,] _pi ) |-> ( ( D ` N ) ` ( x - X ) ) ) ` y ) ) <_ ( abs ` ( ( x e. ( -u _pi [,] _pi ) |-> ( ( D ` N ) ` ( x - X ) ) ) ` c ) ) /\ E. z e. ( -u _pi [,] _pi ) A. w e. ( -u _pi [,] _pi ) ( abs ` ( ( x e. ( -u _pi [,] _pi ) |-> ( ( D ` N ) ` ( x - X ) ) ) ` z ) ) <_ ( abs ` ( ( x e. ( -u _pi [,] _pi ) |-> ( ( D ` N ) ` ( x - X ) ) ) ` w ) ) ) )
539 538 simpld 
 |-  ( ph -> E. c e. ( -u _pi [,] _pi ) A. y e. ( -u _pi [,] _pi ) ( abs ` ( ( x e. ( -u _pi [,] _pi ) |-> ( ( D ` N ) ` ( x - X ) ) ) ` y ) ) <_ ( abs ` ( ( x e. ( -u _pi [,] _pi ) |-> ( ( D ` N ) ` ( x - X ) ) ) ` c ) ) )
540 eqidd 
 |-  ( ( ph /\ y e. ( -u _pi [,] _pi ) ) -> ( x e. ( -u _pi [,] _pi ) |-> ( ( D ` N ) ` ( x - X ) ) ) = ( x e. ( -u _pi [,] _pi ) |-> ( ( D ` N ) ` ( x - X ) ) ) )
541 421 fveq2d 
 |-  ( x = y -> ( ( D ` N ) ` ( x - X ) ) = ( ( D ` N ) ` ( y - X ) ) )
542 541 adantl 
 |-  ( ( ( ph /\ y e. ( -u _pi [,] _pi ) ) /\ x = y ) -> ( ( D ` N ) ` ( x - X ) ) = ( ( D ` N ) ` ( y - X ) ) )
543 simpr 
 |-  ( ( ph /\ y e. ( -u _pi [,] _pi ) ) -> y e. ( -u _pi [,] _pi ) )
544 518 adantr 
 |-  ( ( ph /\ y e. ( -u _pi [,] _pi ) ) -> ( D ` N ) : RR --> RR )
545 515 543 sselid 
 |-  ( ( ph /\ y e. ( -u _pi [,] _pi ) ) -> y e. RR )
546 6 adantr 
 |-  ( ( ph /\ y e. ( -u _pi [,] _pi ) ) -> X e. RR )
547 545 546 resubcld 
 |-  ( ( ph /\ y e. ( -u _pi [,] _pi ) ) -> ( y - X ) e. RR )
548 544 547 ffvelrnd 
 |-  ( ( ph /\ y e. ( -u _pi [,] _pi ) ) -> ( ( D ` N ) ` ( y - X ) ) e. RR )
549 540 542 543 548 fvmptd 
 |-  ( ( ph /\ y e. ( -u _pi [,] _pi ) ) -> ( ( x e. ( -u _pi [,] _pi ) |-> ( ( D ` N ) ` ( x - X ) ) ) ` y ) = ( ( D ` N ) ` ( y - X ) ) )
550 549 fveq2d 
 |-  ( ( ph /\ y e. ( -u _pi [,] _pi ) ) -> ( abs ` ( ( x e. ( -u _pi [,] _pi ) |-> ( ( D ` N ) ` ( x - X ) ) ) ` y ) ) = ( abs ` ( ( D ` N ) ` ( y - X ) ) ) )
551 550 adantlr 
 |-  ( ( ( ph /\ c e. ( -u _pi [,] _pi ) ) /\ y e. ( -u _pi [,] _pi ) ) -> ( abs ` ( ( x e. ( -u _pi [,] _pi ) |-> ( ( D ` N ) ` ( x - X ) ) ) ` y ) ) = ( abs ` ( ( D ` N ) ` ( y - X ) ) ) )
552 eqidd 
 |-  ( ( ph /\ c e. ( -u _pi [,] _pi ) ) -> ( x e. ( -u _pi [,] _pi ) |-> ( ( D ` N ) ` ( x - X ) ) ) = ( x e. ( -u _pi [,] _pi ) |-> ( ( D ` N ) ` ( x - X ) ) ) )
553 oveq1 
 |-  ( x = c -> ( x - X ) = ( c - X ) )
554 553 fveq2d 
 |-  ( x = c -> ( ( D ` N ) ` ( x - X ) ) = ( ( D ` N ) ` ( c - X ) ) )
555 554 adantl 
 |-  ( ( ( ph /\ c e. ( -u _pi [,] _pi ) ) /\ x = c ) -> ( ( D ` N ) ` ( x - X ) ) = ( ( D ` N ) ` ( c - X ) ) )
556 simpr 
 |-  ( ( ph /\ c e. ( -u _pi [,] _pi ) ) -> c e. ( -u _pi [,] _pi ) )
557 518 adantr 
 |-  ( ( ph /\ c e. ( -u _pi [,] _pi ) ) -> ( D ` N ) : RR --> RR )
558 515 556 sselid 
 |-  ( ( ph /\ c e. ( -u _pi [,] _pi ) ) -> c e. RR )
559 6 adantr 
 |-  ( ( ph /\ c e. ( -u _pi [,] _pi ) ) -> X e. RR )
560 558 559 resubcld 
 |-  ( ( ph /\ c e. ( -u _pi [,] _pi ) ) -> ( c - X ) e. RR )
561 557 560 ffvelrnd 
 |-  ( ( ph /\ c e. ( -u _pi [,] _pi ) ) -> ( ( D ` N ) ` ( c - X ) ) e. RR )
562 552 555 556 561 fvmptd 
 |-  ( ( ph /\ c e. ( -u _pi [,] _pi ) ) -> ( ( x e. ( -u _pi [,] _pi ) |-> ( ( D ` N ) ` ( x - X ) ) ) ` c ) = ( ( D ` N ) ` ( c - X ) ) )
563 562 fveq2d 
 |-  ( ( ph /\ c e. ( -u _pi [,] _pi ) ) -> ( abs ` ( ( x e. ( -u _pi [,] _pi ) |-> ( ( D ` N ) ` ( x - X ) ) ) ` c ) ) = ( abs ` ( ( D ` N ) ` ( c - X ) ) ) )
564 563 adantr 
 |-  ( ( ( ph /\ c e. ( -u _pi [,] _pi ) ) /\ y e. ( -u _pi [,] _pi ) ) -> ( abs ` ( ( x e. ( -u _pi [,] _pi ) |-> ( ( D ` N ) ` ( x - X ) ) ) ` c ) ) = ( abs ` ( ( D ` N ) ` ( c - X ) ) ) )
565 551 564 breq12d 
 |-  ( ( ( ph /\ c e. ( -u _pi [,] _pi ) ) /\ y e. ( -u _pi [,] _pi ) ) -> ( ( abs ` ( ( x e. ( -u _pi [,] _pi ) |-> ( ( D ` N ) ` ( x - X ) ) ) ` y ) ) <_ ( abs ` ( ( x e. ( -u _pi [,] _pi ) |-> ( ( D ` N ) ` ( x - X ) ) ) ` c ) ) <-> ( abs ` ( ( D ` N ) ` ( y - X ) ) ) <_ ( abs ` ( ( D ` N ) ` ( c - X ) ) ) ) )
566 565 ralbidva 
 |-  ( ( ph /\ c e. ( -u _pi [,] _pi ) ) -> ( A. y e. ( -u _pi [,] _pi ) ( abs ` ( ( x e. ( -u _pi [,] _pi ) |-> ( ( D ` N ) ` ( x - X ) ) ) ` y ) ) <_ ( abs ` ( ( x e. ( -u _pi [,] _pi ) |-> ( ( D ` N ) ` ( x - X ) ) ) ` c ) ) <-> A. y e. ( -u _pi [,] _pi ) ( abs ` ( ( D ` N ) ` ( y - X ) ) ) <_ ( abs ` ( ( D ` N ) ` ( c - X ) ) ) ) )
567 566 rexbidva 
 |-  ( ph -> ( E. c e. ( -u _pi [,] _pi ) A. y e. ( -u _pi [,] _pi ) ( abs ` ( ( x e. ( -u _pi [,] _pi ) |-> ( ( D ` N ) ` ( x - X ) ) ) ` y ) ) <_ ( abs ` ( ( x e. ( -u _pi [,] _pi ) |-> ( ( D ` N ) ` ( x - X ) ) ) ` c ) ) <-> E. c e. ( -u _pi [,] _pi ) A. y e. ( -u _pi [,] _pi ) ( abs ` ( ( D ` N ) ` ( y - X ) ) ) <_ ( abs ` ( ( D ` N ) ` ( c - X ) ) ) ) )
568 539 567 mpbid 
 |-  ( ph -> E. c e. ( -u _pi [,] _pi ) A. y e. ( -u _pi [,] _pi ) ( abs ` ( ( D ` N ) ` ( y - X ) ) ) <_ ( abs ` ( ( D ` N ) ` ( c - X ) ) ) )
569 561 recnd 
 |-  ( ( ph /\ c e. ( -u _pi [,] _pi ) ) -> ( ( D ` N ) ` ( c - X ) ) e. CC )
570 569 abscld 
 |-  ( ( ph /\ c e. ( -u _pi [,] _pi ) ) -> ( abs ` ( ( D ` N ) ` ( c - X ) ) ) e. RR )
571 570 3adant3 
 |-  ( ( ph /\ c e. ( -u _pi [,] _pi ) /\ A. y e. ( -u _pi [,] _pi ) ( abs ` ( ( D ` N ) ` ( y - X ) ) ) <_ ( abs ` ( ( D ` N ) ` ( c - X ) ) ) ) -> ( abs ` ( ( D ` N ) ` ( c - X ) ) ) e. RR )
572 nfv 
 |-  F/ y ph
573 nfv 
 |-  F/ y c e. ( -u _pi [,] _pi )
574 nfra1 
 |-  F/ y A. y e. ( -u _pi [,] _pi ) ( abs ` ( ( D ` N ) ` ( y - X ) ) ) <_ ( abs ` ( ( D ` N ) ` ( c - X ) ) )
575 572 573 574 nf3an 
 |-  F/ y ( ph /\ c e. ( -u _pi [,] _pi ) /\ A. y e. ( -u _pi [,] _pi ) ( abs ` ( ( D ` N ) ` ( y - X ) ) ) <_ ( abs ` ( ( D ` N ) ` ( c - X ) ) ) )
576 simpr 
 |-  ( ( ph /\ y e. dom ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) ) -> y e. dom ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) )
577 482 ralrimiva 
 |-  ( ph -> A. x e. C ( ( D ` N ) ` ( x - X ) ) e. RR )
578 dmmptg 
 |-  ( A. x e. C ( ( D ` N ) ` ( x - X ) ) e. RR -> dom ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) = C )
579 577 578 syl 
 |-  ( ph -> dom ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) = C )
580 579 adantr 
 |-  ( ( ph /\ y e. dom ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) ) -> dom ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) = C )
581 576 580 eleqtrd 
 |-  ( ( ph /\ y e. dom ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) ) -> y e. C )
582 581 3ad2antl1 
 |-  ( ( ( ph /\ c e. ( -u _pi [,] _pi ) /\ A. y e. ( -u _pi [,] _pi ) ( abs ` ( ( D ` N ) ` ( y - X ) ) ) <_ ( abs ` ( ( D ` N ) ` ( c - X ) ) ) ) /\ y e. dom ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) ) -> y e. C )
583 eqidd 
 |-  ( ( ph /\ y e. C ) -> ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) = ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) )
584 541 adantl 
 |-  ( ( ( ph /\ y e. C ) /\ x = y ) -> ( ( D ` N ) ` ( x - X ) ) = ( ( D ` N ) ` ( y - X ) ) )
585 simpr 
 |-  ( ( ph /\ y e. C ) -> y e. C )
586 518 adantr 
 |-  ( ( ph /\ y e. C ) -> ( D ` N ) : RR --> RR )
587 137 585 sselid 
 |-  ( ( ph /\ y e. C ) -> y e. RR )
588 6 adantr 
 |-  ( ( ph /\ y e. C ) -> X e. RR )
589 587 588 resubcld 
 |-  ( ( ph /\ y e. C ) -> ( y - X ) e. RR )
590 586 589 ffvelrnd 
 |-  ( ( ph /\ y e. C ) -> ( ( D ` N ) ` ( y - X ) ) e. RR )
591 583 584 585 590 fvmptd 
 |-  ( ( ph /\ y e. C ) -> ( ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) ` y ) = ( ( D ` N ) ` ( y - X ) ) )
592 591 fveq2d 
 |-  ( ( ph /\ y e. C ) -> ( abs ` ( ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) ` y ) ) = ( abs ` ( ( D ` N ) ` ( y - X ) ) ) )
593 592 adantlr 
 |-  ( ( ( ph /\ A. y e. ( -u _pi [,] _pi ) ( abs ` ( ( D ` N ) ` ( y - X ) ) ) <_ ( abs ` ( ( D ` N ) ` ( c - X ) ) ) ) /\ y e. C ) -> ( abs ` ( ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) ` y ) ) = ( abs ` ( ( D ` N ) ` ( y - X ) ) ) )
594 simplr 
 |-  ( ( ( ph /\ A. y e. ( -u _pi [,] _pi ) ( abs ` ( ( D ` N ) ` ( y - X ) ) ) <_ ( abs ` ( ( D ` N ) ` ( c - X ) ) ) ) /\ y e. C ) -> A. y e. ( -u _pi [,] _pi ) ( abs ` ( ( D ` N ) ` ( y - X ) ) ) <_ ( abs ` ( ( D ` N ) ` ( c - X ) ) ) )
595 133 sseli 
 |-  ( y e. C -> y e. ( -u _pi [,] _pi ) )
596 595 adantl 
 |-  ( ( ( ph /\ A. y e. ( -u _pi [,] _pi ) ( abs ` ( ( D ` N ) ` ( y - X ) ) ) <_ ( abs ` ( ( D ` N ) ` ( c - X ) ) ) ) /\ y e. C ) -> y e. ( -u _pi [,] _pi ) )
597 rspa 
 |-  ( ( A. y e. ( -u _pi [,] _pi ) ( abs ` ( ( D ` N ) ` ( y - X ) ) ) <_ ( abs ` ( ( D ` N ) ` ( c - X ) ) ) /\ y e. ( -u _pi [,] _pi ) ) -> ( abs ` ( ( D ` N ) ` ( y - X ) ) ) <_ ( abs ` ( ( D ` N ) ` ( c - X ) ) ) )
598 594 596 597 syl2anc 
 |-  ( ( ( ph /\ A. y e. ( -u _pi [,] _pi ) ( abs ` ( ( D ` N ) ` ( y - X ) ) ) <_ ( abs ` ( ( D ` N ) ` ( c - X ) ) ) ) /\ y e. C ) -> ( abs ` ( ( D ` N ) ` ( y - X ) ) ) <_ ( abs ` ( ( D ` N ) ` ( c - X ) ) ) )
599 593 598 eqbrtrd 
 |-  ( ( ( ph /\ A. y e. ( -u _pi [,] _pi ) ( abs ` ( ( D ` N ) ` ( y - X ) ) ) <_ ( abs ` ( ( D ` N ) ` ( c - X ) ) ) ) /\ y e. C ) -> ( abs ` ( ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) ` y ) ) <_ ( abs ` ( ( D ` N ) ` ( c - X ) ) ) )
600 599 3adantl2 
 |-  ( ( ( ph /\ c e. ( -u _pi [,] _pi ) /\ A. y e. ( -u _pi [,] _pi ) ( abs ` ( ( D ` N ) ` ( y - X ) ) ) <_ ( abs ` ( ( D ` N ) ` ( c - X ) ) ) ) /\ y e. C ) -> ( abs ` ( ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) ` y ) ) <_ ( abs ` ( ( D ` N ) ` ( c - X ) ) ) )
601 582 600 syldan 
 |-  ( ( ( ph /\ c e. ( -u _pi [,] _pi ) /\ A. y e. ( -u _pi [,] _pi ) ( abs ` ( ( D ` N ) ` ( y - X ) ) ) <_ ( abs ` ( ( D ` N ) ` ( c - X ) ) ) ) /\ y e. dom ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) ) -> ( abs ` ( ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) ` y ) ) <_ ( abs ` ( ( D ` N ) ` ( c - X ) ) ) )
602 601 ex 
 |-  ( ( ph /\ c e. ( -u _pi [,] _pi ) /\ A. y e. ( -u _pi [,] _pi ) ( abs ` ( ( D ` N ) ` ( y - X ) ) ) <_ ( abs ` ( ( D ` N ) ` ( c - X ) ) ) ) -> ( y e. dom ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) -> ( abs ` ( ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) ` y ) ) <_ ( abs ` ( ( D ` N ) ` ( c - X ) ) ) ) )
603 575 602 ralrimi 
 |-  ( ( ph /\ c e. ( -u _pi [,] _pi ) /\ A. y e. ( -u _pi [,] _pi ) ( abs ` ( ( D ` N ) ` ( y - X ) ) ) <_ ( abs ` ( ( D ` N ) ` ( c - X ) ) ) ) -> A. y e. dom ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) ( abs ` ( ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) ` y ) ) <_ ( abs ` ( ( D ` N ) ` ( c - X ) ) ) )
604 breq2 
 |-  ( b = ( abs ` ( ( D ` N ) ` ( c - X ) ) ) -> ( ( abs ` ( ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) ` y ) ) <_ b <-> ( abs ` ( ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) ` y ) ) <_ ( abs ` ( ( D ` N ) ` ( c - X ) ) ) ) )
605 604 ralbidv 
 |-  ( b = ( abs ` ( ( D ` N ) ` ( c - X ) ) ) -> ( A. y e. dom ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) ( abs ` ( ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) ` y ) ) <_ b <-> A. y e. dom ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) ( abs ` ( ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) ` y ) ) <_ ( abs ` ( ( D ` N ) ` ( c - X ) ) ) ) )
606 605 rspcev 
 |-  ( ( ( abs ` ( ( D ` N ) ` ( c - X ) ) ) e. RR /\ A. y e. dom ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) ( abs ` ( ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) ` y ) ) <_ ( abs ` ( ( D ` N ) ` ( c - X ) ) ) ) -> E. b e. RR A. y e. dom ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) ( abs ` ( ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) ` y ) ) <_ b )
607 571 603 606 syl2anc 
 |-  ( ( ph /\ c e. ( -u _pi [,] _pi ) /\ A. y e. ( -u _pi [,] _pi ) ( abs ` ( ( D ` N ) ` ( y - X ) ) ) <_ ( abs ` ( ( D ` N ) ` ( c - X ) ) ) ) -> E. b e. RR A. y e. dom ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) ( abs ` ( ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) ` y ) ) <_ b )
608 607 rexlimdv3a 
 |-  ( ph -> ( E. c e. ( -u _pi [,] _pi ) A. y e. ( -u _pi [,] _pi ) ( abs ` ( ( D ` N ) ` ( y - X ) ) ) <_ ( abs ` ( ( D ` N ) ` ( c - X ) ) ) -> E. b e. RR A. y e. dom ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) ( abs ` ( ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) ` y ) ) <_ b ) )
609 568 608 mpd 
 |-  ( ph -> E. b e. RR A. y e. dom ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) ( abs ` ( ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) ` y ) ) <_ b )
610 bddmulibl 
 |-  ( ( ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) e. MblFn /\ ( x e. C |-> ( F ` x ) ) e. L^1 /\ E. b e. RR A. y e. dom ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) ( abs ` ( ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) ` y ) ) <_ b ) -> ( ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) oF x. ( x e. C |-> ( F ` x ) ) ) e. L^1 )
611 529 141 609 610 syl3anc 
 |-  ( ph -> ( ( x e. C |-> ( ( D ` N ) ` ( x - X ) ) ) oF x. ( x e. C |-> ( F ` x ) ) ) e. L^1 )
612 491 611 eqeltrd 
 |-  ( ph -> ( x e. C |-> ( ( F ` x ) x. ( ( D ` N ) ` ( x - X ) ) ) ) e. L^1 )
613 143 483 612 itgmulc2 
 |-  ( ph -> ( _pi x. S. C ( ( F ` x ) x. ( ( D ` N ) ` ( x - X ) ) ) _d x ) = S. C ( _pi x. ( ( F ` x ) x. ( ( D ` N ) ` ( x - X ) ) ) ) _d x )
614 143 adantr 
 |-  ( ( ph /\ x e. C ) -> _pi e. CC )
615 121 488 614 mul13d 
 |-  ( ( ph /\ x e. C ) -> ( ( F ` x ) x. ( ( ( D ` N ) ` ( x - X ) ) x. _pi ) ) = ( _pi x. ( ( ( D ` N ) ` ( x - X ) ) x. ( F ` x ) ) ) )
616 489 oveq2d 
 |-  ( ( ph /\ x e. C ) -> ( _pi x. ( ( ( D ` N ) ` ( x - X ) ) x. ( F ` x ) ) ) = ( _pi x. ( ( F ` x ) x. ( ( D ` N ) ` ( x - X ) ) ) ) )
617 615 616 eqtrd 
 |-  ( ( ph /\ x e. C ) -> ( ( F ` x ) x. ( ( ( D ` N ) ` ( x - X ) ) x. _pi ) ) = ( _pi x. ( ( F ` x ) x. ( ( D ` N ) ` ( x - X ) ) ) ) )
618 617 itgeq2dv 
 |-  ( ph -> S. C ( ( F ` x ) x. ( ( ( D ` N ) ` ( x - X ) ) x. _pi ) ) _d x = S. C ( _pi x. ( ( F ` x ) x. ( ( D ` N ) ` ( x - X ) ) ) ) _d x )
619 613 618 eqtr4d 
 |-  ( ph -> ( _pi x. S. C ( ( F ` x ) x. ( ( D ` N ) ` ( x - X ) ) ) _d x ) = S. C ( ( F ` x ) x. ( ( ( D ` N ) ` ( x - X ) ) x. _pi ) ) _d x )
620 149 adantr 
 |-  ( ( ph /\ x e. C ) -> ( 1 / 2 ) e. CC )
621 620 121 mulcomd 
 |-  ( ( ph /\ x e. C ) -> ( ( 1 / 2 ) x. ( F ` x ) ) = ( ( F ` x ) x. ( 1 / 2 ) ) )
622 397 an32s 
 |-  ( ( ( ph /\ x e. C ) /\ n e. ( 1 ... N ) ) -> ( cos ` ( n x. ( x - X ) ) ) e. CC )
623 474 121 622 fsummulc2 
 |-  ( ( ph /\ x e. C ) -> ( ( F ` x ) x. sum_ n e. ( 1 ... N ) ( cos ` ( n x. ( x - X ) ) ) ) = sum_ n e. ( 1 ... N ) ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) )
624 623 eqcomd 
 |-  ( ( ph /\ x e. C ) -> sum_ n e. ( 1 ... N ) ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) = ( ( F ` x ) x. sum_ n e. ( 1 ... N ) ( cos ` ( n x. ( x - X ) ) ) ) )
625 621 624 oveq12d 
 |-  ( ( ph /\ x e. C ) -> ( ( ( 1 / 2 ) x. ( F ` x ) ) + sum_ n e. ( 1 ... N ) ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) ) = ( ( ( F ` x ) x. ( 1 / 2 ) ) + ( ( F ` x ) x. sum_ n e. ( 1 ... N ) ( cos ` ( n x. ( x - X ) ) ) ) ) )
626 474 622 fsumcl 
 |-  ( ( ph /\ x e. C ) -> sum_ n e. ( 1 ... N ) ( cos ` ( n x. ( x - X ) ) ) e. CC )
627 121 620 626 adddid 
 |-  ( ( ph /\ x e. C ) -> ( ( F ` x ) x. ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. ( x - X ) ) ) ) ) = ( ( ( F ` x ) x. ( 1 / 2 ) ) + ( ( F ` x ) x. sum_ n e. ( 1 ... N ) ( cos ` ( n x. ( x - X ) ) ) ) ) )
628 481 oveq1d 
 |-  ( ( ph /\ x e. C ) -> ( ( ( D ` N ) ` ( x - X ) ) x. _pi ) = ( ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. ( x - X ) ) ) ) / _pi ) x. _pi ) )
629 620 626 addcld 
 |-  ( ( ph /\ x e. C ) -> ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. ( x - X ) ) ) ) e. CC )
630 629 614 479 divcan1d 
 |-  ( ( ph /\ x e. C ) -> ( ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. ( x - X ) ) ) ) / _pi ) x. _pi ) = ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. ( x - X ) ) ) ) )
631 628 630 eqtr2d 
 |-  ( ( ph /\ x e. C ) -> ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. ( x - X ) ) ) ) = ( ( ( D ` N ) ` ( x - X ) ) x. _pi ) )
632 631 oveq2d 
 |-  ( ( ph /\ x e. C ) -> ( ( F ` x ) x. ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. ( x - X ) ) ) ) ) = ( ( F ` x ) x. ( ( ( D ` N ) ` ( x - X ) ) x. _pi ) ) )
633 625 627 632 3eqtr2rd 
 |-  ( ( ph /\ x e. C ) -> ( ( F ` x ) x. ( ( ( D ` N ) ` ( x - X ) ) x. _pi ) ) = ( ( ( 1 / 2 ) x. ( F ` x ) ) + sum_ n e. ( 1 ... N ) ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) ) )
634 633 itgeq2dv 
 |-  ( ph -> S. C ( ( F ` x ) x. ( ( ( D ` N ) ` ( x - X ) ) x. _pi ) ) _d x = S. C ( ( ( 1 / 2 ) x. ( F ` x ) ) + sum_ n e. ( 1 ... N ) ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) ) _d x )
635 remulcl 
 |-  ( ( ( 1 / 2 ) e. RR /\ ( F ` x ) e. RR ) -> ( ( 1 / 2 ) x. ( F ` x ) ) e. RR )
636 472 120 635 sylancr 
 |-  ( ( ph /\ x e. C ) -> ( ( 1 / 2 ) x. ( F ` x ) ) e. RR )
637 149 120 141 iblmulc2 
 |-  ( ph -> ( x e. C |-> ( ( 1 / 2 ) x. ( F ` x ) ) ) e. L^1 )
638 392 an32s 
 |-  ( ( ( ph /\ x e. C ) /\ n e. ( 1 ... N ) ) -> ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) e. RR )
639 474 638 fsumrecl 
 |-  ( ( ph /\ x e. C ) -> sum_ n e. ( 1 ... N ) ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) e. RR )
640 454 simpld 
 |-  ( ph -> ( x e. C |-> sum_ n e. ( 1 ... N ) ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) ) e. L^1 )
641 636 637 639 640 itgadd 
 |-  ( ph -> S. C ( ( ( 1 / 2 ) x. ( F ` x ) ) + sum_ n e. ( 1 ... N ) ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) ) _d x = ( S. C ( ( 1 / 2 ) x. ( F ` x ) ) _d x + S. C sum_ n e. ( 1 ... N ) ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) _d x ) )
642 619 634 641 3eqtrrd 
 |-  ( ph -> ( S. C ( ( 1 / 2 ) x. ( F ` x ) ) _d x + S. C sum_ n e. ( 1 ... N ) ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) _d x ) = ( _pi x. S. C ( ( F ` x ) x. ( ( D ` N ) ` ( x - X ) ) ) _d x ) )
643 642 oveq1d 
 |-  ( ph -> ( ( S. C ( ( 1 / 2 ) x. ( F ` x ) ) _d x + S. C sum_ n e. ( 1 ... N ) ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) _d x ) / _pi ) = ( ( _pi x. S. C ( ( F ` x ) x. ( ( D ` N ) ` ( x - X ) ) ) _d x ) / _pi ) )
644 636 637 itgcl 
 |-  ( ph -> S. C ( ( 1 / 2 ) x. ( F ` x ) ) _d x e. CC )
645 639 640 itgcl 
 |-  ( ph -> S. C sum_ n e. ( 1 ... N ) ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) _d x e. CC )
646 644 645 143 103 divdird 
 |-  ( ph -> ( ( S. C ( ( 1 / 2 ) x. ( F ` x ) ) _d x + S. C sum_ n e. ( 1 ... N ) ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) _d x ) / _pi ) = ( ( S. C ( ( 1 / 2 ) x. ( F ` x ) ) _d x / _pi ) + ( S. C sum_ n e. ( 1 ... N ) ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) _d x / _pi ) ) )
647 483 612 itgcl 
 |-  ( ph -> S. C ( ( F ` x ) x. ( ( D ` N ) ` ( x - X ) ) ) _d x e. CC )
648 647 143 103 divcan3d 
 |-  ( ph -> ( ( _pi x. S. C ( ( F ` x ) x. ( ( D ` N ) ` ( x - X ) ) ) _d x ) / _pi ) = S. C ( ( F ` x ) x. ( ( D ` N ) ` ( x - X ) ) ) _d x )
649 643 646 648 3eqtr3d 
 |-  ( ph -> ( ( S. C ( ( 1 / 2 ) x. ( F ` x ) ) _d x / _pi ) + ( S. C sum_ n e. ( 1 ... N ) ( ( F ` x ) x. ( cos ` ( n x. ( x - X ) ) ) ) _d x / _pi ) ) = S. C ( ( F ` x ) x. ( ( D ` N ) ` ( x - X ) ) ) _d x )
650 91 459 649 3eqtrd 
 |-  ( ph -> ( S ` N ) = S. C ( ( F ` x ) x. ( ( D ` N ) ` ( x - X ) ) ) _d x )