Metamath Proof Explorer

Theorem basellem3

Description: Lemma for basel . Using the binomial theorem and de Moivre's formula, we have the identity _e ^i N x / ( sin x ) ^ n = sum m e. ( 0 ... N ) ( NC m ) ( i ^ m ) ( cot x ) ^ ( N - m ) , so taking imaginary parts yields sin ( N x ) / ( sin x ) ^ N = sum_ j e. ( 0 ... M ) ( N _C 2 j ) ( -u 1 ) ^ ( M - j ) ( cot x ) ^ ( -u 2 j ) = P ( ( cot x ) ^ 2 ) , where N = 2 M + 1 . (Contributed by Mario Carneiro, 30-Jul-2014)

Ref Expression
Hypotheses basel.n 
|- N = ( ( 2 x. M ) + 1 )
basel.p 
|- P = ( t e. CC |-> sum_ j e. ( 0 ... M ) ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( t ^ j ) ) )
Assertion basellem3 
|- ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( P ` ( ( tan ` A ) ^ -u 2 ) ) = ( ( sin ` ( N x. A ) ) / ( ( sin ` A ) ^ N ) ) )

Proof

Step Hyp Ref Expression
1 basel.n 
 |-  N = ( ( 2 x. M ) + 1 )
2 basel.p 
 |-  P = ( t e. CC |-> sum_ j e. ( 0 ... M ) ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( t ^ j ) ) )
3 tanrpcl 
 |-  ( A e. ( 0 (,) ( _pi / 2 ) ) -> ( tan ` A ) e. RR+ )
4 3 adantl 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( tan ` A ) e. RR+ )
5 4 rpreccld 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( 1 / ( tan ` A ) ) e. RR+ )
6 5 rpcnd 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( 1 / ( tan ` A ) ) e. CC )
7 ax-icn 
 |-  _i e. CC
8 7 a1i 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> _i e. CC )
9 2nn 
 |-  2 e. NN
10 simpl 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> M e. NN )
11 nnmulcl 
 |-  ( ( 2 e. NN /\ M e. NN ) -> ( 2 x. M ) e. NN )
12 9 10 11 sylancr 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( 2 x. M ) e. NN )
13 12 peano2nnd 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( ( 2 x. M ) + 1 ) e. NN )
14 1 13 eqeltrid 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> N e. NN )
15 14 nnnn0d 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> N e. NN0 )
16 binom 
 |-  ( ( ( 1 / ( tan ` A ) ) e. CC /\ _i e. CC /\ N e. NN0 ) -> ( ( ( 1 / ( tan ` A ) ) + _i ) ^ N ) = sum_ m e. ( 0 ... N ) ( ( N _C m ) x. ( ( ( 1 / ( tan ` A ) ) ^ ( N - m ) ) x. ( _i ^ m ) ) ) )
17 6 8 15 16 syl3anc 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( ( ( 1 / ( tan ` A ) ) + _i ) ^ N ) = sum_ m e. ( 0 ... N ) ( ( N _C m ) x. ( ( ( 1 / ( tan ` A ) ) ^ ( N - m ) ) x. ( _i ^ m ) ) ) )
18 elioore 
 |-  ( A e. ( 0 (,) ( _pi / 2 ) ) -> A e. RR )
19 18 adantl 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> A e. RR )
20 19 recoscld 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( cos ` A ) e. RR )
21 20 recnd 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( cos ` A ) e. CC )
22 19 resincld 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( sin ` A ) e. RR )
23 22 recnd 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( sin ` A ) e. CC )
24 mulcl 
 |-  ( ( _i e. CC /\ ( sin ` A ) e. CC ) -> ( _i x. ( sin ` A ) ) e. CC )
25 7 23 24 sylancr 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( _i x. ( sin ` A ) ) e. CC )
26 21 25 addcld 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) e. CC )
27 sincosq1sgn 
 |-  ( A e. ( 0 (,) ( _pi / 2 ) ) -> ( 0 < ( sin ` A ) /\ 0 < ( cos ` A ) ) )
28 27 adantl 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( 0 < ( sin ` A ) /\ 0 < ( cos ` A ) ) )
29 28 simpld 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> 0 < ( sin ` A ) )
30 29 gt0ne0d 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( sin ` A ) =/= 0 )
31 26 23 30 15 expdivd 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( ( ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) / ( sin ` A ) ) ^ N ) = ( ( ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) ^ N ) / ( ( sin ` A ) ^ N ) ) )
32 21 25 23 30 divdird 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) / ( sin ` A ) ) = ( ( ( cos ` A ) / ( sin ` A ) ) + ( ( _i x. ( sin ` A ) ) / ( sin ` A ) ) ) )
33 19 recnd 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> A e. CC )
34 28 simprd 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> 0 < ( cos ` A ) )
35 34 gt0ne0d 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( cos ` A ) =/= 0 )
36 tanval 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( tan ` A ) = ( ( sin ` A ) / ( cos ` A ) ) )
37 33 35 36 syl2anc 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( tan ` A ) = ( ( sin ` A ) / ( cos ` A ) ) )
38 37 oveq2d 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( 1 / ( tan ` A ) ) = ( 1 / ( ( sin ` A ) / ( cos ` A ) ) ) )
39 23 21 30 35 recdivd 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( 1 / ( ( sin ` A ) / ( cos ` A ) ) ) = ( ( cos ` A ) / ( sin ` A ) ) )
40 38 39 eqtr2d 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( ( cos ` A ) / ( sin ` A ) ) = ( 1 / ( tan ` A ) ) )
41 8 23 30 divcan4d 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( ( _i x. ( sin ` A ) ) / ( sin ` A ) ) = _i )
42 40 41 oveq12d 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( ( ( cos ` A ) / ( sin ` A ) ) + ( ( _i x. ( sin ` A ) ) / ( sin ` A ) ) ) = ( ( 1 / ( tan ` A ) ) + _i ) )
43 32 42 eqtrd 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) / ( sin ` A ) ) = ( ( 1 / ( tan ` A ) ) + _i ) )
44 43 oveq1d 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( ( ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) / ( sin ` A ) ) ^ N ) = ( ( ( 1 / ( tan ` A ) ) + _i ) ^ N ) )
45 14 nnzd 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> N e. ZZ )
46 demoivre 
 |-  ( ( A e. CC /\ N e. ZZ ) -> ( ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) ^ N ) = ( ( cos ` ( N x. A ) ) + ( _i x. ( sin ` ( N x. A ) ) ) ) )
47 33 45 46 syl2anc 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) ^ N ) = ( ( cos ` ( N x. A ) ) + ( _i x. ( sin ` ( N x. A ) ) ) ) )
48 47 oveq1d 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( ( ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) ^ N ) / ( ( sin ` A ) ^ N ) ) = ( ( ( cos ` ( N x. A ) ) + ( _i x. ( sin ` ( N x. A ) ) ) ) / ( ( sin ` A ) ^ N ) ) )
49 31 44 48 3eqtr3d 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( ( ( 1 / ( tan ` A ) ) + _i ) ^ N ) = ( ( ( cos ` ( N x. A ) ) + ( _i x. ( sin ` ( N x. A ) ) ) ) / ( ( sin ` A ) ^ N ) ) )
50 14 nnred 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> N e. RR )
51 50 19 remulcld 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( N x. A ) e. RR )
52 51 recoscld 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( cos ` ( N x. A ) ) e. RR )
53 52 recnd 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( cos ` ( N x. A ) ) e. CC )
54 51 resincld 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( sin ` ( N x. A ) ) e. RR )
55 54 recnd 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( sin ` ( N x. A ) ) e. CC )
56 mulcl 
 |-  ( ( _i e. CC /\ ( sin ` ( N x. A ) ) e. CC ) -> ( _i x. ( sin ` ( N x. A ) ) ) e. CC )
57 7 55 56 sylancr 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( _i x. ( sin ` ( N x. A ) ) ) e. CC )
58 22 29 elrpd 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( sin ` A ) e. RR+ )
59 58 45 rpexpcld 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( ( sin ` A ) ^ N ) e. RR+ )
60 59 rpcnd 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( ( sin ` A ) ^ N ) e. CC )
61 59 rpne0d 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( ( sin ` A ) ^ N ) =/= 0 )
62 53 57 60 61 divdird 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( ( ( cos ` ( N x. A ) ) + ( _i x. ( sin ` ( N x. A ) ) ) ) / ( ( sin ` A ) ^ N ) ) = ( ( ( cos ` ( N x. A ) ) / ( ( sin ` A ) ^ N ) ) + ( ( _i x. ( sin ` ( N x. A ) ) ) / ( ( sin ` A ) ^ N ) ) ) )
63 8 55 60 61 divassd 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( ( _i x. ( sin ` ( N x. A ) ) ) / ( ( sin ` A ) ^ N ) ) = ( _i x. ( ( sin ` ( N x. A ) ) / ( ( sin ` A ) ^ N ) ) ) )
64 63 oveq2d 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( ( ( cos ` ( N x. A ) ) / ( ( sin ` A ) ^ N ) ) + ( ( _i x. ( sin ` ( N x. A ) ) ) / ( ( sin ` A ) ^ N ) ) ) = ( ( ( cos ` ( N x. A ) ) / ( ( sin ` A ) ^ N ) ) + ( _i x. ( ( sin ` ( N x. A ) ) / ( ( sin ` A ) ^ N ) ) ) ) )
65 49 62 64 3eqtrd 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( ( ( 1 / ( tan ` A ) ) + _i ) ^ N ) = ( ( ( cos ` ( N x. A ) ) / ( ( sin ` A ) ^ N ) ) + ( _i x. ( ( sin ` ( N x. A ) ) / ( ( sin ` A ) ^ N ) ) ) ) )
66 17 65 eqtr3d 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> sum_ m e. ( 0 ... N ) ( ( N _C m ) x. ( ( ( 1 / ( tan ` A ) ) ^ ( N - m ) ) x. ( _i ^ m ) ) ) = ( ( ( cos ` ( N x. A ) ) / ( ( sin ` A ) ^ N ) ) + ( _i x. ( ( sin ` ( N x. A ) ) / ( ( sin ` A ) ^ N ) ) ) ) )
67 66 fveq2d 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( Im ` sum_ m e. ( 0 ... N ) ( ( N _C m ) x. ( ( ( 1 / ( tan ` A ) ) ^ ( N - m ) ) x. ( _i ^ m ) ) ) ) = ( Im ` ( ( ( cos ` ( N x. A ) ) / ( ( sin ` A ) ^ N ) ) + ( _i x. ( ( sin ` ( N x. A ) ) / ( ( sin ` A ) ^ N ) ) ) ) ) )
68 oveq2 
 |-  ( m = ( N - ( 2 x. j ) ) -> ( N _C m ) = ( N _C ( N - ( 2 x. j ) ) ) )
69 oveq2 
 |-  ( m = ( N - ( 2 x. j ) ) -> ( N - m ) = ( N - ( N - ( 2 x. j ) ) ) )
70 69 oveq2d 
 |-  ( m = ( N - ( 2 x. j ) ) -> ( ( 1 / ( tan ` A ) ) ^ ( N - m ) ) = ( ( 1 / ( tan ` A ) ) ^ ( N - ( N - ( 2 x. j ) ) ) ) )
71 oveq2 
 |-  ( m = ( N - ( 2 x. j ) ) -> ( _i ^ m ) = ( _i ^ ( N - ( 2 x. j ) ) ) )
72 70 71 oveq12d 
 |-  ( m = ( N - ( 2 x. j ) ) -> ( ( ( 1 / ( tan ` A ) ) ^ ( N - m ) ) x. ( _i ^ m ) ) = ( ( ( 1 / ( tan ` A ) ) ^ ( N - ( N - ( 2 x. j ) ) ) ) x. ( _i ^ ( N - ( 2 x. j ) ) ) ) )
73 68 72 oveq12d 
 |-  ( m = ( N - ( 2 x. j ) ) -> ( ( N _C m ) x. ( ( ( 1 / ( tan ` A ) ) ^ ( N - m ) ) x. ( _i ^ m ) ) ) = ( ( N _C ( N - ( 2 x. j ) ) ) x. ( ( ( 1 / ( tan ` A ) ) ^ ( N - ( N - ( 2 x. j ) ) ) ) x. ( _i ^ ( N - ( 2 x. j ) ) ) ) ) )
74 73 fveq2d 
 |-  ( m = ( N - ( 2 x. j ) ) -> ( Im ` ( ( N _C m ) x. ( ( ( 1 / ( tan ` A ) ) ^ ( N - m ) ) x. ( _i ^ m ) ) ) ) = ( Im ` ( ( N _C ( N - ( 2 x. j ) ) ) x. ( ( ( 1 / ( tan ` A ) ) ^ ( N - ( N - ( 2 x. j ) ) ) ) x. ( _i ^ ( N - ( 2 x. j ) ) ) ) ) ) )
75 fzfid 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( 0 ... M ) e. Fin )
76 2nn0 
 |-  2 e. NN0
77 elfznn0 
 |-  ( k e. ( 0 ... M ) -> k e. NN0 )
78 77 adantl 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ k e. ( 0 ... M ) ) -> k e. NN0 )
79 nn0mulcl 
 |-  ( ( 2 e. NN0 /\ k e. NN0 ) -> ( 2 x. k ) e. NN0 )
80 76 78 79 sylancr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ k e. ( 0 ... M ) ) -> ( 2 x. k ) e. NN0 )
81 80 nn0red 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ k e. ( 0 ... M ) ) -> ( 2 x. k ) e. RR )
82 12 nnred 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( 2 x. M ) e. RR )
83 82 adantr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ k e. ( 0 ... M ) ) -> ( 2 x. M ) e. RR )
84 50 adantr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ k e. ( 0 ... M ) ) -> N e. RR )
85 elfzle2 
 |-  ( k e. ( 0 ... M ) -> k <_ M )
86 85 adantl 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ k e. ( 0 ... M ) ) -> k <_ M )
87 78 nn0red 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ k e. ( 0 ... M ) ) -> k e. RR )
88 nnre 
 |-  ( M e. NN -> M e. RR )
89 88 ad2antrr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ k e. ( 0 ... M ) ) -> M e. RR )
90 2re 
 |-  2 e. RR
91 2pos 
 |-  0 < 2
92 90 91 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
93 92 a1i 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ k e. ( 0 ... M ) ) -> ( 2 e. RR /\ 0 < 2 ) )
94 lemul2 
 |-  ( ( k e. RR /\ M e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( k <_ M <-> ( 2 x. k ) <_ ( 2 x. M ) ) )
95 87 89 93 94 syl3anc 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ k e. ( 0 ... M ) ) -> ( k <_ M <-> ( 2 x. k ) <_ ( 2 x. M ) ) )
96 86 95 mpbid 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ k e. ( 0 ... M ) ) -> ( 2 x. k ) <_ ( 2 x. M ) )
97 83 lep1d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ k e. ( 0 ... M ) ) -> ( 2 x. M ) <_ ( ( 2 x. M ) + 1 ) )
98 97 1 breqtrrdi 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ k e. ( 0 ... M ) ) -> ( 2 x. M ) <_ N )
99 81 83 84 96 98 letrd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ k e. ( 0 ... M ) ) -> ( 2 x. k ) <_ N )
100 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
101 80 100 eleqtrdi 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ k e. ( 0 ... M ) ) -> ( 2 x. k ) e. ( ZZ>= ` 0 ) )
102 45 adantr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ k e. ( 0 ... M ) ) -> N e. ZZ )
103 elfz5 
 |-  ( ( ( 2 x. k ) e. ( ZZ>= ` 0 ) /\ N e. ZZ ) -> ( ( 2 x. k ) e. ( 0 ... N ) <-> ( 2 x. k ) <_ N ) )
104 101 102 103 syl2anc 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ k e. ( 0 ... M ) ) -> ( ( 2 x. k ) e. ( 0 ... N ) <-> ( 2 x. k ) <_ N ) )
105 99 104 mpbird 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ k e. ( 0 ... M ) ) -> ( 2 x. k ) e. ( 0 ... N ) )
106 fznn0sub2 
 |-  ( ( 2 x. k ) e. ( 0 ... N ) -> ( N - ( 2 x. k ) ) e. ( 0 ... N ) )
107 105 106 syl 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ k e. ( 0 ... M ) ) -> ( N - ( 2 x. k ) ) e. ( 0 ... N ) )
108 107 ex 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( k e. ( 0 ... M ) -> ( N - ( 2 x. k ) ) e. ( 0 ... N ) ) )
109 14 nncnd 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> N e. CC )
110 109 adantr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( k e. ( 0 ... M ) /\ m e. ( 0 ... M ) ) ) -> N e. CC )
111 2cn 
 |-  2 e. CC
112 elfzelz 
 |-  ( k e. ( 0 ... M ) -> k e. ZZ )
113 112 zcnd 
 |-  ( k e. ( 0 ... M ) -> k e. CC )
114 113 ad2antrl 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( k e. ( 0 ... M ) /\ m e. ( 0 ... M ) ) ) -> k e. CC )
115 mulcl 
 |-  ( ( 2 e. CC /\ k e. CC ) -> ( 2 x. k ) e. CC )
116 111 114 115 sylancr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( k e. ( 0 ... M ) /\ m e. ( 0 ... M ) ) ) -> ( 2 x. k ) e. CC )
117 113 ssriv 
 |-  ( 0 ... M ) C_ CC
118 simprr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( k e. ( 0 ... M ) /\ m e. ( 0 ... M ) ) ) -> m e. ( 0 ... M ) )
119 117 118 sselid 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( k e. ( 0 ... M ) /\ m e. ( 0 ... M ) ) ) -> m e. CC )
120 mulcl 
 |-  ( ( 2 e. CC /\ m e. CC ) -> ( 2 x. m ) e. CC )
121 111 119 120 sylancr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( k e. ( 0 ... M ) /\ m e. ( 0 ... M ) ) ) -> ( 2 x. m ) e. CC )
122 110 116 121 subcanad 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( k e. ( 0 ... M ) /\ m e. ( 0 ... M ) ) ) -> ( ( N - ( 2 x. k ) ) = ( N - ( 2 x. m ) ) <-> ( 2 x. k ) = ( 2 x. m ) ) )
123 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
124 123 a1i 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( k e. ( 0 ... M ) /\ m e. ( 0 ... M ) ) ) -> ( 2 e. CC /\ 2 =/= 0 ) )
125 mulcan 
 |-  ( ( k e. CC /\ m e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( 2 x. k ) = ( 2 x. m ) <-> k = m ) )
126 114 119 124 125 syl3anc 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( k e. ( 0 ... M ) /\ m e. ( 0 ... M ) ) ) -> ( ( 2 x. k ) = ( 2 x. m ) <-> k = m ) )
127 122 126 bitrd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( k e. ( 0 ... M ) /\ m e. ( 0 ... M ) ) ) -> ( ( N - ( 2 x. k ) ) = ( N - ( 2 x. m ) ) <-> k = m ) )
128 127 ex 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( ( k e. ( 0 ... M ) /\ m e. ( 0 ... M ) ) -> ( ( N - ( 2 x. k ) ) = ( N - ( 2 x. m ) ) <-> k = m ) ) )
129 108 128 dom2lem 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) : ( 0 ... M ) -1-1-> ( 0 ... N ) )
130 f1f1orn 
 |-  ( ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) : ( 0 ... M ) -1-1-> ( 0 ... N ) -> ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) : ( 0 ... M ) -1-1-onto-> ran ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) )
131 129 130 syl 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) : ( 0 ... M ) -1-1-onto-> ran ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) )
132 oveq2 
 |-  ( k = j -> ( 2 x. k ) = ( 2 x. j ) )
133 132 oveq2d 
 |-  ( k = j -> ( N - ( 2 x. k ) ) = ( N - ( 2 x. j ) ) )
134 eqid 
 |-  ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) = ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) )
135 ovex 
 |-  ( N - ( 2 x. j ) ) e. _V
136 133 134 135 fvmpt 
 |-  ( j e. ( 0 ... M ) -> ( ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) ` j ) = ( N - ( 2 x. j ) ) )
137 136 adantl 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) ` j ) = ( N - ( 2 x. j ) ) )
138 107 fmpttd 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) : ( 0 ... M ) --> ( 0 ... N ) )
139 138 frnd 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ran ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) C_ ( 0 ... N ) )
140 139 sselda 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ m e. ran ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) ) -> m e. ( 0 ... N ) )
141 bccl2 
 |-  ( m e. ( 0 ... N ) -> ( N _C m ) e. NN )
142 141 adantl 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ m e. ( 0 ... N ) ) -> ( N _C m ) e. NN )
143 142 nncnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ m e. ( 0 ... N ) ) -> ( N _C m ) e. CC )
144 4 rprecred 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( 1 / ( tan ` A ) ) e. RR )
145 fznn0sub 
 |-  ( m e. ( 0 ... N ) -> ( N - m ) e. NN0 )
146 reexpcl 
 |-  ( ( ( 1 / ( tan ` A ) ) e. RR /\ ( N - m ) e. NN0 ) -> ( ( 1 / ( tan ` A ) ) ^ ( N - m ) ) e. RR )
147 144 145 146 syl2an 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ m e. ( 0 ... N ) ) -> ( ( 1 / ( tan ` A ) ) ^ ( N - m ) ) e. RR )
148 147 recnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ m e. ( 0 ... N ) ) -> ( ( 1 / ( tan ` A ) ) ^ ( N - m ) ) e. CC )
149 elfznn0 
 |-  ( m e. ( 0 ... N ) -> m e. NN0 )
150 149 adantl 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ m e. ( 0 ... N ) ) -> m e. NN0 )
151 expcl 
 |-  ( ( _i e. CC /\ m e. NN0 ) -> ( _i ^ m ) e. CC )
152 7 150 151 sylancr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ m e. ( 0 ... N ) ) -> ( _i ^ m ) e. CC )
153 148 152 mulcld 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ m e. ( 0 ... N ) ) -> ( ( ( 1 / ( tan ` A ) ) ^ ( N - m ) ) x. ( _i ^ m ) ) e. CC )
154 143 153 mulcld 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ m e. ( 0 ... N ) ) -> ( ( N _C m ) x. ( ( ( 1 / ( tan ` A ) ) ^ ( N - m ) ) x. ( _i ^ m ) ) ) e. CC )
155 140 154 syldan 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ m e. ran ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) ) -> ( ( N _C m ) x. ( ( ( 1 / ( tan ` A ) ) ^ ( N - m ) ) x. ( _i ^ m ) ) ) e. CC )
156 155 imcld 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ m e. ran ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) ) -> ( Im ` ( ( N _C m ) x. ( ( ( 1 / ( tan ` A ) ) ^ ( N - m ) ) x. ( _i ^ m ) ) ) ) e. RR )
157 156 recnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ m e. ran ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) ) -> ( Im ` ( ( N _C m ) x. ( ( ( 1 / ( tan ` A ) ) ^ ( N - m ) ) x. ( _i ^ m ) ) ) ) e. CC )
158 74 75 131 137 157 fsumf1o 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> sum_ m e. ran ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) ( Im ` ( ( N _C m ) x. ( ( ( 1 / ( tan ` A ) ) ^ ( N - m ) ) x. ( _i ^ m ) ) ) ) = sum_ j e. ( 0 ... M ) ( Im ` ( ( N _C ( N - ( 2 x. j ) ) ) x. ( ( ( 1 / ( tan ` A ) ) ^ ( N - ( N - ( 2 x. j ) ) ) ) x. ( _i ^ ( N - ( 2 x. j ) ) ) ) ) ) )
159 eldifi 
 |-  ( m e. ( ( 0 ... N ) \ ran ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) ) -> m e. ( 0 ... N ) )
160 142 nnred 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ m e. ( 0 ... N ) ) -> ( N _C m ) e. RR )
161 159 160 sylan2 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ m e. ( ( 0 ... N ) \ ran ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) ) ) -> ( N _C m ) e. RR )
162 159 147 sylan2 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ m e. ( ( 0 ... N ) \ ran ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) ) ) -> ( ( 1 / ( tan ` A ) ) ^ ( N - m ) ) e. RR )
163 eldif 
 |-  ( m e. ( ( 0 ... N ) \ ran ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) ) <-> ( m e. ( 0 ... N ) /\ -. m e. ran ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) ) )
164 elfzelz 
 |-  ( m e. ( 0 ... N ) -> m e. ZZ )
165 164 adantl 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ m e. ( 0 ... N ) ) -> m e. ZZ )
166 zeo 
 |-  ( m e. ZZ -> ( ( m / 2 ) e. ZZ \/ ( ( m + 1 ) / 2 ) e. ZZ ) )
167 165 166 syl 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ m e. ( 0 ... N ) ) -> ( ( m / 2 ) e. ZZ \/ ( ( m + 1 ) / 2 ) e. ZZ ) )
168 i2 
 |-  ( _i ^ 2 ) = -u 1
169 168 oveq1i 
 |-  ( ( _i ^ 2 ) ^ ( m / 2 ) ) = ( -u 1 ^ ( m / 2 ) )
170 simprr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( m / 2 ) e. ZZ ) ) -> ( m / 2 ) e. ZZ )
171 149 ad2antrl 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( m / 2 ) e. ZZ ) ) -> m e. NN0 )
172 nn0re 
 |-  ( m e. NN0 -> m e. RR )
173 nn0ge0 
 |-  ( m e. NN0 -> 0 <_ m )
174 divge0 
 |-  ( ( ( m e. RR /\ 0 <_ m ) /\ ( 2 e. RR /\ 0 < 2 ) ) -> 0 <_ ( m / 2 ) )
175 90 91 174 mpanr12 
 |-  ( ( m e. RR /\ 0 <_ m ) -> 0 <_ ( m / 2 ) )
176 172 173 175 syl2anc 
 |-  ( m e. NN0 -> 0 <_ ( m / 2 ) )
177 171 176 syl 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( m / 2 ) e. ZZ ) ) -> 0 <_ ( m / 2 ) )
178 elnn0z 
 |-  ( ( m / 2 ) e. NN0 <-> ( ( m / 2 ) e. ZZ /\ 0 <_ ( m / 2 ) ) )
179 170 177 178 sylanbrc 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( m / 2 ) e. ZZ ) ) -> ( m / 2 ) e. NN0 )
180 expmul 
 |-  ( ( _i e. CC /\ 2 e. NN0 /\ ( m / 2 ) e. NN0 ) -> ( _i ^ ( 2 x. ( m / 2 ) ) ) = ( ( _i ^ 2 ) ^ ( m / 2 ) ) )
181 7 76 179 180 mp3an12i 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( m / 2 ) e. ZZ ) ) -> ( _i ^ ( 2 x. ( m / 2 ) ) ) = ( ( _i ^ 2 ) ^ ( m / 2 ) ) )
182 171 nn0cnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( m / 2 ) e. ZZ ) ) -> m e. CC )
183 2ne0 
 |-  2 =/= 0
184 divcan2 
 |-  ( ( m e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( 2 x. ( m / 2 ) ) = m )
185 111 183 184 mp3an23 
 |-  ( m e. CC -> ( 2 x. ( m / 2 ) ) = m )
186 182 185 syl 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( m / 2 ) e. ZZ ) ) -> ( 2 x. ( m / 2 ) ) = m )
187 186 oveq2d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( m / 2 ) e. ZZ ) ) -> ( _i ^ ( 2 x. ( m / 2 ) ) ) = ( _i ^ m ) )
188 181 187 eqtr3d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( m / 2 ) e. ZZ ) ) -> ( ( _i ^ 2 ) ^ ( m / 2 ) ) = ( _i ^ m ) )
189 169 188 eqtr3id 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( m / 2 ) e. ZZ ) ) -> ( -u 1 ^ ( m / 2 ) ) = ( _i ^ m ) )
190 neg1rr 
 |-  -u 1 e. RR
191 reexpcl 
 |-  ( ( -u 1 e. RR /\ ( m / 2 ) e. NN0 ) -> ( -u 1 ^ ( m / 2 ) ) e. RR )
192 190 179 191 sylancr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( m / 2 ) e. ZZ ) ) -> ( -u 1 ^ ( m / 2 ) ) e. RR )
193 189 192 eqeltrrd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( m / 2 ) e. ZZ ) ) -> ( _i ^ m ) e. RR )
194 193 expr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ m e. ( 0 ... N ) ) -> ( ( m / 2 ) e. ZZ -> ( _i ^ m ) e. RR ) )
195 0zd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> 0 e. ZZ )
196 nnz 
 |-  ( M e. NN -> M e. ZZ )
197 196 ad2antrr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> M e. ZZ )
198 109 adantr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> N e. CC )
199 149 ad2antrl 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> m e. NN0 )
200 199 nn0cnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> m e. CC )
201 1cnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> 1 e. CC )
202 198 200 201 pnpcan2d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( ( N + 1 ) - ( m + 1 ) ) = ( N - m ) )
203 2t1e2 
 |-  ( 2 x. 1 ) = 2
204 df-2 
 |-  2 = ( 1 + 1 )
205 203 204 eqtr2i 
 |-  ( 1 + 1 ) = ( 2 x. 1 )
206 205 oveq2i 
 |-  ( ( 2 x. M ) + ( 1 + 1 ) ) = ( ( 2 x. M ) + ( 2 x. 1 ) )
207 1 oveq1i 
 |-  ( N + 1 ) = ( ( ( 2 x. M ) + 1 ) + 1 )
208 12 nncnd 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( 2 x. M ) e. CC )
209 208 adantr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( 2 x. M ) e. CC )
210 209 201 201 addassd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( ( ( 2 x. M ) + 1 ) + 1 ) = ( ( 2 x. M ) + ( 1 + 1 ) ) )
211 207 210 eqtrid 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( N + 1 ) = ( ( 2 x. M ) + ( 1 + 1 ) ) )
212 2cnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> 2 e. CC )
213 nncn 
 |-  ( M e. NN -> M e. CC )
214 213 ad2antrr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> M e. CC )
215 212 214 201 adddid 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( 2 x. ( M + 1 ) ) = ( ( 2 x. M ) + ( 2 x. 1 ) ) )
216 206 211 215 3eqtr4a 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( N + 1 ) = ( 2 x. ( M + 1 ) ) )
217 216 oveq1d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( ( N + 1 ) - ( m + 1 ) ) = ( ( 2 x. ( M + 1 ) ) - ( m + 1 ) ) )
218 202 217 eqtr3d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( N - m ) = ( ( 2 x. ( M + 1 ) ) - ( m + 1 ) ) )
219 218 oveq1d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( ( N - m ) / 2 ) = ( ( ( 2 x. ( M + 1 ) ) - ( m + 1 ) ) / 2 ) )
220 197 peano2zd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( M + 1 ) e. ZZ )
221 220 zcnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( M + 1 ) e. CC )
222 mulcl 
 |-  ( ( 2 e. CC /\ ( M + 1 ) e. CC ) -> ( 2 x. ( M + 1 ) ) e. CC )
223 111 221 222 sylancr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( 2 x. ( M + 1 ) ) e. CC )
224 peano2cn 
 |-  ( m e. CC -> ( m + 1 ) e. CC )
225 200 224 syl 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( m + 1 ) e. CC )
226 123 a1i 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( 2 e. CC /\ 2 =/= 0 ) )
227 divsubdir 
 |-  ( ( ( 2 x. ( M + 1 ) ) e. CC /\ ( m + 1 ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( ( 2 x. ( M + 1 ) ) - ( m + 1 ) ) / 2 ) = ( ( ( 2 x. ( M + 1 ) ) / 2 ) - ( ( m + 1 ) / 2 ) ) )
228 223 225 226 227 syl3anc 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( ( ( 2 x. ( M + 1 ) ) - ( m + 1 ) ) / 2 ) = ( ( ( 2 x. ( M + 1 ) ) / 2 ) - ( ( m + 1 ) / 2 ) ) )
229 183 a1i 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> 2 =/= 0 )
230 221 212 229 divcan3d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( ( 2 x. ( M + 1 ) ) / 2 ) = ( M + 1 ) )
231 230 oveq1d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( ( ( 2 x. ( M + 1 ) ) / 2 ) - ( ( m + 1 ) / 2 ) ) = ( ( M + 1 ) - ( ( m + 1 ) / 2 ) ) )
232 219 228 231 3eqtrd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( ( N - m ) / 2 ) = ( ( M + 1 ) - ( ( m + 1 ) / 2 ) ) )
233 simprr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( ( m + 1 ) / 2 ) e. ZZ )
234 220 233 zsubcld 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( ( M + 1 ) - ( ( m + 1 ) / 2 ) ) e. ZZ )
235 232 234 eqeltrd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( ( N - m ) / 2 ) e. ZZ )
236 145 ad2antrl 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( N - m ) e. NN0 )
237 nn0re 
 |-  ( ( N - m ) e. NN0 -> ( N - m ) e. RR )
238 nn0ge0 
 |-  ( ( N - m ) e. NN0 -> 0 <_ ( N - m ) )
239 divge0 
 |-  ( ( ( ( N - m ) e. RR /\ 0 <_ ( N - m ) ) /\ ( 2 e. RR /\ 0 < 2 ) ) -> 0 <_ ( ( N - m ) / 2 ) )
240 90 91 239 mpanr12 
 |-  ( ( ( N - m ) e. RR /\ 0 <_ ( N - m ) ) -> 0 <_ ( ( N - m ) / 2 ) )
241 237 238 240 syl2anc 
 |-  ( ( N - m ) e. NN0 -> 0 <_ ( ( N - m ) / 2 ) )
242 236 241 syl 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> 0 <_ ( ( N - m ) / 2 ) )
243 236 nn0red 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( N - m ) e. RR )
244 50 adantr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> N e. RR )
245 peano2re 
 |-  ( N e. RR -> ( N + 1 ) e. RR )
246 244 245 syl 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( N + 1 ) e. RR )
247 199 173 syl 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> 0 <_ m )
248 199 nn0red 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> m e. RR )
249 244 248 subge02d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( 0 <_ m <-> ( N - m ) <_ N ) )
250 247 249 mpbid 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( N - m ) <_ N )
251 244 ltp1d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> N < ( N + 1 ) )
252 243 244 246 250 251 lelttrd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( N - m ) < ( N + 1 ) )
253 252 216 breqtrd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( N - m ) < ( 2 x. ( M + 1 ) ) )
254 220 zred 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( M + 1 ) e. RR )
255 92 a1i 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( 2 e. RR /\ 0 < 2 ) )
256 ltdivmul 
 |-  ( ( ( N - m ) e. RR /\ ( M + 1 ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( ( N - m ) / 2 ) < ( M + 1 ) <-> ( N - m ) < ( 2 x. ( M + 1 ) ) ) )
257 243 254 255 256 syl3anc 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( ( ( N - m ) / 2 ) < ( M + 1 ) <-> ( N - m ) < ( 2 x. ( M + 1 ) ) ) )
258 253 257 mpbird 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( ( N - m ) / 2 ) < ( M + 1 ) )
259 zleltp1 
 |-  ( ( ( ( N - m ) / 2 ) e. ZZ /\ M e. ZZ ) -> ( ( ( N - m ) / 2 ) <_ M <-> ( ( N - m ) / 2 ) < ( M + 1 ) ) )
260 235 197 259 syl2anc 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( ( ( N - m ) / 2 ) <_ M <-> ( ( N - m ) / 2 ) < ( M + 1 ) ) )
261 258 260 mpbird 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( ( N - m ) / 2 ) <_ M )
262 195 197 235 242 261 elfzd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( ( N - m ) / 2 ) e. ( 0 ... M ) )
263 oveq2 
 |-  ( k = ( ( N - m ) / 2 ) -> ( 2 x. k ) = ( 2 x. ( ( N - m ) / 2 ) ) )
264 263 oveq2d 
 |-  ( k = ( ( N - m ) / 2 ) -> ( N - ( 2 x. k ) ) = ( N - ( 2 x. ( ( N - m ) / 2 ) ) ) )
265 ovex 
 |-  ( N - ( 2 x. ( ( N - m ) / 2 ) ) ) e. _V
266 264 134 265 fvmpt 
 |-  ( ( ( N - m ) / 2 ) e. ( 0 ... M ) -> ( ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) ` ( ( N - m ) / 2 ) ) = ( N - ( 2 x. ( ( N - m ) / 2 ) ) ) )
267 262 266 syl 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) ` ( ( N - m ) / 2 ) ) = ( N - ( 2 x. ( ( N - m ) / 2 ) ) ) )
268 236 nn0cnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( N - m ) e. CC )
269 268 212 229 divcan2d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( 2 x. ( ( N - m ) / 2 ) ) = ( N - m ) )
270 269 oveq2d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( N - ( 2 x. ( ( N - m ) / 2 ) ) ) = ( N - ( N - m ) ) )
271 198 200 nncand 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( N - ( N - m ) ) = m )
272 267 270 271 3eqtrd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) ` ( ( N - m ) / 2 ) ) = m )
273 138 ffnd 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) Fn ( 0 ... M ) )
274 fnfvelrn 
 |-  ( ( ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) Fn ( 0 ... M ) /\ ( ( N - m ) / 2 ) e. ( 0 ... M ) ) -> ( ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) ` ( ( N - m ) / 2 ) ) e. ran ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) )
275 273 262 274 syl2an2r 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) ` ( ( N - m ) / 2 ) ) e. ran ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) )
276 272 275 eqeltrrd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> m e. ran ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) )
277 276 expr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ m e. ( 0 ... N ) ) -> ( ( ( m + 1 ) / 2 ) e. ZZ -> m e. ran ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) ) )
278 194 277 orim12d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ m e. ( 0 ... N ) ) -> ( ( ( m / 2 ) e. ZZ \/ ( ( m + 1 ) / 2 ) e. ZZ ) -> ( ( _i ^ m ) e. RR \/ m e. ran ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) ) ) )
279 167 278 mpd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ m e. ( 0 ... N ) ) -> ( ( _i ^ m ) e. RR \/ m e. ran ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) ) )
280 279 orcomd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ m e. ( 0 ... N ) ) -> ( m e. ran ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) \/ ( _i ^ m ) e. RR ) )
281 280 ord 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ m e. ( 0 ... N ) ) -> ( -. m e. ran ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) -> ( _i ^ m ) e. RR ) )
282 281 impr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ -. m e. ran ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) ) ) -> ( _i ^ m ) e. RR )
283 163 282 sylan2b 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ m e. ( ( 0 ... N ) \ ran ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) ) ) -> ( _i ^ m ) e. RR )
284 162 283 remulcld 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ m e. ( ( 0 ... N ) \ ran ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) ) ) -> ( ( ( 1 / ( tan ` A ) ) ^ ( N - m ) ) x. ( _i ^ m ) ) e. RR )
285 161 284 remulcld 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ m e. ( ( 0 ... N ) \ ran ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) ) ) -> ( ( N _C m ) x. ( ( ( 1 / ( tan ` A ) ) ^ ( N - m ) ) x. ( _i ^ m ) ) ) e. RR )
286 285 reim0d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ m e. ( ( 0 ... N ) \ ran ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) ) ) -> ( Im ` ( ( N _C m ) x. ( ( ( 1 / ( tan ` A ) ) ^ ( N - m ) ) x. ( _i ^ m ) ) ) ) = 0 )
287 fzfid 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( 0 ... N ) e. Fin )
288 139 157 286 287 fsumss 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> sum_ m e. ran ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) ( Im ` ( ( N _C m ) x. ( ( ( 1 / ( tan ` A ) ) ^ ( N - m ) ) x. ( _i ^ m ) ) ) ) = sum_ m e. ( 0 ... N ) ( Im ` ( ( N _C m ) x. ( ( ( 1 / ( tan ` A ) ) ^ ( N - m ) ) x. ( _i ^ m ) ) ) ) )
289 elfznn0 
 |-  ( j e. ( 0 ... M ) -> j e. NN0 )
290 289 adantl 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> j e. NN0 )
291 nn0mulcl 
 |-  ( ( 2 e. NN0 /\ j e. NN0 ) -> ( 2 x. j ) e. NN0 )
292 76 290 291 sylancr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( 2 x. j ) e. NN0 )
293 292 nn0zd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( 2 x. j ) e. ZZ )
294 bccl 
 |-  ( ( N e. NN0 /\ ( 2 x. j ) e. ZZ ) -> ( N _C ( 2 x. j ) ) e. NN0 )
295 15 293 294 syl2an2r 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( N _C ( 2 x. j ) ) e. NN0 )
296 295 nn0red 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( N _C ( 2 x. j ) ) e. RR )
297 fznn0sub 
 |-  ( j e. ( 0 ... M ) -> ( M - j ) e. NN0 )
298 297 adantl 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( M - j ) e. NN0 )
299 reexpcl 
 |-  ( ( -u 1 e. RR /\ ( M - j ) e. NN0 ) -> ( -u 1 ^ ( M - j ) ) e. RR )
300 190 298 299 sylancr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( -u 1 ^ ( M - j ) ) e. RR )
301 296 300 remulcld 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) e. RR )
302 2z 
 |-  2 e. ZZ
303 znegcl 
 |-  ( 2 e. ZZ -> -u 2 e. ZZ )
304 302 303 ax-mp 
 |-  -u 2 e. ZZ
305 rpexpcl 
 |-  ( ( ( tan ` A ) e. RR+ /\ -u 2 e. ZZ ) -> ( ( tan ` A ) ^ -u 2 ) e. RR+ )
306 4 304 305 sylancl 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( ( tan ` A ) ^ -u 2 ) e. RR+ )
307 306 rpred 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( ( tan ` A ) ^ -u 2 ) e. RR )
308 reexpcl 
 |-  ( ( ( ( tan ` A ) ^ -u 2 ) e. RR /\ j e. NN0 ) -> ( ( ( tan ` A ) ^ -u 2 ) ^ j ) e. RR )
309 307 289 308 syl2an 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( ( ( tan ` A ) ^ -u 2 ) ^ j ) e. RR )
310 301 309 remulcld 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) e. RR )
311 310 recnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) e. CC )
312 mulcl 
 |-  ( ( _i e. CC /\ ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) e. CC ) -> ( _i x. ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) ) e. CC )
313 7 311 312 sylancr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( _i x. ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) ) e. CC )
314 313 addid2d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( 0 + ( _i x. ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) ) ) = ( _i x. ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) ) )
315 295 nn0cnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( N _C ( 2 x. j ) ) e. CC )
316 300 recnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( -u 1 ^ ( M - j ) ) e. CC )
317 309 recnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( ( ( tan ` A ) ^ -u 2 ) ^ j ) e. CC )
318 315 316 317 mulassd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) = ( ( N _C ( 2 x. j ) ) x. ( ( -u 1 ^ ( M - j ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) ) )
319 318 oveq2d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( _i x. ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) ) = ( _i x. ( ( N _C ( 2 x. j ) ) x. ( ( -u 1 ^ ( M - j ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) ) ) )
320 7 a1i 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> _i e. CC )
321 316 317 mulcld 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( ( -u 1 ^ ( M - j ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) e. CC )
322 320 315 321 mul12d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( _i x. ( ( N _C ( 2 x. j ) ) x. ( ( -u 1 ^ ( M - j ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) ) ) = ( ( N _C ( 2 x. j ) ) x. ( _i x. ( ( -u 1 ^ ( M - j ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) ) ) )
323 319 322 eqtrd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( _i x. ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) ) = ( ( N _C ( 2 x. j ) ) x. ( _i x. ( ( -u 1 ^ ( M - j ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) ) ) )
324 bccmpl 
 |-  ( ( N e. NN0 /\ ( 2 x. j ) e. ZZ ) -> ( N _C ( 2 x. j ) ) = ( N _C ( N - ( 2 x. j ) ) ) )
325 15 293 324 syl2an2r 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( N _C ( 2 x. j ) ) = ( N _C ( N - ( 2 x. j ) ) ) )
326 109 adantr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> N e. CC )
327 292 nn0cnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( 2 x. j ) e. CC )
328 326 327 nncand 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( N - ( N - ( 2 x. j ) ) ) = ( 2 x. j ) )
329 328 oveq2d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( ( 1 / ( tan ` A ) ) ^ ( N - ( N - ( 2 x. j ) ) ) ) = ( ( 1 / ( tan ` A ) ) ^ ( 2 x. j ) ) )
330 4 adantr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( tan ` A ) e. RR+ )
331 330 rpcnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( tan ` A ) e. CC )
332 expneg 
 |-  ( ( ( tan ` A ) e. CC /\ ( 2 x. j ) e. NN0 ) -> ( ( tan ` A ) ^ -u ( 2 x. j ) ) = ( 1 / ( ( tan ` A ) ^ ( 2 x. j ) ) ) )
333 331 292 332 syl2anc 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( ( tan ` A ) ^ -u ( 2 x. j ) ) = ( 1 / ( ( tan ` A ) ^ ( 2 x. j ) ) ) )
334 290 nn0cnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> j e. CC )
335 mulneg1 
 |-  ( ( 2 e. CC /\ j e. CC ) -> ( -u 2 x. j ) = -u ( 2 x. j ) )
336 111 334 335 sylancr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( -u 2 x. j ) = -u ( 2 x. j ) )
337 336 oveq2d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( ( tan ` A ) ^ ( -u 2 x. j ) ) = ( ( tan ` A ) ^ -u ( 2 x. j ) ) )
338 330 rpne0d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( tan ` A ) =/= 0 )
339 331 338 293 exprecd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( ( 1 / ( tan ` A ) ) ^ ( 2 x. j ) ) = ( 1 / ( ( tan ` A ) ^ ( 2 x. j ) ) ) )
340 333 337 339 3eqtr4d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( ( tan ` A ) ^ ( -u 2 x. j ) ) = ( ( 1 / ( tan ` A ) ) ^ ( 2 x. j ) ) )
341 304 a1i 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> -u 2 e. ZZ )
342 290 nn0zd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> j e. ZZ )
343 expmulz 
 |-  ( ( ( ( tan ` A ) e. CC /\ ( tan ` A ) =/= 0 ) /\ ( -u 2 e. ZZ /\ j e. ZZ ) ) -> ( ( tan ` A ) ^ ( -u 2 x. j ) ) = ( ( ( tan ` A ) ^ -u 2 ) ^ j ) )
344 331 338 341 342 343 syl22anc 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( ( tan ` A ) ^ ( -u 2 x. j ) ) = ( ( ( tan ` A ) ^ -u 2 ) ^ j ) )
345 329 340 344 3eqtr2d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( ( 1 / ( tan ` A ) ) ^ ( N - ( N - ( 2 x. j ) ) ) ) = ( ( ( tan ` A ) ^ -u 2 ) ^ j ) )
346 1 oveq1i 
 |-  ( N - ( 2 x. j ) ) = ( ( ( 2 x. M ) + 1 ) - ( 2 x. j ) )
347 12 adantr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( 2 x. M ) e. NN )
348 347 nncnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( 2 x. M ) e. CC )
349 1cnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> 1 e. CC )
350 348 349 327 addsubd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( ( ( 2 x. M ) + 1 ) - ( 2 x. j ) ) = ( ( ( 2 x. M ) - ( 2 x. j ) ) + 1 ) )
351 2cnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> 2 e. CC )
352 213 ad2antrr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> M e. CC )
353 351 352 334 subdid 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( 2 x. ( M - j ) ) = ( ( 2 x. M ) - ( 2 x. j ) ) )
354 353 oveq1d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( ( 2 x. ( M - j ) ) + 1 ) = ( ( ( 2 x. M ) - ( 2 x. j ) ) + 1 ) )
355 350 354 eqtr4d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( ( ( 2 x. M ) + 1 ) - ( 2 x. j ) ) = ( ( 2 x. ( M - j ) ) + 1 ) )
356 346 355 eqtrid 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( N - ( 2 x. j ) ) = ( ( 2 x. ( M - j ) ) + 1 ) )
357 356 oveq2d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( _i ^ ( N - ( 2 x. j ) ) ) = ( _i ^ ( ( 2 x. ( M - j ) ) + 1 ) ) )
358 nn0mulcl 
 |-  ( ( 2 e. NN0 /\ ( M - j ) e. NN0 ) -> ( 2 x. ( M - j ) ) e. NN0 )
359 76 298 358 sylancr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( 2 x. ( M - j ) ) e. NN0 )
360 expp1 
 |-  ( ( _i e. CC /\ ( 2 x. ( M - j ) ) e. NN0 ) -> ( _i ^ ( ( 2 x. ( M - j ) ) + 1 ) ) = ( ( _i ^ ( 2 x. ( M - j ) ) ) x. _i ) )
361 7 359 360 sylancr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( _i ^ ( ( 2 x. ( M - j ) ) + 1 ) ) = ( ( _i ^ ( 2 x. ( M - j ) ) ) x. _i ) )
362 76 a1i 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> 2 e. NN0 )
363 320 298 362 expmuld 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( _i ^ ( 2 x. ( M - j ) ) ) = ( ( _i ^ 2 ) ^ ( M - j ) ) )
364 168 oveq1i 
 |-  ( ( _i ^ 2 ) ^ ( M - j ) ) = ( -u 1 ^ ( M - j ) )
365 363 364 eqtrdi 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( _i ^ ( 2 x. ( M - j ) ) ) = ( -u 1 ^ ( M - j ) ) )
366 365 oveq1d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( ( _i ^ ( 2 x. ( M - j ) ) ) x. _i ) = ( ( -u 1 ^ ( M - j ) ) x. _i ) )
367 357 361 366 3eqtrd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( _i ^ ( N - ( 2 x. j ) ) ) = ( ( -u 1 ^ ( M - j ) ) x. _i ) )
368 mulcom 
 |-  ( ( ( -u 1 ^ ( M - j ) ) e. CC /\ _i e. CC ) -> ( ( -u 1 ^ ( M - j ) ) x. _i ) = ( _i x. ( -u 1 ^ ( M - j ) ) ) )
369 316 7 368 sylancl 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( ( -u 1 ^ ( M - j ) ) x. _i ) = ( _i x. ( -u 1 ^ ( M - j ) ) ) )
370 367 369 eqtrd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( _i ^ ( N - ( 2 x. j ) ) ) = ( _i x. ( -u 1 ^ ( M - j ) ) ) )
371 345 370 oveq12d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( ( ( 1 / ( tan ` A ) ) ^ ( N - ( N - ( 2 x. j ) ) ) ) x. ( _i ^ ( N - ( 2 x. j ) ) ) ) = ( ( ( ( tan ` A ) ^ -u 2 ) ^ j ) x. ( _i x. ( -u 1 ^ ( M - j ) ) ) ) )
372 mulcl 
 |-  ( ( _i e. CC /\ ( -u 1 ^ ( M - j ) ) e. CC ) -> ( _i x. ( -u 1 ^ ( M - j ) ) ) e. CC )
373 7 316 372 sylancr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( _i x. ( -u 1 ^ ( M - j ) ) ) e. CC )
374 373 317 mulcomd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( ( _i x. ( -u 1 ^ ( M - j ) ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) = ( ( ( ( tan ` A ) ^ -u 2 ) ^ j ) x. ( _i x. ( -u 1 ^ ( M - j ) ) ) ) )
375 320 316 317 mulassd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( ( _i x. ( -u 1 ^ ( M - j ) ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) = ( _i x. ( ( -u 1 ^ ( M - j ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) ) )
376 371 374 375 3eqtr2rd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( _i x. ( ( -u 1 ^ ( M - j ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) ) = ( ( ( 1 / ( tan ` A ) ) ^ ( N - ( N - ( 2 x. j ) ) ) ) x. ( _i ^ ( N - ( 2 x. j ) ) ) ) )
377 325 376 oveq12d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( ( N _C ( 2 x. j ) ) x. ( _i x. ( ( -u 1 ^ ( M - j ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) ) ) = ( ( N _C ( N - ( 2 x. j ) ) ) x. ( ( ( 1 / ( tan ` A ) ) ^ ( N - ( N - ( 2 x. j ) ) ) ) x. ( _i ^ ( N - ( 2 x. j ) ) ) ) ) )
378 314 323 377 3eqtrd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( 0 + ( _i x. ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) ) ) = ( ( N _C ( N - ( 2 x. j ) ) ) x. ( ( ( 1 / ( tan ` A ) ) ^ ( N - ( N - ( 2 x. j ) ) ) ) x. ( _i ^ ( N - ( 2 x. j ) ) ) ) ) )
379 378 fveq2d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( Im ` ( 0 + ( _i x. ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) ) ) ) = ( Im ` ( ( N _C ( N - ( 2 x. j ) ) ) x. ( ( ( 1 / ( tan ` A ) ) ^ ( N - ( N - ( 2 x. j ) ) ) ) x. ( _i ^ ( N - ( 2 x. j ) ) ) ) ) ) )
380 0re 
 |-  0 e. RR
381 crim 
 |-  ( ( 0 e. RR /\ ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) e. RR ) -> ( Im ` ( 0 + ( _i x. ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) ) ) ) = ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) )
382 380 310 381 sylancr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( Im ` ( 0 + ( _i x. ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) ) ) ) = ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) )
383 379 382 eqtr3d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( Im ` ( ( N _C ( N - ( 2 x. j ) ) ) x. ( ( ( 1 / ( tan ` A ) ) ^ ( N - ( N - ( 2 x. j ) ) ) ) x. ( _i ^ ( N - ( 2 x. j ) ) ) ) ) ) = ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) )
384 383 sumeq2dv 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> sum_ j e. ( 0 ... M ) ( Im ` ( ( N _C ( N - ( 2 x. j ) ) ) x. ( ( ( 1 / ( tan ` A ) ) ^ ( N - ( N - ( 2 x. j ) ) ) ) x. ( _i ^ ( N - ( 2 x. j ) ) ) ) ) ) = sum_ j e. ( 0 ... M ) ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) )
385 158 288 384 3eqtr3d 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> sum_ m e. ( 0 ... N ) ( Im ` ( ( N _C m ) x. ( ( ( 1 / ( tan ` A ) ) ^ ( N - m ) ) x. ( _i ^ m ) ) ) ) = sum_ j e. ( 0 ... M ) ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) )
386 287 154 fsumim 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( Im ` sum_ m e. ( 0 ... N ) ( ( N _C m ) x. ( ( ( 1 / ( tan ` A ) ) ^ ( N - m ) ) x. ( _i ^ m ) ) ) ) = sum_ m e. ( 0 ... N ) ( Im ` ( ( N _C m ) x. ( ( ( 1 / ( tan ` A ) ) ^ ( N - m ) ) x. ( _i ^ m ) ) ) ) )
387 306 rpcnd 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( ( tan ` A ) ^ -u 2 ) e. CC )
388 oveq1 
 |-  ( t = ( ( tan ` A ) ^ -u 2 ) -> ( t ^ j ) = ( ( ( tan ` A ) ^ -u 2 ) ^ j ) )
389 388 oveq2d 
 |-  ( t = ( ( tan ` A ) ^ -u 2 ) -> ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( t ^ j ) ) = ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) )
390 389 sumeq2sdv 
 |-  ( t = ( ( tan ` A ) ^ -u 2 ) -> sum_ j e. ( 0 ... M ) ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( t ^ j ) ) = sum_ j e. ( 0 ... M ) ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) )
391 sumex 
 |-  sum_ j e. ( 0 ... M ) ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) e. _V
392 390 2 391 fvmpt 
 |-  ( ( ( tan ` A ) ^ -u 2 ) e. CC -> ( P ` ( ( tan ` A ) ^ -u 2 ) ) = sum_ j e. ( 0 ... M ) ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) )
393 387 392 syl 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( P ` ( ( tan ` A ) ^ -u 2 ) ) = sum_ j e. ( 0 ... M ) ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) )
394 385 386 393 3eqtr4d 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( Im ` sum_ m e. ( 0 ... N ) ( ( N _C m ) x. ( ( ( 1 / ( tan ` A ) ) ^ ( N - m ) ) x. ( _i ^ m ) ) ) ) = ( P ` ( ( tan ` A ) ^ -u 2 ) ) )
395 52 59 rerpdivcld 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( ( cos ` ( N x. A ) ) / ( ( sin ` A ) ^ N ) ) e. RR )
396 54 59 rerpdivcld 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( ( sin ` ( N x. A ) ) / ( ( sin ` A ) ^ N ) ) e. RR )
397 395 396 crimd 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( Im ` ( ( ( cos ` ( N x. A ) ) / ( ( sin ` A ) ^ N ) ) + ( _i x. ( ( sin ` ( N x. A ) ) / ( ( sin ` A ) ^ N ) ) ) ) ) = ( ( sin ` ( N x. A ) ) / ( ( sin ` A ) ^ N ) ) )
398 67 394 397 3eqtr3d 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( P ` ( ( tan ` A ) ^ -u 2 ) ) = ( ( sin ` ( N x. A ) ) / ( ( sin ` A ) ^ N ) ) )