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

Proof

Step	Hyp	Ref	Expression
1		coshalfpi	⊢ ( cos ‘ ( π / 2 ) ) = 0
2		c0ex	⊢ 0 ∈ V
3	2	snid	⊢ 0 ∈ { 0 }
4	1 3	eqeltri	⊢ ( cos ‘ ( π / 2 ) ) ∈ { 0 }
5		eldifn	⊢ ( ( cos ‘ ( π / 2 ) ) ∈ ( ℂ ∖ { 0 } ) → ¬ ( cos ‘ ( π / 2 ) ) ∈ { 0 } )
6	4 5	mt2	⊢ ¬ ( cos ‘ ( π / 2 ) ) ∈ ( ℂ ∖ { 0 } )
7		cosf	⊢ cos : ℂ ⟶ ℂ
8		ffun	⊢ ( cos : ℂ ⟶ ℂ → Fun cos )
9	7 8	ax-mp	⊢ Fun cos
10		picn	⊢ π ∈ ℂ
11		halfcl	⊢ ( π ∈ ℂ → ( π / 2 ) ∈ ℂ )
12	10 11	ax-mp	⊢ ( π / 2 ) ∈ ℂ
13	7	fdmi	⊢ dom cos = ℂ
14	12 13	eleqtrri	⊢ ( π / 2 ) ∈ dom cos
15		fvimacnv	⊢ ( ( Fun cos ∧ ( π / 2 ) ∈ dom cos ) → ( ( cos ‘ ( π / 2 ) ) ∈ ( ℂ ∖ { 0 } ) ↔ ( π / 2 ) ∈ ( ◡ cos “ ( ℂ ∖ { 0 } ) ) ) )
16	9 14 15	mp2an	⊢ ( ( cos ‘ ( π / 2 ) ) ∈ ( ℂ ∖ { 0 } ) ↔ ( π / 2 ) ∈ ( ◡ cos “ ( ℂ ∖ { 0 } ) ) )
17	6 16	mtbi	⊢ ¬ ( π / 2 ) ∈ ( ◡ cos “ ( ℂ ∖ { 0 } ) )
18		df-tan	⊢ tan = ( 𝑥 ∈ ( ◡ cos “ ( ℂ ∖ { 0 } ) ) ↦ ( ( sin ‘ 𝑥 ) / ( cos ‘ 𝑥 ) ) )
19	18	dmmptss	⊢ dom tan ⊆ ( ◡ cos “ ( ℂ ∖ { 0 } ) )
20	19	sseli	⊢ ( ( π / 2 ) ∈ dom tan → ( π / 2 ) ∈ ( ◡ cos “ ( ℂ ∖ { 0 } ) ) )
21	17 20	mto	⊢ ¬ ( π / 2 ) ∈ dom tan
22		plyf	⊢ ( tan ∈ ( Poly ‘ ℂ ) → tan : ℂ ⟶ ℂ )
23		fdm	⊢ ( tan : ℂ ⟶ ℂ → dom tan = ℂ )
24		eleq2	⊢ ( dom tan = ℂ → ( ( π / 2 ) ∈ dom tan ↔ ( π / 2 ) ∈ ℂ ) )
25	12 24	mpbiri	⊢ ( dom tan = ℂ → ( π / 2 ) ∈ dom tan )
26	22 23 25	3syl	⊢ ( tan ∈ ( Poly ‘ ℂ ) → ( π / 2 ) ∈ dom tan )
27	21 26	mto	⊢ ¬ tan ∈ ( Poly ‘ ℂ )