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	|- -. tan e. ( Poly ` CC )

Proof

Step	Hyp	Ref	Expression
1		coshalfpi	|- ( cos ` ( _pi / 2 ) ) = 0
2		c0ex	|- 0 e. _V
3	2	snid	|- 0 e. { 0 }
4	1 3	eqeltri	|- ( cos ` ( _pi / 2 ) ) e. { 0 }
5		eldifn	|- ( ( cos ` ( _pi / 2 ) ) e. ( CC \ { 0 } ) -> -. ( cos ` ( _pi / 2 ) ) e. { 0 } )
6	4 5	mt2	|- -. ( cos ` ( _pi / 2 ) ) e. ( CC \ { 0 } )
7		cosf	|- cos : CC --> CC
8		ffun	|- ( cos : CC --> CC -> Fun cos )
9	7 8	ax-mp	|- Fun cos
10		picn	|- _pi e. CC
11		halfcl	|- ( _pi e. CC -> ( _pi / 2 ) e. CC )
12	10 11	ax-mp	|- ( _pi / 2 ) e. CC
13	7	fdmi	|- dom cos = CC
14	12 13	eleqtrri	|- ( _pi / 2 ) e. dom cos
15		fvimacnv	|- ( ( Fun cos /\ ( _pi / 2 ) e. dom cos ) -> ( ( cos ` ( _pi / 2 ) ) e. ( CC \ { 0 } ) <-> ( _pi / 2 ) e. ( `' cos " ( CC \ { 0 } ) ) ) )
16	9 14 15	mp2an	|- ( ( cos ` ( _pi / 2 ) ) e. ( CC \ { 0 } ) <-> ( _pi / 2 ) e. ( `' cos " ( CC \ { 0 } ) ) )
17	6 16	mtbi	|- -. ( _pi / 2 ) e. ( `' cos " ( CC \ { 0 } ) )
18		df-tan	|- tan = ( x e. ( `' cos " ( CC \ { 0 } ) ) |-> ( ( sin ` x ) / ( cos ` x ) ) )
19	18	dmmptss	|- dom tan C_ ( `' cos " ( CC \ { 0 } ) )
20	19	sseli	|- ( ( _pi / 2 ) e. dom tan -> ( _pi / 2 ) e. ( `' cos " ( CC \ { 0 } ) ) )
21	17 20	mto	|- -. ( _pi / 2 ) e. dom tan
22		plyf	|- ( tan e. ( Poly ` CC ) -> tan : CC --> CC )
23		fdm	|- ( tan : CC --> CC -> dom tan = CC )
24		eleq2	|- ( dom tan = CC -> ( ( _pi / 2 ) e. dom tan <-> ( _pi / 2 ) e. CC ) )
25	12 24	mpbiri	|- ( dom tan = CC -> ( _pi / 2 ) e. dom tan )
26	22 23 25	3syl	|- ( tan e. ( Poly ` CC ) -> ( _pi / 2 ) e. dom tan )
27	21 26	mto	|- -. tan e. ( Poly ` CC )