Metamath Proof Explorer

Theorem sinnpoly

Description: Sine function is not a polynomial with complex coefficients. Indeed, it has infinitely many zeros but is not constant zero, contrary to fta1 . (Contributed by Ender Ting, 10-Dec-2025)

Ref Expression
Assertion sinnpoly 
|- -. sin e. ( Poly ` CC )

Proof

Step Hyp Ref Expression
1 nnnfi 
 |-  -. NN e. Fin
2 4re 
 |-  4 e. RR
3 resincl 
 |-  ( 4 e. RR -> ( sin ` 4 ) e. RR )
4 2 3 ax-mp 
 |-  ( sin ` 4 ) e. RR
5 sin4lt0 
 |-  ( sin ` 4 ) < 0
6 df-0p 
 |-  0p = ( CC X. { 0 } )
7 6 fveq1i 
 |-  ( 0p ` 4 ) = ( ( CC X. { 0 } ) ` 4 )
8 4cn 
 |-  4 e. CC
9 c0ex 
 |-  0 e. _V
10 9 fvconst2 
 |-  ( 4 e. CC -> ( ( CC X. { 0 } ) ` 4 ) = 0 )
11 8 10 ax-mp 
 |-  ( ( CC X. { 0 } ) ` 4 ) = 0
12 7 11 eqtri 
 |-  ( 0p ` 4 ) = 0
13 12 eqcomi 
 |-  0 = ( 0p ` 4 )
14 5 13 breqtri 
 |-  ( sin ` 4 ) < ( 0p ` 4 )
15 4 14 ltneii 
 |-  ( sin ` 4 ) =/= ( 0p ` 4 )
16 fveq1 
 |-  ( sin = 0p -> ( sin ` 4 ) = ( 0p ` 4 ) )
17 16 necon3i 
 |-  ( ( sin ` 4 ) =/= ( 0p ` 4 ) -> sin =/= 0p )
18 15 17 ax-mp 
 |-  sin =/= 0p
19 eqid 
 |-  ( `' sin " { 0 } ) = ( `' sin " { 0 } )
20 19 fta1 
 |-  ( ( sin e. ( Poly ` CC ) /\ sin =/= 0p ) -> ( ( `' sin " { 0 } ) e. Fin /\ ( # ` ( `' sin " { 0 } ) ) <_ ( deg ` sin ) ) )
21 18 20 mpan2 
 |-  ( sin e. ( Poly ` CC ) -> ( ( `' sin " { 0 } ) e. Fin /\ ( # ` ( `' sin " { 0 } ) ) <_ ( deg ` sin ) ) )
22 21 simpld 
 |-  ( sin e. ( Poly ` CC ) -> ( `' sin " { 0 } ) e. Fin )
23 ovexd 
 |-  ( z e. ZZ -> ( z x. _pi ) e. _V )
24 23 rgen 
 |-  A. z e. ZZ ( z x. _pi ) e. _V
25 nfcv 
 |-  F/_ z ZZ
26 25 mptfnf 
 |-  ( A. z e. ZZ ( z x. _pi ) e. _V <-> ( z e. ZZ |-> ( z x. _pi ) ) Fn ZZ )
27 24 26 mpbi 
 |-  ( z e. ZZ |-> ( z x. _pi ) ) Fn ZZ
28 sinkpi 
 |-  ( z e. ZZ -> ( sin ` ( z x. _pi ) ) = 0 )
29 9 snid 
 |-  0 e. { 0 }
30 28 29 eqeltrdi 
 |-  ( z e. ZZ -> ( sin ` ( z x. _pi ) ) e. { 0 } )
31 sinf 
 |-  sin : CC --> CC
32 ffun 
 |-  ( sin : CC --> CC -> Fun sin )
33 31 32 ax-mp 
 |-  Fun sin
34 33 a1i 
 |-  ( z e. ZZ -> Fun sin )
35 zcn 
 |-  ( z e. ZZ -> z e. CC )
36 picn 
 |-  _pi e. CC
37 mulcl 
 |-  ( ( z e. CC /\ _pi e. CC ) -> ( z x. _pi ) e. CC )
38 35 36 37 sylancl 
 |-  ( z e. ZZ -> ( z x. _pi ) e. CC )
39 31 fdmi 
 |-  dom sin = CC
40 39 eleq2i 
 |-  ( ( z x. _pi ) e. dom sin <-> ( z x. _pi ) e. CC )
41 38 40 sylibr 
 |-  ( z e. ZZ -> ( z x. _pi ) e. dom sin )
42 fvimacnv 
 |-  ( ( Fun sin /\ ( z x. _pi ) e. dom sin ) -> ( ( sin ` ( z x. _pi ) ) e. { 0 } <-> ( z x. _pi ) e. ( `' sin " { 0 } ) ) )
43 34 41 42 syl2anc 
 |-  ( z e. ZZ -> ( ( sin ` ( z x. _pi ) ) e. { 0 } <-> ( z x. _pi ) e. ( `' sin " { 0 } ) ) )
44 30 43 mpbid 
 |-  ( z e. ZZ -> ( z x. _pi ) e. ( `' sin " { 0 } ) )
45 44 rgen 
 |-  A. z e. ZZ ( z x. _pi ) e. ( `' sin " { 0 } )
46 eqid 
 |-  ( z e. ZZ |-> ( z x. _pi ) ) = ( z e. ZZ |-> ( z x. _pi ) )
47 46 rnmptss 
 |-  ( A. z e. ZZ ( z x. _pi ) e. ( `' sin " { 0 } ) -> ran ( z e. ZZ |-> ( z x. _pi ) ) C_ ( `' sin " { 0 } ) )
48 45 47 ax-mp 
 |-  ran ( z e. ZZ |-> ( z x. _pi ) ) C_ ( `' sin " { 0 } )
49 27 48 pm3.2i 
 |-  ( ( z e. ZZ |-> ( z x. _pi ) ) Fn ZZ /\ ran ( z e. ZZ |-> ( z x. _pi ) ) C_ ( `' sin " { 0 } ) )
50 df-f 
 |-  ( ( z e. ZZ |-> ( z x. _pi ) ) : ZZ --> ( `' sin " { 0 } ) <-> ( ( z e. ZZ |-> ( z x. _pi ) ) Fn ZZ /\ ran ( z e. ZZ |-> ( z x. _pi ) ) C_ ( `' sin " { 0 } ) ) )
51 49 50 mpbir 
 |-  ( z e. ZZ |-> ( z x. _pi ) ) : ZZ --> ( `' sin " { 0 } )
52 moeq 
 |-  E* x x = ( y / _pi )
53 simpr 
 |-  ( ( x e. ZZ /\ y = ( x x. _pi ) ) -> y = ( x x. _pi ) )
54 oveq1 
 |-  ( y = ( x x. _pi ) -> ( y / _pi ) = ( ( x x. _pi ) / _pi ) )
55 53 54 syl 
 |-  ( ( x e. ZZ /\ y = ( x x. _pi ) ) -> ( y / _pi ) = ( ( x x. _pi ) / _pi ) )
56 simpl 
 |-  ( ( x e. ZZ /\ y = ( x x. _pi ) ) -> x e. ZZ )
57 zcn 
 |-  ( x e. ZZ -> x e. CC )
58 56 57 syl 
 |-  ( ( x e. ZZ /\ y = ( x x. _pi ) ) -> x e. CC )
59 pine0 
 |-  _pi =/= 0
60 divcan4 
 |-  ( ( x e. CC /\ _pi e. CC /\ _pi =/= 0 ) -> ( ( x x. _pi ) / _pi ) = x )
61 36 59 60 mp3an23 
 |-  ( x e. CC -> ( ( x x. _pi ) / _pi ) = x )
62 58 61 syl 
 |-  ( ( x e. ZZ /\ y = ( x x. _pi ) ) -> ( ( x x. _pi ) / _pi ) = x )
63 55 62 eqtrd 
 |-  ( ( x e. ZZ /\ y = ( x x. _pi ) ) -> ( y / _pi ) = x )
64 63 eqcomd 
 |-  ( ( x e. ZZ /\ y = ( x x. _pi ) ) -> x = ( y / _pi ) )
65 64 moimi 
 |-  ( E* x x = ( y / _pi ) -> E* x ( x e. ZZ /\ y = ( x x. _pi ) ) )
66 52 65 ax-mp 
 |-  E* x ( x e. ZZ /\ y = ( x x. _pi ) )
67 66 ax-gen 
 |-  A. y E* x ( x e. ZZ /\ y = ( x x. _pi ) )
68 vex 
 |-  x e. _V
69 vex 
 |-  y e. _V
70 eleq1w 
 |-  ( z = x -> ( z e. ZZ <-> x e. ZZ ) )
71 70 adantr 
 |-  ( ( z = x /\ t = y ) -> ( z e. ZZ <-> x e. ZZ ) )
72 eqeq1 
 |-  ( t = y -> ( t = ( z x. _pi ) <-> y = ( z x. _pi ) ) )
73 oveq1 
 |-  ( z = x -> ( z x. _pi ) = ( x x. _pi ) )
74 73 eqeq2d 
 |-  ( z = x -> ( y = ( z x. _pi ) <-> y = ( x x. _pi ) ) )
75 72 74 sylan9bbr 
 |-  ( ( z = x /\ t = y ) -> ( t = ( z x. _pi ) <-> y = ( x x. _pi ) ) )
76 71 75 anbi12d 
 |-  ( ( z = x /\ t = y ) -> ( ( z e. ZZ /\ t = ( z x. _pi ) ) <-> ( x e. ZZ /\ y = ( x x. _pi ) ) ) )
77 df-mpt 
 |-  ( z e. ZZ |-> ( z x. _pi ) ) = { <. z , t >. | ( z e. ZZ /\ t = ( z x. _pi ) ) }
78 68 69 76 77 braba 
 |-  ( x ( z e. ZZ |-> ( z x. _pi ) ) y <-> ( x e. ZZ /\ y = ( x x. _pi ) ) )
79 78 mobii 
 |-  ( E* x x ( z e. ZZ |-> ( z x. _pi ) ) y <-> E* x ( x e. ZZ /\ y = ( x x. _pi ) ) )
80 79 albii 
 |-  ( A. y E* x x ( z e. ZZ |-> ( z x. _pi ) ) y <-> A. y E* x ( x e. ZZ /\ y = ( x x. _pi ) ) )
81 67 80 mpbir 
 |-  A. y E* x x ( z e. ZZ |-> ( z x. _pi ) ) y
82 51 81 pm3.2i 
 |-  ( ( z e. ZZ |-> ( z x. _pi ) ) : ZZ --> ( `' sin " { 0 } ) /\ A. y E* x x ( z e. ZZ |-> ( z x. _pi ) ) y )
83 dff12 
 |-  ( ( z e. ZZ |-> ( z x. _pi ) ) : ZZ -1-1-> ( `' sin " { 0 } ) <-> ( ( z e. ZZ |-> ( z x. _pi ) ) : ZZ --> ( `' sin " { 0 } ) /\ A. y E* x x ( z e. ZZ |-> ( z x. _pi ) ) y ) )
84 82 83 mpbir 
 |-  ( z e. ZZ |-> ( z x. _pi ) ) : ZZ -1-1-> ( `' sin " { 0 } )
85 f1fi 
 |-  ( ( ( `' sin " { 0 } ) e. Fin /\ ( z e. ZZ |-> ( z x. _pi ) ) : ZZ -1-1-> ( `' sin " { 0 } ) ) -> ZZ e. Fin )
86 nnssz 
 |-  NN C_ ZZ
87 ssfi 
 |-  ( ( ZZ e. Fin /\ NN C_ ZZ ) -> NN e. Fin )
88 86 87 mpan2 
 |-  ( ZZ e. Fin -> NN e. Fin )
89 85 88 syl 
 |-  ( ( ( `' sin " { 0 } ) e. Fin /\ ( z e. ZZ |-> ( z x. _pi ) ) : ZZ -1-1-> ( `' sin " { 0 } ) ) -> NN e. Fin )
90 84 89 mpan2 
 |-  ( ( `' sin " { 0 } ) e. Fin -> NN e. Fin )
91 22 90 syl 
 |-  ( sin e. ( Poly ` CC ) -> NN e. Fin )
92 1 91 mto 
 |-  -. sin e. ( Poly ` CC )