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	5 12	breqtrri	⊢ ( sin ‘ 4 ) < ( 0𝑝 ‘ 4 )
14	4 13	ltneii	⊢ ( sin ‘ 4 ) ≠ ( 0𝑝 ‘ 4 )
15		fveq1	⊢ ( sin = 0𝑝 → ( sin ‘ 4 ) = ( 0𝑝 ‘ 4 ) )
16	15	necon3i	⊢ ( ( sin ‘ 4 ) ≠ ( 0𝑝 ‘ 4 ) → sin ≠ 0𝑝 )
17	14 16	ax-mp	⊢ sin ≠ 0𝑝
18		eqid	⊢ ( ◡ sin “ { 0 } ) = ( ◡ sin “ { 0 } )
19	18	fta1	⊢ ( ( sin ∈ ( Poly ‘ ℂ ) ∧ sin ≠ 0𝑝 ) → ( ( ◡ sin “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( ◡ sin “ { 0 } ) ) ≤ ( deg ‘ sin ) ) )
20	17 19	mpan2	⊢ ( sin ∈ ( Poly ‘ ℂ ) → ( ( ◡ sin “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( ◡ sin “ { 0 } ) ) ≤ ( deg ‘ sin ) ) )
21	20	simpld	⊢ ( sin ∈ ( Poly ‘ ℂ ) → ( ◡ sin “ { 0 } ) ∈ Fin )
22		eqid	⊢ ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) = ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) )
23		sinkpi	⊢ ( 𝑧 ∈ ℤ → ( sin ‘ ( 𝑧 · π ) ) = 0 )
24	9	snid	⊢ 0 ∈ { 0 }
25	23 24	eqeltrdi	⊢ ( 𝑧 ∈ ℤ → ( sin ‘ ( 𝑧 · π ) ) ∈ { 0 } )
26		sinf	⊢ sin : ℂ ⟶ ℂ
27		ffun	⊢ ( sin : ℂ ⟶ ℂ → Fun sin )
28	26 27	ax-mp	⊢ Fun sin
29		zcn	⊢ ( 𝑧 ∈ ℤ → 𝑧 ∈ ℂ )
30		picn	⊢ π ∈ ℂ
31		mulcl	⊢ ( ( 𝑧 ∈ ℂ ∧ π ∈ ℂ ) → ( 𝑧 · π ) ∈ ℂ )
32	29 30 31	sylancl	⊢ ( 𝑧 ∈ ℤ → ( 𝑧 · π ) ∈ ℂ )
33	26	fdmi	⊢ dom sin = ℂ
34	32 33	eleqtrrdi	⊢ ( 𝑧 ∈ ℤ → ( 𝑧 · π ) ∈ dom sin )
35		fvimacnv	⊢ ( ( Fun sin ∧ ( 𝑧 · π ) ∈ dom sin ) → ( ( sin ‘ ( 𝑧 · π ) ) ∈ { 0 } ↔ ( 𝑧 · π ) ∈ ( ◡ sin “ { 0 } ) ) )
36	28 34 35	sylancr	⊢ ( 𝑧 ∈ ℤ → ( ( sin ‘ ( 𝑧 · π ) ) ∈ { 0 } ↔ ( 𝑧 · π ) ∈ ( ◡ sin “ { 0 } ) ) )
37	25 36	mpbid	⊢ ( 𝑧 ∈ ℤ → ( 𝑧 · π ) ∈ ( ◡ sin “ { 0 } ) )
38	22 37	fmpti	⊢ ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) : ℤ ⟶ ( ◡ sin “ { 0 } )
39		vex	⊢ 𝑥 ∈ V
40		vex	⊢ 𝑦 ∈ V
41		eleq1w	⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ ℤ ↔ 𝑥 ∈ ℤ ) )
42	41	adantr	⊢ ( ( 𝑧 = 𝑥 ∧ 𝑡 = 𝑦 ) → ( 𝑧 ∈ ℤ ↔ 𝑥 ∈ ℤ ) )
43		eqeq1	⊢ ( 𝑡 = 𝑦 → ( 𝑡 = ( 𝑧 · π ) ↔ 𝑦 = ( 𝑧 · π ) ) )
44		oveq1	⊢ ( 𝑧 = 𝑥 → ( 𝑧 · π ) = ( 𝑥 · π ) )
45	44	eqeq2d	⊢ ( 𝑧 = 𝑥 → ( 𝑦 = ( 𝑧 · π ) ↔ 𝑦 = ( 𝑥 · π ) ) )
46	43 45	sylan9bbr	⊢ ( ( 𝑧 = 𝑥 ∧ 𝑡 = 𝑦 ) → ( 𝑡 = ( 𝑧 · π ) ↔ 𝑦 = ( 𝑥 · π ) ) )
47	42 46	anbi12d	⊢ ( ( 𝑧 = 𝑥 ∧ 𝑡 = 𝑦 ) → ( ( 𝑧 ∈ ℤ ∧ 𝑡 = ( 𝑧 · π ) ) ↔ ( 𝑥 ∈ ℤ ∧ 𝑦 = ( 𝑥 · π ) ) ) )
48		df-mpt	⊢ ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) = { ⟨ 𝑧 , 𝑡 ⟩ ∣ ( 𝑧 ∈ ℤ ∧ 𝑡 = ( 𝑧 · π ) ) }
49	39 40 47 48	braba	⊢ ( 𝑥 ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) 𝑦 ↔ ( 𝑥 ∈ ℤ ∧ 𝑦 = ( 𝑥 · π ) ) )
50	49	mobii	⊢ ( ∃* 𝑥 𝑥 ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) 𝑦 ↔ ∃* 𝑥 ( 𝑥 ∈ ℤ ∧ 𝑦 = ( 𝑥 · π ) ) )
51	50	albii	⊢ ( ∀ 𝑦 ∃* 𝑥 𝑥 ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) 𝑦 ↔ ∀ 𝑦 ∃* 𝑥 ( 𝑥 ∈ ℤ ∧ 𝑦 = ( 𝑥 · π ) ) )
52		moeq	⊢ ∃* 𝑥 𝑥 = ( 𝑦 / π )
53		simpr	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 = ( 𝑥 · π ) ) → 𝑦 = ( 𝑥 · π ) )
54	53	oveq1d	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 = ( 𝑥 · π ) ) → ( 𝑦 / π ) = ( ( 𝑥 · π ) / π ) )
55		zcn	⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
56	55	adantr	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 = ( 𝑥 · π ) ) → 𝑥 ∈ ℂ )
57		pine0	⊢ π ≠ 0
58		divcan4	⊢ ( ( 𝑥 ∈ ℂ ∧ π ∈ ℂ ∧ π ≠ 0 ) → ( ( 𝑥 · π ) / π ) = 𝑥 )
59	30 57 58	mp3an23	⊢ ( 𝑥 ∈ ℂ → ( ( 𝑥 · π ) / π ) = 𝑥 )
60	56 59	syl	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 = ( 𝑥 · π ) ) → ( ( 𝑥 · π ) / π ) = 𝑥 )
61	54 60	eqtr2d	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 = ( 𝑥 · π ) ) → 𝑥 = ( 𝑦 / π ) )
62	61	moimi	⊢ ( ∃* 𝑥 𝑥 = ( 𝑦 / π ) → ∃* 𝑥 ( 𝑥 ∈ ℤ ∧ 𝑦 = ( 𝑥 · π ) ) )
63	52 62	ax-mp	⊢ ∃* 𝑥 ( 𝑥 ∈ ℤ ∧ 𝑦 = ( 𝑥 · π ) )
64	51 63	mpgbir	⊢ ∀ 𝑦 ∃* 𝑥 𝑥 ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) 𝑦
65		dff12	⊢ ( ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) : ℤ –1-1→ ( ◡ sin “ { 0 } ) ↔ ( ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) : ℤ ⟶ ( ◡ sin “ { 0 } ) ∧ ∀ 𝑦 ∃* 𝑥 𝑥 ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) 𝑦 ) )
66	38 64 65	mpbir2an	⊢ ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) : ℤ –1-1→ ( ◡ sin “ { 0 } )
67		f1fi	⊢ ( ( ( ◡ sin “ { 0 } ) ∈ Fin ∧ ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) : ℤ –1-1→ ( ◡ sin “ { 0 } ) ) → ℤ ∈ Fin )
68		nnssz	⊢ ℕ ⊆ ℤ
69		ssfi	⊢ ( ( ℤ ∈ Fin ∧ ℕ ⊆ ℤ ) → ℕ ∈ Fin )
70	67 68 69	sylancl	⊢ ( ( ( ◡ sin “ { 0 } ) ∈ Fin ∧ ( 𝑧 ∈ ℤ ↦ ( 𝑧 · π ) ) : ℤ –1-1→ ( ◡ sin “ { 0 } ) ) → ℕ ∈ Fin )
71	21 66 70	sylancl	⊢ ( sin ∈ ( Poly ‘ ℂ ) → ℕ ∈ Fin )
72	1 71	mto	⊢ ¬ sin ∈ ( Poly ‘ ℂ )