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

Proof

Step	Hyp	Ref	Expression
1		cnex	$⊢ ℂ \in V$
2		1ex	$⊢ 1 \in V$
3		fconstmpt	$⊢ ℂ \times \{1\} = (x \in ℂ ⟼ 1)$
4	2 3	fnmpti	$⊢ (ℂ \times \{1\}) Fn ℂ$
5		fnresi	$⊢ ({I ↾}_{ℂ}) Fn ℂ$
6		df-idp	$⊢ X^{p} = {I ↾}_{ℂ}$
7	6	fneq1i	$⊢ X^{p} Fn ℂ \leftrightarrow ({I ↾}_{ℂ}) Fn ℂ$
8	5 7	mpbir	$⊢ X^{p} Fn ℂ$
9	8	a1i	$⊢ ⊤ \to X^{p} Fn ℂ$
10		cjf	$⊢ * : ℂ ⟶ ℂ$
11		ffn	$⊢ * : ℂ ⟶ ℂ \to * Fn ℂ$
12	10 11	ax-mp	$⊢ * Fn ℂ$
13	12	a1i	$⊢ ⊤ \to * Fn ℂ$
14	1	a1i	$⊢ ⊤ \to ℂ \in V$
15		inidm	$⊢ ℂ \cap ℂ = ℂ$
16	9 13 14 14 15	offn	$⊢ ⊤ \to (X^{p} \times_{f} *) Fn ℂ$
17	16	mptru	$⊢ (X^{p} \times_{f} *) Fn ℂ$
18		fnfvof	$⊢ (((ℂ \times \{1\}) Fn ℂ \land (X^{p} \times_{f} ) Fn ℂ) \land (ℂ \in V \land x \in ℂ)) \to ((ℂ \times \{1\}) +_{f} (X^{p} \times_{f} )) (x) = (ℂ \times \{1\}) (x) + (X^{p} \times_{f} *) (x)$
19	4 17 18	mpanl12	$⊢ (ℂ \in V \land x \in ℂ) \to ((ℂ \times \{1\}) +_{f} (X^{p} \times_{f} )) (x) = (ℂ \times \{1\}) (x) + (X^{p} \times_{f} ) (x)$
20	1 19	mpan	$⊢ x \in ℂ \to ((ℂ \times \{1\}) +_{f} (X^{p} \times_{f} )) (x) = (ℂ \times \{1\}) (x) + (X^{p} \times_{f} ) (x)$
21	2	fvconst2	$⊢ x \in ℂ \to (ℂ \times \{1\}) (x) = 1$
22	21	oveq1d	$⊢ x \in ℂ \to (ℂ \times \{1\}) (x) + (X^{p} \times_{f} ) (x) = 1 + (X^{p} \times_{f} ) (x)$
23		fnfvof	$⊢ ((X^{p} Fn ℂ \land * Fn ℂ) \land (ℂ \in V \land x \in ℂ)) \to (X^{p} \times_{f} *) (x) = X^{p} (x) \overline{x}$
24	8 12 23	mpanl12	$⊢ (ℂ \in V \land x \in ℂ) \to (X^{p} \times_{f} *) (x) = X^{p} (x) \overline{x}$
25	1 24	mpan	$⊢ x \in ℂ \to (X^{p} \times_{f} *) (x) = X^{p} (x) \overline{x}$
26	6	fveq1i	$⊢ X^{p} (x) = ({I ↾}_{ℂ}) (x)$
27		fvres	$⊢ x \in ℂ \to ({I ↾}_{ℂ}) (x) = I (x)$
28	26 27	eqtrid	$⊢ x \in ℂ \to X^{p} (x) = I (x)$
29		fvi	$⊢ x \in ℂ \to I (x) = x$
30	28 29	eqtrd	$⊢ x \in ℂ \to X^{p} (x) = x$
31	30	oveq1d	$⊢ x \in ℂ \to X^{p} (x) \overline{x} = x \overline{x}$
32	25 31	eqtrd	$⊢ x \in ℂ \to (X^{p} \times_{f} *) (x) = x \overline{x}$
33	32	oveq2d	$⊢ x \in ℂ \to 1 + (X^{p} \times_{f} *) (x) = 1 + x \overline{x}$
34	20 22 33	3eqtrd	$⊢ x \in ℂ \to ((ℂ \times \{1\}) +_{f} (X^{p} \times_{f} *)) (x) = 1 + x \overline{x}$
35		1red	$⊢ x \in ℂ \to 1 \in ℝ$
36		cjmulrcl	$⊢ x \in ℂ \to x \overline{x} \in ℝ$
37		0lt1	$⊢ 0 < 1$
38	37	a1i	$⊢ x \in ℂ \to 0 < 1$
39		cjmulge0	$⊢ x \in ℂ \to 0 \leq x \overline{x}$
40	35 36 38 39	addgtge0d	$⊢ x \in ℂ \to 0 < 1 + x \overline{x}$
41	40	gt0ne0d	$⊢ x \in ℂ \to 1 + x \overline{x} \neq 0$
42	34 41	eqnetrd	$⊢ x \in ℂ \to ((ℂ \times \{1\}) +_{f} (X^{p} \times_{f} *)) (x) \neq 0$
43	42	neneqd	$⊢ x \in ℂ \to \neg ((ℂ \times \{1\}) +_{f} (X^{p} \times_{f} *)) (x) = 0$
44	43	nrex	$⊢ \neg \exists x \in ℂ ((ℂ \times \{1\}) +_{f} (X^{p} \times_{f} *)) (x) = 0$
45		ssid	$⊢ ℂ \subseteq ℂ$
46		ax-1cn	$⊢ 1 \in ℂ$
47		plyconst	$⊢ (ℂ \subseteq ℂ \land 1 \in ℂ) \to ℂ \times \{1\} \in Poly (ℂ)$
48	45 46 47	mp2an	$⊢ ℂ \times \{1\} \in Poly (ℂ)$
49		plyid	$⊢ (ℂ \subseteq ℂ \land 1 \in ℂ) \to X^{p} \in Poly (ℂ)$
50	45 46 49	mp2an	$⊢ X^{p} \in Poly (ℂ)$
51		plymulcl	$⊢ (X^{p} \in Poly (ℂ) \land * \in Poly (ℂ)) \to X^{p} \times_{f} * \in Poly (ℂ)$
52	50 51	mpan	$⊢ * \in Poly (ℂ) \to X^{p} \times_{f} * \in Poly (ℂ)$
53		plyaddcl	$⊢ (ℂ \times \{1\} \in Poly (ℂ) \land X^{p} \times_{f} * \in Poly (ℂ)) \to (ℂ \times \{1\}) +_{f} (X^{p} \times_{f} *) \in Poly (ℂ)$
54	48 52 53	sylancr	$⊢ * \in Poly (ℂ) \to (ℂ \times \{1\}) +_{f} (X^{p} \times_{f} *) \in Poly (ℂ)$
55		1re	$⊢ 1 \in ℝ$
56		cjre	$⊢ 1 \in ℝ \to \overline{1} = 1$
57	55 56	ax-mp	$⊢ \overline{1} = 1$
58		ax-1ne0	$⊢ 1 \neq 0$
59	57 58	eqnetri	$⊢ \overline{1} \neq 0$
60		ne0p	$⊢ (1 \in ℂ \land \overline{1} \neq 0) \to * \neq 0_{𝑝}$
61	46 59 60	mp2an	$⊢ * \neq 0_{𝑝}$
62	6	fveq1i	$⊢ X^{p} (1) = ({I ↾}_{ℂ}) (1)$
63		fvres	$⊢ 1 \in ℂ \to ({I ↾}_{ℂ}) (1) = I (1)$
64	46 63	ax-mp	$⊢ ({I ↾}_{ℂ}) (1) = I (1)$
65		fvi	$⊢ 1 \in V \to I (1) = 1$
66	2 65	ax-mp	$⊢ I (1) = 1$
67	62 64 66	3eqtri	$⊢ X^{p} (1) = 1$
68	67 58	eqnetri	$⊢ X^{p} (1) \neq 0$
69		ne0p	$⊢ (1 \in ℂ \land X^{p} (1) \neq 0) \to X^{p} \neq 0_{𝑝}$
70	46 68 69	mp2an	$⊢ X^{p} \neq 0_{𝑝}$
71		dgrid	$⊢ \deg (X^{p}) = 1$
72	71	eqcomi	$⊢ 1 = \deg (X^{p})$
73		eqid	$⊢ \deg () = \deg ()$
74	72 73	dgrmul	$⊢ ((X^{p} \in Poly (ℂ) \land X^{p} \neq 0_{𝑝}) \land (* \in Poly (ℂ) \land * \neq 0_{𝑝})) \to \deg (X^{p} \times_{f} ) = 1 + \deg ()$
75	50 70 74	mpanl12	$⊢ (* \in Poly (ℂ) \land * \neq 0_{𝑝}) \to \deg (X^{p} \times_{f} ) = 1 + \deg ()$
76	61 75	mpan2	$⊢ * \in Poly (ℂ) \to \deg (X^{p} \times_{f} ) = 1 + \deg ()$
77		dgrcl	$⊢ * \in Poly (ℂ) \to \deg (*) \in ℕ_{0}$
78		nn0cn	$⊢ \deg () \in ℕ_{0} \to \deg () \in ℂ$
79		1cnd	$⊢ \deg (*) \in ℕ_{0} \to 1 \in ℂ$
80	78 79	addcomd	$⊢ \deg () \in ℕ_{0} \to \deg () + 1 = 1 + \deg (*)$
81		nn0p1nn	$⊢ \deg () \in ℕ_{0} \to \deg () + 1 \in ℕ$
82	80 81	eqeltrrd	$⊢ \deg () \in ℕ_{0} \to 1 + \deg () \in ℕ$
83	77 82	syl	$⊢ * \in Poly (ℂ) \to 1 + \deg (*) \in ℕ$
84	76 83	eqeltrd	$⊢ * \in Poly (ℂ) \to \deg (X^{p} \times_{f} *) \in ℕ$
85	84	nngt0d	$⊢ * \in Poly (ℂ) \to 0 < \deg (X^{p} \times_{f} *)$
86		0dgr	$⊢ 1 \in ℂ \to \deg (ℂ \times \{1\}) = 0$
87	46 86	ax-mp	$⊢ \deg (ℂ \times \{1\}) = 0$
88	87	eqcomi	$⊢ 0 = \deg (ℂ \times \{1\})$
89		eqid	$⊢ \deg (X^{p} \times_{f} ) = \deg (X^{p} \times_{f} )$
90	88 89	dgradd2	$⊢ (ℂ \times \{1\} \in Poly (ℂ) \land X^{p} \times_{f} * \in Poly (ℂ) \land 0 < \deg (X^{p} \times_{f} )) \to \deg ((ℂ \times \{1\}) +_{f} (X^{p} \times_{f} )) = \deg (X^{p} \times_{f} *)$
91	48 52 85 90	mp3an2i	$⊢ * \in Poly (ℂ) \to \deg ((ℂ \times \{1\}) +_{f} (X^{p} \times_{f} )) = \deg (X^{p} \times_{f} )$
92	91 84	eqeltrd	$⊢ * \in Poly (ℂ) \to \deg ((ℂ \times \{1\}) +_{f} (X^{p} \times_{f} *)) \in ℕ$
93		fta	$⊢ ((ℂ \times \{1\}) +_{f} (X^{p} \times_{f} ) \in Poly (ℂ) \land \deg ((ℂ \times \{1\}) +_{f} (X^{p} \times_{f} )) \in ℕ) \to \exists x \in ℂ ((ℂ \times \{1\}) +_{f} (X^{p} \times_{f} *)) (x) = 0$
94	54 92 93	syl2anc	$⊢ * \in Poly (ℂ) \to \exists x \in ℂ ((ℂ \times \{1\}) +_{f} (X^{p} \times_{f} *)) (x) = 0$
95	44 94	mto	$⊢ \neg * \in Poly (ℂ)$

Metamath Proof Explorer

Theorem cjnpoly

Proof