Metamath Proof Explorer

Theorem cjnpoly

Description: Complex conjugation operator is not a polynomial with complex coefficients. Indeed; if it was, then multiplying x conjugate by x itself and adding 1 would yield a nowhere-zero non-constant polynomial, contrary to the fta . (Contributed by Ender Ting, 8-Dec-2025)

Ref Expression
Assertion cjnpoly 
|- -. * e. ( Poly ` CC )

Proof

Step Hyp Ref Expression
1 cnex 
 |-  CC e. _V
2 1ex 
 |-  1 e. _V
3 fconstmpt 
 |-  ( CC X. { 1 } ) = ( x e. CC |-> 1 )
4 2 3 fnmpti 
 |-  ( CC X. { 1 } ) Fn CC
5 fnresi 
 |-  ( _I |` CC ) Fn CC
6 df-idp 
 |-  Xp = ( _I |` CC )
7 6 fneq1i 
 |-  ( Xp Fn CC <-> ( _I |` CC ) Fn CC )
8 5 7 mpbir 
 |-  Xp Fn CC
9 8 a1i 
 |-  ( T. -> Xp Fn CC )
10 cjf 
 |-  * : CC --> CC
11 ffn 
 |-  ( * : CC --> CC -> * Fn CC )
12 10 11 ax-mp 
 |-  * Fn CC
13 12 a1i 
 |-  ( T. -> * Fn CC )
14 1 a1i 
 |-  ( T. -> CC e. _V )
15 inidm 
 |-  ( CC i^i CC ) = CC
16 9 13 14 14 15 offn 
 |-  ( T. -> ( Xp oF x. * ) Fn CC )
17 16 mptru 
 |-  ( Xp oF x. * ) Fn CC
18 fnfvof 
 |-  ( ( ( ( CC X. { 1 } ) Fn CC /\ ( Xp oF x. * ) Fn CC ) /\ ( CC e. _V /\ x e. CC ) ) -> ( ( ( CC X. { 1 } ) oF + ( Xp oF x. * ) ) ` x ) = ( ( ( CC X. { 1 } ) ` x ) + ( ( Xp oF x. * ) ` x ) ) )
19 4 17 18 mpanl12 
 |-  ( ( CC e. _V /\ x e. CC ) -> ( ( ( CC X. { 1 } ) oF + ( Xp oF x. * ) ) ` x ) = ( ( ( CC X. { 1 } ) ` x ) + ( ( Xp oF x. * ) ` x ) ) )
20 1 19 mpan 
 |-  ( x e. CC -> ( ( ( CC X. { 1 } ) oF + ( Xp oF x. * ) ) ` x ) = ( ( ( CC X. { 1 } ) ` x ) + ( ( Xp oF x. * ) ` x ) ) )
21 2 fvconst2 
 |-  ( x e. CC -> ( ( CC X. { 1 } ) ` x ) = 1 )
22 21 oveq1d 
 |-  ( x e. CC -> ( ( ( CC X. { 1 } ) ` x ) + ( ( Xp oF x. * ) ` x ) ) = ( 1 + ( ( Xp oF x. * ) ` x ) ) )
23 fnfvof 
 |-  ( ( ( Xp Fn CC /\ * Fn CC ) /\ ( CC e. _V /\ x e. CC ) ) -> ( ( Xp oF x. * ) ` x ) = ( ( Xp ` x ) x. ( * ` x ) ) )
24 8 12 23 mpanl12 
 |-  ( ( CC e. _V /\ x e. CC ) -> ( ( Xp oF x. * ) ` x ) = ( ( Xp ` x ) x. ( * ` x ) ) )
25 1 24 mpan 
 |-  ( x e. CC -> ( ( Xp oF x. * ) ` x ) = ( ( Xp ` x ) x. ( * ` x ) ) )
26 6 fveq1i 
 |-  ( Xp ` x ) = ( ( _I |` CC ) ` x )
27 fvres 
 |-  ( x e. CC -> ( ( _I |` CC ) ` x ) = ( _I ` x ) )
28 26 27 eqtrid 
 |-  ( x e. CC -> ( Xp ` x ) = ( _I ` x ) )
29 fvi 
 |-  ( x e. CC -> ( _I ` x ) = x )
30 28 29 eqtrd 
 |-  ( x e. CC -> ( Xp ` x ) = x )
31 30 oveq1d 
 |-  ( x e. CC -> ( ( Xp ` x ) x. ( * ` x ) ) = ( x x. ( * ` x ) ) )
32 25 31 eqtrd 
 |-  ( x e. CC -> ( ( Xp oF x. * ) ` x ) = ( x x. ( * ` x ) ) )
33 32 oveq2d 
 |-  ( x e. CC -> ( 1 + ( ( Xp oF x. * ) ` x ) ) = ( 1 + ( x x. ( * ` x ) ) ) )
34 20 22 33 3eqtrd 
 |-  ( x e. CC -> ( ( ( CC X. { 1 } ) oF + ( Xp oF x. * ) ) ` x ) = ( 1 + ( x x. ( * ` x ) ) ) )
35 1red 
 |-  ( x e. CC -> 1 e. RR )
36 cjmulrcl 
 |-  ( x e. CC -> ( x x. ( * ` x ) ) e. RR )
37 0lt1 
 |-  0 < 1
38 37 a1i 
 |-  ( x e. CC -> 0 < 1 )
39 cjmulge0 
 |-  ( x e. CC -> 0 <_ ( x x. ( * ` x ) ) )
40 35 36 38 39 addgtge0d 
 |-  ( x e. CC -> 0 < ( 1 + ( x x. ( * ` x ) ) ) )
41 40 gt0ne0d 
 |-  ( x e. CC -> ( 1 + ( x x. ( * ` x ) ) ) =/= 0 )
42 34 41 eqnetrd 
 |-  ( x e. CC -> ( ( ( CC X. { 1 } ) oF + ( Xp oF x. * ) ) ` x ) =/= 0 )
43 42 neneqd 
 |-  ( x e. CC -> -. ( ( ( CC X. { 1 } ) oF + ( Xp oF x. * ) ) ` x ) = 0 )
44 43 nrex 
 |-  -. E. x e. CC ( ( ( CC X. { 1 } ) oF + ( Xp oF x. * ) ) ` x ) = 0
45 ssid 
 |-  CC C_ CC
46 ax-1cn 
 |-  1 e. CC
47 plyconst 
 |-  ( ( CC C_ CC /\ 1 e. CC ) -> ( CC X. { 1 } ) e. ( Poly ` CC ) )
48 45 46 47 mp2an 
 |-  ( CC X. { 1 } ) e. ( Poly ` CC )
49 plyid 
 |-  ( ( CC C_ CC /\ 1 e. CC ) -> Xp e. ( Poly ` CC ) )
50 45 46 49 mp2an 
 |-  Xp e. ( Poly ` CC )
51 plymulcl 
 |-  ( ( Xp e. ( Poly ` CC ) /\ * e. ( Poly ` CC ) ) -> ( Xp oF x. * ) e. ( Poly ` CC ) )
52 50 51 mpan 
 |-  ( * e. ( Poly ` CC ) -> ( Xp oF x. * ) e. ( Poly ` CC ) )
53 plyaddcl 
 |-  ( ( ( CC X. { 1 } ) e. ( Poly ` CC ) /\ ( Xp oF x. * ) e. ( Poly ` CC ) ) -> ( ( CC X. { 1 } ) oF + ( Xp oF x. * ) ) e. ( Poly ` CC ) )
54 48 52 53 sylancr 
 |-  ( * e. ( Poly ` CC ) -> ( ( CC X. { 1 } ) oF + ( Xp oF x. * ) ) e. ( Poly ` CC ) )
55 1re 
 |-  1 e. RR
56 cjre 
 |-  ( 1 e. RR -> ( * ` 1 ) = 1 )
57 55 56 ax-mp 
 |-  ( * ` 1 ) = 1
58 ax-1ne0 
 |-  1 =/= 0
59 57 58 eqnetri 
 |-  ( * ` 1 ) =/= 0
60 ne0p 
 |-  ( ( 1 e. CC /\ ( * ` 1 ) =/= 0 ) -> * =/= 0p )
61 46 59 60 mp2an 
 |-  * =/= 0p
62 6 fveq1i 
 |-  ( Xp ` 1 ) = ( ( _I |` CC ) ` 1 )
63 fvres 
 |-  ( 1 e. CC -> ( ( _I |` CC ) ` 1 ) = ( _I ` 1 ) )
64 46 63 ax-mp 
 |-  ( ( _I |` CC ) ` 1 ) = ( _I ` 1 )
65 fvi 
 |-  ( 1 e. _V -> ( _I ` 1 ) = 1 )
66 2 65 ax-mp 
 |-  ( _I ` 1 ) = 1
67 62 64 66 3eqtri 
 |-  ( Xp ` 1 ) = 1
68 67 58 eqnetri 
 |-  ( Xp ` 1 ) =/= 0
69 ne0p 
 |-  ( ( 1 e. CC /\ ( Xp ` 1 ) =/= 0 ) -> Xp =/= 0p )
70 46 68 69 mp2an 
 |-  Xp =/= 0p
71 dgrid 
 |-  ( deg ` Xp ) = 1
72 71 eqcomi 
 |-  1 = ( deg ` Xp )
73 eqid 
 |-  ( deg ` * ) = ( deg ` * )
74 72 73 dgrmul 
 |-  ( ( ( Xp e. ( Poly ` CC ) /\ Xp =/= 0p ) /\ ( * e. ( Poly ` CC ) /\ * =/= 0p ) ) -> ( deg ` ( Xp oF x. * ) ) = ( 1 + ( deg ` * ) ) )
75 50 70 74 mpanl12 
 |-  ( ( * e. ( Poly ` CC ) /\ * =/= 0p ) -> ( deg ` ( Xp oF x. * ) ) = ( 1 + ( deg ` * ) ) )
76 61 75 mpan2 
 |-  ( * e. ( Poly ` CC ) -> ( deg ` ( Xp oF x. * ) ) = ( 1 + ( deg ` * ) ) )
77 dgrcl 
 |-  ( * e. ( Poly ` CC ) -> ( deg ` * ) e. NN0 )
78 nn0cn 
 |-  ( ( deg ` * ) e. NN0 -> ( deg ` * ) e. CC )
79 1cnd 
 |-  ( ( deg ` * ) e. NN0 -> 1 e. CC )
80 78 79 addcomd 
 |-  ( ( deg ` * ) e. NN0 -> ( ( deg ` * ) + 1 ) = ( 1 + ( deg ` * ) ) )
81 nn0p1nn 
 |-  ( ( deg ` * ) e. NN0 -> ( ( deg ` * ) + 1 ) e. NN )
82 80 81 eqeltrrd 
 |-  ( ( deg ` * ) e. NN0 -> ( 1 + ( deg ` * ) ) e. NN )
83 77 82 syl 
 |-  ( * e. ( Poly ` CC ) -> ( 1 + ( deg ` * ) ) e. NN )
84 76 83 eqeltrd 
 |-  ( * e. ( Poly ` CC ) -> ( deg ` ( Xp oF x. * ) ) e. NN )
85 84 nngt0d 
 |-  ( * e. ( Poly ` CC ) -> 0 < ( deg ` ( Xp oF x. * ) ) )
86 0dgr 
 |-  ( 1 e. CC -> ( deg ` ( CC X. { 1 } ) ) = 0 )
87 46 86 ax-mp 
 |-  ( deg ` ( CC X. { 1 } ) ) = 0
88 87 eqcomi 
 |-  0 = ( deg ` ( CC X. { 1 } ) )
89 eqid 
 |-  ( deg ` ( Xp oF x. * ) ) = ( deg ` ( Xp oF x. * ) )
90 88 89 dgradd2 
 |-  ( ( ( CC X. { 1 } ) e. ( Poly ` CC ) /\ ( Xp oF x. * ) e. ( Poly ` CC ) /\ 0 < ( deg ` ( Xp oF x. * ) ) ) -> ( deg ` ( ( CC X. { 1 } ) oF + ( Xp oF x. * ) ) ) = ( deg ` ( Xp oF x. * ) ) )
91 48 52 85 90 mp3an2i 
 |-  ( * e. ( Poly ` CC ) -> ( deg ` ( ( CC X. { 1 } ) oF + ( Xp oF x. * ) ) ) = ( deg ` ( Xp oF x. * ) ) )
92 91 84 eqeltrd 
 |-  ( * e. ( Poly ` CC ) -> ( deg ` ( ( CC X. { 1 } ) oF + ( Xp oF x. * ) ) ) e. NN )
93 fta 
 |-  ( ( ( ( CC X. { 1 } ) oF + ( Xp oF x. * ) ) e. ( Poly ` CC ) /\ ( deg ` ( ( CC X. { 1 } ) oF + ( Xp oF x. * ) ) ) e. NN ) -> E. x e. CC ( ( ( CC X. { 1 } ) oF + ( Xp oF x. * ) ) ` x ) = 0 )
94 54 92 93 syl2anc 
 |-  ( * e. ( Poly ` CC ) -> E. x e. CC ( ( ( CC X. { 1 } ) oF + ( Xp oF x. * ) ) ` x ) = 0 )
95 44 94 mto 
 |-  -. * e. ( Poly ` CC )