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 Poly (ℂ)$

Proof

Step	Hyp	Ref	Expression
1		nnnfi	$⊢ \neg ℕ \in 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 \{0\}$
7	6	fveq1i	$⊢ 0_{𝑝} (4) = (ℂ \times \{0\}) (4)$
8		4cn	$⊢ 4 \in ℂ$
9		c0ex	$⊢ 0 \in V$
10	9	fvconst2	$⊢ 4 \in ℂ \to (ℂ \times \{0\}) (4) = 0$
11	8 10	ax-mp	$⊢ (ℂ \times \{0\}) (4) = 0$
12	7 11	eqtri	$⊢ 0_{𝑝} (4) = 0$
13	12	eqcomi	$⊢ 0 = 0_{𝑝} (4)$
14	5 13	breqtri	$⊢ \sin 4 < 0_{𝑝} (4)$
15	4 14	ltneii	$⊢ \sin 4 \neq 0_{𝑝} (4)$
16		fveq1	$⊢ \sin = 0_{𝑝} \to \sin 4 = 0_{𝑝} (4)$
17	16	necon3i	$⊢ \sin 4 \neq 0_{𝑝} (4) \to \sin \neq 0_{𝑝}$
18	15 17	ax-mp	$⊢ \sin \neq 0_{𝑝}$
19		eqid	$⊢ \sin^{-1} [\{0\}] = \sin^{-1} [\{0\}]$
20	19	fta1	$⊢ (\sin \in Poly (ℂ) \land \sin \neq 0_{𝑝}) \to (\sin^{-1} [\{0\}] \in Fin \land \|\sin^{-1} [\{0\}]\| \leq \deg (\sin))$
21	18 20	mpan2	$⊢ \sin \in Poly (ℂ) \to (\sin^{-1} [\{0\}] \in Fin \land \|\sin^{-1} [\{0\}]\| \leq \deg (\sin))$
22	21	simpld	$⊢ \sin \in Poly (ℂ) \to \sin^{-1} [\{0\}] \in Fin$
23		ovexd	$⊢ z \in ℤ \to z π \in V$
24	23	rgen	$⊢ \forall z \in ℤ z π \in V$
25		nfcv	$⊢ \underline{Ⅎ} z ℤ$
26	25	mptfnf	$⊢ \forall z \in ℤ z π \in V \leftrightarrow (z \in ℤ ⟼ z π) Fn ℤ$
27	24 26	mpbi	$⊢ (z \in ℤ ⟼ z π) Fn ℤ$
28		sinkpi	$⊢ z \in ℤ \to \sin z π = 0$
29	9	snid	$⊢ 0 \in \{0\}$
30	28 29	eqeltrdi	$⊢ z \in ℤ \to \sin z π \in \{0\}$
31		sinf	$⊢ \sin : ℂ ⟶ ℂ$
32		ffun	$⊢ \sin : ℂ ⟶ ℂ \to Fun \sin$
33	31 32	ax-mp	$⊢ Fun \sin$
34	33	a1i	$⊢ z \in ℤ \to Fun \sin$
35		zcn	$⊢ z \in ℤ \to z \in ℂ$
36		picn	$⊢ π \in ℂ$
37		mulcl	$⊢ (z \in ℂ \land π \in ℂ) \to z π \in ℂ$
38	35 36 37	sylancl	$⊢ z \in ℤ \to z π \in ℂ$
39	31	fdmi	$⊢ dom \sin = ℂ$
40	39	eleq2i	$⊢ z π \in dom \sin \leftrightarrow z π \in ℂ$
41	38 40	sylibr	$⊢ z \in ℤ \to z π \in dom \sin$
42		fvimacnv	$⊢ (Fun \sin \land z π \in dom \sin) \to (\sin z π \in \{0\} \leftrightarrow z π \in \sin^{-1} [\{0\}])$
43	34 41 42	syl2anc	$⊢ z \in ℤ \to (\sin z π \in \{0\} \leftrightarrow z π \in \sin^{-1} [\{0\}])$
44	30 43	mpbid	$⊢ z \in ℤ \to z π \in \sin^{-1} [\{0\}]$
45	44	rgen	$⊢ \forall z \in ℤ z π \in \sin^{-1} [\{0\}]$
46		eqid	$⊢ (z \in ℤ ⟼ z π) = (z \in ℤ ⟼ z π)$
47	46	rnmptss	$⊢ \forall z \in ℤ z π \in \sin^{-1} [\{0\}] \to ran (z \in ℤ ⟼ z π) \subseteq \sin^{-1} [\{0\}]$
48	45 47	ax-mp	$⊢ ran (z \in ℤ ⟼ z π) \subseteq \sin^{-1} [\{0\}]$
49	27 48	pm3.2i	$⊢ ((z \in ℤ ⟼ z π) Fn ℤ \land ran (z \in ℤ ⟼ z π) \subseteq \sin^{-1} [\{0\}])$
50		df-f	$⊢ (z \in ℤ ⟼ z π) : ℤ ⟶ \sin^{-1} [\{0\}] \leftrightarrow ((z \in ℤ ⟼ z π) Fn ℤ \land ran (z \in ℤ ⟼ z π) \subseteq \sin^{-1} [\{0\}])$
51	49 50	mpbir	$⊢ (z \in ℤ ⟼ z π) : ℤ ⟶ \sin^{-1} [\{0\}]$
52		moeq	$⊢ \exists^{*} x x = \frac{y}{π}$
53		simpr	$⊢ (x \in ℤ \land y = x π) \to y = x π$
54		oveq1	$⊢ y = x π \to \frac{y}{π} = \frac{x π}{π}$
55	53 54	syl	$⊢ (x \in ℤ \land y = x π) \to \frac{y}{π} = \frac{x π}{π}$
56		simpl	$⊢ (x \in ℤ \land y = x π) \to x \in ℤ$
57		zcn	$⊢ x \in ℤ \to x \in ℂ$
58	56 57	syl	$⊢ (x \in ℤ \land y = x π) \to x \in ℂ$
59		pine0	$⊢ π \neq 0$
60		divcan4	$⊢ (x \in ℂ \land π \in ℂ \land π \neq 0) \to \frac{x π}{π} = x$
61	36 59 60	mp3an23	$⊢ x \in ℂ \to \frac{x π}{π} = x$
62	58 61	syl	$⊢ (x \in ℤ \land y = x π) \to \frac{x π}{π} = x$
63	55 62	eqtrd	$⊢ (x \in ℤ \land y = x π) \to \frac{y}{π} = x$
64	63	eqcomd	$⊢ (x \in ℤ \land y = x π) \to x = \frac{y}{π}$
65	64	moimi	$⊢ \exists^{} x x = \frac{y}{π} \to \exists^{} x (x \in ℤ \land y = x π)$
66	52 65	ax-mp	$⊢ \exists^{*} x (x \in ℤ \land y = x π)$
67	66	ax-gen	$⊢ \forall y \exists^{*} x (x \in ℤ \land y = x π)$
68		vex	$⊢ x \in V$
69		vex	$⊢ y \in V$
70		eleq1w	$⊢ z = x \to (z \in ℤ \leftrightarrow x \in ℤ)$
71	70	adantr	$⊢ (z = x \land t = y) \to (z \in ℤ \leftrightarrow x \in ℤ)$
72		eqeq1	$⊢ t = y \to (t = z π \leftrightarrow y = z π)$
73		oveq1	$⊢ z = x \to z π = x π$
74	73	eqeq2d	$⊢ z = x \to (y = z π \leftrightarrow y = x π)$
75	72 74	sylan9bbr	$⊢ (z = x \land t = y) \to (t = z π \leftrightarrow y = x π)$
76	71 75	anbi12d	$⊢ (z = x \land t = y) \to ((z \in ℤ \land t = z π) \leftrightarrow (x \in ℤ \land y = x π))$
77		df-mpt	$⊢ (z \in ℤ ⟼ z π) = \{⟨z, t⟩ \| (z \in ℤ \land t = z π)\}$
78	68 69 76 77	braba	$⊢ x (z \in ℤ ⟼ z π) y \leftrightarrow (x \in ℤ \land y = x π)$
79	78	mobii	$⊢ \exists^{} x x (z \in ℤ ⟼ z π) y \leftrightarrow \exists^{} x (x \in ℤ \land y = x π)$
80	79	albii	$⊢ \forall y \exists^{} x x (z \in ℤ ⟼ z π) y \leftrightarrow \forall y \exists^{} x (x \in ℤ \land y = x π)$
81	67 80	mpbir	$⊢ \forall y \exists^{*} x x (z \in ℤ ⟼ z π) y$
82	51 81	pm3.2i	$⊢ ((z \in ℤ ⟼ z π) : ℤ ⟶ \sin^{-1} [\{0\}] \land \forall y \exists^{*} x x (z \in ℤ ⟼ z π) y)$
83		dff12	$⊢ (z \in ℤ ⟼ z π) : ℤ \underset{1-1}{⟶} \sin^{-1} [\{0\}] \leftrightarrow ((z \in ℤ ⟼ z π) : ℤ ⟶ \sin^{-1} [\{0\}] \land \forall y \exists^{*} x x (z \in ℤ ⟼ z π) y)$
84	82 83	mpbir	$⊢ (z \in ℤ ⟼ z π) : ℤ \underset{1-1}{⟶} \sin^{-1} [\{0\}]$
85		f1fi	$⊢ (\sin^{-1} [\{0\}] \in Fin \land (z \in ℤ ⟼ z π) : ℤ \underset{1-1}{⟶} \sin^{-1} [\{0\}]) \to ℤ \in Fin$
86		nnssz	$⊢ ℕ \subseteq ℤ$
87		ssfi	$⊢ (ℤ \in Fin \land ℕ \subseteq ℤ) \to ℕ \in Fin$
88	86 87	mpan2	$⊢ ℤ \in Fin \to ℕ \in Fin$
89	85 88	syl	$⊢ (\sin^{-1} [\{0\}] \in Fin \land (z \in ℤ ⟼ z π) : ℤ \underset{1-1}{⟶} \sin^{-1} [\{0\}]) \to ℕ \in Fin$
90	84 89	mpan2	$⊢ \sin^{-1} [\{0\}] \in Fin \to ℕ \in Fin$
91	22 90	syl	$⊢ \sin \in Poly (ℂ) \to ℕ \in Fin$
92	1 91	mto	$⊢ \neg \sin \in Poly (ℂ)$

Metamath Proof Explorer

Theorem sinnpoly

Proof