Theorem tannpoly

Description: The tangent function is not a polynomial with complex coefficients, as it is not defined on the whole complex plane. (Contributed by Ender Ting, 10-Dec-2025)

	Ref	Expression
Assertion	tannpoly	$$⊢\neg \tan \in \mathrm{Poly}\left(ℂ\right)$$

Proof

Step	Hyp	Ref	Expression
1		coshalfpi	$$⊢\cos \left(\frac{\mathrm{\pi }}{2}\right)=0$$
2		c0ex	$$⊢0\in \mathrm{V}$$
3	2	snid	$$⊢0\in \left\{0\right\}$$
4	1 3	eqeltri	$$⊢\cos \left(\frac{\mathrm{\pi }}{2}\right)\in \left\{0\right\}$$
5		eldifn	$$⊢\cos \left(\frac{\mathrm{\pi }}{2}\right)\in \left(ℂ\setminus \left\{0\right\}\right)\to \neg \cos \left(\frac{\mathrm{\pi }}{2}\right)\in \left\{0\right\}$$
6	4 5	mt2	$$⊢\neg \cos \left(\frac{\mathrm{\pi }}{2}\right)\in \left(ℂ\setminus \left\{0\right\}\right)$$
7		cosf	$$⊢\cos :ℂ⟶ℂ$$
8		ffun	$$⊢\cos :ℂ⟶ℂ\to \mathrm{Fun}\cos$$
9	7 8	ax-mp	$$⊢\mathrm{Fun}\cos$$
10		picn	$$⊢\mathrm{\pi }\in ℂ$$
11		halfcl	$$⊢\mathrm{\pi }\in ℂ\to \frac{\mathrm{\pi }}{2}\in ℂ$$
12	10 11	ax-mp	$$⊢\frac{\mathrm{\pi }}{2}\in ℂ$$
13	7	fdmi	$$⊢\mathrm{dom}\cos =ℂ$$
14	12 13	eleqtrri	$$⊢\frac{\mathrm{\pi }}{2}\in \mathrm{dom}\cos$$
15		fvimacnv	$$⊢\left(\mathrm{Fun}\cos \wedge \frac{\mathrm{\pi }}{2}\in \mathrm{dom}\cos \right)\to \left(\cos \left(\frac{\mathrm{\pi }}{2}\right)\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \frac{\mathrm{\pi }}{2}\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\right)$$
16	9 14 15	mp2an	$$⊢\cos \left(\frac{\mathrm{\pi }}{2}\right)\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \frac{\mathrm{\pi }}{2}\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]$$
17	6 16	mtbi	$$⊢\neg \frac{\mathrm{\pi }}{2}\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]$$
18		df-tan	$$⊢\tan =\left(x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼\frac{\sin x}{\cos x}\right)$$
19	18	dmmptss	$$⊢\mathrm{dom}\tan \subseteq {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]$$
20	19	sseli	$$⊢\frac{\mathrm{\pi }}{2}\in \mathrm{dom}\tan \to \frac{\mathrm{\pi }}{2}\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]$$
21	17 20	mto	$$⊢\neg \frac{\mathrm{\pi }}{2}\in \mathrm{dom}\tan$$
22		plyf	$$⊢\tan \in \mathrm{Poly}\left(ℂ\right)\to \tan :ℂ⟶ℂ$$
23		fdm	$$⊢\tan :ℂ⟶ℂ\to \mathrm{dom}\tan =ℂ$$
24		eleq2	$$⊢\mathrm{dom}\tan =ℂ\to \left(\frac{\mathrm{\pi }}{2}\in \mathrm{dom}\tan \leftrightarrow \frac{\mathrm{\pi }}{2}\in ℂ\right)$$
25	12 24	mpbiri	$$⊢\mathrm{dom}\tan =ℂ\to \frac{\mathrm{\pi }}{2}\in \mathrm{dom}\tan$$
26	22 23 25	3syl	$$⊢\tan \in \mathrm{Poly}\left(ℂ\right)\to \frac{\mathrm{\pi }}{2}\in \mathrm{dom}\tan$$
27	21 26	mto	$$⊢\neg \tan \in \mathrm{Poly}\left(ℂ\right)$$