Metamath Proof Explorer

Theorem sqrtnpoly

Description: Square root function is not polynomial with complex coefficients either. Otherwise, its composition with a square monomial - the identity - would have to be of even degree. (Contributed by Ender Ting, 22-Jul-2026)

Ref Expression
Assertion sqrtnpoly 
|- -. sqrt e. ( Poly ` CC )

Proof

Step Hyp Ref Expression
1 n2dvds1 
 |-  -. 2 || 1
2 dgrcl 
 |-  ( sqrt e. ( Poly ` CC ) -> ( deg ` sqrt ) e. NN0 )
3 2 nn0zd 
 |-  ( sqrt e. ( Poly ` CC ) -> ( deg ` sqrt ) e. ZZ )
4 2z 
 |-  2 e. ZZ
5 dvdsmul1 
 |-  ( ( 2 e. ZZ /\ ( deg ` sqrt ) e. ZZ ) -> 2 || ( 2 x. ( deg ` sqrt ) ) )
6 4 5 mpan 
 |-  ( ( deg ` sqrt ) e. ZZ -> 2 || ( 2 x. ( deg ` sqrt ) ) )
7 3 6 syl 
 |-  ( sqrt e. ( Poly ` CC ) -> 2 || ( 2 x. ( deg ` sqrt ) ) )
8 df-idp 
 |-  Xp = ( _I |` CC )
9 idfn 
 |-  _I Fn _V
10 ovex 
 |-  ( x ^ 2 ) e. _V
11 10 rgenw 
 |-  A. x e. CC ( x ^ 2 ) e. _V
12 nfcv 
 |-  F/_ x CC
13 12 mptfnf 
 |-  ( A. x e. CC ( x ^ 2 ) e. _V <-> ( x e. CC |-> ( x ^ 2 ) ) Fn CC )
14 11 13 mpbi 
 |-  ( x e. CC |-> ( x ^ 2 ) ) Fn CC
15 sqrtf 
 |-  sqrt : CC --> CC
16 fnfco 
 |-  ( ( ( x e. CC |-> ( x ^ 2 ) ) Fn CC /\ sqrt : CC --> CC ) -> ( ( x e. CC |-> ( x ^ 2 ) ) o. sqrt ) Fn CC )
17 14 15 16 mp2an 
 |-  ( ( x e. CC |-> ( x ^ 2 ) ) o. sqrt ) Fn CC
18 9 17 pm3.2i 
 |-  ( _I Fn _V /\ ( ( x e. CC |-> ( x ^ 2 ) ) o. sqrt ) Fn CC )
19 ssv 
 |-  CC C_ _V
20 fvreseq1 
 |-  ( ( ( _I Fn _V /\ ( ( x e. CC |-> ( x ^ 2 ) ) o. sqrt ) Fn CC ) /\ CC C_ _V ) -> ( ( _I |` CC ) = ( ( x e. CC |-> ( x ^ 2 ) ) o. sqrt ) <-> A. y e. CC ( _I ` y ) = ( ( ( x e. CC |-> ( x ^ 2 ) ) o. sqrt ) ` y ) ) )
21 18 19 20 mp2an 
 |-  ( ( _I |` CC ) = ( ( x e. CC |-> ( x ^ 2 ) ) o. sqrt ) <-> A. y e. CC ( _I ` y ) = ( ( ( x e. CC |-> ( x ^ 2 ) ) o. sqrt ) ` y ) )
22 sqrtcl 
 |-  ( y e. CC -> ( sqrt ` y ) e. CC )
23 oveq1 
 |-  ( x = ( sqrt ` y ) -> ( x ^ 2 ) = ( ( sqrt ` y ) ^ 2 ) )
24 eqid 
 |-  ( x e. CC |-> ( x ^ 2 ) ) = ( x e. CC |-> ( x ^ 2 ) )
25 ovex 
 |-  ( ( sqrt ` y ) ^ 2 ) e. _V
26 23 24 25 fvmpt 
 |-  ( ( sqrt ` y ) e. CC -> ( ( x e. CC |-> ( x ^ 2 ) ) ` ( sqrt ` y ) ) = ( ( sqrt ` y ) ^ 2 ) )
27 22 26 syl 
 |-  ( y e. CC -> ( ( x e. CC |-> ( x ^ 2 ) ) ` ( sqrt ` y ) ) = ( ( sqrt ` y ) ^ 2 ) )
28 sqrtth 
 |-  ( y e. CC -> ( ( sqrt ` y ) ^ 2 ) = y )
29 27 28 eqtr2d 
 |-  ( y e. CC -> y = ( ( x e. CC |-> ( x ^ 2 ) ) ` ( sqrt ` y ) ) )
30 fvi 
 |-  ( y e. CC -> ( _I ` y ) = y )
31 fvco3 
 |-  ( ( sqrt : CC --> CC /\ y e. CC ) -> ( ( ( x e. CC |-> ( x ^ 2 ) ) o. sqrt ) ` y ) = ( ( x e. CC |-> ( x ^ 2 ) ) ` ( sqrt ` y ) ) )
32 15 31 mpan 
 |-  ( y e. CC -> ( ( ( x e. CC |-> ( x ^ 2 ) ) o. sqrt ) ` y ) = ( ( x e. CC |-> ( x ^ 2 ) ) ` ( sqrt ` y ) ) )
33 29 30 32 3eqtr4d 
 |-  ( y e. CC -> ( _I ` y ) = ( ( ( x e. CC |-> ( x ^ 2 ) ) o. sqrt ) ` y ) )
34 21 33 mprgbir 
 |-  ( _I |` CC ) = ( ( x e. CC |-> ( x ^ 2 ) ) o. sqrt )
35 8 34 eqtr2i 
 |-  ( ( x e. CC |-> ( x ^ 2 ) ) o. sqrt ) = Xp
36 35 a1i 
 |-  ( sqrt e. ( Poly ` CC ) -> ( ( x e. CC |-> ( x ^ 2 ) ) o. sqrt ) = Xp )
37 36 fveq2d 
 |-  ( sqrt e. ( Poly ` CC ) -> ( deg ` ( ( x e. CC |-> ( x ^ 2 ) ) o. sqrt ) ) = ( deg ` Xp ) )
38 ax-1cn 
 |-  1 e. CC
39 ax-1ne0 
 |-  1 =/= 0
40 2nn0 
 |-  2 e. NN0
41 sqcl 
 |-  ( x e. CC -> ( x ^ 2 ) e. CC )
42 mullid 
 |-  ( ( x ^ 2 ) e. CC -> ( 1 x. ( x ^ 2 ) ) = ( x ^ 2 ) )
43 42 eqcomd 
 |-  ( ( x ^ 2 ) e. CC -> ( x ^ 2 ) = ( 1 x. ( x ^ 2 ) ) )
44 41 43 syl 
 |-  ( x e. CC -> ( x ^ 2 ) = ( 1 x. ( x ^ 2 ) ) )
45 44 mpteq2ia 
 |-  ( x e. CC |-> ( x ^ 2 ) ) = ( x e. CC |-> ( 1 x. ( x ^ 2 ) ) )
46 45 dgr1term 
 |-  ( ( 1 e. CC /\ 1 =/= 0 /\ 2 e. NN0 ) -> ( deg ` ( x e. CC |-> ( x ^ 2 ) ) ) = 2 )
47 38 39 40 46 mp3an 
 |-  ( deg ` ( x e. CC |-> ( x ^ 2 ) ) ) = 2
48 47 eqcomi 
 |-  2 = ( deg ` ( x e. CC |-> ( x ^ 2 ) ) )
49 eqid 
 |-  ( deg ` sqrt ) = ( deg ` sqrt )
50 ssid 
 |-  CC C_ CC
51 plypow 
 |-  ( ( CC C_ CC /\ 1 e. CC /\ 2 e. NN0 ) -> ( x e. CC |-> ( x ^ 2 ) ) e. ( Poly ` CC ) )
52 50 38 40 51 mp3an 
 |-  ( x e. CC |-> ( x ^ 2 ) ) e. ( Poly ` CC )
53 52 a1i 
 |-  ( sqrt e. ( Poly ` CC ) -> ( x e. CC |-> ( x ^ 2 ) ) e. ( Poly ` CC ) )
54 id 
 |-  ( sqrt e. ( Poly ` CC ) -> sqrt e. ( Poly ` CC ) )
55 48 49 53 54 dgrco 
 |-  ( sqrt e. ( Poly ` CC ) -> ( deg ` ( ( x e. CC |-> ( x ^ 2 ) ) o. sqrt ) ) = ( 2 x. ( deg ` sqrt ) ) )
56 dgrid 
 |-  ( deg ` Xp ) = 1
57 56 a1i 
 |-  ( sqrt e. ( Poly ` CC ) -> ( deg ` Xp ) = 1 )
58 37 55 57 3eqtr3d 
 |-  ( sqrt e. ( Poly ` CC ) -> ( 2 x. ( deg ` sqrt ) ) = 1 )
59 7 58 breqtrd 
 |-  ( sqrt e. ( Poly ` CC ) -> 2 || 1 )
60 1 59 mto 
 |-  -. sqrt e. ( Poly ` CC )