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

Theorem basellem3 20320
Description: Lemma for basel 20327. 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 19872 . . . . . . . 8  |-  ( A  e.  ( 0 (,) ( pi  /  2
) )  ->  ( tan `  A )  e.  RR+ )
21adantl 452 . . . . . . 7  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( tan `  A
)  e.  RR+ )
32rpreccld 10400 . . . . . 6  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( 1  / 
( tan `  A
) )  e.  RR+ )
43rpcnd 10392 . . . . 5  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( 1  / 
( tan `  A
) )  e.  CC )
5 ax-icn 8796 . . . . . 6  |-  _i  e.  CC
65a1i 10 . . . . 5  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  _i  e.  CC )
7 basel.n . . . . . . 7  |-  N  =  ( ( 2  x.  M )  +  1 )
8 2nn 9877 . . . . . . . . 9  |-  2  e.  NN
9 simpl 443 . . . . . . . . 9  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  M  e.  NN )
10 nnmulcl 9769 . . . . . . . . 9  |-  ( ( 2  e.  NN  /\  M  e.  NN )  ->  ( 2  x.  M
)  e.  NN )
118, 9, 10sylancr 644 . . . . . . . 8  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( 2  x.  M )  e.  NN )
1211peano2nnd 9763 . . . . . . 7  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( ( 2  x.  M )  +  1 )  e.  NN )
137, 12syl5eqel 2367 . . . . . 6  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  N  e.  NN )
1413nnnn0d 10018 . . . . 5  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  N  e.  NN0 )
15 binom 12288 . . . . 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 1182 . . . 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 10686 . . . . . . . . . . 11  |-  ( A  e.  ( 0 (,) ( pi  /  2
) )  ->  A  e.  RR )
1817adantl 452 . . . . . . . . . 10  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  A  e.  RR )
1918recoscld 12424 . . . . . . . . 9  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( cos `  A
)  e.  RR )
2019recnd 8861 . . . . . . . 8  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( cos `  A
)  e.  CC )
2118resincld 12423 . . . . . . . . . 10  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( sin `  A
)  e.  RR )
2221recnd 8861 . . . . . . . . 9  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( sin `  A
)  e.  CC )
23 mulcl 8821 . . . . . . . . 9  |-  ( ( _i  e.  CC  /\  ( sin `  A )  e.  CC )  -> 
( _i  x.  ( sin `  A ) )  e.  CC )
245, 22, 23sylancr 644 . . . . . . . 8  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( _i  x.  ( sin `  A ) )  e.  CC )
2520, 24addcld 8854 . . . . . . 7  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( ( cos `  A )  +  ( _i  x.  ( sin `  A ) ) )  e.  CC )
26 sincosq1sgn 19866 . . . . . . . . . 10  |-  ( A  e.  ( 0 (,) ( pi  /  2
) )  ->  (
0  <  ( sin `  A )  /\  0  <  ( cos `  A
) ) )
2726adantl 452 . . . . . . . . 9  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( 0  < 
( sin `  A
)  /\  0  <  ( cos `  A ) ) )
2827simpld 445 . . . . . . . 8  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  0  <  ( sin `  A ) )
2928gt0ne0d 9337 . . . . . . 7  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( sin `  A
)  =/=  0 )
3025, 22, 29, 14expdivd 11259 . . . . . 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 9574 . . . . . . . 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 8861 . . . . . . . . . . . 12  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  A  e.  CC )
3327simprd 449 . . . . . . . . . . . . 13  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  0  <  ( cos `  A ) )
3433gt0ne0d 9337 . . . . . . . . . . . 12  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( cos `  A
)  =/=  0 )
35 tanval 12408 . . . . . . . . . . . 12  |-  ( ( A  e.  CC  /\  ( cos `  A )  =/=  0 )  -> 
( tan `  A
)  =  ( ( sin `  A )  /  ( cos `  A
) ) )
3632, 34, 35syl2anc 642 . . . . . . . . . . 11  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( tan `  A
)  =  ( ( sin `  A )  /  ( cos `  A
) ) )
3736oveq2d 5874 . . . . . . . . . 10  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( 1  / 
( tan `  A
) )  =  ( 1  /  ( ( sin `  A )  /  ( cos `  A
) ) ) )
3822, 20, 29, 34recdivd 9553 . . . . . . . . . 10  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( 1  / 
( ( sin `  A
)  /  ( cos `  A ) ) )  =  ( ( cos `  A )  /  ( sin `  A ) ) )
3937, 38eqtr2d 2316 . . . . . . . . 9  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( ( cos `  A )  /  ( sin `  A ) )  =  ( 1  / 
( tan `  A
) ) )
406, 22, 29divcan4d 9542 . . . . . . . . 9  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( ( _i  x.  ( sin `  A
) )  /  ( sin `  A ) )  =  _i )
4139, 40oveq12d 5876 . . . . . . . 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 2315 . . . . . . 7  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( ( ( cos `  A )  +  ( _i  x.  ( sin `  A ) ) )  /  ( sin `  A ) )  =  ( ( 1  /  ( tan `  A
) )  +  _i ) )
4342oveq1d 5873 . . . . . 6  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( ( ( ( cos `  A
)  +  ( _i  x.  ( sin `  A
) ) )  / 
( sin `  A
) ) ^ N
)  =  ( ( ( 1  /  ( tan `  A ) )  +  _i ) ^ N ) )
4413nnzd 10116 . . . . . . . 8  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  N  e.  ZZ )
45 demoivre 12480 . . . . . . . 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 642 . . . . . . 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 5873 . . . . . 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 2323 . . . . 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 9761 . . . . . . . . 9  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  N  e.  RR )
5049, 18remulcld 8863 . . . . . . . 8  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( N  x.  A )  e.  RR )
5150recoscld 12424 . . . . . . 7  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( cos `  ( N  x.  A )
)  e.  RR )
5251recnd 8861 . . . . . 6  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( cos `  ( N  x.  A )
)  e.  CC )
5350resincld 12423 . . . . . . . 8  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( sin `  ( N  x.  A )
)  e.  RR )
5453recnd 8861 . . . . . . 7  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( sin `  ( N  x.  A )
)  e.  CC )
55 mulcl 8821 . . . . . . 7  |-  ( ( _i  e.  CC  /\  ( sin `  ( N  x.  A ) )  e.  CC )  -> 
( _i  x.  ( sin `  ( N  x.  A ) ) )  e.  CC )
565, 54, 55sylancr 644 . . . . . 6  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( _i  x.  ( sin `  ( N  x.  A ) ) )  e.  CC )
5721, 28elrpd 10388 . . . . . . . 8  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( sin `  A
)  e.  RR+ )
5857, 44rpexpcld 11268 . . . . . . 7  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( ( sin `  A ) ^ N
)  e.  RR+ )
5958rpcnd 10392 . . . . . 6  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( ( sin `  A ) ^ N
)  e.  CC )
6058rpne0d 10395 . . . . . 6  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( ( sin `  A ) ^ N
)  =/=  0 )
6152, 56, 59, 60divdird 9574 . . . . 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 9571 . . . . . 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 5874 . . . . 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 2319 . . . 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 2317 . . 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 5529 . 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 5866 . . . . . . 7  |-  ( m  =  ( N  -  ( 2  x.  j
) )  ->  ( N  _C  m )  =  ( N  _C  ( N  -  ( 2  x.  j ) ) ) )
68 oveq2 5866 . . . . . . . . 9  |-  ( m  =  ( N  -  ( 2  x.  j
) )  ->  ( N  -  m )  =  ( N  -  ( N  -  (
2  x.  j ) ) ) )
6968oveq2d 5874 . . . . . . . 8  |-  ( m  =  ( N  -  ( 2  x.  j
) )  ->  (
( 1  /  ( tan `  A ) ) ^ ( N  -  m ) )  =  ( ( 1  / 
( tan `  A
) ) ^ ( N  -  ( N  -  ( 2  x.  j ) ) ) ) )
70 oveq2 5866 . . . . . . . 8  |-  ( m  =  ( N  -  ( 2  x.  j
) )  ->  (
_i ^ m )  =  ( _i ^
( N  -  (
2  x.  j ) ) ) )
7169, 70oveq12d 5876 . . . . . . 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 5876 . . . . . 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 5529 . . . . 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 11035 . . . . 5  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( 0 ... M )  e.  Fin )
75 2nn0 9982 . . . . . . . . . . . . 13  |-  2  e.  NN0
76 elfznn0 10822 . . . . . . . . . . . . . 14  |-  ( k  e.  ( 0 ... M )  ->  k  e.  NN0 )
7776adantl 452 . . . . . . . . . . . . 13  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  k  e.  NN0 )
78 nn0mulcl 10000 . . . . . . . . . . . . 13  |-  ( ( 2  e.  NN0  /\  k  e.  NN0 )  -> 
( 2  x.  k
)  e.  NN0 )
7975, 77, 78sylancr 644 . . . . . . . . . . . 12  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  ( 2  x.  k )  e. 
NN0 )
8079nn0red 10019 . . . . . . . . . . 11  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  ( 2  x.  k )  e.  RR )
8111nnred 9761 . . . . . . . . . . . 12  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( 2  x.  M )  e.  RR )
8281adantr 451 . . . . . . . . . . 11  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  ( 2  x.  M )  e.  RR )
8349adantr 451 . . . . . . . . . . 11  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  N  e.  RR )
84 elfzle2 10800 . . . . . . . . . . . . 13  |-  ( k  e.  ( 0 ... M )  ->  k  <_  M )
8584adantl 452 . . . . . . . . . . . 12  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  k  <_  M )
8677nn0red 10019 . . . . . . . . . . . . 13  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  k  e.  RR )
87 nnre 9753 . . . . . . . . . . . . . 14  |-  ( M  e.  NN  ->  M  e.  RR )
8887ad2antrr 706 . . . . . . . . . . . . 13  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  M  e.  RR )
89 2re 9815 . . . . . . . . . . . . . . 15  |-  2  e.  RR
90 2pos 9828 . . . . . . . . . . . . . . 15  |-  0  <  2
9189, 90pm3.2i 441 . . . . . . . . . . . . . 14  |-  ( 2  e.  RR  /\  0  <  2 )
9291a1i 10 . . . . . . . . . . . . 13  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  ( 2  e.  RR  /\  0  <  2 ) )
93 lemul2 9609 . . . . . . . . . . . . 13  |-  ( ( k  e.  RR  /\  M  e.  RR  /\  (
2  e.  RR  /\  0  <  2 ) )  ->  ( k  <_  M 
<->  ( 2  x.  k
)  <_  ( 2  x.  M ) ) )
9486, 88, 92, 93syl3anc 1182 . . . . . . . . . . . 12  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  ( k  <_  M  <->  ( 2  x.  k )  <_  (
2  x.  M ) ) )
9585, 94mpbid 201 . . . . . . . . . . 11  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  ( 2  x.  k )  <_ 
( 2  x.  M
) )
9682lep1d 9688 . . . . . . . . . . . 12  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  ( 2  x.  M )  <_ 
( ( 2  x.  M )  +  1 ) )
9796, 7syl6breqr 4063 . . . . . . . . . . 11  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  ( 2  x.  M )  <_  N )
9880, 82, 83, 95, 97letrd 8973 . . . . . . . . . 10  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  ( 2  x.  k )  <_  N )
99 nn0uz 10262 . . . . . . . . . . . 12  |-  NN0  =  ( ZZ>= `  0 )
10079, 99syl6eleq 2373 . . . . . . . . . . 11  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  ( 2  x.  k )  e.  ( ZZ>= `  0 )
)
10144adantr 451 . . . . . . . . . . 11  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  N  e.  ZZ )
102 elfz5 10790 . . . . . . . . . . 11  |-  ( ( ( 2  x.  k
)  e.  ( ZZ>= ` 
0 )  /\  N  e.  ZZ )  ->  (
( 2  x.  k
)  e.  ( 0 ... N )  <->  ( 2  x.  k )  <_  N ) )
103100, 101, 102syl2anc 642 . . . . . . . . . 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 223 . . . . . . . . 9  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  ( 2  x.  k )  e.  ( 0 ... N
) )
105 fznn0sub2 10825 . . . . . . . . 9  |-  ( ( 2  x.  k )  e.  ( 0 ... N )  ->  ( N  -  ( 2  x.  k ) )  e.  ( 0 ... N ) )
106104, 105syl 15 . . . . . . . 8  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  k  e.  ( 0 ... M ) )  ->  ( N  -  ( 2  x.  k ) )  e.  ( 0 ... N
) )
107106ex 423 . . . . . . 7  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( k  e.  ( 0 ... M
)  ->  ( N  -  ( 2  x.  k ) )  e.  ( 0 ... N
) ) )
10813nncnd 9762 . . . . . . . . . . 11  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  N  e.  CC )
109108adantr 451 . . . . . . . . . 10  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( k  e.  ( 0 ... M
)  /\  m  e.  ( 0 ... M
) ) )  ->  N  e.  CC )
110 2cn 9816 . . . . . . . . . . 11  |-  2  e.  CC
111 elfzelz 10798 . . . . . . . . . . . . 13  |-  ( k  e.  ( 0 ... M )  ->  k  e.  ZZ )
112111zcnd 10118 . . . . . . . . . . . 12  |-  ( k  e.  ( 0 ... M )  ->  k  e.  CC )
113112ad2antrl 708 . . . . . . . . . . 11  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( k  e.  ( 0 ... M
)  /\  m  e.  ( 0 ... M
) ) )  -> 
k  e.  CC )
114 mulcl 8821 . . . . . . . . . . 11  |-  ( ( 2  e.  CC  /\  k  e.  CC )  ->  ( 2  x.  k
)  e.  CC )
115110, 113, 114sylancr 644 . . . . . . . . . 10  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( k  e.  ( 0 ... M
)  /\  m  e.  ( 0 ... M
) ) )  -> 
( 2  x.  k
)  e.  CC )
116112ssriv 3184 . . . . . . . . . . . 12  |-  ( 0 ... M )  C_  CC
117 simprr 733 . . . . . . . . . . . 12  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( k  e.  ( 0 ... M
)  /\  m  e.  ( 0 ... M
) ) )  ->  m  e.  ( 0 ... M ) )
118116, 117sseldi 3178 . . . . . . . . . . 11  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( k  e.  ( 0 ... M
)  /\  m  e.  ( 0 ... M
) ) )  ->  m  e.  CC )
119 mulcl 8821 . . . . . . . . . . 11  |-  ( ( 2  e.  CC  /\  m  e.  CC )  ->  ( 2  x.  m
)  e.  CC )
120110, 118, 119sylancr 644 . . . . . . . . . 10  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( k  e.  ( 0 ... M
)  /\  m  e.  ( 0 ... M
) ) )  -> 
( 2  x.  m
)  e.  CC )
121 subcan 9102 . . . . . . . . . 10  |-  ( ( N  e.  CC  /\  ( 2  x.  k
)  e.  CC  /\  ( 2  x.  m
)  e.  CC )  ->  ( ( N  -  ( 2  x.  k ) )  =  ( N  -  (
2  x.  m ) )  <->  ( 2  x.  k )  =  ( 2  x.  m ) ) )
122109, 115, 120, 121syl3anc 1182 . . . . . . . . 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 ) ) )
123 2ne0 9829 . . . . . . . . . . . 12  |-  2  =/=  0
124110, 123pm3.2i 441 . . . . . . . . . . 11  |-  ( 2  e.  CC  /\  2  =/=  0 )
125124a1i 10 . . . . . . . . . 10  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( k  e.  ( 0 ... M
)  /\  m  e.  ( 0 ... M
) ) )  -> 
( 2  e.  CC  /\  2  =/=  0 ) )
126 mulcan 9405 . . . . . . . . . 10  |-  ( ( k  e.  CC  /\  m  e.  CC  /\  (
2  e.  CC  /\  2  =/=  0 ) )  ->  ( ( 2  x.  k )  =  ( 2  x.  m
)  <->  k  =  m ) )
127113, 118, 125, 126syl3anc 1182 . . . . . . . . 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 ) )
128122, 127bitrd 244 . . . . . . . 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 ) )
129128ex 423 . . . . . . 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 ) ) )
130107, 129dom2lem 6901 . . . . . 6  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( k  e.  ( 0 ... M
)  |->  ( N  -  ( 2  x.  k
) ) ) : ( 0 ... M
) -1-1-> ( 0 ... N ) )
131 f1f1orn 5483 . . . . . 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 ) ) ) )
132130, 131syl 15 . . . . 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 ) ) ) )
133 oveq2 5866 . . . . . . . 8  |-  ( k  =  j  ->  (
2  x.  k )  =  ( 2  x.  j ) )
134133oveq2d 5874 . . . . . . 7  |-  ( k  =  j  ->  ( N  -  ( 2  x.  k ) )  =  ( N  -  ( 2  x.  j
) ) )
135 eqid 2283 . . . . . . 7  |-  ( k  e.  ( 0 ... M )  |->  ( N  -  ( 2  x.  k ) ) )  =  ( k  e.  ( 0 ... M
)  |->  ( N  -  ( 2  x.  k
) ) )
136 ovex 5883 . . . . . . 7  |-  ( N  -  ( 2  x.  j ) )  e. 
_V
137134, 135, 136fvmpt 5602 . . . . . 6  |-  ( j  e.  ( 0 ... M )  ->  (
( k  e.  ( 0 ... M ) 
|->  ( N  -  (
2  x.  k ) ) ) `  j
)  =  ( N  -  ( 2  x.  j ) ) )
138137adantl 452 . . . . 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
) ) )
139 f1f 5437 . . . . . . . . . . 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 ) )
140130, 139syl 15 . . . . . . . . . 10  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( k  e.  ( 0 ... M
)  |->  ( N  -  ( 2  x.  k
) ) ) : ( 0 ... M
) --> ( 0 ... N ) )
141 frn 5395 . . . . . . . . . 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
) )
142140, 141syl 15 . . . . . . . . 9  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ran  ( k  e.  ( 0 ... M
)  |->  ( N  -  ( 2  x.  k
) ) )  C_  ( 0 ... N
) )
143142sselda 3180 . . . . . . . 8  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  m  e.  ran  ( k  e.  ( 0 ... M ) 
|->  ( N  -  (
2  x.  k ) ) ) )  ->  m  e.  ( 0 ... N ) )
144 bccl2 11335 . . . . . . . . . . 11  |-  ( m  e.  ( 0 ... N )  ->  ( N  _C  m )  e.  NN )
145144adantl 452 . . . . . . . . . 10  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  m  e.  ( 0 ... N ) )  ->  ( N  _C  m )  e.  NN )
146145nncnd 9762 . . . . . . . . 9  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  m  e.  ( 0 ... N ) )  ->  ( N  _C  m )  e.  CC )
1472rprecred 10401 . . . . . . . . . . . 12  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( 1  / 
( tan `  A
) )  e.  RR )
148 fznn0sub 10824 . . . . . . . . . . . 12  |-  ( m  e.  ( 0 ... N )  ->  ( N  -  m )  e.  NN0 )
149 reexpcl 11120 . . . . . . . . . . . 12  |-  ( ( ( 1  /  ( tan `  A ) )  e.  RR  /\  ( N  -  m )  e.  NN0 )  ->  (
( 1  /  ( tan `  A ) ) ^ ( N  -  m ) )  e.  RR )
150147, 148, 149syl2an 463 . . . . . . . . . . 11  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  m  e.  ( 0 ... N ) )  ->  ( (
1  /  ( tan `  A ) ) ^
( N  -  m
) )  e.  RR )
151150recnd 8861 . . . . . . . . . 10  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  m  e.  ( 0 ... N ) )  ->  ( (
1  /  ( tan `  A ) ) ^
( N  -  m
) )  e.  CC )
152 elfznn0 10822 . . . . . . . . . . . 12  |-  ( m  e.  ( 0 ... N )  ->  m  e.  NN0 )
153152adantl 452 . . . . . . . . . . 11  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  m  e.  ( 0 ... N ) )  ->  m  e.  NN0 )
154 expcl 11121 . . . . . . . . . . 11  |-  ( ( _i  e.  CC  /\  m  e.  NN0 )  -> 
( _i ^ m
)  e.  CC )
1555, 153, 154sylancr 644 . . . . . . . . . 10  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  m  e.  ( 0 ... N ) )  ->  ( _i ^ m )  e.  CC )
156151, 155mulcld 8855 . . . . . . . . 9  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  m  e.  ( 0 ... N ) )  ->  ( (
( 1  /  ( tan `  A ) ) ^ ( N  -  m ) )  x.  ( _i ^ m
) )  e.  CC )
157146, 156mulcld 8855 . . . . . . . 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 )
158143, 157syldan 456 . . . . . . 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 )
159158imcld 11680 . . . . . 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 )
160159recnd 8861 . . . . 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 )
16173, 74, 132, 138, 160fsumf1o 12196 . . . 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 ) ) ) ) ) ) )
162 eldifi 3298 . . . . . . . 8  |-  ( m  e.  ( ( 0 ... N )  \  ran  ( k  e.  ( 0 ... M ) 
|->  ( N  -  (
2  x.  k ) ) ) )  ->  m  e.  ( 0 ... N ) )
163145nnred 9761 . . . . . . . 8  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  m  e.  ( 0 ... N ) )  ->  ( N  _C  m )  e.  RR )
164162, 163sylan2 460 . . . . . . 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 )
165162, 150sylan2 460 . . . . . . . 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 )
166 eldif 3162 . . . . . . . . 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
) ) ) ) )
167 elfzelz 10798 . . . . . . . . . . . . . . 15  |-  ( m  e.  ( 0 ... N )  ->  m  e.  ZZ )
168167adantl 452 . . . . . . . . . . . . . 14  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  m  e.  ( 0 ... N ) )  ->  m  e.  ZZ )
169 zeo 10097 . . . . . . . . . . . . . 14  |-  ( m  e.  ZZ  ->  (
( m  /  2
)  e.  ZZ  \/  ( ( m  + 
1 )  /  2
)  e.  ZZ ) )
170168, 169syl 15 . . . . . . . . . . . . 13  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  m  e.  ( 0 ... N ) )  ->  ( (
m  /  2 )  e.  ZZ  \/  (
( m  +  1 )  /  2 )  e.  ZZ ) )
171 i2 11203 . . . . . . . . . . . . . . . . . 18  |-  ( _i
^ 2 )  = 
-u 1
172171oveq1i 5868 . . . . . . . . . . . . . . . . 17  |-  ( ( _i ^ 2 ) ^ ( m  / 
2 ) )  =  ( -u 1 ^ ( m  /  2
) )
173 simprr 733 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( m  /  2 )  e.  ZZ ) )  -> 
( m  /  2
)  e.  ZZ )
174152ad2antrl 708 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( m  /  2 )  e.  ZZ ) )  ->  m  e.  NN0 )
175 nn0re 9974 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( m  e.  NN0  ->  m  e.  RR )
176 nn0ge0 9991 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( m  e.  NN0  ->  0  <_  m )
177 divge0 9625 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( m  e.  RR  /\  0  <_  m )  /\  ( 2  e.  RR  /\  0  <  2 ) )  ->  0  <_  ( m  /  2 ) )
17889, 90, 177mpanr12 666 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( m  e.  RR  /\  0  <_  m )  -> 
0  <_  ( m  /  2 ) )
179175, 176, 178syl2anc 642 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  e.  NN0  ->  0  <_ 
( m  /  2
) )
180174, 179syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( m  /  2 )  e.  ZZ ) )  -> 
0  <_  ( m  /  2 ) )
181 elnn0z 10036 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( m  /  2 )  e.  NN0  <->  ( ( m  /  2 )  e.  ZZ  /\  0  <_ 
( m  /  2
) ) )
182173, 180, 181sylanbrc 645 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( m  /  2 )  e.  ZZ ) )  -> 
( m  /  2
)  e.  NN0 )
183 expmul 11147 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( _i  e.  CC  /\  2  e.  NN0  /\  (
m  /  2 )  e.  NN0 )  -> 
( _i ^ (
2  x.  ( m  /  2 ) ) )  =  ( ( _i ^ 2 ) ^ ( m  / 
2 ) ) )
1845, 75, 183mp3an12 1267 . . . . . . . . . . . . . . . . . . 19  |-  ( ( m  /  2 )  e.  NN0  ->  ( _i
^ ( 2  x.  ( m  /  2
) ) )  =  ( ( _i ^
2 ) ^ (
m  /  2 ) ) )
185182, 184syl 15 . . . . . . . . . . . . . . . . . 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 ) ) )
186174nn0cnd 10020 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( m  /  2 )  e.  ZZ ) )  ->  m  e.  CC )
187 divcan2 9432 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( m  e.  CC  /\  2  e.  CC  /\  2  =/=  0 )  ->  (
2  x.  ( m  /  2 ) )  =  m )
188110, 123, 187mp3an23 1269 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  e.  CC  ->  (
2  x.  ( m  /  2 ) )  =  m )
189186, 188syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( m  /  2 )  e.  ZZ ) )  -> 
( 2  x.  (
m  /  2 ) )  =  m )
190189oveq2d 5874 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( m  /  2 )  e.  ZZ ) )  -> 
( _i ^ (
2  x.  ( m  /  2 ) ) )  =  ( _i
^ m ) )
191185, 190eqtr3d 2317 . . . . . . . . . . . . . . . . 17  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( m  /  2 )  e.  ZZ ) )  -> 
( ( _i ^
2 ) ^ (
m  /  2 ) )  =  ( _i
^ m ) )
192172, 191syl5eqr 2329 . . . . . . . . . . . . . . . 16  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( m  /  2 )  e.  ZZ ) )  -> 
( -u 1 ^ (
m  /  2 ) )  =  ( _i
^ m ) )
193 1re 8837 . . . . . . . . . . . . . . . . . 18  |-  1  e.  RR
194193renegcli 9108 . . . . . . . . . . . . . . . . 17  |-  -u 1  e.  RR
195 reexpcl 11120 . . . . . . . . . . . . . . . . 17  |-  ( (
-u 1  e.  RR  /\  ( m  /  2
)  e.  NN0 )  ->  ( -u 1 ^ ( m  /  2
) )  e.  RR )
196194, 182, 195sylancr 644 . . . . . . . . . . . . . . . 16  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( m  /  2 )  e.  ZZ ) )  -> 
( -u 1 ^ (
m  /  2 ) )  e.  RR )
197192, 196eqeltrrd 2358 . . . . . . . . . . . . . . 15  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( m  /  2 )  e.  ZZ ) )  -> 
( _i ^ m
)  e.  RR )
198197expr 598 . . . . . . . . . . . . . 14  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  m  e.  ( 0 ... N ) )  ->  ( (
m  /  2 )  e.  ZZ  ->  (
_i ^ m )  e.  RR ) )
199148ad2antrl 708 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( N  -  m
)  e.  NN0 )
200 nn0re 9974 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( N  -  m )  e.  NN0  ->  ( N  -  m )  e.  RR )
201 nn0ge0 9991 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( N  -  m )  e.  NN0  ->  0  <_ 
( N  -  m
) )
202 divge0 9625 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( N  -  m )  e.  RR  /\  0  <_  ( N  -  m ) )  /\  ( 2  e.  RR  /\  0  <  2 ) )  ->  0  <_  ( ( N  -  m
)  /  2 ) )
20389, 90, 202mpanr12 666 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( N  -  m
)  e.  RR  /\  0  <_  ( N  -  m ) )  -> 
0  <_  ( ( N  -  m )  /  2 ) )
204200, 201, 203syl2anc 642 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( N  -  m )  e.  NN0  ->  0  <_ 
( ( N  -  m )  /  2
) )
205199, 204syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
0  <_  ( ( N  -  m )  /  2 ) )
206199nn0red 10019 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( N  -  m
)  e.  RR )
20749adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  ->  N  e.  RR )
208 peano2re 8985 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( N  e.  RR  ->  ( N  +  1 )  e.  RR )
209207, 208syl 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( N  +  1 )  e.  RR )
210152ad2antrl 708 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  ->  m  e.  NN0 )
211210, 176syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
0  <_  m )
212210nn0red 10019 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  ->  m  e.  RR )
213207, 212subge02d 9364 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( 0  <_  m  <->  ( N  -  m )  <_  N ) )
214211, 213mpbid 201 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( N  -  m
)  <_  N )
215207ltp1d 9687 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  ->  N  <  ( N  + 
1 ) )
216206, 207, 209, 214, 215lelttrd 8974 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( N  -  m
)  <  ( N  +  1 ) )
217110mulid1i 8839 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 2  x.  1 )  =  2
218 df-2 9804 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  2  =  ( 1  +  1 )
219217, 218eqtr2i 2304 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 1  +  1 )  =  ( 2  x.  1 )
220219oveq2i 5869 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 2  x.  M )  +  ( 1  +  1 ) )  =  ( ( 2  x.  M )  +  ( 2  x.  1 ) )
2217oveq1i 5868 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( N  +  1 )  =  ( ( ( 2  x.  M )  +  1 )  +  1 )
22211nncnd 9762 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( 2  x.  M )  e.  CC )
223222adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( 2  x.  M
)  e.  CC )
224 ax-1cn 8795 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  1  e.  CC
225224a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
1  e.  CC )
226223, 225, 225addassd 8857 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
227221, 226syl5eq 2327 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
228110a1i 10 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
2  e.  CC )
229 nncn 9754 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( M  e.  NN  ->  M  e.  CC )
230229ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  ->  M  e.  CC )
231228, 230, 225adddid 8859 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
232220, 227, 2313eqtr4a 2341 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( N  +  1 )  =  ( 2  x.  ( M  + 
1 ) ) )
233216, 232breqtrd 4047 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( N  -  m
)  <  ( 2  x.  ( M  + 
1 ) ) )
234 nnz 10045 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( M  e.  NN  ->  M  e.  ZZ )
235234ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  ->  M  e.  ZZ )
236235peano2zd 10120 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( M  +  1 )  e.  ZZ )
237236zred 10117 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( M  +  1 )  e.  RR )
23891a1i 10 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( 2  e.  RR  /\  0  <  2 ) )
239 ltdivmul 9628 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
240206, 237, 238, 239syl3anc 1182 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
241233, 240mpbird 223 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( ( N  -  m )  /  2
)  <  ( M  +  1 ) )
242108adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  ->  N  e.  CC )
243210nn0cnd 10020 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  ->  m  e.  CC )
244242, 243, 225pnpcan2d 9195 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( ( N  + 
1 )  -  (
m  +  1 ) )  =  ( N  -  m ) )
245232oveq1d 5873 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
246244, 245eqtr3d 2317 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
247246oveq1d 5873 . . . . . . . . . . . . . . . . . . . . . . 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 ) )
248236zcnd 10118 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( M  +  1 )  e.  CC )
249 mulcl 8821 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 2  e.  CC  /\  ( M  +  1
)  e.  CC )  ->  ( 2  x.  ( M  +  1 ) )  e.  CC )
250110, 248, 249sylancr 644 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( 2  x.  ( M  +  1 ) )  e.  CC )
251 peano2cn 8984 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( m  e.  CC  ->  (
m  +  1 )  e.  CC )
252243, 251syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( m  +  1 )  e.  CC )
253124a1i 10 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( 2  e.  CC  /\  2  =/=  0 ) )
254 divsubdir 9456 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
255250, 252, 253, 254syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
256123a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
2  =/=  0 )
257248, 228, 256divcan3d 9541 . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
258257oveq1d 5873 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
259247, 255, 2583eqtrd 2319 . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
260 simprr 733 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( ( m  + 
1 )  /  2
)  e.  ZZ )
261236, 260zsubcld 10122 . . . . . . . . . . . . . . . . . . . . . 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 )
262259, 261eqeltrd 2357 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( ( N  -  m )  /  2
)  e.  ZZ )
263 zleltp1 10068 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( N  -  m )  /  2
)  e.  ZZ  /\  M  e.  ZZ )  ->  ( ( ( N  -  m )  / 
2 )  <_  M  <->  ( ( N  -  m
)  /  2 )  <  ( M  + 
1 ) ) )
264262, 235, 263syl2anc 642 . . . . . . . . . . . . . . . . . . . 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 ) ) )
265241, 264mpbird 223 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( ( N  -  m )  /  2
)  <_  M )
266 0z 10035 . . . . . . . . . . . . . . . . . . . . 21  |-  0  e.  ZZ
267266a1i 10 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
0  e.  ZZ )
268 elfz 10788 . . . . . . . . . . . . . . . . . . . 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 ) ) )
269262, 267, 235, 268syl3anc 1182 . . . . . . . . . . . . . . . . . . 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
) ) )
270205, 265, 269mpbir2and 888 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( ( N  -  m )  /  2
)  e.  ( 0 ... M ) )
271 oveq2 5866 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  ( ( N  -  m )  / 
2 )  ->  (
2  x.  k )  =  ( 2  x.  ( ( N  -  m )  /  2
) ) )
272271oveq2d 5874 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  ( ( N  -  m )  / 
2 )  ->  ( N  -  ( 2  x.  k ) )  =  ( N  -  ( 2  x.  (
( N  -  m
)  /  2 ) ) ) )
273 ovex 5883 . . . . . . . . . . . . . . . . . . 19  |-  ( N  -  ( 2  x.  ( ( N  -  m )  /  2
) ) )  e. 
_V
274272, 135, 273fvmpt 5602 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( N  -  m
)  /  2 )  e.  ( 0 ... M )  ->  (
( k  e.  ( 0 ... M ) 
|->  ( N  -  (
2  x.  k ) ) ) `  (
( N  -  m
)  /  2 ) )  =  ( N  -  ( 2  x.  ( ( N  -  m )  /  2
) ) ) )
275270, 274syl 15 . . . . . . . . . . . . . . . . 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 ) ) ) )
276199nn0cnd 10020 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( N  -  m
)  e.  CC )
277276, 228, 256divcan2d 9538 . . . . . . . . . . . . . . . . . 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 ) )
278277oveq2d 5874 . . . . . . . . . . . . . . . . 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 ) ) )
279242, 243nncand 9162 . . . . . . . . . . . . . . . . 17  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  ( m  e.  ( 0 ... N
)  /\  ( (
m  +  1 )  /  2 )  e.  ZZ ) )  -> 
( N  -  ( N  -  m )
)  =  m )
280275, 278, 2793eqtrd 2319 . . . . . . . . . . . . . . . 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 )
281 ffn 5389 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  ( 0 ... M )  |->  ( N  -  ( 2  x.  k ) ) ) : ( 0 ... M ) --> ( 0 ... N )  ->  ( k  e.  ( 0 ... M
)  |->  ( N  -  ( 2  x.  k
) ) )  Fn  ( 0 ... M
) )
282140, 281syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( k  e.  ( 0 ... M
)  |->  ( N  -  ( 2  x.  k
) ) )  Fn  ( 0 ... M
) )
283282adantr 451 . . . . . . . . . . . . . . . . 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 ) )
284 fnfvelrn 5662 . . . . . . . . . . . . . . . . 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
) ) ) )
285283, 270, 284syl2anc 642 . . . . . . . . . . . . . . . 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 ) ) ) )
286280, 285eqeltrrd 2358 . . . . . . . . . . . . . . 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 ) ) ) )
287286expr 598 . . . . . . . . . . . . . 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
) ) ) ) )
288198, 287orim12d 811 . . . . . . . . . . . . 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
) ) ) ) ) )
289170, 288mpd 14 . . . . . . . . . . . 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
) ) ) ) )
290289orcomd 377 . . . . . . . . . . 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 ) )
291290ord 366 . . . . . . . . . 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 ) )
292291impr 602 . . . . . . . . 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 )
293166, 292sylan2b 461 . . . . . . . 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 )
294165, 293remulcld 8863 . . . . . . 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 )
295164, 294remulcld 8863 . . . . . 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 )
296295reim0d 11710 . . . . 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 )
297 fzfid 11035 . . . . 5  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( 0 ... N )  e.  Fin )
298142, 160, 296, 297fsumss 12198 . . . 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 ) ) ) ) )
29914adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  N  e.  NN0 )
300 elfznn0 10822 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( 0 ... M )  ->  j  e.  NN0 )
301300adantl 452 . . . . . . . . . . . . . . . . 17  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  j  e.  NN0 )
302 nn0mulcl 10000 . . . . . . . . . . . . . . . . 17  |-  ( ( 2  e.  NN0  /\  j  e.  NN0 )  -> 
( 2  x.  j
)  e.  NN0 )
30375, 301, 302sylancr 644 . . . . . . . . . . . . . . . 16  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( 2  x.  j )  e. 
NN0 )
304303nn0zd 10115 . . . . . . . . . . . . . . 15  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( 2  x.  j )  e.  ZZ )
305 bccl 11334 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  NN0  /\  ( 2  x.  j
)  e.  ZZ )  ->  ( N  _C  ( 2  x.  j
) )  e.  NN0 )
306299, 304, 305syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( N  _C  ( 2  x.  j
) )  e.  NN0 )
307306nn0red 10019 . . . . . . . . . . . . 13  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( N  _C  ( 2  x.  j
) )  e.  RR )
308 fznn0sub 10824 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 0 ... M )  ->  ( M  -  j )  e.  NN0 )
309308adantl 452 . . . . . . . . . . . . . 14  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( M  -  j )  e. 
NN0 )
310 reexpcl 11120 . . . . . . . . . . . . . 14  |-  ( (
-u 1  e.  RR  /\  ( M  -  j
)  e.  NN0 )  ->  ( -u 1 ^ ( M  -  j
) )  e.  RR )
311194, 309, 310sylancr 644 . . . . . . . . . . . . 13  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( -u 1 ^ ( M  -  j ) )  e.  RR )
312307, 311remulcld 8863 . . . . . . . . . . . 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 )
313 2z 10054 . . . . . . . . . . . . . . . 16  |-  2  e.  ZZ
314 znegcl 10055 . . . . . . . . . . . . . . . 16  |-  ( 2  e.  ZZ  ->  -u 2  e.  ZZ )
315313, 314ax-mp 8 . . . . . . . . . . . . . . 15  |-  -u 2  e.  ZZ
316 rpexpcl 11122 . . . . . . . . . . . . . . 15  |-  ( ( ( tan `  A
)  e.  RR+  /\  -u 2  e.  ZZ )  ->  (
( tan `  A
) ^ -u 2
)  e.  RR+ )
3172, 315, 316sylancl 643 . . . . . . . . . . . . . 14  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( ( tan `  A ) ^ -u 2
)  e.  RR+ )
318317rpred 10390 . . . . . . . . . . . . 13  |-  ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  ->  ( ( tan `  A ) ^ -u 2
)  e.  RR )
319 reexpcl 11120 . . . . . . . . . . . . 13  |-  ( ( ( ( tan `  A
) ^ -u 2
)  e.  RR  /\  j  e.  NN0 )  -> 
( ( ( tan `  A ) ^ -u 2
) ^ j )  e.  RR )
320318, 300, 319syl2an 463 . . . . . . . . . . . 12  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( (
( tan `  A
) ^ -u 2
) ^ j )  e.  RR )
321312, 320remulcld 8863 . . . . . . . . . . 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 )
322321recnd 8861 . . . . . . . . . 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 )
323 mulcl 8821 . . . . . . . . . 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 )
3245, 322, 323sylancr 644 . . . . . . . . 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 )
325324addid2d 9013 . . . . . . . 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 ) ) ) )
326306nn0cnd 10020 . . . . . . . . . . 11  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( N  _C  ( 2  x.  j
) )  e.  CC )
327311recnd 8861 . . . . . . . . . . 11  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( -u 1 ^ ( M  -  j ) )  e.  CC )
328320recnd 8861 . . . . . . . . . . 11  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( (
( tan `  A
) ^ -u 2
) ^ j )  e.  CC )
329326, 327, 328mulassd 8858 . . . . . . . . . 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 ) ) ) )
330329oveq2d 5874 . . . . . . . . 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 ) ) ) ) )
3315a1i 10 . . . . . . . . . 10  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  _i  e.  CC )
332327, 328mulcld 8855 . . . . . . . . . 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 )
333331, 326, 332mul12d 9021 . . . . . . . . 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 ) ) ) ) )
334330, 333eqtrd 2315 . . . . . . . 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 ) ) ) ) )
335 bccmpl 11322 . . . . . . . . . 10  |-  ( ( N  e.  NN0  /\  ( 2  x.  j
)  e.  ZZ )  ->  ( N  _C  ( 2  x.  j
) )  =  ( N  _C  ( N  -  ( 2  x.  j ) ) ) )
336299, 304, 335syl2anc 642 . . . . . . . . 9  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( N  _C  ( 2  x.  j
) )  =  ( N  _C  ( N  -  ( 2  x.  j ) ) ) )
337108adantr 451 . . . . . . . . . . . . . 14  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  N  e.  CC )
338303nn0cnd 10020 . . . . . . . . . . . . . 14  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( 2  x.  j )  e.  CC )
339337, 338nncand 9162 . . . . . . . . . . . . 13  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( N  -  ( N  -  ( 2  x.  j
) ) )  =  ( 2  x.  j
) )
340339oveq2d 5874 . . . . . . . . . . . 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 ) ) )
3412adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( tan `  A )  e.  RR+ )
342341rpcnd 10392 . . . . . . . . . . . . . 14  |-  ( ( ( M  e.  NN  /\  A  e.  ( 0 (,) ( pi  / 
2 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( tan `  A )  e.  CC )
343 expneg 11111 . . . . . . . . . . . . . 14  |-  ( ( ( tan `  A
)  e.  CC  /\  ( 2  x.  j
)  e.  NN0 )  ->  ( ( tan `  A
) ^ -u (
2  x.  j ) )  =  ( 1  /  ( ( tan `  A ) ^ (
2  x.  j ) ) ) )
344342, 303, 343syl2anc 642 . . . . . . . . . . . . 13