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	$$⊢\neg \sin \in \mathrm{Poly}\left(ℂ\right)$$

Proof

Step	Hyp	Ref	Expression
1		nnnfi	$$⊢\neg \mathbb{N}\in \mathrm{Fin}$$
2		4re	$$⊢4\in ℝ$$
3		resincl	$$⊢4\in ℝ\to \sin 4\in ℝ$$
4	2 3	ax-mp	$$⊢\sin 4\in ℝ$$
5		sin4lt0	$$⊢\sin 4<0$$
6		df-0p	$$⊢0_{𝑝}=ℂ\times \left\{0\right\}$$
7	6	fveq1i	$$⊢0_{𝑝}\left(4\right)=\left(ℂ\times \left\{0\right\}\right)\left(4\right)$$
8		4cn	$$⊢4\in ℂ$$
9		c0ex	$$⊢0\in \mathrm{V}$$
10	9	fvconst2	$$⊢4\in ℂ\to \left(ℂ\times \left\{0\right\}\right)\left(4\right)=0$$
11	8 10	ax-mp	$$⊢\left(ℂ\times \left\{0\right\}\right)\left(4\right)=0$$
12	7 11	eqtri	$$⊢0_{𝑝}\left(4\right)=0$$
13	5 12	breqtrri	$$⊢\sin 4<0_{𝑝}\left(4\right)$$
14	4 13	ltneii	$$⊢\sin 4\ne 0_{𝑝}\left(4\right)$$
15		fveq1	$$⊢\sin =0_{𝑝}\to \sin 4=0_{𝑝}\left(4\right)$$
16	15	necon3i	$$⊢\sin 4\ne 0_{𝑝}\left(4\right)\to \sin \ne 0_{𝑝}$$
17	14 16	ax-mp	$$⊢\sin \ne 0_{𝑝}$$
18		eqid	$$⊢{\sin }^{-1}\left[\left\{0\right\}\right]={\sin }^{-1}\left[\left\{0\right\}\right]$$
19	18	fta1	$$⊢\left(\sin \in \mathrm{Poly}\left(ℂ\right)\wedge \sin \ne 0_{𝑝}\right)\to \left({\sin }^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{\sin }^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left(\sin \right)\right)$$
20	17 19	mpan2	$$⊢\sin \in \mathrm{Poly}\left(ℂ\right)\to \left({\sin }^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left|{\sin }^{-1}\left[\left\{0\right\}\right]\right|\le \mathrm{deg}\left(\sin \right)\right)$$
21	20	simpld	$$⊢\sin \in \mathrm{Poly}\left(ℂ\right)\to {\sin }^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}$$
22		eqid	$$⊢\left(z\in \mathbb{Z}⟼z\mathrm{\pi }\right)=\left(z\in \mathbb{Z}⟼z\mathrm{\pi }\right)$$
23		sinkpi	$$⊢z\in \mathbb{Z}\to \sin z\mathrm{\pi }=0$$
24	9	snid	$$⊢0\in \left\{0\right\}$$
25	23 24	eqeltrdi	$$⊢z\in \mathbb{Z}\to \sin z\mathrm{\pi }\in \left\{0\right\}$$
26		sinf	$$⊢\sin :ℂ⟶ℂ$$
27		ffun	$$⊢\sin :ℂ⟶ℂ\to \mathrm{Fun}\sin$$
28	26 27	ax-mp	$$⊢\mathrm{Fun}\sin$$
29		zcn	$$⊢z\in \mathbb{Z}\to z\in ℂ$$
30		picn	$$⊢\mathrm{\pi }\in ℂ$$
31		mulcl	$$⊢\left(z\in ℂ\wedge \mathrm{\pi }\in ℂ\right)\to z\mathrm{\pi }\in ℂ$$
32	29 30 31	sylancl	$$⊢z\in \mathbb{Z}\to z\mathrm{\pi }\in ℂ$$
33	26	fdmi	$$⊢\mathrm{dom}\sin =ℂ$$
34	32 33	eleqtrrdi	$$⊢z\in \mathbb{Z}\to z\mathrm{\pi }\in \mathrm{dom}\sin$$
35		fvimacnv	$$⊢\left(\mathrm{Fun}\sin \wedge z\mathrm{\pi }\in \mathrm{dom}\sin \right)\to \left(\sin z\mathrm{\pi }\in \left\{0\right\}\leftrightarrow z\mathrm{\pi }\in {\sin }^{-1}\left[\left\{0\right\}\right]\right)$$
36	28 34 35	sylancr	$$⊢z\in \mathbb{Z}\to \left(\sin z\mathrm{\pi }\in \left\{0\right\}\leftrightarrow z\mathrm{\pi }\in {\sin }^{-1}\left[\left\{0\right\}\right]\right)$$
37	25 36	mpbid	$$⊢z\in \mathbb{Z}\to z\mathrm{\pi }\in {\sin }^{-1}\left[\left\{0\right\}\right]$$
38	22 37	fmpti	$$⊢\left(z\in \mathbb{Z}⟼z\mathrm{\pi }\right):\mathbb{Z}⟶{\sin }^{-1}\left[\left\{0\right\}\right]$$
39		vex	$$⊢x\in \mathrm{V}$$
40		vex	$$⊢y\in \mathrm{V}$$
41		eleq1w	$$⊢z=x\to \left(z\in \mathbb{Z}\leftrightarrow x\in \mathbb{Z}\right)$$
42	41	adantr	$$⊢\left(z=x\wedge t=y\right)\to \left(z\in \mathbb{Z}\leftrightarrow x\in \mathbb{Z}\right)$$
43		eqeq1	$$⊢t=y\to \left(t=z\mathrm{\pi }\leftrightarrow y=z\mathrm{\pi }\right)$$
44		oveq1	$$⊢z=x\to z\mathrm{\pi }=x\mathrm{\pi }$$
45	44	eqeq2d	$$⊢z=x\to \left(y=z\mathrm{\pi }\leftrightarrow y=x\mathrm{\pi }\right)$$
46	43 45	sylan9bbr	$$⊢\left(z=x\wedge t=y\right)\to \left(t=z\mathrm{\pi }\leftrightarrow y=x\mathrm{\pi }\right)$$
47	42 46	anbi12d	$$⊢\left(z=x\wedge t=y\right)\to \left(\left(z\in \mathbb{Z}\wedge t=z\mathrm{\pi }\right)\leftrightarrow \left(x\in \mathbb{Z}\wedge y=x\mathrm{\pi }\right)\right)$$
48		df-mpt	$$⊢\left(z\in \mathbb{Z}⟼z\mathrm{\pi }\right)=\left\{⟨z,t⟩|\left(z\in \mathbb{Z}\wedge t=z\mathrm{\pi }\right)\right\}$$
49	39 40 47 48	braba	$$⊢x\left(z\in \mathbb{Z}⟼z\mathrm{\pi }\right)y\leftrightarrow \left(x\in \mathbb{Z}\wedge y=x\mathrm{\pi }\right)$$
50	49	mobii	$$⊢{\exists }^{*}xx\left(z\in \mathbb{Z}⟼z\mathrm{\pi }\right)y\leftrightarrow {\exists }^{*}x\left(x\in \mathbb{Z}\wedge y=x\mathrm{\pi }\right)$$
51	50	albii	$$⊢\forall y{\exists }^{*}xx\left(z\in \mathbb{Z}⟼z\mathrm{\pi }\right)y\leftrightarrow \forall y{\exists }^{*}x\left(x\in \mathbb{Z}\wedge y=x\mathrm{\pi }\right)$$
52		moeq	$$⊢{\exists }^{*}xx=\frac{y}{\mathrm{\pi }}$$
53		simpr	$$⊢\left(x\in \mathbb{Z}\wedge y=x\mathrm{\pi }\right)\to y=x\mathrm{\pi }$$
54	53	oveq1d	$$⊢\left(x\in \mathbb{Z}\wedge y=x\mathrm{\pi }\right)\to \frac{y}{\mathrm{\pi }}=\frac{x\mathrm{\pi }}{\mathrm{\pi }}$$
55		zcn	$$⊢x\in \mathbb{Z}\to x\in ℂ$$
56	55	adantr	$$⊢\left(x\in \mathbb{Z}\wedge y=x\mathrm{\pi }\right)\to x\in ℂ$$
57		pine0	$$⊢\mathrm{\pi }\ne 0$$
58		divcan4	$$⊢\left(x\in ℂ\wedge \mathrm{\pi }\in ℂ\wedge \mathrm{\pi }\ne 0\right)\to \frac{x\mathrm{\pi }}{\mathrm{\pi }}=x$$
59	30 57 58	mp3an23	$$⊢x\in ℂ\to \frac{x\mathrm{\pi }}{\mathrm{\pi }}=x$$
60	56 59	syl	$$⊢\left(x\in \mathbb{Z}\wedge y=x\mathrm{\pi }\right)\to \frac{x\mathrm{\pi }}{\mathrm{\pi }}=x$$
61	54 60	eqtr2d	$$⊢\left(x\in \mathbb{Z}\wedge y=x\mathrm{\pi }\right)\to x=\frac{y}{\mathrm{\pi }}$$
62	61	moimi	$$⊢{\exists }^{*}xx=\frac{y}{\mathrm{\pi }}\to {\exists }^{*}x\left(x\in \mathbb{Z}\wedge y=x\mathrm{\pi }\right)$$
63	52 62	ax-mp	$$⊢{\exists }^{*}x\left(x\in \mathbb{Z}\wedge y=x\mathrm{\pi }\right)$$
64	51 63	mpgbir	$$⊢\forall y{\exists }^{*}xx\left(z\in \mathbb{Z}⟼z\mathrm{\pi }\right)y$$
65		dff12	$$⊢\left(z\in \mathbb{Z}⟼z\mathrm{\pi }\right):\mathbb{Z}\underset{1-1}{⟶}{\sin }^{-1}\left[\left\{0\right\}\right]\leftrightarrow \left(\left(z\in \mathbb{Z}⟼z\mathrm{\pi }\right):\mathbb{Z}⟶{\sin }^{-1}\left[\left\{0\right\}\right]\wedge \forall y{\exists }^{*}xx\left(z\in \mathbb{Z}⟼z\mathrm{\pi }\right)y\right)$$
66	38 64 65	mpbir2an	$$⊢\left(z\in \mathbb{Z}⟼z\mathrm{\pi }\right):\mathbb{Z}\underset{1-1}{⟶}{\sin }^{-1}\left[\left\{0\right\}\right]$$
67		f1fi	$$⊢\left({\sin }^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left(z\in \mathbb{Z}⟼z\mathrm{\pi }\right):\mathbb{Z}\underset{1-1}{⟶}{\sin }^{-1}\left[\left\{0\right\}\right]\right)\to \mathbb{Z}\in \mathrm{Fin}$$
68		nnssz	$$⊢\mathbb{N}\subseteq \mathbb{Z}$$
69		ssfi	$$⊢\left(\mathbb{Z}\in \mathrm{Fin}\wedge \mathbb{N}\subseteq \mathbb{Z}\right)\to \mathbb{N}\in \mathrm{Fin}$$
70	67 68 69	sylancl	$$⊢\left({\sin }^{-1}\left[\left\{0\right\}\right]\in \mathrm{Fin}\wedge \left(z\in \mathbb{Z}⟼z\mathrm{\pi }\right):\mathbb{Z}\underset{1-1}{⟶}{\sin }^{-1}\left[\left\{0\right\}\right]\right)\to \mathbb{N}\in \mathrm{Fin}$$
71	21 66 70	sylancl	$$⊢\sin \in \mathrm{Poly}\left(ℂ\right)\to \mathbb{N}\in \mathrm{Fin}$$
72	1 71	mto	$$⊢\neg \sin \in \mathrm{Poly}\left(ℂ\right)$$