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		eleq1	$$⊢\cos \left(\frac{\mathrm{\pi }}{2}\right)=0\to \left(\cos \left(\frac{\mathrm{\pi }}{2}\right)\in \left\{0\right\}\leftrightarrow 0\in \left\{0\right\}\right)$$
5	4	biimprd	$$⊢\cos \left(\frac{\mathrm{\pi }}{2}\right)=0\to \left(0\in \left\{0\right\}\to \cos \left(\frac{\mathrm{\pi }}{2}\right)\in \left\{0\right\}\right)$$
6	3 5	mpi	$$⊢\cos \left(\frac{\mathrm{\pi }}{2}\right)=0\to \cos \left(\frac{\mathrm{\pi }}{2}\right)\in \left\{0\right\}$$
7	1 6	ax-mp	$$⊢\cos \left(\frac{\mathrm{\pi }}{2}\right)\in \left\{0\right\}$$
8		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\}$$
9	7 8	mt2	$$⊢\neg \cos \left(\frac{\mathrm{\pi }}{2}\right)\in \left(ℂ\setminus \left\{0\right\}\right)$$
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		cosf	$$⊢\cos :ℂ⟶ℂ$$
14		fdm	$$⊢\cos :ℂ⟶ℂ\to \mathrm{dom}\cos =ℂ$$
15	13 14	ax-mp	$$⊢\mathrm{dom}\cos =ℂ$$
16	15	eleq2i	$$⊢\frac{\mathrm{\pi }}{2}\in \mathrm{dom}\cos \leftrightarrow \frac{\mathrm{\pi }}{2}\in ℂ$$
17	12 16	mpbir	$$⊢\frac{\mathrm{\pi }}{2}\in \mathrm{dom}\cos$$
18		ffun	$$⊢\cos :ℂ⟶ℂ\to \mathrm{Fun}\cos$$
19	13 18	ax-mp	$$⊢\mathrm{Fun}\cos$$
20		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)$$
21	19 20	mpan	$$⊢\frac{\mathrm{\pi }}{2}\in \mathrm{dom}\cos \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)$$
22	17 21	ax-mp	$$⊢\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]$$
23	9 22	mtbi	$$⊢\neg \frac{\mathrm{\pi }}{2}\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]$$
24		df-tan	$$⊢\tan =\left(x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼\frac{\sin x}{\cos x}\right)$$
25	24	dmmptss	$$⊢\mathrm{dom}\tan \subseteq {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]$$
26	25	sseli	$$⊢\frac{\mathrm{\pi }}{2}\in \mathrm{dom}\tan \to \frac{\mathrm{\pi }}{2}\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]$$
27	23 26	mto	$$⊢\neg \frac{\mathrm{\pi }}{2}\in \mathrm{dom}\tan$$
28		plyf	$$⊢\tan \in \mathrm{Poly}\left(ℂ\right)\to \tan :ℂ⟶ℂ$$
29		fdm	$$⊢\tan :ℂ⟶ℂ\to \mathrm{dom}\tan =ℂ$$
30		eleq2	$$⊢\mathrm{dom}\tan =ℂ\to \left(\frac{\mathrm{\pi }}{2}\in \mathrm{dom}\tan \leftrightarrow \frac{\mathrm{\pi }}{2}\in ℂ\right)$$
31	30	biimprd	$$⊢\mathrm{dom}\tan =ℂ\to \left(\frac{\mathrm{\pi }}{2}\in ℂ\to \frac{\mathrm{\pi }}{2}\in \mathrm{dom}\tan \right)$$
32	12 31	mpi	$$⊢\mathrm{dom}\tan =ℂ\to \frac{\mathrm{\pi }}{2}\in \mathrm{dom}\tan$$
33	28 29 32	3syl	$$⊢\tan \in \mathrm{Poly}\left(ℂ\right)\to \frac{\mathrm{\pi }}{2}\in \mathrm{dom}\tan$$
34	27 33	mto	$$⊢\neg \tan \in \mathrm{Poly}\left(ℂ\right)$$