Metamath Proof Explorer

Theorem dirkertrigeqlem2

Description: Trigonomic equality lemma for the Dirichlet Kernel trigonomic equality. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dirkertrigeqlem2.a 
|- ( ph -> A e. RR )
dirkertrigeqlem2.sinne0 
|- ( ph -> ( sin ` A ) =/= 0 )
dirkertrigeqlem2.n 
|- ( ph -> N e. NN )
Assertion dirkertrigeqlem2 
|- ( ph -> ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) ) / _pi ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / ( ( 2 x. _pi ) x. ( sin ` ( A / 2 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dirkertrigeqlem2.a 
 |-  ( ph -> A e. RR )
2 dirkertrigeqlem2.sinne0 
 |-  ( ph -> ( sin ` A ) =/= 0 )
3 dirkertrigeqlem2.n 
 |-  ( ph -> N e. NN )
4 1cnd 
 |-  ( ph -> 1 e. CC )
5 4 halfcld 
 |-  ( ph -> ( 1 / 2 ) e. CC )
6 fzfid 
 |-  ( ph -> ( 1 ... N ) e. Fin )
7 elfzelz 
 |-  ( n e. ( 1 ... N ) -> n e. ZZ )
8 7 zcnd 
 |-  ( n e. ( 1 ... N ) -> n e. CC )
9 8 adantl 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> n e. CC )
10 1 recnd 
 |-  ( ph -> A e. CC )
11 10 adantr 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> A e. CC )
12 9 11 mulcld 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( n x. A ) e. CC )
13 12 coscld 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( cos ` ( n x. A ) ) e. CC )
14 6 13 fsumcl 
 |-  ( ph -> sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) e. CC )
15 5 14 addcld 
 |-  ( ph -> ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) ) e. CC )
16 10 sincld 
 |-  ( ph -> ( sin ` A ) e. CC )
17 15 16 2 divcan4d 
 |-  ( ph -> ( ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) ) x. ( sin ` A ) ) / ( sin ` A ) ) = ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) ) )
18 17 eqcomd 
 |-  ( ph -> ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) ) = ( ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) ) x. ( sin ` A ) ) / ( sin ` A ) ) )
19 6 16 13 fsummulc1 
 |-  ( ph -> ( sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) x. ( sin ` A ) ) = sum_ n e. ( 1 ... N ) ( ( cos ` ( n x. A ) ) x. ( sin ` A ) ) )
20 16 adantr 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( sin ` A ) e. CC )
21 13 20 mulcomd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( cos ` ( n x. A ) ) x. ( sin ` A ) ) = ( ( sin ` A ) x. ( cos ` ( n x. A ) ) ) )
22 sinmulcos 
 |-  ( ( A e. CC /\ ( n x. A ) e. CC ) -> ( ( sin ` A ) x. ( cos ` ( n x. A ) ) ) = ( ( ( sin ` ( A + ( n x. A ) ) ) + ( sin ` ( A - ( n x. A ) ) ) ) / 2 ) )
23 11 12 22 syl2anc 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( sin ` A ) x. ( cos ` ( n x. A ) ) ) = ( ( ( sin ` ( A + ( n x. A ) ) ) + ( sin ` ( A - ( n x. A ) ) ) ) / 2 ) )
24 1cnd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> 1 e. CC )
25 9 24 11 adddird 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( n + 1 ) x. A ) = ( ( n x. A ) + ( 1 x. A ) ) )
26 24 11 mulcld 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( 1 x. A ) e. CC )
27 12 26 addcomd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( n x. A ) + ( 1 x. A ) ) = ( ( 1 x. A ) + ( n x. A ) ) )
28 10 mulid2d 
 |-  ( ph -> ( 1 x. A ) = A )
29 28 oveq1d 
 |-  ( ph -> ( ( 1 x. A ) + ( n x. A ) ) = ( A + ( n x. A ) ) )
30 29 adantr 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( 1 x. A ) + ( n x. A ) ) = ( A + ( n x. A ) ) )
31 25 27 30 3eqtrrd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( A + ( n x. A ) ) = ( ( n + 1 ) x. A ) )
32 31 fveq2d 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( sin ` ( A + ( n x. A ) ) ) = ( sin ` ( ( n + 1 ) x. A ) ) )
33 12 11 negsubdi2d 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> -u ( ( n x. A ) - A ) = ( A - ( n x. A ) ) )
34 33 eqcomd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( A - ( n x. A ) ) = -u ( ( n x. A ) - A ) )
35 34 fveq2d 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( sin ` ( A - ( n x. A ) ) ) = ( sin ` -u ( ( n x. A ) - A ) ) )
36 12 11 subcld 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( n x. A ) - A ) e. CC )
37 sinneg 
 |-  ( ( ( n x. A ) - A ) e. CC -> ( sin ` -u ( ( n x. A ) - A ) ) = -u ( sin ` ( ( n x. A ) - A ) ) )
38 36 37 syl 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( sin ` -u ( ( n x. A ) - A ) ) = -u ( sin ` ( ( n x. A ) - A ) ) )
39 35 38 eqtrd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( sin ` ( A - ( n x. A ) ) ) = -u ( sin ` ( ( n x. A ) - A ) ) )
40 32 39 oveq12d 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( sin ` ( A + ( n x. A ) ) ) + ( sin ` ( A - ( n x. A ) ) ) ) = ( ( sin ` ( ( n + 1 ) x. A ) ) + -u ( sin ` ( ( n x. A ) - A ) ) ) )
41 11 12 addcld 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( A + ( n x. A ) ) e. CC )
42 41 sincld 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( sin ` ( A + ( n x. A ) ) ) e. CC )
43 32 42 eqeltrrd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( sin ` ( ( n + 1 ) x. A ) ) e. CC )
44 36 sincld 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( sin ` ( ( n x. A ) - A ) ) e. CC )
45 43 44 negsubd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( sin ` ( ( n + 1 ) x. A ) ) + -u ( sin ` ( ( n x. A ) - A ) ) ) = ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( ( n x. A ) - A ) ) ) )
46 9 11 mulsubfacd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( n x. A ) - A ) = ( ( n - 1 ) x. A ) )
47 46 fveq2d 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( sin ` ( ( n x. A ) - A ) ) = ( sin ` ( ( n - 1 ) x. A ) ) )
48 47 oveq2d 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( ( n x. A ) - A ) ) ) = ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) )
49 40 45 48 3eqtrd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( sin ` ( A + ( n x. A ) ) ) + ( sin ` ( A - ( n x. A ) ) ) ) = ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) )
50 49 oveq1d 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( ( sin ` ( A + ( n x. A ) ) ) + ( sin ` ( A - ( n x. A ) ) ) ) / 2 ) = ( ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) / 2 ) )
51 21 23 50 3eqtrd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( cos ` ( n x. A ) ) x. ( sin ` A ) ) = ( ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) / 2 ) )
52 51 sumeq2dv 
 |-  ( ph -> sum_ n e. ( 1 ... N ) ( ( cos ` ( n x. A ) ) x. ( sin ` A ) ) = sum_ n e. ( 1 ... N ) ( ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) / 2 ) )
53 2cnd 
 |-  ( ph -> 2 e. CC )
54 peano2cnm 
 |-  ( n e. CC -> ( n - 1 ) e. CC )
55 9 54 syl 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( n - 1 ) e. CC )
56 55 11 mulcld 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( n - 1 ) x. A ) e. CC )
57 56 sincld 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( sin ` ( ( n - 1 ) x. A ) ) e. CC )
58 43 57 subcld 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) e. CC )
59 2ne0 
 |-  2 =/= 0
60 59 a1i 
 |-  ( ph -> 2 =/= 0 )
61 6 53 58 60 fsumdivc 
 |-  ( ph -> ( sum_ n e. ( 1 ... N ) ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) / 2 ) = sum_ n e. ( 1 ... N ) ( ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) / 2 ) )
62 6 58 fsumcl 
 |-  ( ph -> sum_ n e. ( 1 ... N ) ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) e. CC )
63 62 53 60 divrec2d 
 |-  ( ph -> ( sum_ n e. ( 1 ... N ) ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) / 2 ) = ( ( 1 / 2 ) x. sum_ n e. ( 1 ... N ) ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) ) )
64 61 63 eqtr3d 
 |-  ( ph -> sum_ n e. ( 1 ... N ) ( ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) / 2 ) = ( ( 1 / 2 ) x. sum_ n e. ( 1 ... N ) ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) ) )
65 19 52 64 3eqtrd 
 |-  ( ph -> ( sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) x. ( sin ` A ) ) = ( ( 1 / 2 ) x. sum_ n e. ( 1 ... N ) ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) ) )
66 65 oveq2d 
 |-  ( ph -> ( ( ( 1 / 2 ) x. ( sin ` A ) ) + ( sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) x. ( sin ` A ) ) ) = ( ( ( 1 / 2 ) x. ( sin ` A ) ) + ( ( 1 / 2 ) x. sum_ n e. ( 1 ... N ) ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) ) ) )
67 5 14 16 adddird 
 |-  ( ph -> ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) ) x. ( sin ` A ) ) = ( ( ( 1 / 2 ) x. ( sin ` A ) ) + ( sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) x. ( sin ` A ) ) ) )
68 5 16 62 adddid 
 |-  ( ph -> ( ( 1 / 2 ) x. ( ( sin ` A ) + sum_ n e. ( 1 ... N ) ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) ) ) = ( ( ( 1 / 2 ) x. ( sin ` A ) ) + ( ( 1 / 2 ) x. sum_ n e. ( 1 ... N ) ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) ) ) )
69 66 67 68 3eqtr4d 
 |-  ( ph -> ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) ) x. ( sin ` A ) ) = ( ( 1 / 2 ) x. ( ( sin ` A ) + sum_ n e. ( 1 ... N ) ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) ) ) )
70 69 oveq1d 
 |-  ( ph -> ( ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) ) x. ( sin ` A ) ) / ( sin ` A ) ) = ( ( ( 1 / 2 ) x. ( ( sin ` A ) + sum_ n e. ( 1 ... N ) ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) ) ) / ( sin ` A ) ) )
71 12 sincld 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( sin ` ( n x. A ) ) e. CC )
72 43 71 57 npncand 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( n x. A ) ) ) + ( ( sin ` ( n x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) ) = ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) )
73 72 eqcomd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) = ( ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( n x. A ) ) ) + ( ( sin ` ( n x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) ) )
74 73 sumeq2dv 
 |-  ( ph -> sum_ n e. ( 1 ... N ) ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) = sum_ n e. ( 1 ... N ) ( ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( n x. A ) ) ) + ( ( sin ` ( n x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) ) )
75 43 71 subcld 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( n x. A ) ) ) e. CC )
76 71 57 subcld 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( sin ` ( n x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) e. CC )
77 6 75 76 fsumadd 
 |-  ( ph -> sum_ n e. ( 1 ... N ) ( ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( n x. A ) ) ) + ( ( sin ` ( n x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) ) = ( sum_ n e. ( 1 ... N ) ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( n x. A ) ) ) + sum_ n e. ( 1 ... N ) ( ( sin ` ( n x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) ) )
78 fvoveq1 
 |-  ( j = n -> ( sin ` ( j x. A ) ) = ( sin ` ( n x. A ) ) )
79 fvoveq1 
 |-  ( j = ( n + 1 ) -> ( sin ` ( j x. A ) ) = ( sin ` ( ( n + 1 ) x. A ) ) )
80 fvoveq1 
 |-  ( j = 1 -> ( sin ` ( j x. A ) ) = ( sin ` ( 1 x. A ) ) )
81 fvoveq1 
 |-  ( j = ( N + 1 ) -> ( sin ` ( j x. A ) ) = ( sin ` ( ( N + 1 ) x. A ) ) )
82 3 nnzd 
 |-  ( ph -> N e. ZZ )
83 nnuz 
 |-  NN = ( ZZ>= ` 1 )
84 3 83 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 1 ) )
85 peano2uz 
 |-  ( N e. ( ZZ>= ` 1 ) -> ( N + 1 ) e. ( ZZ>= ` 1 ) )
86 84 85 syl 
 |-  ( ph -> ( N + 1 ) e. ( ZZ>= ` 1 ) )
87 elfzelz 
 |-  ( j e. ( 1 ... ( N + 1 ) ) -> j e. ZZ )
88 87 zcnd 
 |-  ( j e. ( 1 ... ( N + 1 ) ) -> j e. CC )
89 88 adantl 
 |-  ( ( ph /\ j e. ( 1 ... ( N + 1 ) ) ) -> j e. CC )
90 10 adantr 
 |-  ( ( ph /\ j e. ( 1 ... ( N + 1 ) ) ) -> A e. CC )
91 89 90 mulcld 
 |-  ( ( ph /\ j e. ( 1 ... ( N + 1 ) ) ) -> ( j x. A ) e. CC )
92 91 sincld 
 |-  ( ( ph /\ j e. ( 1 ... ( N + 1 ) ) ) -> ( sin ` ( j x. A ) ) e. CC )
93 78 79 80 81 82 86 92 telfsum2 
 |-  ( ph -> sum_ n e. ( 1 ... N ) ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( n x. A ) ) ) = ( ( sin ` ( ( N + 1 ) x. A ) ) - ( sin ` ( 1 x. A ) ) ) )
94 1cnd 
 |-  ( n e. ( 1 ... N ) -> 1 e. CC )
95 8 94 pncand 
 |-  ( n e. ( 1 ... N ) -> ( ( n + 1 ) - 1 ) = n )
96 95 eqcomd 
 |-  ( n e. ( 1 ... N ) -> n = ( ( n + 1 ) - 1 ) )
97 96 adantl 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> n = ( ( n + 1 ) - 1 ) )
98 97 fvoveq1d 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( sin ` ( n x. A ) ) = ( sin ` ( ( ( n + 1 ) - 1 ) x. A ) ) )
99 98 oveq1d 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( sin ` ( n x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) = ( ( sin ` ( ( ( n + 1 ) - 1 ) x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) )
100 99 sumeq2dv 
 |-  ( ph -> sum_ n e. ( 1 ... N ) ( ( sin ` ( n x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) = sum_ n e. ( 1 ... N ) ( ( sin ` ( ( ( n + 1 ) - 1 ) x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) )
101 oveq1 
 |-  ( j = n -> ( j - 1 ) = ( n - 1 ) )
102 101 fvoveq1d 
 |-  ( j = n -> ( sin ` ( ( j - 1 ) x. A ) ) = ( sin ` ( ( n - 1 ) x. A ) ) )
103 oveq1 
 |-  ( j = ( n + 1 ) -> ( j - 1 ) = ( ( n + 1 ) - 1 ) )
104 103 fvoveq1d 
 |-  ( j = ( n + 1 ) -> ( sin ` ( ( j - 1 ) x. A ) ) = ( sin ` ( ( ( n + 1 ) - 1 ) x. A ) ) )
105 oveq1 
 |-  ( j = 1 -> ( j - 1 ) = ( 1 - 1 ) )
106 105 fvoveq1d 
 |-  ( j = 1 -> ( sin ` ( ( j - 1 ) x. A ) ) = ( sin ` ( ( 1 - 1 ) x. A ) ) )
107 oveq1 
 |-  ( j = ( N + 1 ) -> ( j - 1 ) = ( ( N + 1 ) - 1 ) )
108 107 fvoveq1d 
 |-  ( j = ( N + 1 ) -> ( sin ` ( ( j - 1 ) x. A ) ) = ( sin ` ( ( ( N + 1 ) - 1 ) x. A ) ) )
109 1cnd 
 |-  ( ( ph /\ j e. ( 1 ... ( N + 1 ) ) ) -> 1 e. CC )
110 89 109 subcld 
 |-  ( ( ph /\ j e. ( 1 ... ( N + 1 ) ) ) -> ( j - 1 ) e. CC )
111 110 90 mulcld 
 |-  ( ( ph /\ j e. ( 1 ... ( N + 1 ) ) ) -> ( ( j - 1 ) x. A ) e. CC )
112 111 sincld 
 |-  ( ( ph /\ j e. ( 1 ... ( N + 1 ) ) ) -> ( sin ` ( ( j - 1 ) x. A ) ) e. CC )
113 102 104 106 108 82 86 112 telfsum2 
 |-  ( ph -> sum_ n e. ( 1 ... N ) ( ( sin ` ( ( ( n + 1 ) - 1 ) x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) = ( ( sin ` ( ( ( N + 1 ) - 1 ) x. A ) ) - ( sin ` ( ( 1 - 1 ) x. A ) ) ) )
114 3 nnred 
 |-  ( ph -> N e. RR )
115 114 recnd 
 |-  ( ph -> N e. CC )
116 115 4 pncand 
 |-  ( ph -> ( ( N + 1 ) - 1 ) = N )
117 116 fvoveq1d 
 |-  ( ph -> ( sin ` ( ( ( N + 1 ) - 1 ) x. A ) ) = ( sin ` ( N x. A ) ) )
118 4 subidd 
 |-  ( ph -> ( 1 - 1 ) = 0 )
119 118 oveq1d 
 |-  ( ph -> ( ( 1 - 1 ) x. A ) = ( 0 x. A ) )
120 10 mul02d 
 |-  ( ph -> ( 0 x. A ) = 0 )
121 119 120 eqtrd 
 |-  ( ph -> ( ( 1 - 1 ) x. A ) = 0 )
122 121 fveq2d 
 |-  ( ph -> ( sin ` ( ( 1 - 1 ) x. A ) ) = ( sin ` 0 ) )
123 sin0 
 |-  ( sin ` 0 ) = 0
124 123 a1i 
 |-  ( ph -> ( sin ` 0 ) = 0 )
125 122 124 eqtrd 
 |-  ( ph -> ( sin ` ( ( 1 - 1 ) x. A ) ) = 0 )
126 117 125 oveq12d 
 |-  ( ph -> ( ( sin ` ( ( ( N + 1 ) - 1 ) x. A ) ) - ( sin ` ( ( 1 - 1 ) x. A ) ) ) = ( ( sin ` ( N x. A ) ) - 0 ) )
127 100 113 126 3eqtrd 
 |-  ( ph -> sum_ n e. ( 1 ... N ) ( ( sin ` ( n x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) = ( ( sin ` ( N x. A ) ) - 0 ) )
128 93 127 oveq12d 
 |-  ( ph -> ( sum_ n e. ( 1 ... N ) ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( n x. A ) ) ) + sum_ n e. ( 1 ... N ) ( ( sin ` ( n x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) ) = ( ( ( sin ` ( ( N + 1 ) x. A ) ) - ( sin ` ( 1 x. A ) ) ) + ( ( sin ` ( N x. A ) ) - 0 ) ) )
129 74 77 128 3eqtrd 
 |-  ( ph -> sum_ n e. ( 1 ... N ) ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) = ( ( ( sin ` ( ( N + 1 ) x. A ) ) - ( sin ` ( 1 x. A ) ) ) + ( ( sin ` ( N x. A ) ) - 0 ) ) )
130 129 oveq2d 
 |-  ( ph -> ( ( sin ` A ) + sum_ n e. ( 1 ... N ) ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) ) = ( ( sin ` A ) + ( ( ( sin ` ( ( N + 1 ) x. A ) ) - ( sin ` ( 1 x. A ) ) ) + ( ( sin ` ( N x. A ) ) - 0 ) ) ) )
131 28 fveq2d 
 |-  ( ph -> ( sin ` ( 1 x. A ) ) = ( sin ` A ) )
132 131 oveq2d 
 |-  ( ph -> ( ( sin ` ( ( N + 1 ) x. A ) ) - ( sin ` ( 1 x. A ) ) ) = ( ( sin ` ( ( N + 1 ) x. A ) ) - ( sin ` A ) ) )
133 132 oveq1d 
 |-  ( ph -> ( ( ( sin ` ( ( N + 1 ) x. A ) ) - ( sin ` ( 1 x. A ) ) ) + ( ( sin ` ( N x. A ) ) - 0 ) ) = ( ( ( sin ` ( ( N + 1 ) x. A ) ) - ( sin ` A ) ) + ( ( sin ` ( N x. A ) ) - 0 ) ) )
134 133 oveq2d 
 |-  ( ph -> ( ( sin ` A ) + ( ( ( sin ` ( ( N + 1 ) x. A ) ) - ( sin ` ( 1 x. A ) ) ) + ( ( sin ` ( N x. A ) ) - 0 ) ) ) = ( ( sin ` A ) + ( ( ( sin ` ( ( N + 1 ) x. A ) ) - ( sin ` A ) ) + ( ( sin ` ( N x. A ) ) - 0 ) ) ) )
135 115 4 addcld 
 |-  ( ph -> ( N + 1 ) e. CC )
136 135 10 mulcld 
 |-  ( ph -> ( ( N + 1 ) x. A ) e. CC )
137 136 sincld 
 |-  ( ph -> ( sin ` ( ( N + 1 ) x. A ) ) e. CC )
138 137 16 subcld 
 |-  ( ph -> ( ( sin ` ( ( N + 1 ) x. A ) ) - ( sin ` A ) ) e. CC )
139 115 10 mulcld 
 |-  ( ph -> ( N x. A ) e. CC )
140 139 sincld 
 |-  ( ph -> ( sin ` ( N x. A ) ) e. CC )
141 0cnd 
 |-  ( ph -> 0 e. CC )
142 140 141 subcld 
 |-  ( ph -> ( ( sin ` ( N x. A ) ) - 0 ) e. CC )
143 16 138 142 addassd 
 |-  ( ph -> ( ( ( sin ` A ) + ( ( sin ` ( ( N + 1 ) x. A ) ) - ( sin ` A ) ) ) + ( ( sin ` ( N x. A ) ) - 0 ) ) = ( ( sin ` A ) + ( ( ( sin ` ( ( N + 1 ) x. A ) ) - ( sin ` A ) ) + ( ( sin ` ( N x. A ) ) - 0 ) ) ) )
144 143 eqcomd 
 |-  ( ph -> ( ( sin ` A ) + ( ( ( sin ` ( ( N + 1 ) x. A ) ) - ( sin ` A ) ) + ( ( sin ` ( N x. A ) ) - 0 ) ) ) = ( ( ( sin ` A ) + ( ( sin ` ( ( N + 1 ) x. A ) ) - ( sin ` A ) ) ) + ( ( sin ` ( N x. A ) ) - 0 ) ) )
145 16 137 pncan3d 
 |-  ( ph -> ( ( sin ` A ) + ( ( sin ` ( ( N + 1 ) x. A ) ) - ( sin ` A ) ) ) = ( sin ` ( ( N + 1 ) x. A ) ) )
146 140 subid1d 
 |-  ( ph -> ( ( sin ` ( N x. A ) ) - 0 ) = ( sin ` ( N x. A ) ) )
147 145 146 oveq12d 
 |-  ( ph -> ( ( ( sin ` A ) + ( ( sin ` ( ( N + 1 ) x. A ) ) - ( sin ` A ) ) ) + ( ( sin ` ( N x. A ) ) - 0 ) ) = ( ( sin ` ( ( N + 1 ) x. A ) ) + ( sin ` ( N x. A ) ) ) )
148 137 140 addcomd 
 |-  ( ph -> ( ( sin ` ( ( N + 1 ) x. A ) ) + ( sin ` ( N x. A ) ) ) = ( ( sin ` ( N x. A ) ) + ( sin ` ( ( N + 1 ) x. A ) ) ) )
149 147 148 eqtrd 
 |-  ( ph -> ( ( ( sin ` A ) + ( ( sin ` ( ( N + 1 ) x. A ) ) - ( sin ` A ) ) ) + ( ( sin ` ( N x. A ) ) - 0 ) ) = ( ( sin ` ( N x. A ) ) + ( sin ` ( ( N + 1 ) x. A ) ) ) )
150 134 144 149 3eqtrd 
 |-  ( ph -> ( ( sin ` A ) + ( ( ( sin ` ( ( N + 1 ) x. A ) ) - ( sin ` ( 1 x. A ) ) ) + ( ( sin ` ( N x. A ) ) - 0 ) ) ) = ( ( sin ` ( N x. A ) ) + ( sin ` ( ( N + 1 ) x. A ) ) ) )
151 130 150 eqtrd 
 |-  ( ph -> ( ( sin ` A ) + sum_ n e. ( 1 ... N ) ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) ) = ( ( sin ` ( N x. A ) ) + ( sin ` ( ( N + 1 ) x. A ) ) ) )
152 151 oveq2d 
 |-  ( ph -> ( ( 1 / 2 ) x. ( ( sin ` A ) + sum_ n e. ( 1 ... N ) ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) ) ) = ( ( 1 / 2 ) x. ( ( sin ` ( N x. A ) ) + ( sin ` ( ( N + 1 ) x. A ) ) ) ) )
153 152 oveq1d 
 |-  ( ph -> ( ( ( 1 / 2 ) x. ( ( sin ` A ) + sum_ n e. ( 1 ... N ) ( ( sin ` ( ( n + 1 ) x. A ) ) - ( sin ` ( ( n - 1 ) x. A ) ) ) ) ) / ( sin ` A ) ) = ( ( ( 1 / 2 ) x. ( ( sin ` ( N x. A ) ) + ( sin ` ( ( N + 1 ) x. A ) ) ) ) / ( sin ` A ) ) )
154 18 70 153 3eqtrd 
 |-  ( ph -> ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) ) = ( ( ( 1 / 2 ) x. ( ( sin ` ( N x. A ) ) + ( sin ` ( ( N + 1 ) x. A ) ) ) ) / ( sin ` A ) ) )
155 halfre 
 |-  ( 1 / 2 ) e. RR
156 155 a1i 
 |-  ( ph -> ( 1 / 2 ) e. RR )
157 114 156 readdcld 
 |-  ( ph -> ( N + ( 1 / 2 ) ) e. RR )
158 157 1 remulcld 
 |-  ( ph -> ( ( N + ( 1 / 2 ) ) x. A ) e. RR )
159 158 recnd 
 |-  ( ph -> ( ( N + ( 1 / 2 ) ) x. A ) e. CC )
160 5 10 mulcld 
 |-  ( ph -> ( ( 1 / 2 ) x. A ) e. CC )
161 sinmulcos 
 |-  ( ( ( ( N + ( 1 / 2 ) ) x. A ) e. CC /\ ( ( 1 / 2 ) x. A ) e. CC ) -> ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) x. ( cos ` ( ( 1 / 2 ) x. A ) ) ) = ( ( ( sin ` ( ( ( N + ( 1 / 2 ) ) x. A ) + ( ( 1 / 2 ) x. A ) ) ) + ( sin ` ( ( ( N + ( 1 / 2 ) ) x. A ) - ( ( 1 / 2 ) x. A ) ) ) ) / 2 ) )
162 159 160 161 syl2anc 
 |-  ( ph -> ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) x. ( cos ` ( ( 1 / 2 ) x. A ) ) ) = ( ( ( sin ` ( ( ( N + ( 1 / 2 ) ) x. A ) + ( ( 1 / 2 ) x. A ) ) ) + ( sin ` ( ( ( N + ( 1 / 2 ) ) x. A ) - ( ( 1 / 2 ) x. A ) ) ) ) / 2 ) )
163 115 5 10 adddird 
 |-  ( ph -> ( ( N + ( 1 / 2 ) ) x. A ) = ( ( N x. A ) + ( ( 1 / 2 ) x. A ) ) )
164 163 oveq1d 
 |-  ( ph -> ( ( ( N + ( 1 / 2 ) ) x. A ) + ( ( 1 / 2 ) x. A ) ) = ( ( ( N x. A ) + ( ( 1 / 2 ) x. A ) ) + ( ( 1 / 2 ) x. A ) ) )
165 139 160 160 addassd 
 |-  ( ph -> ( ( ( N x. A ) + ( ( 1 / 2 ) x. A ) ) + ( ( 1 / 2 ) x. A ) ) = ( ( N x. A ) + ( ( ( 1 / 2 ) x. A ) + ( ( 1 / 2 ) x. A ) ) ) )
166 5 5 10 adddird 
 |-  ( ph -> ( ( ( 1 / 2 ) + ( 1 / 2 ) ) x. A ) = ( ( ( 1 / 2 ) x. A ) + ( ( 1 / 2 ) x. A ) ) )
167 4 2halvesd 
 |-  ( ph -> ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1 )
168 167 oveq1d 
 |-  ( ph -> ( ( ( 1 / 2 ) + ( 1 / 2 ) ) x. A ) = ( 1 x. A ) )
169 166 168 eqtr3d 
 |-  ( ph -> ( ( ( 1 / 2 ) x. A ) + ( ( 1 / 2 ) x. A ) ) = ( 1 x. A ) )
170 169 oveq2d 
 |-  ( ph -> ( ( N x. A ) + ( ( ( 1 / 2 ) x. A ) + ( ( 1 / 2 ) x. A ) ) ) = ( ( N x. A ) + ( 1 x. A ) ) )
171 115 4 10 adddird 
 |-  ( ph -> ( ( N + 1 ) x. A ) = ( ( N x. A ) + ( 1 x. A ) ) )
172 170 171 eqtr4d 
 |-  ( ph -> ( ( N x. A ) + ( ( ( 1 / 2 ) x. A ) + ( ( 1 / 2 ) x. A ) ) ) = ( ( N + 1 ) x. A ) )
173 164 165 172 3eqtrrd 
 |-  ( ph -> ( ( N + 1 ) x. A ) = ( ( ( N + ( 1 / 2 ) ) x. A ) + ( ( 1 / 2 ) x. A ) ) )
174 173 fveq2d 
 |-  ( ph -> ( sin ` ( ( N + 1 ) x. A ) ) = ( sin ` ( ( ( N + ( 1 / 2 ) ) x. A ) + ( ( 1 / 2 ) x. A ) ) ) )
175 163 oveq1d 
 |-  ( ph -> ( ( ( N + ( 1 / 2 ) ) x. A ) - ( ( 1 / 2 ) x. A ) ) = ( ( ( N x. A ) + ( ( 1 / 2 ) x. A ) ) - ( ( 1 / 2 ) x. A ) ) )
176 139 160 pncand 
 |-  ( ph -> ( ( ( N x. A ) + ( ( 1 / 2 ) x. A ) ) - ( ( 1 / 2 ) x. A ) ) = ( N x. A ) )
177 175 176 eqtr2d 
 |-  ( ph -> ( N x. A ) = ( ( ( N + ( 1 / 2 ) ) x. A ) - ( ( 1 / 2 ) x. A ) ) )
178 177 fveq2d 
 |-  ( ph -> ( sin ` ( N x. A ) ) = ( sin ` ( ( ( N + ( 1 / 2 ) ) x. A ) - ( ( 1 / 2 ) x. A ) ) ) )
179 174 178 oveq12d 
 |-  ( ph -> ( ( sin ` ( ( N + 1 ) x. A ) ) + ( sin ` ( N x. A ) ) ) = ( ( sin ` ( ( ( N + ( 1 / 2 ) ) x. A ) + ( ( 1 / 2 ) x. A ) ) ) + ( sin ` ( ( ( N + ( 1 / 2 ) ) x. A ) - ( ( 1 / 2 ) x. A ) ) ) ) )
180 179 oveq1d 
 |-  ( ph -> ( ( ( sin ` ( ( N + 1 ) x. A ) ) + ( sin ` ( N x. A ) ) ) / 2 ) = ( ( ( sin ` ( ( ( N + ( 1 / 2 ) ) x. A ) + ( ( 1 / 2 ) x. A ) ) ) + ( sin ` ( ( ( N + ( 1 / 2 ) ) x. A ) - ( ( 1 / 2 ) x. A ) ) ) ) / 2 ) )
181 162 180 eqtr4d 
 |-  ( ph -> ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) x. ( cos ` ( ( 1 / 2 ) x. A ) ) ) = ( ( ( sin ` ( ( N + 1 ) x. A ) ) + ( sin ` ( N x. A ) ) ) / 2 ) )
182 148 oveq1d 
 |-  ( ph -> ( ( ( sin ` ( ( N + 1 ) x. A ) ) + ( sin ` ( N x. A ) ) ) / 2 ) = ( ( ( sin ` ( N x. A ) ) + ( sin ` ( ( N + 1 ) x. A ) ) ) / 2 ) )
183 140 137 addcld 
 |-  ( ph -> ( ( sin ` ( N x. A ) ) + ( sin ` ( ( N + 1 ) x. A ) ) ) e. CC )
184 183 53 60 divrec2d 
 |-  ( ph -> ( ( ( sin ` ( N x. A ) ) + ( sin ` ( ( N + 1 ) x. A ) ) ) / 2 ) = ( ( 1 / 2 ) x. ( ( sin ` ( N x. A ) ) + ( sin ` ( ( N + 1 ) x. A ) ) ) ) )
185 181 182 184 3eqtrrd 
 |-  ( ph -> ( ( 1 / 2 ) x. ( ( sin ` ( N x. A ) ) + ( sin ` ( ( N + 1 ) x. A ) ) ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) x. ( cos ` ( ( 1 / 2 ) x. A ) ) ) )
186 185 oveq1d 
 |-  ( ph -> ( ( ( 1 / 2 ) x. ( ( sin ` ( N x. A ) ) + ( sin ` ( ( N + 1 ) x. A ) ) ) ) / ( sin ` A ) ) = ( ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) x. ( cos ` ( ( 1 / 2 ) x. A ) ) ) / ( sin ` A ) ) )
187 10 53 60 divcan2d 
 |-  ( ph -> ( 2 x. ( A / 2 ) ) = A )
188 187 eqcomd 
 |-  ( ph -> A = ( 2 x. ( A / 2 ) ) )
189 188 fveq2d 
 |-  ( ph -> ( sin ` A ) = ( sin ` ( 2 x. ( A / 2 ) ) ) )
190 10 halfcld 
 |-  ( ph -> ( A / 2 ) e. CC )
191 sin2t 
 |-  ( ( A / 2 ) e. CC -> ( sin ` ( 2 x. ( A / 2 ) ) ) = ( 2 x. ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) ) )
192 190 191 syl 
 |-  ( ph -> ( sin ` ( 2 x. ( A / 2 ) ) ) = ( 2 x. ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) ) )
193 189 192 eqtrd 
 |-  ( ph -> ( sin ` A ) = ( 2 x. ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) ) )
194 193 oveq2d 
 |-  ( ph -> ( ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) x. ( cos ` ( ( 1 / 2 ) x. A ) ) ) / ( sin ` A ) ) = ( ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) x. ( cos ` ( ( 1 / 2 ) x. A ) ) ) / ( 2 x. ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) ) ) )
195 190 sincld 
 |-  ( ph -> ( sin ` ( A / 2 ) ) e. CC )
196 190 coscld 
 |-  ( ph -> ( cos ` ( A / 2 ) ) e. CC )
197 53 195 196 mulassd 
 |-  ( ph -> ( ( 2 x. ( sin ` ( A / 2 ) ) ) x. ( cos ` ( A / 2 ) ) ) = ( 2 x. ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) ) )
198 10 53 60 divrec2d 
 |-  ( ph -> ( A / 2 ) = ( ( 1 / 2 ) x. A ) )
199 198 fveq2d 
 |-  ( ph -> ( cos ` ( A / 2 ) ) = ( cos ` ( ( 1 / 2 ) x. A ) ) )
200 199 oveq2d 
 |-  ( ph -> ( ( 2 x. ( sin ` ( A / 2 ) ) ) x. ( cos ` ( A / 2 ) ) ) = ( ( 2 x. ( sin ` ( A / 2 ) ) ) x. ( cos ` ( ( 1 / 2 ) x. A ) ) ) )
201 197 200 eqtr3d 
 |-  ( ph -> ( 2 x. ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) ) = ( ( 2 x. ( sin ` ( A / 2 ) ) ) x. ( cos ` ( ( 1 / 2 ) x. A ) ) ) )
202 201 oveq2d 
 |-  ( ph -> ( ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) x. ( cos ` ( ( 1 / 2 ) x. A ) ) ) / ( 2 x. ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) ) ) = ( ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) x. ( cos ` ( ( 1 / 2 ) x. A ) ) ) / ( ( 2 x. ( sin ` ( A / 2 ) ) ) x. ( cos ` ( ( 1 / 2 ) x. A ) ) ) ) )
203 159 sincld 
 |-  ( ph -> ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) e. CC )
204 53 195 mulcld 
 |-  ( ph -> ( 2 x. ( sin ` ( A / 2 ) ) ) e. CC )
205 160 coscld 
 |-  ( ph -> ( cos ` ( ( 1 / 2 ) x. A ) ) e. CC )
206 195 196 mulcld 
 |-  ( ph -> ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) e. CC )
207 193 2 eqnetrrd 
 |-  ( ph -> ( 2 x. ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) ) =/= 0 )
208 53 206 207 mulne0bbd 
 |-  ( ph -> ( ( sin ` ( A / 2 ) ) x. ( cos ` ( A / 2 ) ) ) =/= 0 )
209 195 196 208 mulne0bad 
 |-  ( ph -> ( sin ` ( A / 2 ) ) =/= 0 )
210 53 195 60 209 mulne0d 
 |-  ( ph -> ( 2 x. ( sin ` ( A / 2 ) ) ) =/= 0 )
211 195 196 208 mulne0bbd 
 |-  ( ph -> ( cos ` ( A / 2 ) ) =/= 0 )
212 199 211 eqnetrrd 
 |-  ( ph -> ( cos ` ( ( 1 / 2 ) x. A ) ) =/= 0 )
213 203 204 205 210 212 divcan5rd 
 |-  ( ph -> ( ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) x. ( cos ` ( ( 1 / 2 ) x. A ) ) ) / ( ( 2 x. ( sin ` ( A / 2 ) ) ) x. ( cos ` ( ( 1 / 2 ) x. A ) ) ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / ( 2 x. ( sin ` ( A / 2 ) ) ) ) )
214 194 202 213 3eqtrd 
 |-  ( ph -> ( ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) x. ( cos ` ( ( 1 / 2 ) x. A ) ) ) / ( sin ` A ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / ( 2 x. ( sin ` ( A / 2 ) ) ) ) )
215 154 186 214 3eqtrd 
 |-  ( ph -> ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / ( 2 x. ( sin ` ( A / 2 ) ) ) ) )
216 215 oveq1d 
 |-  ( ph -> ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) ) / _pi ) = ( ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / ( 2 x. ( sin ` ( A / 2 ) ) ) ) / _pi ) )
217 picn 
 |-  _pi e. CC
218 217 a1i 
 |-  ( ph -> _pi e. CC )
219 pire 
 |-  _pi e. RR
220 pipos 
 |-  0 < _pi
221 219 220 gt0ne0ii 
 |-  _pi =/= 0
222 221 a1i 
 |-  ( ph -> _pi =/= 0 )
223 203 204 218 210 222 divdiv32d 
 |-  ( ph -> ( ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / ( 2 x. ( sin ` ( A / 2 ) ) ) ) / _pi ) = ( ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / _pi ) / ( 2 x. ( sin ` ( A / 2 ) ) ) ) )
224 203 218 204 222 210 divdiv1d 
 |-  ( ph -> ( ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / _pi ) / ( 2 x. ( sin ` ( A / 2 ) ) ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / ( _pi x. ( 2 x. ( sin ` ( A / 2 ) ) ) ) ) )
225 218 53 195 mulassd 
 |-  ( ph -> ( ( _pi x. 2 ) x. ( sin ` ( A / 2 ) ) ) = ( _pi x. ( 2 x. ( sin ` ( A / 2 ) ) ) ) )
226 218 53 mulcomd 
 |-  ( ph -> ( _pi x. 2 ) = ( 2 x. _pi ) )
227 226 oveq1d 
 |-  ( ph -> ( ( _pi x. 2 ) x. ( sin ` ( A / 2 ) ) ) = ( ( 2 x. _pi ) x. ( sin ` ( A / 2 ) ) ) )
228 225 227 eqtr3d 
 |-  ( ph -> ( _pi x. ( 2 x. ( sin ` ( A / 2 ) ) ) ) = ( ( 2 x. _pi ) x. ( sin ` ( A / 2 ) ) ) )
229 228 oveq2d 
 |-  ( ph -> ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / ( _pi x. ( 2 x. ( sin ` ( A / 2 ) ) ) ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / ( ( 2 x. _pi ) x. ( sin ` ( A / 2 ) ) ) ) )
230 224 229 eqtrd 
 |-  ( ph -> ( ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / _pi ) / ( 2 x. ( sin ` ( A / 2 ) ) ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / ( ( 2 x. _pi ) x. ( sin ` ( A / 2 ) ) ) ) )
231 216 223 230 3eqtrd 
 |-  ( ph -> ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) ) / _pi ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / ( ( 2 x. _pi ) x. ( sin ` ( A / 2 ) ) ) ) )