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

Proof

Step	Hyp	Ref	Expression
1		nnnfi	⊢ ¬ ℕ ∈ Fin
2		4re	⊢ 4 ∈ ℝ
3		resincl	⊢ ( 4 ∈ ℝ → ( sin ‘ 4 ) ∈ ℝ )
4	2 3	ax-mp	⊢ ( sin ‘ 4 ) ∈ ℝ
5		sin4lt0	⊢ ( sin ‘ 4 ) < 0
6		df-0p	⊢ 0𝑝 = ( ℂ × { 0 } )
7	6	fveq1i	⊢ ( 0𝑝 ‘ 4 ) = ( ( ℂ × { 0 } ) ‘ 4 )
8		4cn	⊢ 4 ∈ ℂ
9		c0ex	⊢ 0 ∈ V
10	9	fvconst2	⊢ ( 4 ∈ ℂ → ( ( ℂ × { 0 } ) ‘ 4 ) = 0 )
11	8 10	ax-mp	⊢ ( ( ℂ × { 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 ) ≠ ( 0𝑝 ‘ 4 )
16		fveq1	⊢ ( sin = 0𝑝 → ( sin ‘ 4 ) = ( 0𝑝 ‘ 4 ) )
17	16	necon3i	⊢ ( ( sin ‘ 4 ) ≠ ( 0𝑝 ‘ 4 ) → sin ≠ 0𝑝 )
18	15 17	ax-mp	⊢ sin ≠ 0𝑝
19		eqid	⊢ ( ◡ sin “ { 0 } ) = ( ◡ sin “ { 0 } )
20	19	fta1	⊢ ( ( sin ∈ ( Poly ‘ ℂ ) ∧ sin ≠ 0𝑝 ) → ( ( ◡ sin “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( ◡ sin “ { 0 } ) ) ≤ ( deg ‘ sin ) ) )
21	18 20	mpan2	⊢ ( sin ∈ ( Poly ‘ ℂ ) → ( ( ◡ sin “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( ◡ sin “ { 0 } ) ) ≤ ( deg ‘ sin ) ) )
22	21	simpld	⊢ ( sin ∈ ( Poly ‘ ℂ ) → ( ◡ sin “ { 0 } ) ∈ Fin )
23		ovexd	⊢ ( 𝑧 ∈ ℤ → ( 𝑧 · π ) ∈ V )
24	23	rgen	⊢ ∀ 𝑧 ∈ ℤ ( 𝑧 · π ) ∈ V
25		nfcv	⊢ Ⅎ 𝑧 ℤ
26	25	mptfnf	⊢ ( ∀ 𝑧 ∈ ℤ ( 𝑧 · π ) ∈ V ↔ ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) Fn ℤ )
27	24 26	mpbi	⊢ ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) Fn ℤ
28		sinkpi	⊢ ( 𝑧 ∈ ℤ → ( sin ‘ ( 𝑧 · π ) ) = 0 )
29	9	snid	⊢ 0 ∈ { 0 }
30	28 29	eqeltrdi	⊢ ( 𝑧 ∈ ℤ → ( sin ‘ ( 𝑧 · π ) ) ∈ { 0 } )
31		sinf	⊢ sin : ℂ ⟶ ℂ
32		ffun	⊢ ( sin : ℂ ⟶ ℂ → Fun sin )
33	31 32	ax-mp	⊢ Fun sin
34	33	a1i	⊢ ( 𝑧 ∈ ℤ → Fun sin )
35		zcn	⊢ ( 𝑧 ∈ ℤ → 𝑧 ∈ ℂ )
36		picn	⊢ π ∈ ℂ
37		mulcl	⊢ ( ( 𝑧 ∈ ℂ ∧ π ∈ ℂ ) → ( 𝑧 · π ) ∈ ℂ )
38	35 36 37	sylancl	⊢ ( 𝑧 ∈ ℤ → ( 𝑧 · π ) ∈ ℂ )
39	31	fdmi	⊢ dom sin = ℂ
40	39	eleq2i	⊢ ( ( 𝑧 · π ) ∈ dom sin ↔ ( 𝑧 · π ) ∈ ℂ )
41	38 40	sylibr	⊢ ( 𝑧 ∈ ℤ → ( 𝑧 · π ) ∈ dom sin )
42		fvimacnv	⊢ ( ( Fun sin ∧ ( 𝑧 · π ) ∈ dom sin ) → ( ( sin ‘ ( 𝑧 · π ) ) ∈ { 0 } ↔ ( 𝑧 · π ) ∈ ( ◡ sin “ { 0 } ) ) )
43	34 41 42	syl2anc	⊢ ( 𝑧 ∈ ℤ → ( ( sin ‘ ( 𝑧 · π ) ) ∈ { 0 } ↔ ( 𝑧 · π ) ∈ ( ◡ sin “ { 0 } ) ) )
44	30 43	mpbid	⊢ ( 𝑧 ∈ ℤ → ( 𝑧 · π ) ∈ ( ◡ sin “ { 0 } ) )
45	44	rgen	⊢ ∀ 𝑧 ∈ ℤ ( 𝑧 · π ) ∈ ( ◡ sin “ { 0 } )
46		eqid	⊢ ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) = ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) )
47	46	rnmptss	⊢ ( ∀ 𝑧 ∈ ℤ ( 𝑧 · π ) ∈ ( ◡ sin “ { 0 } ) → ran ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) ⊆ ( ◡ sin “ { 0 } ) )
48	45 47	ax-mp	⊢ ran ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) ⊆ ( ◡ sin “ { 0 } )
49	27 48	pm3.2i	⊢ ( ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) Fn ℤ ∧ ran ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) ⊆ ( ◡ sin “ { 0 } ) )
50		df-f	⊢ ( ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) : ℤ ⟶ ( ◡ sin “ { 0 } ) ↔ ( ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) Fn ℤ ∧ ran ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) ⊆ ( ◡ sin “ { 0 } ) ) )
51	49 50	mpbir	⊢ ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) : ℤ ⟶ ( ◡ sin “ { 0 } )
52		moeq	⊢ ∃* 𝑥 𝑥 = ( 𝑦 / π )
53		simpr	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 = ( 𝑥 · π ) ) → 𝑦 = ( 𝑥 · π ) )
54		oveq1	⊢ ( 𝑦 = ( 𝑥 · π ) → ( 𝑦 / π ) = ( ( 𝑥 · π ) / π ) )
55	53 54	syl	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 = ( 𝑥 · π ) ) → ( 𝑦 / π ) = ( ( 𝑥 · π ) / π ) )
56		simpl	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 = ( 𝑥 · π ) ) → 𝑥 ∈ ℤ )
57		zcn	⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
58	56 57	syl	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 = ( 𝑥 · π ) ) → 𝑥 ∈ ℂ )
59		pine0	⊢ π ≠ 0
60		divcan4	⊢ ( ( 𝑥 ∈ ℂ ∧ π ∈ ℂ ∧ π ≠ 0 ) → ( ( 𝑥 · π ) / π ) = 𝑥 )
61	36 59 60	mp3an23	⊢ ( 𝑥 ∈ ℂ → ( ( 𝑥 · π ) / π ) = 𝑥 )
62	58 61	syl	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 = ( 𝑥 · π ) ) → ( ( 𝑥 · π ) / π ) = 𝑥 )
63	55 62	eqtrd	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 = ( 𝑥 · π ) ) → ( 𝑦 / π ) = 𝑥 )
64	63	eqcomd	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 = ( 𝑥 · π ) ) → 𝑥 = ( 𝑦 / π ) )
65	64	moimi	⊢ ( ∃* 𝑥 𝑥 = ( 𝑦 / π ) → ∃* 𝑥 ( 𝑥 ∈ ℤ ∧ 𝑦 = ( 𝑥 · π ) ) )
66	52 65	ax-mp	⊢ ∃* 𝑥 ( 𝑥 ∈ ℤ ∧ 𝑦 = ( 𝑥 · π ) )
67	66	ax-gen	⊢ ∀ 𝑦 ∃* 𝑥 ( 𝑥 ∈ ℤ ∧ 𝑦 = ( 𝑥 · π ) )
68		vex	⊢ 𝑥 ∈ V
69		vex	⊢ 𝑦 ∈ V
70		eleq1w	⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ ℤ ↔ 𝑥 ∈ ℤ ) )
71	70	adantr	⊢ ( ( 𝑧 = 𝑥 ∧ 𝑡 = 𝑦 ) → ( 𝑧 ∈ ℤ ↔ 𝑥 ∈ ℤ ) )
72		eqeq1	⊢ ( 𝑡 = 𝑦 → ( 𝑡 = ( 𝑧 · π ) ↔ 𝑦 = ( 𝑧 · π ) ) )
73		oveq1	⊢ ( 𝑧 = 𝑥 → ( 𝑧 · π ) = ( 𝑥 · π ) )
74	73	eqeq2d	⊢ ( 𝑧 = 𝑥 → ( 𝑦 = ( 𝑧 · π ) ↔ 𝑦 = ( 𝑥 · π ) ) )
75	72 74	sylan9bbr	⊢ ( ( 𝑧 = 𝑥 ∧ 𝑡 = 𝑦 ) → ( 𝑡 = ( 𝑧 · π ) ↔ 𝑦 = ( 𝑥 · π ) ) )
76	71 75	anbi12d	⊢ ( ( 𝑧 = 𝑥 ∧ 𝑡 = 𝑦 ) → ( ( 𝑧 ∈ ℤ ∧ 𝑡 = ( 𝑧 · π ) ) ↔ ( 𝑥 ∈ ℤ ∧ 𝑦 = ( 𝑥 · π ) ) ) )
77		df-mpt	⊢ ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) = { ⟨ 𝑧 , 𝑡 ⟩ ∣ ( 𝑧 ∈ ℤ ∧ 𝑡 = ( 𝑧 · π ) ) }
78	68 69 76 77	braba	⊢ ( 𝑥 ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) 𝑦 ↔ ( 𝑥 ∈ ℤ ∧ 𝑦 = ( 𝑥 · π ) ) )
79	78	mobii	⊢ ( ∃* 𝑥 𝑥 ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) 𝑦 ↔ ∃* 𝑥 ( 𝑥 ∈ ℤ ∧ 𝑦 = ( 𝑥 · π ) ) )
80	79	albii	⊢ ( ∀ 𝑦 ∃* 𝑥 𝑥 ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) 𝑦 ↔ ∀ 𝑦 ∃* 𝑥 ( 𝑥 ∈ ℤ ∧ 𝑦 = ( 𝑥 · π ) ) )
81	67 80	mpbir	⊢ ∀ 𝑦 ∃* 𝑥 𝑥 ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) 𝑦
82	51 81	pm3.2i	⊢ ( ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) : ℤ ⟶ ( ◡ sin “ { 0 } ) ∧ ∀ 𝑦 ∃* 𝑥 𝑥 ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) 𝑦 )
83		dff12	⊢ ( ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) : ℤ –1-1→ ( ◡ sin “ { 0 } ) ↔ ( ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) : ℤ ⟶ ( ◡ sin “ { 0 } ) ∧ ∀ 𝑦 ∃* 𝑥 𝑥 ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) 𝑦 ) )
84	82 83	mpbir	⊢ ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) : ℤ –1-1→ ( ◡ sin “ { 0 } )
85		f1fi	⊢ ( ( ( ◡ sin “ { 0 } ) ∈ Fin ∧ ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) : ℤ –1-1→ ( ◡ sin “ { 0 } ) ) → ℤ ∈ Fin )
86		nnssz	⊢ ℕ ⊆ ℤ
87		ssfi	⊢ ( ( ℤ ∈ Fin ∧ ℕ ⊆ ℤ ) → ℕ ∈ Fin )
88	86 87	mpan2	⊢ ( ℤ ∈ Fin → ℕ ∈ Fin )
89	85 88	syl	⊢ ( ( ( ◡ sin “ { 0 } ) ∈ Fin ∧ ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) : ℤ –1-1→ ( ◡ sin “ { 0 } ) ) → ℕ ∈ Fin )
90	84 89	mpan2	⊢ ( ( ◡ sin “ { 0 } ) ∈ Fin → ℕ ∈ Fin )
91	22 90	syl	⊢ ( sin ∈ ( Poly ‘ ℂ ) → ℕ ∈ Fin )
92	1 91	mto	⊢ ¬ sin ∈ ( Poly ‘ ℂ )