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 ¬ √ ∈ ( Poly ‘ ℂ )

Proof

Step Hyp Ref Expression
1 n2dvds1 ⊢ ¬ 2 ∥ 1
2 dgrcl ⊢ ( √ ∈ ( Poly ‘ ℂ ) → ( deg ‘ √ ) ∈ ℕ0 )
3 2 nn0zd ⊢ ( √ ∈ ( Poly ‘ ℂ ) → ( deg ‘ √ ) ∈ ℤ )
4 2z ⊢ 2 ∈ ℤ
5 dvdsmul1 ⊢ ( ( 2 ∈ ℤ ∧ ( deg ‘ √ ) ∈ ℤ ) → 2 ∥ ( 2 · ( deg ‘ √ ) ) )
6 4 5 mpan ⊢ ( ( deg ‘ √ ) ∈ ℤ → 2 ∥ ( 2 · ( deg ‘ √ ) ) )
7 3 6 syl ⊢ ( √ ∈ ( Poly ‘ ℂ ) → 2 ∥ ( 2 · ( deg ‘ √ ) ) )
8 df-idp ⊢ Xp = ( I ↾ ℂ )
9 idfn ⊢ I Fn V
10 ovex ⊢ ( 𝑥 ↑ 2 ) ∈ V
11 10 rgenw ⊢ ∀ 𝑥 ∈ ℂ ( 𝑥 ↑ 2 ) ∈ V
12 nfcv ⊢ Ⅎ 𝑥 ℂ
13 12 mptfnf ⊢ ( ∀ 𝑥 ∈ ℂ ( 𝑥 ↑ 2 ) ∈ V ↔ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) Fn ℂ )
14 11 13 mpbi ⊢ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) Fn ℂ
15 sqrtf ⊢ √ : ℂ ⟶ ℂ
16 fnfco ⊢ ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) Fn ℂ ∧ √ : ℂ ⟶ ℂ ) → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ∘ √ ) Fn ℂ )
17 14 15 16 mp2an ⊢ ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ∘ √ ) Fn ℂ
18 9 17 pm3.2i ⊢ ( I Fn V ∧ ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ∘ √ ) Fn ℂ )
19 ssv ⊢ ℂ ⊆ V
20 fvreseq1 ⊢ ( ( ( I Fn V ∧ ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ∘ √ ) Fn ℂ ) ∧ ℂ ⊆ V ) → ( ( I ↾ ℂ ) = ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ∘ √ ) ↔ ∀ 𝑦 ∈ ℂ ( I ‘ 𝑦 ) = ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ∘ √ ) ‘ 𝑦 ) ) )
21 18 19 20 mp2an ⊢ ( ( I ↾ ℂ ) = ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ∘ √ ) ↔ ∀ 𝑦 ∈ ℂ ( I ‘ 𝑦 ) = ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ∘ √ ) ‘ 𝑦 ) )
22 sqrtcl ⊢ ( 𝑦 ∈ ℂ → ( √ ‘ 𝑦 ) ∈ ℂ )
23 oveq1 ⊢ ( 𝑥 = ( √ ‘ 𝑦 ) → ( 𝑥 ↑ 2 ) = ( ( √ ‘ 𝑦 ) ↑ 2 ) )
24 eqid ⊢ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) )
25 ovex ⊢ ( ( √ ‘ 𝑦 ) ↑ 2 ) ∈ V
26 23 24 25 fvmpt ⊢ ( ( √ ‘ 𝑦 ) ∈ ℂ → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ‘ ( √ ‘ 𝑦 ) ) = ( ( √ ‘ 𝑦 ) ↑ 2 ) )
27 22 26 syl ⊢ ( 𝑦 ∈ ℂ → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ‘ ( √ ‘ 𝑦 ) ) = ( ( √ ‘ 𝑦 ) ↑ 2 ) )
28 sqrtth ⊢ ( 𝑦 ∈ ℂ → ( ( √ ‘ 𝑦 ) ↑ 2 ) = 𝑦 )
29 27 28 eqtr2d ⊢ ( 𝑦 ∈ ℂ → 𝑦 = ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ‘ ( √ ‘ 𝑦 ) ) )
30 fvi ⊢ ( 𝑦 ∈ ℂ → ( I ‘ 𝑦 ) = 𝑦 )
31 fvco3 ⊢ ( ( √ : ℂ ⟶ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ∘ √ ) ‘ 𝑦 ) = ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ‘ ( √ ‘ 𝑦 ) ) )
32 15 31 mpan ⊢ ( 𝑦 ∈ ℂ → ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ∘ √ ) ‘ 𝑦 ) = ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ‘ ( √ ‘ 𝑦 ) ) )
33 29 30 32 3eqtr4d ⊢ ( 𝑦 ∈ ℂ → ( I ‘ 𝑦 ) = ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ∘ √ ) ‘ 𝑦 ) )
34 21 33 mprgbir ⊢ ( I ↾ ℂ ) = ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ∘ √ )
35 8 34 eqtr2i ⊢ ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ∘ √ ) = Xp
36 35 a1i ⊢ ( √ ∈ ( Poly ‘ ℂ ) → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ∘ √ ) = Xp )
37 36 fveq2d ⊢ ( √ ∈ ( Poly ‘ ℂ ) → ( deg ‘ ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ∘ √ ) ) = ( deg ‘ Xp ) )
38 ax-1cn ⊢ 1 ∈ ℂ
39 ax-1ne0 ⊢ 1 ≠ 0
40 2nn0 ⊢ 2 ∈ ℕ0
41 sqcl ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ↑ 2 ) ∈ ℂ )
42 mullid ⊢ ( ( 𝑥 ↑ 2 ) ∈ ℂ → ( 1 · ( 𝑥 ↑ 2 ) ) = ( 𝑥 ↑ 2 ) )
43 42 eqcomd ⊢ ( ( 𝑥 ↑ 2 ) ∈ ℂ → ( 𝑥 ↑ 2 ) = ( 1 · ( 𝑥 ↑ 2 ) ) )
44 41 43 syl ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ↑ 2 ) = ( 1 · ( 𝑥 ↑ 2 ) ) )
45 44 mpteq2ia ⊢ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) = ( 𝑥 ∈ ℂ ↦ ( 1 · ( 𝑥 ↑ 2 ) ) )
46 45 dgr1term ⊢ ( ( 1 ∈ ℂ ∧ 1 ≠ 0 ∧ 2 ∈ ℕ0 ) → ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ) = 2 )
47 38 39 40 46 mp3an ⊢ ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ) = 2
48 47 eqcomi ⊢ 2 = ( deg ‘ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) )
49 eqid ⊢ ( deg ‘ √ ) = ( deg ‘ √ )
50 ssid ⊢ ℂ ⊆ ℂ
51 plypow ⊢ ( ( ℂ ⊆ ℂ ∧ 1 ∈ ℂ ∧ 2 ∈ ℕ0 ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ∈ ( Poly ‘ ℂ ) )
52 50 38 40 51 mp3an ⊢ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ∈ ( Poly ‘ ℂ )
53 52 a1i ⊢ ( √ ∈ ( Poly ‘ ℂ ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ∈ ( Poly ‘ ℂ ) )
54 id ⊢ ( √ ∈ ( Poly ‘ ℂ ) → √ ∈ ( Poly ‘ ℂ ) )
55 48 49 53 54 dgrco ⊢ ( √ ∈ ( Poly ‘ ℂ ) → ( deg ‘ ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ∘ √ ) ) = ( 2 · ( deg ‘ √ ) ) )
56 dgrid ⊢ ( deg ‘ Xp ) = 1
57 56 a1i ⊢ ( √ ∈ ( Poly ‘ ℂ ) → ( deg ‘ Xp ) = 1 )
58 37 55 57 3eqtr3d ⊢ ( √ ∈ ( Poly ‘ ℂ ) → ( 2 · ( deg ‘ √ ) ) = 1 )
59 7 58 breqtrd ⊢ ( √ ∈ ( Poly ‘ ℂ ) → 2 ∥ 1 )
60 1 59 mto ⊢ ¬ √ ∈ ( Poly ‘ ℂ )