MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  basellem3 Unicode version

Theorem basellem3 20732
Description: Lemma for basel 20739. 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
) ( N  _C  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.)
Hypotheses
Ref Expression
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
Ref Expression
basellem3  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( P `  ( ( tan `  A
) ^ -u 2
) )  =  ( ( sin `  ( N  x.  A )
)  /  ( ( sin `  A ) ^ N ) ) )
Distinct variable groups:    t, j, A    j, M, t    j, N, t
Allowed substitution hints:    P( t, j)

Proof of Theorem basellem3
Dummy variables  k  m are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tanrpcl 20279 . . . . . . . 8  |-  ( A  e.  ( 0 (,) ( pi  /  2
) )  ->  ( tan `  A )  e.  RR+ )
21adantl 453 . . . . . . 7  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( tan `  A
)  e.  RR+ )
32rpreccld 10590 . . . . . 6  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( 1  / 
( tan `  A
) )  e.  RR+ )
43rpcnd 10582 . . . . 5  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( 1  / 
( tan `  A
) )  e.  CC )
5 ax-icn 8982 . . . . . 6  |-  _i  e.  CC
65a1i 11 . . . . 5  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  _i  e.  CC )
7 basel.n . . . . . . 7  |-  N  =  ( ( 2  x.  M )  +  1 )
8 2nn 10065 . . . . . . . . 9  |-  2  e.  NN
9 simpl 444 . . . . . . . . 9  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  M  e.  NN )
10 nnmulcl 9955 . . . . . . . . 9  |-  ( ( 2  e.  NN  /\  M  e.  NN )  ->  ( 2  x.  M
)  e.  NN )
118, 9, 10sylancr 645 . . . . . . . 8  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( 2  x.  M )  e.  NN )
1211peano2nnd 9949 . . . . . . 7  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( ( 2  x.  M )  +  1 )  e.  NN )
137, 12syl5eqel 2471 . . . . . 6  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  N  e.  NN )
1413nnnn0d 10206 . . . . 5  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  N  e.  NN0 )
15 binom 12536 . . . . 5  |-  ( ( ( 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
) ) ) )
164, 6, 14, 15syl3anc 1184 . . . 4  |-  ( ( 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 ) ) ) )
17 elioore 10878 . . . . . . . . . . 11  |-  ( A  e.  ( 0 (,) ( pi  /  2
) )  ->  A  e.  RR )
1817adantl 453 . . . . . . . . . 10  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  A  e.  RR )
1918recoscld 12672 . . . . . . . . 9  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( cos `  A
)  e.  RR )
2019recnd 9047 . . . . . . . 8  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( cos `  A
)  e.  CC )
2118resincld 12671 . . . . . . . . . 10  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( sin `  A
)  e.  RR )
2221recnd 9047 . . . . . . . . 9  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( sin `  A
)  e.  CC )
23 mulcl 9007 . . . . . . . . 9  |-  ( ( _i  e.  CC  /\  ( sin `  A )  e.  CC )  -> 
( _i  x.  ( sin `  A ) )  e.  CC )
245, 22, 23sylancr 645 . . . . . . . 8  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( _i  x.  ( sin `  A ) )  e.  CC )
2520, 24addcld 9040 . . . . . . 7  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( ( cos `  A )  +  ( _i  x.  ( sin `  A ) ) )  e.  CC )
26 sincosq1sgn 20273 . . . . . . . . . 10  |-  ( A  e.  ( 0 (,) ( pi  /  2
) )  ->  (
0  <  ( sin `  A )  /\  0  <  ( cos `  A
) ) )
2726adantl 453 . . . . . . . . 9  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( 0  < 
( sin `  A
)  /\  0  <  ( cos `  A ) ) )
2827simpld 446 . . . . . . . 8  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  0  <  ( sin `  A ) )
2928gt0ne0d 9523 . . . . . . 7  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( sin `  A
)  =/=  0 )
3025, 22, 29, 14expdivd 11464 . . . . . 6  |-  ( ( 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 ) ) )
3120, 24, 22, 29divdird 9760 . . . . . . . 8  |-  ( ( 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
) ) ) )
3218recnd 9047 . . . . . . . . . . . 12  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  A  e.  CC )
3327simprd 450 . . . . . . . . . . . . 13  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  0  <  ( cos `  A ) )
3433gt0ne0d 9523 . . . . . . . . . . . 12  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( cos `  A
)  =/=  0 )
35 tanval 12656 . . . . . . . . . . . 12  |-  ( ( A  e.  CC  /\  ( cos `  A )  =/=  0 )  -> 
( tan `  A
)  =  ( ( sin `  A )  /  ( cos `  A
) ) )
3632, 34, 35syl2anc 643 . . . . . . . . . . 11  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( tan `  A
)  =  ( ( sin `  A )  /  ( cos `  A
) ) )
3736oveq2d 6036 . . . . . . . . . 10  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( 1  / 
( tan `  A
) )  =  ( 1  /  ( ( sin `  A )  /  ( cos `  A
) ) ) )
3822, 20, 29, 34recdivd 9739 . . . . . . . . . 10  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( 1  / 
( ( sin `  A
)  /  ( cos `  A ) ) )  =  ( ( cos `  A )  /  ( sin `  A ) ) )
3937, 38eqtr2d 2420 . . . . . . . . 9  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( ( cos `  A )  /  ( sin `  A ) )  =  ( 1  / 
( tan `  A
) ) )
406, 22, 29divcan4d 9728 . . . . . . . . 9  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( ( _i  x.  ( sin `  A
) )  /  ( sin `  A ) )  =  _i )
4139, 40oveq12d 6038 . . . . . . . 8  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( ( ( cos `  A )  /  ( sin `  A
) )  +  ( ( _i  x.  ( sin `  A ) )  /  ( sin `  A
) ) )  =  ( ( 1  / 
( tan `  A
) )  +  _i ) )
4231, 41eqtrd 2419 . . . . . . 7  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( ( ( cos `  A )  +  ( _i  x.  ( sin `  A ) ) )  /  ( sin `  A ) )  =  ( ( 1  /  ( tan `  A
) )  +  _i ) )
4342oveq1d 6035 . . . . . 6  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( ( ( ( cos `  A
)  +  ( _i  x.  ( sin `  A
) ) )  / 
( sin `  A
) ) ^ N
)  =  ( ( ( 1  /  ( tan `  A ) )  +  _i ) ^ N ) )
4413nnzd 10306 . . . . . . . 8  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  N  e.  ZZ )
45 demoivre 12728 . . . . . . . 8  |-  ( ( A  e.  CC  /\  N  e.  ZZ )  ->  ( ( ( cos `  A )  +  ( _i  x.  ( sin `  A ) ) ) ^ N )  =  ( ( cos `  ( N  x.  A )
)  +  ( _i  x.  ( sin `  ( N  x.  A )
) ) ) )
4632, 44, 45syl2anc 643 . . . . . . 7  |-  ( ( 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 ) ) ) ) )
4746oveq1d 6035 . . . . . 6  |-  ( ( 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 ) ) )
4830, 43, 473eqtr3d 2427 . . . . 5  |-  ( ( 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 ) ) )
4913nnred 9947 . . . . . . . . 9  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  N  e.  RR )
5049, 18remulcld 9049 . . . . . . . 8  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( N  x.  A )  e.  RR )
5150recoscld 12672 . . . . . . 7  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( cos `  ( N  x.  A )
)  e.  RR )
5251recnd 9047 . . . . . 6  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( cos `  ( N  x.  A )
)  e.  CC )
5350resincld 12671 . . . . . . . 8  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( sin `  ( N  x.  A )
)  e.  RR )
5453recnd 9047 . . . . . . 7  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( sin `  ( N  x.  A )
)  e.  CC )
55 mulcl 9007 . . . . . . 7  |-  ( ( _i  e.  CC  /\  ( sin `  ( N  x.  A ) )  e.  CC )  -> 
( _i  x.  ( sin `  ( N  x.  A ) ) )  e.  CC )
565, 54, 55sylancr 645 . . . . . 6  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( _i  x.  ( sin `  ( N  x.  A ) ) )  e.  CC )
5721, 28elrpd 10578 . . . . . . . 8  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( sin `  A
)  e.  RR+ )
5857, 44rpexpcld 11473 . . . . . . 7  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( ( sin `  A ) ^ N
)  e.  RR+ )
5958rpcnd 10582 . . . . . 6  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( ( sin `  A ) ^ N
)  e.  CC )
6058rpne0d 10585 . . . . . 6  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( ( sin `  A ) ^ N
)  =/=  0 )
6152, 56, 59, 60divdird 9760 . . . . 5  |-  ( ( 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 ) ) ) )
626, 54, 59, 60divassd 9757 . . . . . 6  |-  ( ( 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 ) ) ) )
6362oveq2d 6036 . . . . 5  |-  ( ( 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 ) ) ) ) )
6448, 61, 633eqtrd 2423 . . . 4  |-  ( ( 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 ) ) ) ) )
6516, 64eqtr3d 2421 . . 3  |-  ( ( 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 ) ) ) ) )
6665fveq2d 5672 . 2  |-  ( ( 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 ) ) ) ) ) )
67 oveq2 6028 . . . . . . 7  |-  ( m  =  ( N  -  ( 2  x.  j
) )  ->  ( N  _C  m )  =  ( N  _C  ( N  -  ( 2  x.  j ) ) ) )
68 oveq2 6028 . . . . . . . . 9  |-  ( m  =  ( N  -  ( 2  x.  j
) )  ->  ( N  -  m )  =  ( N  -  ( N  -  (
2  x.  j ) ) ) )
6968oveq2d 6036 . . . . . . . 8  |-  ( m  =  ( N  -  ( 2  x.  j
) )  ->  (
( 1  /  ( tan `  A ) ) ^ ( N  -  m ) )  =  ( ( 1  / 
( tan `  A
) ) ^ ( N  -  ( N  -  ( 2  x.  j ) ) ) ) )
70 oveq2 6028 . . . . . . . 8  |-  ( m  =  ( N  -  ( 2  x.  j
) )  ->  (
_i ^ m )  =  ( _i ^
( N  -  (
2  x.  j ) ) ) )
7169, 70oveq12d 6038 . . . . . . 7  |-  ( 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 ) ) ) ) )
7267, 71oveq12d 6038 . . . . . 6  |-  ( 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
) ) ) ) ) )
7372fveq2d 5672 . . . . 5  |-  ( 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 ) ) ) ) ) ) )
74 fzfid 11239 . . . . 5  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( 0 ... M )  e.  Fin )
75 2nn0 10170 . . . . . . . . . . . . 13  |-  2  e.  NN0
76 elfznn0 11015 . . . . . . . . . . . . . 14  |-  ( k  e.  ( 0 ... M )  ->  k  e.  NN0 )
7776adantl 453 . . . . . . . . . . . . 13  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  k  e.  NN0 )
78 nn0mulcl 10188 . . . . . . . . . . . . 13  |-  ( ( 2  e.  NN0  /\  k  e.  NN0 )  -> 
( 2  x.  k
)  e.  NN0 )
7975, 77, 78sylancr 645 . . . . . . . . . . . 12  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  ( 2  x.  k )  e. 
NN0 )
8079nn0red 10207 . . . . . . . . . . 11  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  ( 2  x.  k )  e.  RR )
8111nnred 9947 . . . . . . . . . . . 12  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( 2  x.  M )  e.  RR )
8281adantr 452 . . . . . . . . . . 11  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  ( 2  x.  M )  e.  RR )
8349adantr 452 . . . . . . . . . . 11  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  N  e.  RR )
84 elfzle2 10993 . . . . . . . . . . . . 13  |-  ( k  e.  ( 0 ... M )  ->  k  <_  M )
8584adantl 453 . . . . . . . . . . . 12  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  k  <_  M )
8677nn0red 10207 . . . . . . . . . . . . 13  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  k  e.  RR )
87 nnre 9939 . . . . . . . . . . . . . 14  |-  ( M  e.  NN  ->  M  e.  RR )
8887ad2antrr 707 . . . . . . . . . . . . 13  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  M  e.  RR )
89 2re 10001 . . . . . . . . . . . . . . 15  |-  2  e.  RR
90 2pos 10014 . . . . . . . . . . . . . . 15  |-  0  <  2
9189, 90pm3.2i 442 . . . . . . . . . . . . . 14  |-  ( 2  e.  RR  /\  0  <  2 )
9291a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  ( 2  e.  RR  /\  0  <  2 ) )
93 lemul2 9795 . . . . . . . . . . . . 13  |-  ( ( k  e.  RR  /\  M  e.  RR  /\  (
2  e.  RR  /\  0  <  2 ) )  ->  ( k  <_  M 
<->  ( 2  x.  k
)  <_  ( 2  x.  M ) ) )
9486, 88, 92, 93syl3anc 1184 . . . . . . . . . . . 12  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  ( k  <_  M  <->  ( 2  x.  k )  <_  (
2  x.  M ) ) )
9585, 94mpbid 202 . . . . . . . . . . 11  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  ( 2  x.  k )  <_ 
( 2  x.  M
) )
9682lep1d 9874 . . . . . . . . . . . 12  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  ( 2  x.  M )  <_ 
( ( 2  x.  M )  +  1 ) )
9796, 7syl6breqr 4193 . . . . . . . . . . 11  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  ( 2  x.  M )  <_  N )
9880, 82, 83, 95, 97letrd 9159 . . . . . . . . . 10  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  ( 2  x.  k )  <_  N )
99 nn0uz 10452 . . . . . . . . . . . 12  |-  NN0  =  ( ZZ>= `  0 )
10079, 99syl6eleq 2477 . . . . . . . . . . 11  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  ( 2  x.  k )  e.  ( ZZ>= `  0 )
)
10144adantr 452 . . . . . . . . . . 11  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  N  e.  ZZ )
102 elfz5 10983 . . . . . . . . . . 11  |-  ( ( ( 2  x.  k
)  e.  ( ZZ>= ` 
0 )  /\  N  e.  ZZ )  ->  (
( 2  x.  k
)  e.  ( 0 ... N )  <->  ( 2  x.  k )  <_  N ) )
103100, 101, 102syl2anc 643 . . . . . . . . . 10  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  ( (
2  x.  k )  e.  ( 0 ... N )  <->  ( 2  x.  k )  <_  N ) )
10498, 103mpbird 224 . . . . . . . . 9  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  ( 2  x.  k )  e.  ( 0 ... N
) )
105 fznn0sub2 11018 . . . . . . . . 9  |-  ( ( 2  x.  k )  e.  ( 0 ... N )  ->  ( N  -  ( 2  x.  k ) )  e.  ( 0 ... N ) )
106104, 105syl 16 . . . . . . . 8  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  ( N  -  ( 2  x.  k ) )  e.  ( 0 ... N
) )
107106ex 424 . . . . . . 7  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( k  e.  ( 0 ... M
)  ->  ( N  -  ( 2  x.  k ) )  e.  ( 0 ... N
) ) )
10813nncnd 9948 . . . . . . . . . . 11  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  N  e.  CC )
109108adantr 452 . . . . . . . . . 10  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( k  e.  ( 0 ... M
)  /\  m  e.  ( 0 ... M
) ) )  ->  N  e.  CC )
110 2cn 10002 . . . . . . . . . . 11  |-  2  e.  CC
111 elfzelz 10991 . . . . . . . . . . . . 13  |-  ( k  e.  ( 0 ... M )  ->  k  e.  ZZ )
112111zcnd 10308 . . . . . . . . . . . 12  |-  ( k  e.  ( 0 ... M )  ->  k  e.  CC )
113112ad2antrl 709 . . . . . . . . . . 11  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( k  e.  ( 0 ... M
)  /\  m  e.  ( 0 ... M
) ) )  -> 
k  e.  CC )
114 mulcl 9007 . . . . . . . . . . 11  |-  ( ( 2  e.  CC  /\  k  e.  CC )  ->  ( 2  x.  k
)  e.  CC )
115110, 113, 114sylancr 645 . . . . . . . . . 10  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( k  e.  ( 0 ... M
)  /\  m  e.  ( 0 ... M
) ) )  -> 
( 2  x.  k
)  e.  CC )
116112ssriv 3295 . . . . . . . . . . . 12  |-  ( 0 ... M )  C_  CC
117 simprr 734 . . . . . . . . . . . 12  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( k  e.  ( 0 ... M
)  /\  m  e.  ( 0 ... M
) ) )  ->  m  e.  ( 0 ... M ) )
118116, 117sseldi 3289 . . . . . . . . . . 11  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( k  e.  ( 0 ... M
)  /\  m  e.  ( 0 ... M
) ) )  ->  m  e.  CC )
119 mulcl 9007 . . . . . . . . . . 11  |-  ( ( 2  e.  CC  /\  m  e.  CC )  ->  ( 2  x.  m
)  e.  CC )
120110, 118, 119sylancr 645 . . . . . . . . . 10  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( k  e.  ( 0 ... M
)  /\  m  e.  ( 0 ... M
) ) )  -> 
( 2  x.  m
)  e.  CC )
121109, 115, 120subcanad 9386 . . . . . . . . 9  |-  ( ( ( 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 ) ) )
122 2ne0 10015 . . . . . . . . . . . 12  |-  2  =/=  0
123110, 122pm3.2i 442 . . . . . . . . . . 11  |-  ( 2  e.  CC  /\  2  =/=  0 )
124123a1i 11 . . . . . . . . . 10  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( k  e.  ( 0 ... M
)  /\  m  e.  ( 0 ... M
) ) )  -> 
( 2  e.  CC  /\  2  =/=  0 ) )
125 mulcan 9591 . . . . . . . . . 10  |-  ( ( k  e.  CC  /\  m  e.  CC  /\  (
2  e.  CC  /\  2  =/=  0 ) )  ->  ( ( 2  x.  k )  =  ( 2  x.  m
)  <->  k  =  m ) )
126113, 118, 124, 125syl3anc 1184 . . . . . . . . 9  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( k  e.  ( 0 ... M
)  /\  m  e.  ( 0 ... M
) ) )  -> 
( ( 2  x.  k )  =  ( 2  x.  m )  <-> 
k  =  m ) )
127121, 126bitrd 245 . . . . . . . 8  |-  ( ( ( 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 ) )
128127ex 424 . . . . . . 7  |-  ( ( 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 ) ) )
129107, 128dom2lem 7083 . . . . . 6  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( k  e.  ( 0 ... M
)  |->  ( N  -  ( 2  x.  k
) ) ) : ( 0 ... M
) -1-1-> ( 0 ... N ) )
130 f1f1orn 5625 . . . . . 6  |-  ( ( 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 ) ) ) )
131129, 130syl 16 . . . . 5  |-  ( ( 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 6028 . . . . . . . 8  |-  ( k  =  j  ->  (
2  x.  k )  =  ( 2  x.  j ) )
133132oveq2d 6036 . . . . . . 7  |-  ( k  =  j  ->  ( N  -  ( 2  x.  k ) )  =  ( N  -  ( 2  x.  j
) ) )
134 eqid 2387 . . . . . . 7  |-  ( k  e.  ( 0 ... M )  |->  ( N  -  ( 2  x.  k ) ) )  =  ( k  e.  ( 0 ... M
)  |->  ( N  -  ( 2  x.  k
) ) )
135 ovex 6045 . . . . . . 7  |-  ( N  -  ( 2  x.  j ) )  e. 
_V
136133, 134, 135fvmpt 5745 . . . . . 6  |-  ( j  e.  ( 0 ... M )  ->  (
( k  e.  ( 0 ... M ) 
|->  ( N  -  (
2  x.  k ) ) ) `  j
)  =  ( N  -  ( 2  x.  j ) ) )
137136adantl 453 . . . . 5  |-  ( ( ( 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 f1f 5579 . . . . . . . . . . 11  |-  ( ( k  e.  ( 0 ... M )  |->  ( N  -  ( 2  x.  k ) ) ) : ( 0 ... M ) -1-1-> ( 0 ... N )  ->  ( k  e.  ( 0 ... M
)  |->  ( N  -  ( 2  x.  k
) ) ) : ( 0 ... M
) --> ( 0 ... N ) )
139129, 138syl 16 . . . . . . . . . 10  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( k  e.  ( 0 ... M
)  |->  ( N  -  ( 2  x.  k
) ) ) : ( 0 ... M
) --> ( 0 ... N ) )
140 frn 5537 . . . . . . . . . 10  |-  ( ( k  e.  ( 0 ... M )  |->  ( N  -  ( 2  x.  k ) ) ) : ( 0 ... M ) --> ( 0 ... N )  ->  ran  ( k  e.  ( 0 ... M
)  |->  ( N  -  ( 2  x.  k
) ) )  C_  ( 0 ... N
) )
141139, 140syl 16 . . . . . . . . 9  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ran  ( k  e.  ( 0 ... M
)  |->  ( N  -  ( 2  x.  k
) ) )  C_  ( 0 ... N
) )
142141sselda 3291 . . . . . . . 8  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  m  e.  ran  ( k  e.  ( 0 ... M ) 
|->  ( N  -  (
2  x.  k ) ) ) )  ->  m  e.  ( 0 ... N ) )
143 bccl2 11541 . . . . . . . . . . 11  |-  ( m  e.  ( 0 ... N )  ->  ( N  _C  m )  e.  NN )
144143adantl 453 . . . . . . . . . 10  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  m  e.  ( 0 ... N ) )  ->  ( N  _C  m )  e.  NN )
145144nncnd 9948 . . . . . . . . 9  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  m  e.  ( 0 ... N ) )  ->  ( N  _C  m )  e.  CC )
1462rprecred 10591 . . . . . . . . . . . 12  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( 1  / 
( tan `  A
) )  e.  RR )
147 fznn0sub 11017 . . . . . . . . . . . 12  |-  ( m  e.  ( 0 ... N )  ->  ( N  -  m )  e.  NN0 )
148 reexpcl 11325 . . . . . . . . . . . 12  |-  ( ( ( 1  /  ( tan `  A ) )  e.  RR  /\  ( N  -  m )  e.  NN0 )  ->  (
( 1  /  ( tan `  A ) ) ^ ( N  -  m ) )  e.  RR )
149146, 147, 148syl2an 464 . . . . . . . . . . 11  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  m  e.  ( 0 ... N ) )  ->  ( (
1  /  ( tan `  A ) ) ^
( N  -  m
) )  e.  RR )
150149recnd 9047 . . . . . . . . . 10  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  m  e.  ( 0 ... N ) )  ->  ( (
1  /  ( tan `  A ) ) ^
( N  -  m
) )  e.  CC )
151 elfznn0 11015 . . . . . . . . . . . 12  |-  ( m  e.  ( 0 ... N )  ->  m  e.  NN0 )
152151adantl 453 . . . . . . . . . . 11  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  m  e.  ( 0 ... N ) )  ->  m  e.  NN0 )
153 expcl 11326 . . . . . . . . . . 11  |-  ( ( _i  e.  CC  /\  m  e.  NN0 )  -> 
( _i ^ m
)  e.  CC )
1545, 152, 153sylancr 645 . . . . . . . . . 10  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  m  e.  ( 0 ... N ) )  ->  ( _i ^ m )  e.  CC )
155150, 154mulcld 9041 . . . . . . . . 9  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  m  e.  ( 0 ... N ) )  ->  ( (
( 1  /  ( tan `  A ) ) ^ ( N  -  m ) )  x.  ( _i ^ m
) )  e.  CC )
156145, 155mulcld 9041 . . . . . . . 8  |-  ( ( ( 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 )
157142, 156syldan 457 . . . . . . 7  |-  ( ( ( 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 )
158157imcld 11927 . . . . . 6  |-  ( ( ( 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 )
159158recnd 9047 . . . . 5  |-  ( ( ( 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 )
16073, 74, 131, 137, 159fsumf1o 12444 . . . 4  |-  ( ( 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 ) ) ) ) ) ) )
161 eldifi 3412 . . . . . . . 8  |-  ( m  e.  ( ( 0 ... N )  \  ran  ( k  e.  ( 0 ... M ) 
|->  ( N  -  (
2  x.  k ) ) ) )  ->  m  e.  ( 0 ... N ) )
162144nnred 9947 . . . . . . . 8  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  m  e.  ( 0 ... N ) )  ->  ( N  _C  m )  e.  RR )
163161, 162sylan2 461 . . . . . . 7  |-  ( ( ( 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 )
164161, 149sylan2 461 . . . . . . . 8  |-  ( ( ( 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 )
165 eldif 3273 . . . . . . . . 9  |-  ( 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
) ) ) ) )
166 elfzelz 10991 . . . . . . . . . . . . . . 15  |-  ( m  e.  ( 0 ... N )  ->  m  e.  ZZ )
167166adantl 453 . . . . . . . . . . . . . 14  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  m  e.  ( 0 ... N ) )  ->  m  e.  ZZ )
168 zeo 10287 . . . . . . . . . . . . . 14  |-  ( m  e.  ZZ  ->  (
( m  /  2
)  e.  ZZ  \/  ( ( m  + 
1 )  /  2
)  e.  ZZ ) )
169167, 168syl 16 . . . . . . . . . . . . 13  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  m  e.  ( 0 ... N ) )  ->  ( (
m  /  2 )  e.  ZZ  \/  (
( m  +  1 )  /  2 )  e.  ZZ ) )
170 i2 11408 . . . . . . . . . . . . . . . . . 18  |-  ( _i
^ 2 )  = 
-u 1
171170oveq1i 6030 . . . . . . . . . . . . . . . . 17  |-  ( ( _i ^ 2 ) ^ ( m  / 
2 ) )  =  ( -u 1 ^ ( m  /  2
) )
172 simprr 734 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( m  /  2 )  e.  ZZ ) )  -> 
( m  /  2
)  e.  ZZ )
173151ad2antrl 709 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( m  /  2 )  e.  ZZ ) )  ->  m  e.  NN0 )
174 nn0re 10162 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( m  e.  NN0  ->  m  e.  RR )
175 nn0ge0 10179 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( m  e.  NN0  ->  0  <_  m )
176 divge0 9811 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( m  e.  RR  /\  0  <_  m )  /\  ( 2  e.  RR  /\  0  <  2 ) )  ->  0  <_  ( m  /  2 ) )
17789, 90, 176mpanr12 667 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( m  e.  RR  /\  0  <_  m )  -> 
0  <_  ( m  /  2 ) )
178174, 175, 177syl2anc 643 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  e.  NN0  ->  0  <_ 
( m  /  2
) )
179173, 178syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( m  /  2 )  e.  ZZ ) )  -> 
0  <_  ( m  /  2 ) )
180 elnn0z 10226 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( m  /  2 )  e.  NN0  <->  ( ( m  /  2 )  e.  ZZ  /\  0  <_ 
( m  /  2
) ) )
181172, 179, 180sylanbrc 646 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( m  /  2 )  e.  ZZ ) )  -> 
( m  /  2
)  e.  NN0 )
182 expmul 11352 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( _i  e.  CC  /\  2  e.  NN0  /\  (
m  /  2 )  e.  NN0 )  -> 
( _i ^ (
2  x.  ( m  /  2 ) ) )  =  ( ( _i ^ 2 ) ^ ( m  / 
2 ) ) )
1835, 75, 182mp3an12 1269 . . . . . . . . . . . . . . . . . . 19  |-  ( ( m  /  2 )  e.  NN0  ->  ( _i
^ ( 2  x.  ( m  /  2
) ) )  =  ( ( _i ^
2 ) ^ (
m  /  2 ) ) )
184181, 183syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 ) ) )
185173nn0cnd 10208 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( m  /  2 )  e.  ZZ ) )  ->  m  e.  CC )
186 divcan2 9618 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( m  e.  CC  /\  2  e.  CC  /\  2  =/=  0 )  ->  (
2  x.  ( m  /  2 ) )  =  m )
187110, 122, 186mp3an23 1271 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  e.  CC  ->  (
2  x.  ( m  /  2 ) )  =  m )
188185, 187syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( m  /  2 )  e.  ZZ ) )  -> 
( 2  x.  (
m  /  2 ) )  =  m )
189188oveq2d 6036 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( m  /  2 )  e.  ZZ ) )  -> 
( _i ^ (
2  x.  ( m  /  2 ) ) )  =  ( _i
^ m ) )
190184, 189eqtr3d 2421 . . . . . . . . . . . . . . . . 17  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( m  /  2 )  e.  ZZ ) )  -> 
( ( _i ^
2 ) ^ (
m  /  2 ) )  =  ( _i
^ m ) )
191171, 190syl5eqr 2433 . . . . . . . . . . . . . . . 16  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( m  /  2 )  e.  ZZ ) )  -> 
( -u 1 ^ (
m  /  2 ) )  =  ( _i
^ m ) )
192 1re 9023 . . . . . . . . . . . . . . . . . 18  |-  1  e.  RR
193192renegcli 9294 . . . . . . . . . . . . . . . . 17  |-  -u 1  e.  RR
194 reexpcl 11325 . . . . . . . . . . . . . . . . 17  |-  ( (
-u 1  e.  RR  /\  ( m  /  2
)  e.  NN0 )  ->  ( -u 1 ^ ( m  /  2
) )  e.  RR )
195193, 181, 194sylancr 645 . . . . . . . . . . . . . . . 16  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( m  /  2 )  e.  ZZ ) )  -> 
( -u 1 ^ (
m  /  2 ) )  e.  RR )
196191, 195eqeltrrd 2462 . . . . . . . . . . . . . . 15  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( m  /  2 )  e.  ZZ ) )  -> 
( _i ^ m
)  e.  RR )
197196expr 599 . . . . . . . . . . . . . 14  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  m  e.  ( 0 ... N ) )  ->  ( (
m  /  2 )  e.  ZZ  ->  (
_i ^ m )  e.  RR ) )
198147ad2antrl 709 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( N  -  m
)  e.  NN0 )
199 nn0re 10162 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( N  -  m )  e.  NN0  ->  ( N  -  m )  e.  RR )
200 nn0ge0 10179 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( N  -  m )  e.  NN0  ->  0  <_ 
( N  -  m
) )
201 divge0 9811 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( N  -  m )  e.  RR  /\  0  <_  ( N  -  m ) )  /\  ( 2  e.  RR  /\  0  <  2 ) )  ->  0  <_  ( ( N  -  m
)  /  2 ) )
20289, 90, 201mpanr12 667 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( N  -  m
)  e.  RR  /\  0  <_  ( N  -  m ) )  -> 
0  <_  ( ( N  -  m )  /  2 ) )
203199, 200, 202syl2anc 643 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( N  -  m )  e.  NN0  ->  0  <_ 
( ( N  -  m )  /  2
) )
204198, 203syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
0  <_  ( ( N  -  m )  /  2 ) )
205198nn0red 10207 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( N  -  m
)  e.  RR )
20649adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  ->  N  e.  RR )
207 peano2re 9171 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( N  e.  RR  ->  ( N  +  1 )  e.  RR )
208206, 207syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( N  +  1 )  e.  RR )
209151ad2antrl 709 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  ->  m  e.  NN0 )
210209, 175syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
0  <_  m )
211209nn0red 10207 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  ->  m  e.  RR )
212206, 211subge02d 9550 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( 0  <_  m  <->  ( N  -  m )  <_  N ) )
213210, 212mpbid 202 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( N  -  m
)  <_  N )
214206ltp1d 9873 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  ->  N  <  ( N  + 
1 ) )
215205, 206, 208, 213, 214lelttrd 9160 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( N  -  m
)  <  ( N  +  1 ) )
216110mulid1i 9025 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 2  x.  1 )  =  2
217 df-2 9990 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  2  =  ( 1  +  1 )
218216, 217eqtr2i 2408 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 1  +  1 )  =  ( 2  x.  1 )
219218oveq2i 6031 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 2  x.  M )  +  ( 1  +  1 ) )  =  ( ( 2  x.  M )  +  ( 2  x.  1 ) )
2207oveq1i 6030 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( N  +  1 )  =  ( ( ( 2  x.  M )  +  1 )  +  1 )
22111nncnd 9948 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( 2  x.  M )  e.  CC )
222221adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( 2  x.  M
)  e.  CC )
223 ax-1cn 8981 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  1  e.  CC
224223a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
1  e.  CC )
225222, 224, 224addassd 9043 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( 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 ) ) )
226220, 225syl5eq 2431 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( N  +  1 )  =  ( ( 2  x.  M )  +  ( 1  +  1 ) ) )
227110a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
2  e.  CC )
228 nncn 9940 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( M  e.  NN  ->  M  e.  CC )
229228ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  ->  M  e.  CC )
230227, 229, 224adddid 9045 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 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 ) ) )
231219, 226, 2303eqtr4a 2445 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( N  +  1 )  =  ( 2  x.  ( M  + 
1 ) ) )
232215, 231breqtrd 4177 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( N  -  m
)  <  ( 2  x.  ( M  + 
1 ) ) )
233 nnz 10235 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( M  e.  NN  ->  M  e.  ZZ )
234233ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  ->  M  e.  ZZ )
235234peano2zd 10310 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( M  +  1 )  e.  ZZ )
236235zred 10307 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( M  +  1 )  e.  RR )
23791a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( 2  e.  RR  /\  0  <  2 ) )
238 ltdivmul 9814 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( N  -  m
)  e.  RR  /\  ( M  +  1
)  e.  RR  /\  ( 2  e.  RR  /\  0  <  2 ) )  ->  ( (
( N  -  m
)  /  2 )  <  ( M  + 
1 )  <->  ( N  -  m )  <  (
2  x.  ( M  +  1 ) ) ) )
239205, 236, 237, 238syl3anc 1184 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( 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 ) ) ) )
240232, 239mpbird 224 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( ( N  -  m )  /  2
)  <  ( M  +  1 ) )
241108adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  ->  N  e.  CC )
242209nn0cnd 10208 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  ->  m  e.  CC )
243241, 242, 224pnpcan2d 9381 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( ( N  + 
1 )  -  (
m  +  1 ) )  =  ( N  -  m ) )
244231oveq1d 6035 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( 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 ) ) )
245243, 244eqtr3d 2421 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( 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 ) ) )
246245oveq1d 6035 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 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 ) )
247235zcnd 10308 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( M  +  1 )  e.  CC )
248 mulcl 9007 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 2  e.  CC  /\  ( M  +  1
)  e.  CC )  ->  ( 2  x.  ( M  +  1 ) )  e.  CC )
249110, 247, 248sylancr 645 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( 2  x.  ( M  +  1 ) )  e.  CC )
250 peano2cn 9170 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( m  e.  CC  ->  (
m  +  1 )  e.  CC )
251242, 250syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( m  +  1 )  e.  CC )
252123a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( 2  e.  CC  /\  2  =/=  0 ) )
253 divsubdir 9642 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( 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 ) ) )
254249, 251, 252, 253syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 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 ) ) )
255122a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
2  =/=  0 )
256247, 227, 255divcan3d 9727 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( ( 2  x.  ( M  +  1 ) )  /  2
)  =  ( M  +  1 ) )
257256oveq1d 6035 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 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 ) ) )
258246, 254, 2573eqtrd 2423 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 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 ) ) )
259 simprr 734 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( ( m  + 
1 )  /  2
)  e.  ZZ )
260235, 259zsubcld 10312 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( ( M  + 
1 )  -  (
( m  +  1 )  /  2 ) )  e.  ZZ )
261258, 260eqeltrd 2461 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( ( N  -  m )  /  2
)  e.  ZZ )
262 zleltp1 10258 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( N  -  m )  /  2
)  e.  ZZ  /\  M  e.  ZZ )  ->  ( ( ( N  -  m )  / 
2 )  <_  M  <->  ( ( N  -  m
)  /  2 )  <  ( M  + 
1 ) ) )
263261, 234, 262syl2anc 643 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 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 ) ) )
264240, 263mpbird 224 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( ( N  -  m )  /  2
)  <_  M )
265 0z 10225 . . . . . . . . . . . . . . . . . . . . 21  |-  0  e.  ZZ
266265a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
0  e.  ZZ )
267 elfz 10981 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 ) ) )
268261, 266, 234, 267syl3anc 1184 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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
) ) )
269204, 264, 268mpbir2and 889 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( ( N  -  m )  /  2
)  e.  ( 0 ... M ) )
270 oveq2 6028 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  ( ( N  -  m )  / 
2 )  ->  (
2  x.  k )  =  ( 2  x.  ( ( N  -  m )  /  2
) ) )
271270oveq2d 6036 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  ( ( N  -  m )  / 
2 )  ->  ( N  -  ( 2  x.  k ) )  =  ( N  -  ( 2  x.  (
( N  -  m
)  /  2 ) ) ) )
272 ovex 6045 . . . . . . . . . . . . . . . . . . 19  |-  ( N  -  ( 2  x.  ( ( N  -  m )  /  2
) ) )  e. 
_V
273271, 134, 272fvmpt 5745 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( N  -  m
)  /  2 )  e.  ( 0 ... M )  ->  (
( k  e.  ( 0 ... M ) 
|->  ( N  -  (
2  x.  k ) ) ) `  (
( N  -  m
)  /  2 ) )  =  ( N  -  ( 2  x.  ( ( N  -  m )  /  2
) ) ) )
274269, 273syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) ) ) )
275198nn0cnd 10208 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( N  -  m
)  e.  CC )
276275, 227, 255divcan2d 9724 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( 2  x.  (
( N  -  m
)  /  2 ) )  =  ( N  -  m ) )
277276oveq2d 6036 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) ) )
278241, 242nncand 9348 . . . . . . . . . . . . . . . . 17  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( N  -  ( N  -  m )
)  =  m )
279274, 277, 2783eqtrd 2423 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 )
280 ffn 5531 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  ( 0 ... M )  |->  ( N  -  ( 2  x.  k ) ) ) : ( 0 ... M ) --> ( 0 ... N )  ->  ( k  e.  ( 0 ... M
)  |->  ( N  -  ( 2  x.  k
) ) )  Fn  ( 0 ... M
) )
281139, 280syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( k  e.  ( 0 ... M
)  |->  ( N  -  ( 2  x.  k
) ) )  Fn  ( 0 ... M
) )
282281adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) ) )  Fn  (
0 ... M ) )
283 fnfvelrn 5806 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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
) ) ) )
284282, 269, 283syl2anc 643 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) ) )
285279, 284eqeltrrd 2462 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) ) ) )
286285expr 599 . . . . . . . . . . . . . 14  |-  ( ( ( 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
) ) ) ) )
287197, 286orim12d 812 . . . . . . . . . . . . 13  |-  ( ( ( 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
) ) ) ) ) )
288169, 287mpd 15 . . . . . . . . . . . 12  |-  ( ( ( 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
) ) ) ) )
289288orcomd 378 . . . . . . . . . . 11  |-  ( ( ( 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 ) )
290289ord 367 . . . . . . . . . 10  |-  ( ( ( 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 ) )
291290impr 603 . . . . . . . . 9  |-  ( ( ( 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 )
292165, 291sylan2b 462 . . . . . . . 8  |-  ( ( ( 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 )
293164, 292remulcld 9049 . . . . . . 7  |-  ( ( ( 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 )
294163, 293remulcld 9049 . . . . . 6  |-  ( ( ( 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 )
295294reim0d 11957 . . . . 5  |-  ( ( ( 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 )
296 fzfid 11239 . . . . 5  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( 0 ... N )  e.  Fin )
297141, 159, 295, 296fsumss 12446 . . . 4  |-  ( ( 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 ) ) ) ) )
29814adantr 452 . . . . . . . . . . . . . . 15  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  N  e.  NN0 )
299 elfznn0 11015 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( 0 ... M )  ->  j  e.  NN0 )
300299adantl 453 . . . . . . . . . . . . . . . . 17  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  j  e.  NN0 )
301 nn0mulcl 10188 . . . . . . . . . . . . . . . . 17  |-  ( ( 2  e.  NN0  /\  j  e.  NN0 )  -> 
( 2  x.  j
)  e.  NN0 )
30275, 300, 301sylancr 645 . . . . . . . . . . . . . . . 16  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( 2  x.  j )  e. 
NN0 )
303302nn0zd 10305 . . . . . . . . . . . . . . 15  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( 2  x.  j )  e.  ZZ )
304 bccl 11540 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  NN0  /\  ( 2  x.  j
)  e.  ZZ )  ->  ( N  _C  ( 2  x.  j
) )  e.  NN0 )
305298, 303, 304syl2anc 643 . . . . . . . . . . . . . 14  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( N  _C  ( 2  x.  j
) )  e.  NN0 )
306305nn0red 10207 . . . . . . . . . . . . 13  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( N  _C  ( 2  x.  j
) )  e.  RR )
307 fznn0sub 11017 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0 ... M )  ->  ( M  -  j )  e.  NN0 )
308307adantl 453 . . . . . . . . . . . . . 14  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( M  -  j )  e. 
NN0 )
309 reexpcl 11325 . . . . . . . . . . . . . 14  |-  ( (
-u 1  e.  RR  /\  ( M  -  j
)  e.  NN0 )  ->  ( -u 1 ^ ( M  -  j
) )  e.  RR )
310193, 308, 309sylancr 645 . . . . . . . . . . . . 13  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( -u 1 ^ ( M  -  j ) )  e.  RR )
311306, 310remulcld 9049 . . . . . . . . . . . 12  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( ( N  _C  ( 2  x.  j ) )  x.  ( -u 1 ^ ( M  -  j
) ) )  e.  RR )
312 2z 10244 . . . . . . . . . . . . . . . 16  |-  2  e.  ZZ
313 znegcl 10245 . . . . . . . . . . . . . . . 16  |-  ( 2  e.  ZZ  ->  -u 2  e.  ZZ )
314312, 313ax-mp 8 . . . . . . . . . . . . . . 15  |-  -u 2  e.  ZZ
315 rpexpcl 11327 . . . . . . . . . . . . . . 15  |-  ( ( ( tan `  A
)  e.  RR+  /\  -u 2  e.  ZZ )  ->  (
( tan `  A
) ^ -u 2
)  e.  RR+ )
3162, 314, 315sylancl 644 . . . . . . . . . . . . . 14  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( ( tan `  A ) ^ -u 2
)  e.  RR+ )
317316rpred 10580 . . . . . . . . . . . . 13  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( ( tan `  A ) ^ -u 2
)  e.  RR )
318 reexpcl 11325 . . . . . . . . . . . . 13  |-  ( ( ( ( tan `  A
) ^ -u 2
)  e.  RR  /\  j  e.  NN0 )  -> 
( ( ( tan `  A ) ^ -u 2
) ^ j )  e.  RR )
319317, 299, 318syl2an 464 . . . . . . . . . . . 12  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( (
( tan `  A
) ^ -u 2
) ^ j )  e.  RR )
320311, 319remulcld 9049 . . . . . . . . . . 11  |-  ( ( ( 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 )
321320recnd 9047 . . . . . . . . . 10  |-  ( ( ( 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 )
322 mulcl 9007 . . . . . . . . . 10  |-  ( ( _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 )
3235, 321, 322sylancr 645 . . . . . . . . 9  |-  ( ( ( 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 )
324323addid2d 9199 . . . . . . . 8  |-  ( ( ( 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 ) ) ) )
325305nn0cnd 10208 . . . . . . . . . . 11  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( N  _C  ( 2  x.  j
) )  e.  CC )
326310recnd 9047 . . . . . . . . . . 11  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( -u 1 ^ ( M  -  j ) )  e.  CC )
327319recnd 9047 . . . . . . . . . . 11  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( (
( tan `  A
) ^ -u 2
) ^ j )  e.  CC )
328325, 326, 327mulassd 9044 . . . . . . . . . 10  |-  ( ( ( 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 ) ) ) )
329328oveq2d 6036 . . . . . . . . 9  |-  ( ( ( 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 ) ) ) ) )
3305a1i 11 . . . . . . . . . 10  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  _i  e.  CC )
331326, 327mulcld 9041 . . . . . . . . . 10  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( ( -u 1 ^ ( M  -  j ) )  x.  ( ( ( tan `  A ) ^ -u 2 ) ^ j ) )  e.  CC )
332330, 325, 331mul12d 9207 . . . . . . . . 9  |-  ( ( ( 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 ) ) ) ) )
333329, 332eqtrd 2419 . . . . . . . 8  |-  ( ( ( 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 ) ) ) ) )
334 bccmpl 11527 . . . . . . . . . 10  |-  ( ( N  e.  NN0  /\  ( 2  x.  j
)  e.  ZZ )  ->  ( N  _C  ( 2  x.  j
) )  =  ( N  _C  ( N  -  ( 2  x.  j ) ) ) )
335298, 303, 334syl2anc 643 . . . . . . . . 9  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( N  _C  ( 2  x.  j
) )  =  ( N  _C  ( N  -  ( 2  x.  j ) ) ) )
336108adantr 452 . . . . . . . . . . . . . 14  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  N  e.  CC )
337302nn0cnd 10208 . . . . . . . . . . . . . 14  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( 2  x.  j )  e.  CC )
338336, 337nncand 9348 . . . . . . . . . . . . 13  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( N  -  ( N  -  ( 2  x.  j
) ) )  =  ( 2  x.  j
) )
339338oveq2d 6036 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) )
3402adantr 452 . . . . . . . . . . . . . . 15  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( tan `  A )  e.  RR+ )
341340rpcnd 10582 . . . . . . . . . . . . . 14  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( tan `  A )  e.  CC )
342 expneg 11316 . . . . . . . . . . . . . 14  |-  ( ( ( tan `  A
)  e.  CC  /\  ( 2  x.  j
)  e.  NN0 )  ->  ( ( tan `  A
) ^ -u (
2  x.  j ) )  =  ( 1  /  ( ( tan `  A ) ^ (
2  x.  j ) ) ) )
343341, 302, 342syl2anc 643 . . . . . . . . . . . . 13  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( ( tan `  A ) ^ -u ( 2  x.  j
) )  =  ( 1  /  ( ( tan `  A ) ^ ( 2  x.  j ) ) ) )
344300nn0cnd 10208 . . . . . . . . . . . . . . 15  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  j  e.  CC )
345 mulneg1 9402 . . . . . . . . . . . . . . 15  |-  ( ( 2  e.  CC  /\  j  e.  CC )  ->  ( -u 2  x.  j )  =  -u ( 2  x.  j
) )
346110, 344, 345sylancr