Metamath Proof Explorer

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 eleq1 
 |-  ( ( cos ` ( _pi / 2 ) ) = 0 -> ( ( cos ` ( _pi / 2 ) ) e. { 0 } <-> 0 e. { 0 } ) )
5 4 biimprd 
 |-  ( ( cos ` ( _pi / 2 ) ) = 0 -> ( 0 e. { 0 } -> ( cos ` ( _pi / 2 ) ) e. { 0 } ) )
6 3 5 mpi 
 |-  ( ( cos ` ( _pi / 2 ) ) = 0 -> ( cos ` ( _pi / 2 ) ) e. { 0 } )
7 1 6 ax-mp 
 |-  ( cos ` ( _pi / 2 ) ) e. { 0 }
8 eldifn 
 |-  ( ( cos ` ( _pi / 2 ) ) e. ( CC \ { 0 } ) -> -. ( cos ` ( _pi / 2 ) ) e. { 0 } )
9 7 8 mt2 
 |-  -. ( cos ` ( _pi / 2 ) ) e. ( CC \ { 0 } )
10 picn 
 |-  _pi e. CC
11 halfcl 
 |-  ( _pi e. CC -> ( _pi / 2 ) e. CC )
12 10 11 ax-mp 
 |-  ( _pi / 2 ) e. CC
13 cosf 
 |-  cos : CC --> CC
14 fdm 
 |-  ( cos : CC --> CC -> dom cos = CC )
15 13 14 ax-mp 
 |-  dom cos = CC
16 15 eleq2i 
 |-  ( ( _pi / 2 ) e. dom cos <-> ( _pi / 2 ) e. CC )
17 12 16 mpbir 
 |-  ( _pi / 2 ) e. dom cos
18 ffun 
 |-  ( cos : CC --> CC -> Fun cos )
19 13 18 ax-mp 
 |-  Fun cos
20 fvimacnv 
 |-  ( ( Fun cos /\ ( _pi / 2 ) e. dom cos ) -> ( ( cos ` ( _pi / 2 ) ) e. ( CC \ { 0 } ) <-> ( _pi / 2 ) e. ( `' cos " ( CC \ { 0 } ) ) ) )
21 19 20 mpan 
 |-  ( ( _pi / 2 ) e. dom cos -> ( ( cos ` ( _pi / 2 ) ) e. ( CC \ { 0 } ) <-> ( _pi / 2 ) e. ( `' cos " ( CC \ { 0 } ) ) ) )
22 17 21 ax-mp 
 |-  ( ( cos ` ( _pi / 2 ) ) e. ( CC \ { 0 } ) <-> ( _pi / 2 ) e. ( `' cos " ( CC \ { 0 } ) ) )
23 9 22 mtbi 
 |-  -. ( _pi / 2 ) e. ( `' cos " ( CC \ { 0 } ) )
24 df-tan 
 |-  tan = ( x e. ( `' cos " ( CC \ { 0 } ) ) |-> ( ( sin ` x ) / ( cos ` x ) ) )
25 24 dmmptss 
 |-  dom tan C_ ( `' cos " ( CC \ { 0 } ) )
26 25 sseli 
 |-  ( ( _pi / 2 ) e. dom tan -> ( _pi / 2 ) e. ( `' cos " ( CC \ { 0 } ) ) )
27 23 26 mto 
 |-  -. ( _pi / 2 ) e. dom tan
28 plyf 
 |-  ( tan e. ( Poly ` CC ) -> tan : CC --> CC )
29 fdm 
 |-  ( tan : CC --> CC -> dom tan = CC )
30 eleq2 
 |-  ( dom tan = CC -> ( ( _pi / 2 ) e. dom tan <-> ( _pi / 2 ) e. CC ) )
31 30 biimprd 
 |-  ( dom tan = CC -> ( ( _pi / 2 ) e. CC -> ( _pi / 2 ) e. dom tan ) )
32 12 31 mpi 
 |-  ( dom tan = CC -> ( _pi / 2 ) e. dom tan )
33 28 29 32 3syl 
 |-  ( tan e. ( Poly ` CC ) -> ( _pi / 2 ) e. dom tan )
34 27 33 mto 
 |-  -. tan e. ( Poly ` CC )