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 sseldi 
 |-  ( ( ( 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 syl5eqr 
 |-  ( ( ( 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 145 ad2antrl 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( N - m ) e. NN0 )
196 nn0re 
 |-  ( ( N - m ) e. NN0 -> ( N - m ) e. RR )
197 nn0ge0 
 |-  ( ( N - m ) e. NN0 -> 0 <_ ( N - m ) )
198 divge0 
 |-  ( ( ( ( N - m ) e. RR /\ 0 <_ ( N - m ) ) /\ ( 2 e. RR /\ 0 < 2 ) ) -> 0 <_ ( ( N - m ) / 2 ) )
199 90 91 198 mpanr12 
 |-  ( ( ( N - m ) e. RR /\ 0 <_ ( N - m ) ) -> 0 <_ ( ( N - m ) / 2 ) )
200 196 197 199 syl2anc 
 |-  ( ( N - m ) e. NN0 -> 0 <_ ( ( N - m ) / 2 ) )
201 195 200 syl 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> 0 <_ ( ( N - m ) / 2 ) )
202 195 nn0red 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( N - m ) e. RR )
203 50 adantr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> N e. RR )
204 peano2re 
 |-  ( N e. RR -> ( N + 1 ) e. RR )
205 203 204 syl 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( N + 1 ) e. RR )
206 149 ad2antrl 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> m e. NN0 )
207 206 173 syl 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> 0 <_ m )
208 206 nn0red 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> m e. RR )
209 203 208 subge02d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( 0 <_ m <-> ( N - m ) <_ N ) )
210 207 209 mpbid 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( N - m ) <_ N )
211 203 ltp1d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> N < ( N + 1 ) )
212 202 203 205 210 211 lelttrd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( N - m ) < ( N + 1 ) )
213 2t1e2 
 |-  ( 2 x. 1 ) = 2
214 df-2 
 |-  2 = ( 1 + 1 )
215 213 214 eqtr2i 
 |-  ( 1 + 1 ) = ( 2 x. 1 )
216 215 oveq2i 
 |-  ( ( 2 x. M ) + ( 1 + 1 ) ) = ( ( 2 x. M ) + ( 2 x. 1 ) )
217 1 oveq1i 
 |-  ( N + 1 ) = ( ( ( 2 x. M ) + 1 ) + 1 )
218 12 nncnd 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( 2 x. M ) e. CC )
219 218 adantr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( 2 x. M ) e. CC )
220 1cnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> 1 e. CC )
221 219 220 220 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 ) ) )
222 217 221 syl5eq 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( N + 1 ) = ( ( 2 x. M ) + ( 1 + 1 ) ) )
223 2cnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> 2 e. CC )
224 nncn 
 |-  ( M e. NN -> M e. CC )
225 224 ad2antrr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> M e. CC )
226 223 225 220 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 ) ) )
227 216 222 226 3eqtr4a 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( N + 1 ) = ( 2 x. ( M + 1 ) ) )
228 212 227 breqtrd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( N - m ) < ( 2 x. ( M + 1 ) ) )
229 nnz 
 |-  ( M e. NN -> M e. ZZ )
230 229 ad2antrr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> M e. ZZ )
231 230 peano2zd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( M + 1 ) e. ZZ )
232 231 zred 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( M + 1 ) e. RR )
233 92 a1i 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( 2 e. RR /\ 0 < 2 ) )
234 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 ) ) ) )
235 202 232 233 234 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 ) ) ) )
236 228 235 mpbird 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( ( N - m ) / 2 ) < ( M + 1 ) )
237 109 adantr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> N e. CC )
238 206 nn0cnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> m e. CC )
239 237 238 220 pnpcan2d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( ( N + 1 ) - ( m + 1 ) ) = ( N - m ) )
240 227 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 ) ) )
241 239 240 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 ) ) )
242 241 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 ) )
243 231 zcnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( M + 1 ) e. CC )
244 mulcl 
 |-  ( ( 2 e. CC /\ ( M + 1 ) e. CC ) -> ( 2 x. ( M + 1 ) ) e. CC )
245 111 243 244 sylancr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( 2 x. ( M + 1 ) ) e. CC )
246 peano2cn 
 |-  ( m e. CC -> ( m + 1 ) e. CC )
247 238 246 syl 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( m + 1 ) e. CC )
248 123 a1i 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( 2 e. CC /\ 2 =/= 0 ) )
249 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 ) ) )
250 245 247 248 249 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 ) ) )
251 183 a1i 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> 2 =/= 0 )
252 243 223 251 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 ) )
253 252 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 ) ) )
254 242 250 253 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 ) ) )
255 simprr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( ( m + 1 ) / 2 ) e. ZZ )
256 231 255 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 )
257 254 256 eqeltrd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( ( N - m ) / 2 ) e. ZZ )
258 zleltp1 
 |-  ( ( ( ( N - m ) / 2 ) e. ZZ /\ M e. ZZ ) -> ( ( ( N - m ) / 2 ) <_ M <-> ( ( N - m ) / 2 ) < ( M + 1 ) ) )
259 257 230 258 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 ) ) )
260 236 259 mpbird 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( ( N - m ) / 2 ) <_ M )
261 0zd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> 0 e. ZZ )
262 elfz 
 |-  ( ( ( ( N - m ) / 2 ) e. ZZ /\ 0 e. ZZ /\ M e. ZZ ) -> ( ( ( N - m ) / 2 ) e. ( 0 ... M ) <-> ( 0 <_ ( ( N - m ) / 2 ) /\ ( ( N - m ) / 2 ) <_ M ) ) )
263 257 261 230 262 syl3anc 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( ( ( N - m ) / 2 ) e. ( 0 ... M ) <-> ( 0 <_ ( ( N - m ) / 2 ) /\ ( ( N - m ) / 2 ) <_ M ) ) )
264 201 260 263 mpbir2and 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( ( N - m ) / 2 ) e. ( 0 ... M ) )
265 oveq2 
 |-  ( k = ( ( N - m ) / 2 ) -> ( 2 x. k ) = ( 2 x. ( ( N - m ) / 2 ) ) )
266 265 oveq2d 
 |-  ( k = ( ( N - m ) / 2 ) -> ( N - ( 2 x. k ) ) = ( N - ( 2 x. ( ( N - m ) / 2 ) ) ) )
267 ovex 
 |-  ( N - ( 2 x. ( ( N - m ) / 2 ) ) ) e. _V
268 266 134 267 fvmpt 
 |-  ( ( ( N - m ) / 2 ) e. ( 0 ... M ) -> ( ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) ` ( ( N - m ) / 2 ) ) = ( N - ( 2 x. ( ( N - m ) / 2 ) ) ) )
269 264 268 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 ) ) ) )
270 195 nn0cnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( N - m ) e. CC )
271 270 223 251 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 ) )
272 271 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 ) ) )
273 237 238 nncand 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( m + 1 ) / 2 ) e. ZZ ) ) -> ( N - ( N - m ) ) = m )
274 269 272 273 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 )
275 138 ffnd 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( k e. ( 0 ... M ) |-> ( N - ( 2 x. k ) ) ) Fn ( 0 ... M ) )
276 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 ) ) ) )
277 275 264 276 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 ) ) ) )
278 274 277 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 ) ) ) )
279 278 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 ) ) ) ) )
280 194 279 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 ) ) ) ) ) )
281 167 280 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 ) ) ) ) )
282 281 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 ) )
283 282 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 ) )
284 283 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 )
285 163 284 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 )
286 162 285 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 )
287 161 286 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 )
288 287 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 )
289 fzfid 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( 0 ... N ) e. Fin )
290 139 157 288 289 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 ) ) ) ) )
291 elfznn0 
 |-  ( j e. ( 0 ... M ) -> j e. NN0 )
292 291 adantl 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> j e. NN0 )
293 nn0mulcl 
 |-  ( ( 2 e. NN0 /\ j e. NN0 ) -> ( 2 x. j ) e. NN0 )
294 76 292 293 sylancr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( 2 x. j ) e. NN0 )
295 294 nn0zd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( 2 x. j ) e. ZZ )
296 bccl 
 |-  ( ( N e. NN0 /\ ( 2 x. j ) e. ZZ ) -> ( N _C ( 2 x. j ) ) e. NN0 )
297 15 295 296 syl2an2r 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( N _C ( 2 x. j ) ) e. NN0 )
298 297 nn0red 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( N _C ( 2 x. j ) ) e. RR )
299 fznn0sub 
 |-  ( j e. ( 0 ... M ) -> ( M - j ) e. NN0 )
300 299 adantl 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( M - j ) e. NN0 )
301 reexpcl 
 |-  ( ( -u 1 e. RR /\ ( M - j ) e. NN0 ) -> ( -u 1 ^ ( M - j ) ) e. RR )
302 190 300 301 sylancr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( -u 1 ^ ( M - j ) ) e. RR )
303 298 302 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 )
304 2z 
 |-  2 e. ZZ
305 znegcl 
 |-  ( 2 e. ZZ -> -u 2 e. ZZ )
306 304 305 ax-mp 
 |-  -u 2 e. ZZ
307 rpexpcl 
 |-  ( ( ( tan ` A ) e. RR+ /\ -u 2 e. ZZ ) -> ( ( tan ` A ) ^ -u 2 ) e. RR+ )
308 4 306 307 sylancl 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( ( tan ` A ) ^ -u 2 ) e. RR+ )
309 308 rpred 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( ( tan ` A ) ^ -u 2 ) e. RR )
310 reexpcl 
 |-  ( ( ( ( tan ` A ) ^ -u 2 ) e. RR /\ j e. NN0 ) -> ( ( ( tan ` A ) ^ -u 2 ) ^ j ) e. RR )
311 309 291 310 syl2an 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( ( ( tan ` A ) ^ -u 2 ) ^ j ) e. RR )
312 303 311 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 )
313 312 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 )
314 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 )
315 7 313 314 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 )
316 315 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 ) ) ) )
317 297 nn0cnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( N _C ( 2 x. j ) ) e. CC )
318 302 recnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( -u 1 ^ ( M - j ) ) e. CC )
319 311 recnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( ( ( tan ` A ) ^ -u 2 ) ^ j ) e. CC )
320 317 318 319 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 ) ) ) )
321 320 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 ) ) ) ) )
322 7 a1i 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> _i e. CC )
323 318 319 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 )
324 322 317 323 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 ) ) ) ) )
325 321 324 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 ) ) ) ) )
326 bccmpl 
 |-  ( ( N e. NN0 /\ ( 2 x. j ) e. ZZ ) -> ( N _C ( 2 x. j ) ) = ( N _C ( N - ( 2 x. j ) ) ) )
327 15 295 326 syl2an2r 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( N _C ( 2 x. j ) ) = ( N _C ( N - ( 2 x. j ) ) ) )
328 109 adantr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> N e. CC )
329 294 nn0cnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( 2 x. j ) e. CC )
330 328 329 nncand 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( N - ( N - ( 2 x. j ) ) ) = ( 2 x. j ) )
331 330 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 ) ) )
332 4 adantr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( tan ` A ) e. RR+ )
333 332 rpcnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( tan ` A ) e. CC )
334 expneg 
 |-  ( ( ( tan ` A ) e. CC /\ ( 2 x. j ) e. NN0 ) -> ( ( tan ` A ) ^ -u ( 2 x. j ) ) = ( 1 / ( ( tan ` A ) ^ ( 2 x. j ) ) ) )
335 333 294 334 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 ) ) ) )
336 292 nn0cnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> j e. CC )
337 mulneg1 
 |-  ( ( 2 e. CC /\ j e. CC ) -> ( -u 2 x. j ) = -u ( 2 x. j ) )
338 111 336 337 sylancr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( -u 2 x. j ) = -u ( 2 x. j ) )
339 338 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 ) ) )
340 332 rpne0d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( tan ` A ) =/= 0 )
341 333 340 295 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 ) ) ) )
342 335 339 341 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 ) ) )
343 306 a1i 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> -u 2 e. ZZ )
344 292 nn0zd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> j e. ZZ )
345 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 ) )
346 333 340 343 344 345 syl22anc 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( ( tan ` A ) ^ ( -u 2 x. j ) ) = ( ( ( tan ` A ) ^ -u 2 ) ^ j ) )
347 331 342 346 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 ) )
348 1 oveq1i 
 |-  ( N - ( 2 x. j ) ) = ( ( ( 2 x. M ) + 1 ) - ( 2 x. j ) )
349 12 adantr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( 2 x. M ) e. NN )
350 349 nncnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( 2 x. M ) e. CC )
351 1cnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> 1 e. CC )
352 350 351 329 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 ) )
353 2cnd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> 2 e. CC )
354 224 ad2antrr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> M e. CC )
355 353 354 336 subdid 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( 2 x. ( M - j ) ) = ( ( 2 x. M ) - ( 2 x. j ) ) )
356 355 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 ) )
357 352 356 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 ) )
358 348 357 syl5eq 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( N - ( 2 x. j ) ) = ( ( 2 x. ( M - j ) ) + 1 ) )
359 358 oveq2d 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( _i ^ ( N - ( 2 x. j ) ) ) = ( _i ^ ( ( 2 x. ( M - j ) ) + 1 ) ) )
360 nn0mulcl 
 |-  ( ( 2 e. NN0 /\ ( M - j ) e. NN0 ) -> ( 2 x. ( M - j ) ) e. NN0 )
361 76 300 360 sylancr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( 2 x. ( M - j ) ) e. NN0 )
362 expp1 
 |-  ( ( _i e. CC /\ ( 2 x. ( M - j ) ) e. NN0 ) -> ( _i ^ ( ( 2 x. ( M - j ) ) + 1 ) ) = ( ( _i ^ ( 2 x. ( M - j ) ) ) x. _i ) )
363 7 361 362 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 ) )
364 76 a1i 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> 2 e. NN0 )
365 322 300 364 expmuld 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( _i ^ ( 2 x. ( M - j ) ) ) = ( ( _i ^ 2 ) ^ ( M - j ) ) )
366 168 oveq1i 
 |-  ( ( _i ^ 2 ) ^ ( M - j ) ) = ( -u 1 ^ ( M - j ) )
367 365 366 syl6eq 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( _i ^ ( 2 x. ( M - j ) ) ) = ( -u 1 ^ ( M - j ) ) )
368 367 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 ) )
369 359 363 368 3eqtrd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( _i ^ ( N - ( 2 x. j ) ) ) = ( ( -u 1 ^ ( M - j ) ) x. _i ) )
370 mulcom 
 |-  ( ( ( -u 1 ^ ( M - j ) ) e. CC /\ _i e. CC ) -> ( ( -u 1 ^ ( M - j ) ) x. _i ) = ( _i x. ( -u 1 ^ ( M - j ) ) ) )
371 318 7 370 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 ) ) ) )
372 369 371 eqtrd 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( _i ^ ( N - ( 2 x. j ) ) ) = ( _i x. ( -u 1 ^ ( M - j ) ) ) )
373 347 372 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 ) ) ) ) )
374 mulcl 
 |-  ( ( _i e. CC /\ ( -u 1 ^ ( M - j ) ) e. CC ) -> ( _i x. ( -u 1 ^ ( M - j ) ) ) e. CC )
375 7 318 374 sylancr 
 |-  ( ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) /\ j e. ( 0 ... M ) ) -> ( _i x. ( -u 1 ^ ( M - j ) ) ) e. CC )
376 375 319 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 ) ) ) ) )
377 322 318 319 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 ) ) ) )
378 373 376 377 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 ) ) ) ) )
379 327 378 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 ) ) ) ) ) )
380 316 325 379 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 ) ) ) ) ) )
381 380 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 ) ) ) ) ) ) )
382 0re 
 |-  0 e. RR
383 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 ) ) )
384 382 312 383 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 ) ) )
385 381 384 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 ) ) )
386 385 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 ) ) )
387 158 290 386 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 ) ) )
388 289 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 ) ) ) ) )
389 308 rpcnd 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( ( tan ` A ) ^ -u 2 ) e. CC )
390 oveq1 
 |-  ( t = ( ( tan ` A ) ^ -u 2 ) -> ( t ^ j ) = ( ( ( tan ` A ) ^ -u 2 ) ^ j ) )
391 390 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 ) ) )
392 391 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 ) ) )
393 sumex 
 |-  sum_ j e. ( 0 ... M ) ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( ( ( tan ` A ) ^ -u 2 ) ^ j ) ) e. _V
394 392 2 393 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 ) ) )
395 389 394 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 ) ) )
396 387 388 395 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 ) ) )
397 52 59 rerpdivcld 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( ( cos ` ( N x. A ) ) / ( ( sin ` A ) ^ N ) ) e. RR )
398 54 59 rerpdivcld 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( ( sin ` ( N x. A ) ) / ( ( sin ` A ) ^ N ) ) e. RR )
399 397 398 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 ) ) )
400 67 396 399 3eqtr3d 
 |-  ( ( M e. NN /\ A e. ( 0 (,) ( _pi / 2 ) ) ) -> ( P ` ( ( tan ` A ) ^ -u 2 ) ) = ( ( sin ` ( N x. A ) ) / ( ( sin ` A ) ^ N ) ) )