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		eleq1	⊢ ( ( cos ‘ ( π / 2 ) ) = 0 → ( ( cos ‘ ( π / 2 ) ) ∈ { 0 } ↔ 0 ∈ { 0 } ) )
5	4	biimprd	⊢ ( ( cos ‘ ( π / 2 ) ) = 0 → ( 0 ∈ { 0 } → ( cos ‘ ( π / 2 ) ) ∈ { 0 } ) )
6	3 5	mpi	⊢ ( ( cos ‘ ( π / 2 ) ) = 0 → ( cos ‘ ( π / 2 ) ) ∈ { 0 } )
7	1 6	ax-mp	⊢ ( cos ‘ ( π / 2 ) ) ∈ { 0 }
8		eldifn	⊢ ( ( cos ‘ ( π / 2 ) ) ∈ ( ℂ ∖ { 0 } ) → ¬ ( cos ‘ ( π / 2 ) ) ∈ { 0 } )
9	7 8	mt2	⊢ ¬ ( cos ‘ ( π / 2 ) ) ∈ ( ℂ ∖ { 0 } )
10		picn	⊢ π ∈ ℂ
11		halfcl	⊢ ( π ∈ ℂ → ( π / 2 ) ∈ ℂ )
12	10 11	ax-mp	⊢ ( π / 2 ) ∈ ℂ
13		cosf	⊢ cos : ℂ ⟶ ℂ
14		fdm	⊢ ( cos : ℂ ⟶ ℂ → dom cos = ℂ )
15	13 14	ax-mp	⊢ dom cos = ℂ
16	15	eleq2i	⊢ ( ( π / 2 ) ∈ dom cos ↔ ( π / 2 ) ∈ ℂ )
17	12 16	mpbir	⊢ ( π / 2 ) ∈ dom cos
18		ffun	⊢ ( cos : ℂ ⟶ ℂ → Fun cos )
19	13 18	ax-mp	⊢ Fun cos
20		fvimacnv	⊢ ( ( Fun cos ∧ ( π / 2 ) ∈ dom cos ) → ( ( cos ‘ ( π / 2 ) ) ∈ ( ℂ ∖ { 0 } ) ↔ ( π / 2 ) ∈ ( ◡ cos “ ( ℂ ∖ { 0 } ) ) ) )
21	19 20	mpan	⊢ ( ( π / 2 ) ∈ dom cos → ( ( cos ‘ ( π / 2 ) ) ∈ ( ℂ ∖ { 0 } ) ↔ ( π / 2 ) ∈ ( ◡ cos “ ( ℂ ∖ { 0 } ) ) ) )
22	17 21	ax-mp	⊢ ( ( cos ‘ ( π / 2 ) ) ∈ ( ℂ ∖ { 0 } ) ↔ ( π / 2 ) ∈ ( ◡ cos “ ( ℂ ∖ { 0 } ) ) )
23	9 22	mtbi	⊢ ¬ ( π / 2 ) ∈ ( ◡ cos “ ( ℂ ∖ { 0 } ) )
24		df-tan	⊢ tan = ( 𝑥 ∈ ( ◡ cos “ ( ℂ ∖ { 0 } ) ) ↦ ( ( sin ‘ 𝑥 ) / ( cos ‘ 𝑥 ) ) )
25	24	dmmptss	⊢ dom tan ⊆ ( ◡ cos “ ( ℂ ∖ { 0 } ) )
26	25	sseli	⊢ ( ( π / 2 ) ∈ dom tan → ( π / 2 ) ∈ ( ◡ cos “ ( ℂ ∖ { 0 } ) ) )
27	23 26	mto	⊢ ¬ ( π / 2 ) ∈ dom tan
28		plyf	⊢ ( tan ∈ ( Poly ‘ ℂ ) → tan : ℂ ⟶ ℂ )
29		fdm	⊢ ( tan : ℂ ⟶ ℂ → dom tan = ℂ )
30		eleq2	⊢ ( dom tan = ℂ → ( ( π / 2 ) ∈ dom tan ↔ ( π / 2 ) ∈ ℂ ) )
31	30	biimprd	⊢ ( dom tan = ℂ → ( ( π / 2 ) ∈ ℂ → ( π / 2 ) ∈ dom tan ) )
32	12 31	mpi	⊢ ( dom tan = ℂ → ( π / 2 ) ∈ dom tan )
33	28 29 32	3syl	⊢ ( tan ∈ ( Poly ‘ ℂ ) → ( π / 2 ) ∈ dom tan )
34	27 33	mto	⊢ ¬ tan ∈ ( Poly ‘ ℂ )