Metamath Proof Explorer

Theorem basellem4

Description: Lemma for basel . By basellem3 , the expression P ( ( cot x ) ^ 2 ) = sin ( N x ) / ( sin x ) ^ N goes to zero whenever x = n _pi / N for some n e. ( 1 ... M ) , so this function enumerates M distinct roots of a degree- M polynomial, which must therefore be all the roots by fta1 . (Contributed by Mario Carneiro, 28-Jul-2014)

Ref Expression
Hypotheses basel.n 
|- N = ( ( 2 x. M ) + 1 )
basel.p 
|- P = ( t e. CC |-> sum_ j e. ( 0 ... M ) ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( t ^ j ) ) )
basel.t 
|- T = ( n e. ( 1 ... M ) |-> ( ( tan ` ( ( n x. _pi ) / N ) ) ^ -u 2 ) )
Assertion basellem4 
|- ( M e. NN -> T : ( 1 ... M ) -1-1-onto-> ( `' P " { 0 } ) )

Proof

Step Hyp Ref Expression
1 basel.n 
 |-  N = ( ( 2 x. M ) + 1 )
2 basel.p 
 |-  P = ( t e. CC |-> sum_ j e. ( 0 ... M ) ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( t ^ j ) ) )
3 basel.t 
 |-  T = ( n e. ( 1 ... M ) |-> ( ( tan ` ( ( n x. _pi ) / N ) ) ^ -u 2 ) )
4 1 basellem1 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( ( n x. _pi ) / N ) e. ( 0 (,) ( _pi / 2 ) ) )
5 tanrpcl 
 |-  ( ( ( n x. _pi ) / N ) e. ( 0 (,) ( _pi / 2 ) ) -> ( tan ` ( ( n x. _pi ) / N ) ) e. RR+ )
6 4 5 syl 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( tan ` ( ( n x. _pi ) / N ) ) e. RR+ )
7 2z 
 |-  2 e. ZZ
8 znegcl 
 |-  ( 2 e. ZZ -> -u 2 e. ZZ )
9 7 8 ax-mp 
 |-  -u 2 e. ZZ
10 rpexpcl 
 |-  ( ( ( tan ` ( ( n x. _pi ) / N ) ) e. RR+ /\ -u 2 e. ZZ ) -> ( ( tan ` ( ( n x. _pi ) / N ) ) ^ -u 2 ) e. RR+ )
11 6 9 10 sylancl 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( ( tan ` ( ( n x. _pi ) / N ) ) ^ -u 2 ) e. RR+ )
12 11 rpcnd 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( ( tan ` ( ( n x. _pi ) / N ) ) ^ -u 2 ) e. CC )
13 1 2 basellem3 
 |-  ( ( M e. NN /\ ( ( n x. _pi ) / N ) e. ( 0 (,) ( _pi / 2 ) ) ) -> ( P ` ( ( tan ` ( ( n x. _pi ) / N ) ) ^ -u 2 ) ) = ( ( sin ` ( N x. ( ( n x. _pi ) / N ) ) ) / ( ( sin ` ( ( n x. _pi ) / N ) ) ^ N ) ) )
14 4 13 syldan 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( P ` ( ( tan ` ( ( n x. _pi ) / N ) ) ^ -u 2 ) ) = ( ( sin ` ( N x. ( ( n x. _pi ) / N ) ) ) / ( ( sin ` ( ( n x. _pi ) / N ) ) ^ N ) ) )
15 elfzelz 
 |-  ( n e. ( 1 ... M ) -> n e. ZZ )
16 15 adantl 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> n e. ZZ )
17 16 zred 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> n e. RR )
18 pire 
 |-  _pi e. RR
19 remulcl 
 |-  ( ( n e. RR /\ _pi e. RR ) -> ( n x. _pi ) e. RR )
20 17 18 19 sylancl 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( n x. _pi ) e. RR )
21 20 recnd 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( n x. _pi ) e. CC )
22 2nn 
 |-  2 e. NN
23 nnmulcl 
 |-  ( ( 2 e. NN /\ M e. NN ) -> ( 2 x. M ) e. NN )
24 22 23 mpan 
 |-  ( M e. NN -> ( 2 x. M ) e. NN )
25 24 peano2nnd 
 |-  ( M e. NN -> ( ( 2 x. M ) + 1 ) e. NN )
26 1 25 eqeltrid 
 |-  ( M e. NN -> N e. NN )
27 26 adantr 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> N e. NN )
28 27 nncnd 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> N e. CC )
29 27 nnne0d 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> N =/= 0 )
30 21 28 29 divcan2d 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( N x. ( ( n x. _pi ) / N ) ) = ( n x. _pi ) )
31 30 fveq2d 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( sin ` ( N x. ( ( n x. _pi ) / N ) ) ) = ( sin ` ( n x. _pi ) ) )
32 sinkpi 
 |-  ( n e. ZZ -> ( sin ` ( n x. _pi ) ) = 0 )
33 16 32 syl 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( sin ` ( n x. _pi ) ) = 0 )
34 31 33 eqtrd 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( sin ` ( N x. ( ( n x. _pi ) / N ) ) ) = 0 )
35 34 oveq1d 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( ( sin ` ( N x. ( ( n x. _pi ) / N ) ) ) / ( ( sin ` ( ( n x. _pi ) / N ) ) ^ N ) ) = ( 0 / ( ( sin ` ( ( n x. _pi ) / N ) ) ^ N ) ) )
36 20 27 nndivred 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( ( n x. _pi ) / N ) e. RR )
37 36 resincld 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( sin ` ( ( n x. _pi ) / N ) ) e. RR )
38 37 recnd 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( sin ` ( ( n x. _pi ) / N ) ) e. CC )
39 27 nnnn0d 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> N e. NN0 )
40 38 39 expcld 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( ( sin ` ( ( n x. _pi ) / N ) ) ^ N ) e. CC )
41 sincosq1sgn 
 |-  ( ( ( n x. _pi ) / N ) e. ( 0 (,) ( _pi / 2 ) ) -> ( 0 < ( sin ` ( ( n x. _pi ) / N ) ) /\ 0 < ( cos ` ( ( n x. _pi ) / N ) ) ) )
42 4 41 syl 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( 0 < ( sin ` ( ( n x. _pi ) / N ) ) /\ 0 < ( cos ` ( ( n x. _pi ) / N ) ) ) )
43 42 simpld 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> 0 < ( sin ` ( ( n x. _pi ) / N ) ) )
44 43 gt0ne0d 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( sin ` ( ( n x. _pi ) / N ) ) =/= 0 )
45 27 nnzd 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> N e. ZZ )
46 38 44 45 expne0d 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( ( sin ` ( ( n x. _pi ) / N ) ) ^ N ) =/= 0 )
47 40 46 div0d 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( 0 / ( ( sin ` ( ( n x. _pi ) / N ) ) ^ N ) ) = 0 )
48 14 35 47 3eqtrd 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( P ` ( ( tan ` ( ( n x. _pi ) / N ) ) ^ -u 2 ) ) = 0 )
49 1 2 basellem2 
 |-  ( M e. NN -> ( P e. ( Poly ` CC ) /\ ( deg ` P ) = M /\ ( coeff ` P ) = ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ) )
50 49 simp1d 
 |-  ( M e. NN -> P e. ( Poly ` CC ) )
51 plyf 
 |-  ( P e. ( Poly ` CC ) -> P : CC --> CC )
52 ffn 
 |-  ( P : CC --> CC -> P Fn CC )
53 50 51 52 3syl 
 |-  ( M e. NN -> P Fn CC )
54 53 adantr 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> P Fn CC )
55 fniniseg 
 |-  ( P Fn CC -> ( ( ( tan ` ( ( n x. _pi ) / N ) ) ^ -u 2 ) e. ( `' P " { 0 } ) <-> ( ( ( tan ` ( ( n x. _pi ) / N ) ) ^ -u 2 ) e. CC /\ ( P ` ( ( tan ` ( ( n x. _pi ) / N ) ) ^ -u 2 ) ) = 0 ) ) )
56 54 55 syl 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( ( ( tan ` ( ( n x. _pi ) / N ) ) ^ -u 2 ) e. ( `' P " { 0 } ) <-> ( ( ( tan ` ( ( n x. _pi ) / N ) ) ^ -u 2 ) e. CC /\ ( P ` ( ( tan ` ( ( n x. _pi ) / N ) ) ^ -u 2 ) ) = 0 ) ) )
57 12 48 56 mpbir2and 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( ( tan ` ( ( n x. _pi ) / N ) ) ^ -u 2 ) e. ( `' P " { 0 } ) )
58 57 3 fmptd 
 |-  ( M e. NN -> T : ( 1 ... M ) --> ( `' P " { 0 } ) )
59 fveq2 
 |-  ( k = m -> ( T ` k ) = ( T ` m ) )
60 fveq2 
 |-  ( k = x -> ( T ` k ) = ( T ` x ) )
61 fveq2 
 |-  ( k = y -> ( T ` k ) = ( T ` y ) )
62 15 zred 
 |-  ( n e. ( 1 ... M ) -> n e. RR )
63 62 ssriv 
 |-  ( 1 ... M ) C_ RR
64 11 rpred 
 |-  ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( ( tan ` ( ( n x. _pi ) / N ) ) ^ -u 2 ) e. RR )
65 64 3 fmptd 
 |-  ( M e. NN -> T : ( 1 ... M ) --> RR )
66 65 ffvelcdmda 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( T ` k ) e. RR )
67 simplr 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> k < m )
68 63 sseli 
 |-  ( k e. ( 1 ... M ) -> k e. RR )
69 68 ad2antrl 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> k e. RR )
70 63 sseli 
 |-  ( m e. ( 1 ... M ) -> m e. RR )
71 70 ad2antll 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> m e. RR )
72 18 a1i 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> _pi e. RR )
73 pipos 
 |-  0 < _pi
74 73 a1i 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> 0 < _pi )
75 ltmul1 
 |-  ( ( k e. RR /\ m e. RR /\ ( _pi e. RR /\ 0 < _pi ) ) -> ( k < m <-> ( k x. _pi ) < ( m x. _pi ) ) )
76 69 71 72 74 75 syl112anc 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( k < m <-> ( k x. _pi ) < ( m x. _pi ) ) )
77 67 76 mpbid 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( k x. _pi ) < ( m x. _pi ) )
78 remulcl 
 |-  ( ( k e. RR /\ _pi e. RR ) -> ( k x. _pi ) e. RR )
79 69 18 78 sylancl 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( k x. _pi ) e. RR )
80 remulcl 
 |-  ( ( m e. RR /\ _pi e. RR ) -> ( m x. _pi ) e. RR )
81 71 18 80 sylancl 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( m x. _pi ) e. RR )
82 26 ad2antrr 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> N e. NN )
83 82 nnred 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> N e. RR )
84 82 nngt0d 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> 0 < N )
85 ltdiv1 
 |-  ( ( ( k x. _pi ) e. RR /\ ( m x. _pi ) e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( ( k x. _pi ) < ( m x. _pi ) <-> ( ( k x. _pi ) / N ) < ( ( m x. _pi ) / N ) ) )
86 79 81 83 84 85 syl112anc 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( ( k x. _pi ) < ( m x. _pi ) <-> ( ( k x. _pi ) / N ) < ( ( m x. _pi ) / N ) ) )
87 77 86 mpbid 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( ( k x. _pi ) / N ) < ( ( m x. _pi ) / N ) )
88 neghalfpirx 
 |-  -u ( _pi / 2 ) e. RR*
89 pirp 
 |-  _pi e. RR+
90 rphalfcl 
 |-  ( _pi e. RR+ -> ( _pi / 2 ) e. RR+ )
91 rpge0 
 |-  ( ( _pi / 2 ) e. RR+ -> 0 <_ ( _pi / 2 ) )
92 89 90 91 mp2b 
 |-  0 <_ ( _pi / 2 )
93 halfpire 
 |-  ( _pi / 2 ) e. RR
94 le0neg2 
 |-  ( ( _pi / 2 ) e. RR -> ( 0 <_ ( _pi / 2 ) <-> -u ( _pi / 2 ) <_ 0 ) )
95 93 94 ax-mp 
 |-  ( 0 <_ ( _pi / 2 ) <-> -u ( _pi / 2 ) <_ 0 )
96 92 95 mpbi 
 |-  -u ( _pi / 2 ) <_ 0
97 iooss1 
 |-  ( ( -u ( _pi / 2 ) e. RR* /\ -u ( _pi / 2 ) <_ 0 ) -> ( 0 (,) ( _pi / 2 ) ) C_ ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
98 88 96 97 mp2an 
 |-  ( 0 (,) ( _pi / 2 ) ) C_ ( -u ( _pi / 2 ) (,) ( _pi / 2 ) )
99 1 basellem1 
 |-  ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( k x. _pi ) / N ) e. ( 0 (,) ( _pi / 2 ) ) )
100 99 ad2ant2r 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( ( k x. _pi ) / N ) e. ( 0 (,) ( _pi / 2 ) ) )
101 98 100 sselid 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( ( k x. _pi ) / N ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
102 1 basellem1 
 |-  ( ( M e. NN /\ m e. ( 1 ... M ) ) -> ( ( m x. _pi ) / N ) e. ( 0 (,) ( _pi / 2 ) ) )
103 102 ad2ant2rl 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( ( m x. _pi ) / N ) e. ( 0 (,) ( _pi / 2 ) ) )
104 98 103 sselid 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( ( m x. _pi ) / N ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
105 tanord 
 |-  ( ( ( ( k x. _pi ) / N ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ ( ( m x. _pi ) / N ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( ( k x. _pi ) / N ) < ( ( m x. _pi ) / N ) <-> ( tan ` ( ( k x. _pi ) / N ) ) < ( tan ` ( ( m x. _pi ) / N ) ) ) )
106 101 104 105 syl2anc 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( ( ( k x. _pi ) / N ) < ( ( m x. _pi ) / N ) <-> ( tan ` ( ( k x. _pi ) / N ) ) < ( tan ` ( ( m x. _pi ) / N ) ) ) )
107 87 106 mpbid 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( tan ` ( ( k x. _pi ) / N ) ) < ( tan ` ( ( m x. _pi ) / N ) ) )
108 tanrpcl 
 |-  ( ( ( k x. _pi ) / N ) e. ( 0 (,) ( _pi / 2 ) ) -> ( tan ` ( ( k x. _pi ) / N ) ) e. RR+ )
109 100 108 syl 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( tan ` ( ( k x. _pi ) / N ) ) e. RR+ )
110 tanrpcl 
 |-  ( ( ( m x. _pi ) / N ) e. ( 0 (,) ( _pi / 2 ) ) -> ( tan ` ( ( m x. _pi ) / N ) ) e. RR+ )
111 103 110 syl 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( tan ` ( ( m x. _pi ) / N ) ) e. RR+ )
112 rprege0 
 |-  ( ( tan ` ( ( k x. _pi ) / N ) ) e. RR+ -> ( ( tan ` ( ( k x. _pi ) / N ) ) e. RR /\ 0 <_ ( tan ` ( ( k x. _pi ) / N ) ) ) )
113 rprege0 
 |-  ( ( tan ` ( ( m x. _pi ) / N ) ) e. RR+ -> ( ( tan ` ( ( m x. _pi ) / N ) ) e. RR /\ 0 <_ ( tan ` ( ( m x. _pi ) / N ) ) ) )
114 lt2sq 
 |-  ( ( ( ( tan ` ( ( k x. _pi ) / N ) ) e. RR /\ 0 <_ ( tan ` ( ( k x. _pi ) / N ) ) ) /\ ( ( tan ` ( ( m x. _pi ) / N ) ) e. RR /\ 0 <_ ( tan ` ( ( m x. _pi ) / N ) ) ) ) -> ( ( tan ` ( ( k x. _pi ) / N ) ) < ( tan ` ( ( m x. _pi ) / N ) ) <-> ( ( tan ` ( ( k x. _pi ) / N ) ) ^ 2 ) < ( ( tan ` ( ( m x. _pi ) / N ) ) ^ 2 ) ) )
115 112 113 114 syl2an 
 |-  ( ( ( tan ` ( ( k x. _pi ) / N ) ) e. RR+ /\ ( tan ` ( ( m x. _pi ) / N ) ) e. RR+ ) -> ( ( tan ` ( ( k x. _pi ) / N ) ) < ( tan ` ( ( m x. _pi ) / N ) ) <-> ( ( tan ` ( ( k x. _pi ) / N ) ) ^ 2 ) < ( ( tan ` ( ( m x. _pi ) / N ) ) ^ 2 ) ) )
116 109 111 115 syl2anc 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( ( tan ` ( ( k x. _pi ) / N ) ) < ( tan ` ( ( m x. _pi ) / N ) ) <-> ( ( tan ` ( ( k x. _pi ) / N ) ) ^ 2 ) < ( ( tan ` ( ( m x. _pi ) / N ) ) ^ 2 ) ) )
117 107 116 mpbid 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( ( tan ` ( ( k x. _pi ) / N ) ) ^ 2 ) < ( ( tan ` ( ( m x. _pi ) / N ) ) ^ 2 ) )
118 rpexpcl 
 |-  ( ( ( tan ` ( ( k x. _pi ) / N ) ) e. RR+ /\ 2 e. ZZ ) -> ( ( tan ` ( ( k x. _pi ) / N ) ) ^ 2 ) e. RR+ )
119 109 7 118 sylancl 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( ( tan ` ( ( k x. _pi ) / N ) ) ^ 2 ) e. RR+ )
120 rpexpcl 
 |-  ( ( ( tan ` ( ( m x. _pi ) / N ) ) e. RR+ /\ 2 e. ZZ ) -> ( ( tan ` ( ( m x. _pi ) / N ) ) ^ 2 ) e. RR+ )
121 111 7 120 sylancl 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( ( tan ` ( ( m x. _pi ) / N ) ) ^ 2 ) e. RR+ )
122 119 121 ltrecd 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( ( ( tan ` ( ( k x. _pi ) / N ) ) ^ 2 ) < ( ( tan ` ( ( m x. _pi ) / N ) ) ^ 2 ) <-> ( 1 / ( ( tan ` ( ( m x. _pi ) / N ) ) ^ 2 ) ) < ( 1 / ( ( tan ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) ) )
123 117 122 mpbid 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( 1 / ( ( tan ` ( ( m x. _pi ) / N ) ) ^ 2 ) ) < ( 1 / ( ( tan ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) )
124 oveq1 
 |-  ( n = m -> ( n x. _pi ) = ( m x. _pi ) )
125 124 fvoveq1d 
 |-  ( n = m -> ( tan ` ( ( n x. _pi ) / N ) ) = ( tan ` ( ( m x. _pi ) / N ) ) )
126 125 oveq1d 
 |-  ( n = m -> ( ( tan ` ( ( n x. _pi ) / N ) ) ^ -u 2 ) = ( ( tan ` ( ( m x. _pi ) / N ) ) ^ -u 2 ) )
127 ovex 
 |-  ( ( tan ` ( ( m x. _pi ) / N ) ) ^ -u 2 ) e. _V
128 126 3 127 fvmpt 
 |-  ( m e. ( 1 ... M ) -> ( T ` m ) = ( ( tan ` ( ( m x. _pi ) / N ) ) ^ -u 2 ) )
129 128 ad2antll 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( T ` m ) = ( ( tan ` ( ( m x. _pi ) / N ) ) ^ -u 2 ) )
130 111 rpcnd 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( tan ` ( ( m x. _pi ) / N ) ) e. CC )
131 2nn0 
 |-  2 e. NN0
132 expneg 
 |-  ( ( ( tan ` ( ( m x. _pi ) / N ) ) e. CC /\ 2 e. NN0 ) -> ( ( tan ` ( ( m x. _pi ) / N ) ) ^ -u 2 ) = ( 1 / ( ( tan ` ( ( m x. _pi ) / N ) ) ^ 2 ) ) )
133 130 131 132 sylancl 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( ( tan ` ( ( m x. _pi ) / N ) ) ^ -u 2 ) = ( 1 / ( ( tan ` ( ( m x. _pi ) / N ) ) ^ 2 ) ) )
134 129 133 eqtrd 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( T ` m ) = ( 1 / ( ( tan ` ( ( m x. _pi ) / N ) ) ^ 2 ) ) )
135 oveq1 
 |-  ( n = k -> ( n x. _pi ) = ( k x. _pi ) )
136 135 fvoveq1d 
 |-  ( n = k -> ( tan ` ( ( n x. _pi ) / N ) ) = ( tan ` ( ( k x. _pi ) / N ) ) )
137 136 oveq1d 
 |-  ( n = k -> ( ( tan ` ( ( n x. _pi ) / N ) ) ^ -u 2 ) = ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) )
138 ovex 
 |-  ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) e. _V
139 137 3 138 fvmpt 
 |-  ( k e. ( 1 ... M ) -> ( T ` k ) = ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) )
140 139 ad2antrl 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( T ` k ) = ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) )
141 109 rpcnd 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( tan ` ( ( k x. _pi ) / N ) ) e. CC )
142 expneg 
 |-  ( ( ( tan ` ( ( k x. _pi ) / N ) ) e. CC /\ 2 e. NN0 ) -> ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) = ( 1 / ( ( tan ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) )
143 141 131 142 sylancl 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( ( tan ` ( ( k x. _pi ) / N ) ) ^ -u 2 ) = ( 1 / ( ( tan ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) )
144 140 143 eqtrd 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( T ` k ) = ( 1 / ( ( tan ` ( ( k x. _pi ) / N ) ) ^ 2 ) ) )
145 123 134 144 3brtr4d 
 |-  ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( T ` m ) < ( T ` k ) )
146 145 an32s 
 |-  ( ( ( M e. NN /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) /\ k < m ) -> ( T ` m ) < ( T ` k ) )
147 146 ex 
 |-  ( ( M e. NN /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( k < m -> ( T ` m ) < ( T ` k ) ) )
148 59 60 61 63 66 147 eqord2 
 |-  ( ( M e. NN /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... M ) ) ) -> ( x = y <-> ( T ` x ) = ( T ` y ) ) )
149 148 biimprd 
 |-  ( ( M e. NN /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... M ) ) ) -> ( ( T ` x ) = ( T ` y ) -> x = y ) )
150 149 ralrimivva 
 |-  ( M e. NN -> A. x e. ( 1 ... M ) A. y e. ( 1 ... M ) ( ( T ` x ) = ( T ` y ) -> x = y ) )
151 dff13 
 |-  ( T : ( 1 ... M ) -1-1-> ( `' P " { 0 } ) <-> ( T : ( 1 ... M ) --> ( `' P " { 0 } ) /\ A. x e. ( 1 ... M ) A. y e. ( 1 ... M ) ( ( T ` x ) = ( T ` y ) -> x = y ) ) )
152 58 150 151 sylanbrc 
 |-  ( M e. NN -> T : ( 1 ... M ) -1-1-> ( `' P " { 0 } ) )
153 49 simp2d 
 |-  ( M e. NN -> ( deg ` P ) = M )
154 nnne0 
 |-  ( M e. NN -> M =/= 0 )
155 153 154 eqnetrd 
 |-  ( M e. NN -> ( deg ` P ) =/= 0 )
156 fveq2 
 |-  ( P = 0p -> ( deg ` P ) = ( deg ` 0p ) )
157 dgr0 
 |-  ( deg ` 0p ) = 0
158 156 157 eqtrdi 
 |-  ( P = 0p -> ( deg ` P ) = 0 )
159 158 necon3i 
 |-  ( ( deg ` P ) =/= 0 -> P =/= 0p )
160 155 159 syl 
 |-  ( M e. NN -> P =/= 0p )
161 eqid 
 |-  ( `' P " { 0 } ) = ( `' P " { 0 } )
162 161 fta1 
 |-  ( ( P e. ( Poly ` CC ) /\ P =/= 0p ) -> ( ( `' P " { 0 } ) e. Fin /\ ( # ` ( `' P " { 0 } ) ) <_ ( deg ` P ) ) )
163 50 160 162 syl2anc 
 |-  ( M e. NN -> ( ( `' P " { 0 } ) e. Fin /\ ( # ` ( `' P " { 0 } ) ) <_ ( deg ` P ) ) )
164 163 simpld 
 |-  ( M e. NN -> ( `' P " { 0 } ) e. Fin )
165 f1domg 
 |-  ( ( `' P " { 0 } ) e. Fin -> ( T : ( 1 ... M ) -1-1-> ( `' P " { 0 } ) -> ( 1 ... M ) ~<_ ( `' P " { 0 } ) ) )
166 164 152 165 sylc 
 |-  ( M e. NN -> ( 1 ... M ) ~<_ ( `' P " { 0 } ) )
167 163 simprd 
 |-  ( M e. NN -> ( # ` ( `' P " { 0 } ) ) <_ ( deg ` P ) )
168 nnnn0 
 |-  ( M e. NN -> M e. NN0 )
169 hashfz1 
 |-  ( M e. NN0 -> ( # ` ( 1 ... M ) ) = M )
170 168 169 syl 
 |-  ( M e. NN -> ( # ` ( 1 ... M ) ) = M )
171 153 170 eqtr4d 
 |-  ( M e. NN -> ( deg ` P ) = ( # ` ( 1 ... M ) ) )
172 167 171 breqtrd 
 |-  ( M e. NN -> ( # ` ( `' P " { 0 } ) ) <_ ( # ` ( 1 ... M ) ) )
173 fzfid 
 |-  ( M e. NN -> ( 1 ... M ) e. Fin )
174 hashdom 
 |-  ( ( ( `' P " { 0 } ) e. Fin /\ ( 1 ... M ) e. Fin ) -> ( ( # ` ( `' P " { 0 } ) ) <_ ( # ` ( 1 ... M ) ) <-> ( `' P " { 0 } ) ~<_ ( 1 ... M ) ) )
175 164 173 174 syl2anc 
 |-  ( M e. NN -> ( ( # ` ( `' P " { 0 } ) ) <_ ( # ` ( 1 ... M ) ) <-> ( `' P " { 0 } ) ~<_ ( 1 ... M ) ) )
176 172 175 mpbid 
 |-  ( M e. NN -> ( `' P " { 0 } ) ~<_ ( 1 ... M ) )
177 sbth 
 |-  ( ( ( 1 ... M ) ~<_ ( `' P " { 0 } ) /\ ( `' P " { 0 } ) ~<_ ( 1 ... M ) ) -> ( 1 ... M ) ~~ ( `' P " { 0 } ) )
178 166 176 177 syl2anc 
 |-  ( M e. NN -> ( 1 ... M ) ~~ ( `' P " { 0 } ) )
179 f1finf1o 
 |-  ( ( ( 1 ... M ) ~~ ( `' P " { 0 } ) /\ ( `' P " { 0 } ) e. Fin ) -> ( T : ( 1 ... M ) -1-1-> ( `' P " { 0 } ) <-> T : ( 1 ... M ) -1-1-onto-> ( `' P " { 0 } ) ) )
180 178 164 179 syl2anc 
 |-  ( M e. NN -> ( T : ( 1 ... M ) -1-1-> ( `' P " { 0 } ) <-> T : ( 1 ... M ) -1-1-onto-> ( `' P " { 0 } ) ) )
181 152 180 mpbid 
 |-  ( M e. NN -> T : ( 1 ... M ) -1-1-onto-> ( `' P " { 0 } ) )