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 20 22 eqtrd 
 |-  ( x e. CC -> ( ( ( CC X. { 1 } ) oF + ( Xp oF x. * ) ) ` x ) = ( 1 + ( ( Xp oF x. * ) ` x ) ) )
24 fnfvof 
 |-  ( ( ( Xp Fn CC /\ * Fn CC ) /\ ( CC e. _V /\ x e. CC ) ) -> ( ( Xp oF x. * ) ` x ) = ( ( Xp ` x ) x. ( * ` x ) ) )
25 8 12 24 mpanl12 
 |-  ( ( CC e. _V /\ x e. CC ) -> ( ( Xp oF x. * ) ` x ) = ( ( Xp ` x ) x. ( * ` x ) ) )
26 1 25 mpan 
 |-  ( x e. CC -> ( ( Xp oF x. * ) ` x ) = ( ( Xp ` x ) x. ( * ` x ) ) )
27 6 fveq1i 
 |-  ( Xp ` x ) = ( ( _I |` CC ) ` x )
28 fvres 
 |-  ( x e. CC -> ( ( _I |` CC ) ` x ) = ( _I ` x ) )
29 27 28 eqtrid 
 |-  ( x e. CC -> ( Xp ` x ) = ( _I ` x ) )
30 fvi 
 |-  ( x e. CC -> ( _I ` x ) = x )
31 29 30 eqtrd 
 |-  ( x e. CC -> ( Xp ` x ) = x )
32 31 oveq1d 
 |-  ( x e. CC -> ( ( Xp ` x ) x. ( * ` x ) ) = ( x x. ( * ` x ) ) )
33 26 32 eqtrd 
 |-  ( x e. CC -> ( ( Xp oF x. * ) ` x ) = ( x x. ( * ` x ) ) )
34 33 oveq2d 
 |-  ( x e. CC -> ( 1 + ( ( Xp oF x. * ) ` x ) ) = ( 1 + ( x x. ( * ` x ) ) ) )
35 23 34 eqtrd 
 |-  ( x e. CC -> ( ( ( CC X. { 1 } ) oF + ( Xp oF x. * ) ) ` x ) = ( 1 + ( x x. ( * ` x ) ) ) )
36 1red 
 |-  ( x e. CC -> 1 e. RR )
37 cjmulrcl 
 |-  ( x e. CC -> ( x x. ( * ` x ) ) e. RR )
38 0lt1 
 |-  0 < 1
39 38 a1i 
 |-  ( x e. CC -> 0 < 1 )
40 cjmulge0 
 |-  ( x e. CC -> 0 <_ ( x x. ( * ` x ) ) )
41 36 37 39 40 addgtge0d 
 |-  ( x e. CC -> 0 < ( 1 + ( x x. ( * ` x ) ) ) )
42 41 gt0ne0d 
 |-  ( x e. CC -> ( 1 + ( x x. ( * ` x ) ) ) =/= 0 )
43 35 42 eqnetrd 
 |-  ( x e. CC -> ( ( ( CC X. { 1 } ) oF + ( Xp oF x. * ) ) ` x ) =/= 0 )
44 43 neneqd 
 |-  ( x e. CC -> -. ( ( ( CC X. { 1 } ) oF + ( Xp oF x. * ) ) ` x ) = 0 )
45 44 nrex 
 |-  -. E. x e. CC ( ( ( CC X. { 1 } ) oF + ( Xp oF x. * ) ) ` x ) = 0
46 ssid 
 |-  CC C_ CC
47 ax-1cn 
 |-  1 e. CC
48 plyconst 
 |-  ( ( CC C_ CC /\ 1 e. CC ) -> ( CC X. { 1 } ) e. ( Poly ` CC ) )
49 46 47 48 mp2an 
 |-  ( CC X. { 1 } ) e. ( Poly ` CC )
50 plyid 
 |-  ( ( CC C_ CC /\ 1 e. CC ) -> Xp e. ( Poly ` CC ) )
51 46 47 50 mp2an 
 |-  Xp e. ( Poly ` CC )
52 plymulcl 
 |-  ( ( Xp e. ( Poly ` CC ) /\ * e. ( Poly ` CC ) ) -> ( Xp oF x. * ) e. ( Poly ` CC ) )
53 51 52 mpan 
 |-  ( * e. ( Poly ` CC ) -> ( Xp oF x. * ) e. ( Poly ` CC ) )
54 plyaddcl 
 |-  ( ( ( CC X. { 1 } ) e. ( Poly ` CC ) /\ ( Xp oF x. * ) e. ( Poly ` CC ) ) -> ( ( CC X. { 1 } ) oF + ( Xp oF x. * ) ) e. ( Poly ` CC ) )
55 49 53 54 sylancr 
 |-  ( * e. ( Poly ` CC ) -> ( ( CC X. { 1 } ) oF + ( Xp oF x. * ) ) e. ( Poly ` CC ) )
56 dgrcl 
 |-  ( * e. ( Poly ` CC ) -> ( deg ` * ) e. NN0 )
57 nn0p1nn 
 |-  ( ( deg ` * ) e. NN0 -> ( ( deg ` * ) + 1 ) e. NN )
58 nn0cn 
 |-  ( ( deg ` * ) e. NN0 -> ( deg ` * ) e. CC )
59 1cnd 
 |-  ( ( deg ` * ) e. NN0 -> 1 e. CC )
60 58 59 addcomd 
 |-  ( ( deg ` * ) e. NN0 -> ( ( deg ` * ) + 1 ) = ( 1 + ( deg ` * ) ) )
61 60 eleq1d 
 |-  ( ( deg ` * ) e. NN0 -> ( ( ( deg ` * ) + 1 ) e. NN <-> ( 1 + ( deg ` * ) ) e. NN ) )
62 57 61 mpbid 
 |-  ( ( deg ` * ) e. NN0 -> ( 1 + ( deg ` * ) ) e. NN )
63 56 62 syl 
 |-  ( * e. ( Poly ` CC ) -> ( 1 + ( deg ` * ) ) e. NN )
64 1re 
 |-  1 e. RR
65 cjre 
 |-  ( 1 e. RR -> ( * ` 1 ) = 1 )
66 64 65 ax-mp 
 |-  ( * ` 1 ) = 1
67 ax-1ne0 
 |-  1 =/= 0
68 66 67 eqnetri 
 |-  ( * ` 1 ) =/= 0
69 ne0p 
 |-  ( ( 1 e. CC /\ ( * ` 1 ) =/= 0 ) -> * =/= 0p )
70 47 68 69 mp2an 
 |-  * =/= 0p
71 6 fveq1i 
 |-  ( Xp ` 1 ) = ( ( _I |` CC ) ` 1 )
72 fvres 
 |-  ( 1 e. CC -> ( ( _I |` CC ) ` 1 ) = ( _I ` 1 ) )
73 47 72 ax-mp 
 |-  ( ( _I |` CC ) ` 1 ) = ( _I ` 1 )
74 71 73 eqtri 
 |-  ( Xp ` 1 ) = ( _I ` 1 )
75 fvi 
 |-  ( 1 e. _V -> ( _I ` 1 ) = 1 )
76 2 75 ax-mp 
 |-  ( _I ` 1 ) = 1
77 74 76 eqtri 
 |-  ( Xp ` 1 ) = 1
78 77 67 eqnetri 
 |-  ( Xp ` 1 ) =/= 0
79 ne0p 
 |-  ( ( 1 e. CC /\ ( Xp ` 1 ) =/= 0 ) -> Xp =/= 0p )
80 47 78 79 mp2an 
 |-  Xp =/= 0p
81 51 80 pm3.2i 
 |-  ( Xp e. ( Poly ` CC ) /\ Xp =/= 0p )
82 dgrid 
 |-  ( deg ` Xp ) = 1
83 82 eqcomi 
 |-  1 = ( deg ` Xp )
84 eqid 
 |-  ( deg ` * ) = ( deg ` * )
85 83 84 dgrmul 
 |-  ( ( ( Xp e. ( Poly ` CC ) /\ Xp =/= 0p ) /\ ( * e. ( Poly ` CC ) /\ * =/= 0p ) ) -> ( deg ` ( Xp oF x. * ) ) = ( 1 + ( deg ` * ) ) )
86 81 85 mpan 
 |-  ( ( * e. ( Poly ` CC ) /\ * =/= 0p ) -> ( deg ` ( Xp oF x. * ) ) = ( 1 + ( deg ` * ) ) )
87 70 86 mpan2 
 |-  ( * e. ( Poly ` CC ) -> ( deg ` ( Xp oF x. * ) ) = ( 1 + ( deg ` * ) ) )
88 87 eleq1d 
 |-  ( * e. ( Poly ` CC ) -> ( ( deg ` ( Xp oF x. * ) ) e. NN <-> ( 1 + ( deg ` * ) ) e. NN ) )
89 63 88 mpbird 
 |-  ( * e. ( Poly ` CC ) -> ( deg ` ( Xp oF x. * ) ) e. NN )
90 49 a1i 
 |-  ( * e. ( Poly ` CC ) -> ( CC X. { 1 } ) e. ( Poly ` CC ) )
91 89 nngt0d 
 |-  ( * e. ( Poly ` CC ) -> 0 < ( deg ` ( Xp oF x. * ) ) )
92 0dgr 
 |-  ( 1 e. CC -> ( deg ` ( CC X. { 1 } ) ) = 0 )
93 47 92 ax-mp 
 |-  ( deg ` ( CC X. { 1 } ) ) = 0
94 93 eqcomi 
 |-  0 = ( deg ` ( CC X. { 1 } ) )
95 eqid 
 |-  ( deg ` ( Xp oF x. * ) ) = ( deg ` ( Xp oF x. * ) )
96 94 95 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. * ) ) )
97 90 53 91 96 syl3anc 
 |-  ( * e. ( Poly ` CC ) -> ( deg ` ( ( CC X. { 1 } ) oF + ( Xp oF x. * ) ) ) = ( deg ` ( Xp oF x. * ) ) )
98 97 eleq1d 
 |-  ( * e. ( Poly ` CC ) -> ( ( deg ` ( ( CC X. { 1 } ) oF + ( Xp oF x. * ) ) ) e. NN <-> ( deg ` ( Xp oF x. * ) ) e. NN ) )
99 98 biimprd 
 |-  ( * e. ( Poly ` CC ) -> ( ( deg ` ( Xp oF x. * ) ) e. NN -> ( deg ` ( ( CC X. { 1 } ) oF + ( Xp oF x. * ) ) ) e. NN ) )
100 89 99 mpd 
 |-  ( * e. ( Poly ` CC ) -> ( deg ` ( ( CC X. { 1 } ) oF + ( Xp oF x. * ) ) ) e. NN )
101 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 )
102 55 100 101 syl2anc 
 |-  ( * e. ( Poly ` CC ) -> E. x e. CC ( ( ( CC X. { 1 } ) oF + ( Xp oF x. * ) ) ` x ) = 0 )
103 45 102 mto 
 |-  -. * e. ( Poly ` CC )