Theorem sqrtnpoly 47826

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.)

Assertion

Ref	Expression
sqrtnpoly	⊢ ¬ √ ∈ (Poly‘ℂ)

Proof of Theorem sqrtnpoly

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		n2dvds1 16483	. 2 ⊢ ¬ 2 ∥ 1
2		dgrcl 26491	. . . . 5 ⊢ (√ ∈ (Poly‘ℂ) → (deg‘√) ∈ ℕ0)
3	2	nn0zd 12665	. . . 4 ⊢ (√ ∈ (Poly‘ℂ) → (deg‘√) ∈ ℤ)
4		2z 12675	. . . . 5 ⊢ 2 ∈ ℤ
5		dvdsmul1 16392	. . . . 5 ⊢ ((2 ∈ ℤ ∧ (deg‘√) ∈ ℤ) → 2 ∥ (2 · (deg‘√)))
6	4, 5	mpan 703	. . . 4 ⊢ ((deg‘√) ∈ ℤ → 2 ∥ (2 · (deg‘√)))
7	3, 6	syl 18	. . 3 ⊢ (√ ∈ (Poly‘ℂ) → 2 ∥ (2 · (deg‘√)))
8		df-idp 26446	. . . . . . 7 ⊢ Xp = ( I ↾ ℂ)
9		idfn 6663	. . . . . . . . . 10 ⊢ I Fn V
10		ovex 7449	. . . . . . . . . . . . 13 ⊢ (𝑥↑2) ∈ V
11	10	rgenw 3080	. . . . . . . . . . . 12 ⊢ ∀𝑥 ∈ ℂ (𝑥↑2) ∈ V
12		nfcv 2922	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥ℂ
13	12	mptfnf 6670	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ ℂ (𝑥↑2) ∈ V ↔ (𝑥 ∈ ℂ ↦ (𝑥↑2)) Fn ℂ)
14	11, 13	mpbi 233	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℂ ↦ (𝑥↑2)) Fn ℂ
15		sqrtf 15476	. . . . . . . . . . 11 ⊢ √:ℂ⟶ℂ
16		fnfco 6743	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℂ ↦ (𝑥↑2)) Fn ℂ ∧ √:ℂ⟶ℂ) → ((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘ √) Fn ℂ)
17	14, 15, 16	mp2an 705	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘ √) Fn ℂ
18	9, 17	pm3.2i 476	. . . . . . . . 9 ⊢ ( I Fn V ∧ ((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘ √) Fn ℂ)
19		ssv 3955	. . . . . . . . 9 ⊢ ℂ ⊆ V
20		fvreseq1 7034	. . . . . . . . 9 ⊢ ((( I Fn V ∧ ((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘ √) Fn ℂ) ∧ ℂ ⊆ V) → (( I ↾ ℂ) = ((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘ √) ↔ ∀𝑦 ∈ ℂ ( I ‘𝑦) = (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘ √)‘𝑦)))
21	18, 19, 20	mp2an 705	. . . . . . . 8 ⊢ (( I ↾ ℂ) = ((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘ √) ↔ ∀𝑦 ∈ ℂ ( I ‘𝑦) = (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘ √)‘𝑦))
22		sqrtcl 15474	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℂ → (√‘𝑦) ∈ ℂ)
23		oveq1 7423	. . . . . . . . . . . 12 ⊢ (𝑥 = (√‘𝑦) → (𝑥↑2) = ((√‘𝑦)↑2))
24		eqid 2760	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ ↦ (𝑥↑2)) = (𝑥 ∈ ℂ ↦ (𝑥↑2))
25		ovex 7449	. . . . . . . . . . . 12 ⊢ ((√‘𝑦)↑2) ∈ V
26	23, 24, 25	fvmpt 6989	. . . . . . . . . . 11 ⊢ ((√‘𝑦) ∈ ℂ → ((𝑥 ∈ ℂ ↦ (𝑥↑2))‘(√‘𝑦)) = ((√‘𝑦)↑2))
27	22, 26	syl 18	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℂ → ((𝑥 ∈ ℂ ↦ (𝑥↑2))‘(√‘𝑦)) = ((√‘𝑦)↑2))
28		sqrtth 15477	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℂ → ((√‘𝑦)↑2) = 𝑦)
29	27, 28	eqtr2d 2796	. . . . . . . . 9 ⊢ (𝑦 ∈ ℂ → 𝑦 = ((𝑥 ∈ ℂ ↦ (𝑥↑2))‘(√‘𝑦)))
30		fvi 6957	. . . . . . . . 9 ⊢ (𝑦 ∈ ℂ → ( I ‘𝑦) = 𝑦)
31		fvco3 6981	. . . . . . . . . 10 ⊢ ((√:ℂ⟶ℂ ∧ 𝑦 ∈ ℂ) → (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘ √)‘𝑦) = ((𝑥 ∈ ℂ ↦ (𝑥↑2))‘(√‘𝑦)))
32	15, 31	mpan 703	. . . . . . . . 9 ⊢ (𝑦 ∈ ℂ → (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘ √)‘𝑦) = ((𝑥 ∈ ℂ ↦ (𝑥↑2))‘(√‘𝑦)))
33	29, 30, 32	3eqtr4d 2805	. . . . . . . 8 ⊢ (𝑦 ∈ ℂ → ( I ‘𝑦) = (((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘ √)‘𝑦))
34	21, 33	mprgbir 3083	. . . . . . 7 ⊢ ( I ↾ ℂ) = ((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘ √)
35	8, 34	eqtr2i 2784	. . . . . 6 ⊢ ((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘ √) = Xp
36	35	a1i 11	. . . . 5 ⊢ (√ ∈ (Poly‘ℂ) → ((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘ √) = Xp)
37	36	fveq2d 6885	. . . 4 ⊢ (√ ∈ (Poly‘ℂ) → (deg‘((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘ √)) = (deg‘Xp))
38		ax-1cn 11207	. . . . . . 7 ⊢ 1 ∈ ℂ
39		ax-1ne0 11218	. . . . . . 7 ⊢ 1 ≠ 0
40		2nn0 12570	. . . . . . 7 ⊢ 2 ∈ ℕ0
41		sqcl 14207	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℂ → (𝑥↑2) ∈ ℂ)
42		mullid 11256	. . . . . . . . . . 11 ⊢ ((𝑥↑2) ∈ ℂ → (1 · (𝑥↑2)) = (𝑥↑2))
43	42	eqcomd 2766	. . . . . . . . . 10 ⊢ ((𝑥↑2) ∈ ℂ → (𝑥↑2) = (1 · (𝑥↑2)))
44	41, 43	syl 18	. . . . . . . . 9 ⊢ (𝑥 ∈ ℂ → (𝑥↑2) = (1 · (𝑥↑2)))
45	44	mpteq2ia 5200	. . . . . . . 8 ⊢ (𝑥 ∈ ℂ ↦ (𝑥↑2)) = (𝑥 ∈ ℂ ↦ (1 · (𝑥↑2)))
46	45	dgr1term 26518	. . . . . . 7 ⊢ ((1 ∈ ℂ ∧ 1 ≠ 0 ∧ 2 ∈ ℕ0) → (deg‘(𝑥 ∈ ℂ ↦ (𝑥↑2))) = 2)
47	38, 39, 40, 46	mp3an 1490	. . . . . 6 ⊢ (deg‘(𝑥 ∈ ℂ ↦ (𝑥↑2))) = 2
48	47	eqcomi 2769	. . . . 5 ⊢ 2 = (deg‘(𝑥 ∈ ℂ ↦ (𝑥↑2)))
49		eqid 2760	. . . . 5 ⊢ (deg‘√) = (deg‘√)
50		ssid 3953	. . . . . . 7 ⊢ ℂ ⊆ ℂ
51		plypow 26462	. . . . . . 7 ⊢ ((ℂ ⊆ ℂ ∧ 1 ∈ ℂ ∧ 2 ∈ ℕ0) → (𝑥 ∈ ℂ ↦ (𝑥↑2)) ∈ (Poly‘ℂ))
52	50, 38, 40, 51	mp3an 1490	. . . . . 6 ⊢ (𝑥 ∈ ℂ ↦ (𝑥↑2)) ∈ (Poly‘ℂ)
53	52	a1i 11	. . . . 5 ⊢ (√ ∈ (Poly‘ℂ) → (𝑥 ∈ ℂ ↦ (𝑥↑2)) ∈ (Poly‘ℂ))
54		id 23	. . . . 5 ⊢ (√ ∈ (Poly‘ℂ) → √ ∈ (Poly‘ℂ))
55	48, 49, 53, 54	dgrco 26533	. . . 4 ⊢ (√ ∈ (Poly‘ℂ) → (deg‘((𝑥 ∈ ℂ ↦ (𝑥↑2)) ∘ √)) = (2 · (deg‘√)))
56		dgrid 26522	. . . . 5 ⊢ (deg‘Xp) = 1
57	56	a1i 11	. . . 4 ⊢ (√ ∈ (Poly‘ℂ) → (deg‘Xp) = 1)
58	37, 55, 57	3eqtr3d 2803	. . 3 ⊢ (√ ∈ (Poly‘ℂ) → (2 · (deg‘√)) = 1)
59	7, 58	breqtrd 5131	. 2 ⊢ (√ ∈ (Poly‘ℂ) → 2 ∥ 1)
60	1, 59	mto 200	1 ⊢ ¬ √ ∈ (Poly‘ℂ)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ≠ wne 2955  ∀wral 3076  Vcvv 3450   ⊆ wss 3899   class class class wbr 5103   ↦ cmpt 5186   I cid 5549   ↾ cres 5657   ∘ ccom 5659   Fn wfn 6530  ⟶wf 6531  ‘cfv 6535  (class class class)co 7416  ℂcc 11147  0cc0 11149  1c1 11150   · cmul 11154  2c2 12344  ℕ₀cn0 12553  ℤcz 12640  ↑cexp 14150  √csqrt 15345   ∥ cdvds 16367  Polycply 26441  X_pcidp 26442  degcdgr 26444

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7742  ax-inf2 9627  ax-cnex 11205  ax-resscn 11206  ax-1cn 11207  ax-icn 11208  ax-addcl 11209  ax-addrcl 11210  ax-mulcl 11211  ax-mulrcl 11212  ax-mulcom 11213  ax-addass 11214  ax-mulass 11215  ax-distr 11216  ax-i2m1 11217  ax-1ne0 11218  ax-1rid 11219  ax-rnegex 11220  ax-rrecex 11221  ax-cnre 11222  ax-pre-lttri 11223  ax-pre-lttrn 11224  ax-pre-ltadd 11225  ax-pre-mulgt0 11226  ax-pre-sup 11227

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6301  df-ord 6362  df-on 6363  df-lim 6364  df-suc 6365  df-iota 6491  df-fun 6537  df-fn 6538  df-f 6539  df-f1 6540  df-fo 6541  df-f1o 6542  df-fv 6543  df-isom 6544  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-of 7684  df-om 7869  df-1st 7992  df-2nd 7993  df-frecs 8285  df-wrecs 8316  df-recs 8365  df-rdg 8404  df-1o 8462  df-er 8703  df-map 8835  df-pm 8836  df-en 8960  df-dom 8961  df-sdom 8962  df-fin 8963  df-sup 9419  df-inf 9420  df-oi 9489  df-card 9969  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11492  df-neg 11493  df-div 11921  df-nn 12283  df-2 12352  df-3 12353  df-n0 12554  df-z 12641  df-uz 12913  df-rp 13068  df-fz 13587  df-fzo 13735  df-fl 13878  df-seq 14091  df-exp 14151  df-hash 14420  df-cj 15211  df-re 15212  df-im 15213  df-sqrt 15347  df-abs 15348  df-clim 15600  df-rlim 15601  df-sum 15799  df-dvds 16368  df-0p 25930  df-ply 26445  df-idp 26446  df-coe 26447  df-dgr 26448

This theorem is used by: (None)