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	$⊢ \neg \sqrt \in Poly (ℂ)$

Proof

Step	Hyp	Ref	Expression
1		n2dvds1	$⊢ \neg 2 ∥ 1$
2		dgrcl	$⊢ \sqrt \in Poly (ℂ) \to \deg (\sqrt) \in ℕ_{0}$
3	2	nn0zd	$⊢ \sqrt \in Poly (ℂ) \to \deg (\sqrt) \in ℤ$
4		2z	$⊢ 2 \in ℤ$
5		dvdsmul1	$⊢ (2 \in ℤ \land \deg (\sqrt) \in ℤ) \to 2 ∥ 2 \deg (\sqrt)$
6	4 5	mpan	$⊢ \deg (\sqrt) \in ℤ \to 2 ∥ 2 \deg (\sqrt)$
7	3 6	syl	$⊢ \sqrt \in Poly (ℂ) \to 2 ∥ 2 \deg (\sqrt)$
8		df-idp	$⊢ X^{p} = {I ↾}_{ℂ}$
9		idfn	$⊢ I Fn V$
10		ovex	$⊢ x^{2} \in V$
11	10	rgenw	$⊢ \forall x \in ℂ x^{2} \in V$
12		nfcv	$⊢ \underline{Ⅎ} x ℂ$
13	12	mptfnf	$⊢ \forall x \in ℂ x^{2} \in V \leftrightarrow (x \in ℂ ⟼ x^{2}) Fn ℂ$
14	11 13	mpbi	$⊢ (x \in ℂ ⟼ x^{2}) Fn ℂ$
15		sqrtf	$⊢ \sqrt : ℂ ⟶ ℂ$
16		fnfco	$⊢ ((x \in ℂ ⟼ x^{2}) Fn ℂ \land \sqrt : ℂ ⟶ ℂ) \to ((x \in ℂ ⟼ x^{2}) \circ \sqrt) Fn ℂ$
17	14 15 16	mp2an	$⊢ ((x \in ℂ ⟼ x^{2}) \circ \sqrt) Fn ℂ$
18	9 17	pm3.2i	$⊢ (I Fn V \land ((x \in ℂ ⟼ x^{2}) \circ \sqrt) Fn ℂ)$
19		ssv	$⊢ ℂ \subseteq V$
20		fvreseq1	$⊢ ((I Fn V \land ((x \in ℂ ⟼ x^{2}) \circ \sqrt) Fn ℂ) \land ℂ \subseteq V) \to ({I ↾}_{ℂ} = (x \in ℂ ⟼ x^{2}) \circ \sqrt \leftrightarrow \forall y \in ℂ I (y) = ((x \in ℂ ⟼ x^{2}) \circ \sqrt) (y))$
21	18 19 20	mp2an	$⊢ {I ↾}_{ℂ} = (x \in ℂ ⟼ x^{2}) \circ \sqrt \leftrightarrow \forall y \in ℂ I (y) = ((x \in ℂ ⟼ x^{2}) \circ \sqrt) (y)$
22		sqrtcl	$⊢ y \in ℂ \to \sqrt{y} \in ℂ$
23		oveq1	$⊢ x = \sqrt{y} \to x^{2} = {\sqrt{y}}^{2}$
24		eqid	$⊢ (x \in ℂ ⟼ x^{2}) = (x \in ℂ ⟼ x^{2})$
25		ovex	$⊢ {\sqrt{y}}^{2} \in V$
26	23 24 25	fvmpt	$⊢ \sqrt{y} \in ℂ \to (x \in ℂ ⟼ x^{2}) (\sqrt{y}) = {\sqrt{y}}^{2}$
27	22 26	syl	$⊢ y \in ℂ \to (x \in ℂ ⟼ x^{2}) (\sqrt{y}) = {\sqrt{y}}^{2}$
28		sqrtth	$⊢ y \in ℂ \to {\sqrt{y}}^{2} = y$
29	27 28	eqtr2d	$⊢ y \in ℂ \to y = (x \in ℂ ⟼ x^{2}) (\sqrt{y})$
30		fvi	$⊢ y \in ℂ \to I (y) = y$
31		fvco3	$⊢ (\sqrt : ℂ ⟶ ℂ \land y \in ℂ) \to ((x \in ℂ ⟼ x^{2}) \circ \sqrt) (y) = (x \in ℂ ⟼ x^{2}) (\sqrt{y})$
32	15 31	mpan	$⊢ y \in ℂ \to ((x \in ℂ ⟼ x^{2}) \circ \sqrt) (y) = (x \in ℂ ⟼ x^{2}) (\sqrt{y})$
33	29 30 32	3eqtr4d	$⊢ y \in ℂ \to I (y) = ((x \in ℂ ⟼ x^{2}) \circ \sqrt) (y)$
34	21 33	mprgbir	$⊢ {I ↾}_{ℂ} = (x \in ℂ ⟼ x^{2}) \circ \sqrt$
35	8 34	eqtr2i	$⊢ (x \in ℂ ⟼ x^{2}) \circ \sqrt = X^{p}$
36	35	a1i	$⊢ \sqrt \in Poly (ℂ) \to (x \in ℂ ⟼ x^{2}) \circ \sqrt = X^{p}$
37	36	fveq2d	$⊢ \sqrt \in Poly (ℂ) \to \deg ((x \in ℂ ⟼ x^{2}) \circ \sqrt) = \deg (X^{p})$
38		ax-1cn	$⊢ 1 \in ℂ$
39		ax-1ne0	$⊢ 1 \neq 0$
40		2nn0	$⊢ 2 \in ℕ_{0}$
41		sqcl	$⊢ x \in ℂ \to x^{2} \in ℂ$
42		mullid	$⊢ x^{2} \in ℂ \to 1 x^{2} = x^{2}$
43	42	eqcomd	$⊢ x^{2} \in ℂ \to x^{2} = 1 x^{2}$
44	41 43	syl	$⊢ x \in ℂ \to x^{2} = 1 x^{2}$
45	44	mpteq2ia	$⊢ (x \in ℂ ⟼ x^{2}) = (x \in ℂ ⟼ 1 x^{2})$
46	45	dgr1term	$⊢ (1 \in ℂ \land 1 \neq 0 \land 2 \in ℕ_{0}) \to \deg ((x \in ℂ ⟼ x^{2})) = 2$
47	38 39 40 46	mp3an	$⊢ \deg ((x \in ℂ ⟼ x^{2})) = 2$
48	47	eqcomi	$⊢ 2 = \deg ((x \in ℂ ⟼ x^{2}))$
49		eqid	$⊢ \deg (\sqrt) = \deg (\sqrt)$
50		ssid	$⊢ ℂ \subseteq ℂ$
51		plypow	$⊢ (ℂ \subseteq ℂ \land 1 \in ℂ \land 2 \in ℕ_{0}) \to (x \in ℂ ⟼ x^{2}) \in Poly (ℂ)$
52	50 38 40 51	mp3an	$⊢ (x \in ℂ ⟼ x^{2}) \in Poly (ℂ)$
53	52	a1i	$⊢ \sqrt \in Poly (ℂ) \to (x \in ℂ ⟼ x^{2}) \in Poly (ℂ)$
54		id	$⊢ \sqrt \in Poly (ℂ) \to \sqrt \in Poly (ℂ)$
55	48 49 53 54	dgrco	$⊢ \sqrt \in Poly (ℂ) \to \deg ((x \in ℂ ⟼ x^{2}) \circ \sqrt) = 2 \deg (\sqrt)$
56		dgrid	$⊢ \deg (X^{p}) = 1$
57	56	a1i	$⊢ \sqrt \in Poly (ℂ) \to \deg (X^{p}) = 1$
58	37 55 57	3eqtr3d	$⊢ \sqrt \in Poly (ℂ) \to 2 \deg (\sqrt) = 1$
59	7 58	breqtrd	$⊢ \sqrt \in Poly (ℂ) \to 2 ∥ 1$
60	1 59	mto	$⊢ \neg \sqrt \in Poly (ℂ)$

Metamath Proof Explorer

Theorem sqrtnpoly

Proof