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 5 12 breqtrri 
 |-  ( sin ` 4 ) < ( 0p ` 4 )
14 4 13 ltneii 
 |-  ( sin ` 4 ) =/= ( 0p ` 4 )
15 fveq1 
 |-  ( sin = 0p -> ( sin ` 4 ) = ( 0p ` 4 ) )
16 15 necon3i 
 |-  ( ( sin ` 4 ) =/= ( 0p ` 4 ) -> sin =/= 0p )
17 14 16 ax-mp 
 |-  sin =/= 0p
18 eqid 
 |-  ( `' sin " { 0 } ) = ( `' sin " { 0 } )
19 18 fta1 
 |-  ( ( sin e. ( Poly ` CC ) /\ sin =/= 0p ) -> ( ( `' sin " { 0 } ) e. Fin /\ ( # ` ( `' sin " { 0 } ) ) <_ ( deg ` sin ) ) )
20 17 19 mpan2 
 |-  ( sin e. ( Poly ` CC ) -> ( ( `' sin " { 0 } ) e. Fin /\ ( # ` ( `' sin " { 0 } ) ) <_ ( deg ` sin ) ) )
21 20 simpld 
 |-  ( sin e. ( Poly ` CC ) -> ( `' sin " { 0 } ) e. Fin )
22 eqid 
 |-  ( z e. ZZ |-> ( z x. _pi ) ) = ( z e. ZZ |-> ( z x. _pi ) )
23 sinkpi 
 |-  ( z e. ZZ -> ( sin ` ( z x. _pi ) ) = 0 )
24 9 snid 
 |-  0 e. { 0 }
25 23 24 eqeltrdi 
 |-  ( z e. ZZ -> ( sin ` ( z x. _pi ) ) e. { 0 } )
26 sinf 
 |-  sin : CC --> CC
27 ffun 
 |-  ( sin : CC --> CC -> Fun sin )
28 26 27 ax-mp 
 |-  Fun sin
29 zcn 
 |-  ( z e. ZZ -> z e. CC )
30 picn 
 |-  _pi e. CC
31 mulcl 
 |-  ( ( z e. CC /\ _pi e. CC ) -> ( z x. _pi ) e. CC )
32 29 30 31 sylancl 
 |-  ( z e. ZZ -> ( z x. _pi ) e. CC )
33 26 fdmi 
 |-  dom sin = CC
34 32 33 eleqtrrdi 
 |-  ( z e. ZZ -> ( z x. _pi ) e. dom sin )
35 fvimacnv 
 |-  ( ( Fun sin /\ ( z x. _pi ) e. dom sin ) -> ( ( sin ` ( z x. _pi ) ) e. { 0 } <-> ( z x. _pi ) e. ( `' sin " { 0 } ) ) )
36 28 34 35 sylancr 
 |-  ( z e. ZZ -> ( ( sin ` ( z x. _pi ) ) e. { 0 } <-> ( z x. _pi ) e. ( `' sin " { 0 } ) ) )
37 25 36 mpbid 
 |-  ( z e. ZZ -> ( z x. _pi ) e. ( `' sin " { 0 } ) )
38 22 37 fmpti 
 |-  ( z e. ZZ |-> ( z x. _pi ) ) : ZZ --> ( `' sin " { 0 } )
39 vex 
 |-  x e. _V
40 vex 
 |-  y e. _V
41 eleq1w 
 |-  ( z = x -> ( z e. ZZ <-> x e. ZZ ) )
42 41 adantr 
 |-  ( ( z = x /\ t = y ) -> ( z e. ZZ <-> x e. ZZ ) )
43 eqeq1 
 |-  ( t = y -> ( t = ( z x. _pi ) <-> y = ( z x. _pi ) ) )
44 oveq1 
 |-  ( z = x -> ( z x. _pi ) = ( x x. _pi ) )
45 44 eqeq2d 
 |-  ( z = x -> ( y = ( z x. _pi ) <-> y = ( x x. _pi ) ) )
46 43 45 sylan9bbr 
 |-  ( ( z = x /\ t = y ) -> ( t = ( z x. _pi ) <-> y = ( x x. _pi ) ) )
47 42 46 anbi12d 
 |-  ( ( z = x /\ t = y ) -> ( ( z e. ZZ /\ t = ( z x. _pi ) ) <-> ( x e. ZZ /\ y = ( x x. _pi ) ) ) )
48 df-mpt 
 |-  ( z e. ZZ |-> ( z x. _pi ) ) = { <. z , t >. | ( z e. ZZ /\ t = ( z x. _pi ) ) }
49 39 40 47 48 braba 
 |-  ( x ( z e. ZZ |-> ( z x. _pi ) ) y <-> ( x e. ZZ /\ y = ( x x. _pi ) ) )
50 49 mobii 
 |-  ( E* x x ( z e. ZZ |-> ( z x. _pi ) ) y <-> E* x ( x e. ZZ /\ y = ( x x. _pi ) ) )
51 50 albii 
 |-  ( A. y E* x x ( z e. ZZ |-> ( z x. _pi ) ) y <-> A. y E* x ( x e. ZZ /\ y = ( x x. _pi ) ) )
52 moeq 
 |-  E* x x = ( y / _pi )
53 simpr 
 |-  ( ( x e. ZZ /\ y = ( x x. _pi ) ) -> y = ( x x. _pi ) )
54 53 oveq1d 
 |-  ( ( x e. ZZ /\ y = ( x x. _pi ) ) -> ( y / _pi ) = ( ( x x. _pi ) / _pi ) )
55 zcn 
 |-  ( x e. ZZ -> x e. CC )
56 55 adantr 
 |-  ( ( x e. ZZ /\ y = ( x x. _pi ) ) -> x e. CC )
57 pine0 
 |-  _pi =/= 0
58 divcan4 
 |-  ( ( x e. CC /\ _pi e. CC /\ _pi =/= 0 ) -> ( ( x x. _pi ) / _pi ) = x )
59 30 57 58 mp3an23 
 |-  ( x e. CC -> ( ( x x. _pi ) / _pi ) = x )
60 56 59 syl 
 |-  ( ( x e. ZZ /\ y = ( x x. _pi ) ) -> ( ( x x. _pi ) / _pi ) = x )
61 54 60 eqtr2d 
 |-  ( ( x e. ZZ /\ y = ( x x. _pi ) ) -> x = ( y / _pi ) )
62 61 moimi 
 |-  ( E* x x = ( y / _pi ) -> E* x ( x e. ZZ /\ y = ( x x. _pi ) ) )
63 52 62 ax-mp 
 |-  E* x ( x e. ZZ /\ y = ( x x. _pi ) )
64 51 63 mpgbir 
 |-  A. y E* x x ( z e. ZZ |-> ( z x. _pi ) ) y
65 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 ) )
66 38 64 65 mpbir2an 
 |-  ( z e. ZZ |-> ( z x. _pi ) ) : ZZ -1-1-> ( `' sin " { 0 } )
67 f1fi 
 |-  ( ( ( `' sin " { 0 } ) e. Fin /\ ( z e. ZZ |-> ( z x. _pi ) ) : ZZ -1-1-> ( `' sin " { 0 } ) ) -> ZZ e. Fin )
68 nnssz 
 |-  NN C_ ZZ
69 ssfi 
 |-  ( ( ZZ e. Fin /\ NN C_ ZZ ) -> NN e. Fin )
70 67 68 69 sylancl 
 |-  ( ( ( `' sin " { 0 } ) e. Fin /\ ( z e. ZZ |-> ( z x. _pi ) ) : ZZ -1-1-> ( `' sin " { 0 } ) ) -> NN e. Fin )
71 21 66 70 sylancl 
 |-  ( sin e. ( Poly ` CC ) -> NN e. Fin )
72 1 71 mto 
 |-  -. sin e. ( Poly ` CC )