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	20 22	eqtrd	$⊢ x \in ℂ \to ((ℂ \times \{1\}) +_{f} (X^{p} \times_{f} )) (x) = 1 + (X^{p} \times_{f} ) (x)$
24		fnfvof	$⊢ ((X^{p} Fn ℂ \land * Fn ℂ) \land (ℂ \in V \land x \in ℂ)) \to (X^{p} \times_{f} *) (x) = X^{p} (x) \overline{x}$
25	8 12 24	mpanl12	$⊢ (ℂ \in V \land x \in ℂ) \to (X^{p} \times_{f} *) (x) = X^{p} (x) \overline{x}$
26	1 25	mpan	$⊢ x \in ℂ \to (X^{p} \times_{f} *) (x) = X^{p} (x) \overline{x}$
27	6	fveq1i	$⊢ X^{p} (x) = ({I ↾}_{ℂ}) (x)$
28		fvres	$⊢ x \in ℂ \to ({I ↾}_{ℂ}) (x) = I (x)$
29	27 28	eqtrid	$⊢ x \in ℂ \to X^{p} (x) = I (x)$
30		fvi	$⊢ x \in ℂ \to I (x) = x$
31	29 30	eqtrd	$⊢ x \in ℂ \to X^{p} (x) = x$
32	31	oveq1d	$⊢ x \in ℂ \to X^{p} (x) \overline{x} = x \overline{x}$
33	26 32	eqtrd	$⊢ x \in ℂ \to (X^{p} \times_{f} *) (x) = x \overline{x}$
34	33	oveq2d	$⊢ x \in ℂ \to 1 + (X^{p} \times_{f} *) (x) = 1 + x \overline{x}$
35	23 34	eqtrd	$⊢ x \in ℂ \to ((ℂ \times \{1\}) +_{f} (X^{p} \times_{f} *)) (x) = 1 + x \overline{x}$
36		1red	$⊢ x \in ℂ \to 1 \in ℝ$
37		cjmulrcl	$⊢ x \in ℂ \to x \overline{x} \in ℝ$
38		0lt1	$⊢ 0 < 1$
39	38	a1i	$⊢ x \in ℂ \to 0 < 1$
40		cjmulge0	$⊢ x \in ℂ \to 0 \leq x \overline{x}$
41	36 37 39 40	addgtge0d	$⊢ x \in ℂ \to 0 < 1 + x \overline{x}$
42	41	gt0ne0d	$⊢ x \in ℂ \to 1 + x \overline{x} \neq 0$
43	35 42	eqnetrd	$⊢ x \in ℂ \to ((ℂ \times \{1\}) +_{f} (X^{p} \times_{f} *)) (x) \neq 0$
44	43	neneqd	$⊢ x \in ℂ \to \neg ((ℂ \times \{1\}) +_{f} (X^{p} \times_{f} *)) (x) = 0$
45	44	nrex	$⊢ \neg \exists x \in ℂ ((ℂ \times \{1\}) +_{f} (X^{p} \times_{f} *)) (x) = 0$
46		ssid	$⊢ ℂ \subseteq ℂ$
47		ax-1cn	$⊢ 1 \in ℂ$
48		plyconst	$⊢ (ℂ \subseteq ℂ \land 1 \in ℂ) \to ℂ \times \{1\} \in Poly (ℂ)$
49	46 47 48	mp2an	$⊢ ℂ \times \{1\} \in Poly (ℂ)$
50		plyid	$⊢ (ℂ \subseteq ℂ \land 1 \in ℂ) \to X^{p} \in Poly (ℂ)$
51	46 47 50	mp2an	$⊢ X^{p} \in Poly (ℂ)$
52		plymulcl	$⊢ (X^{p} \in Poly (ℂ) \land * \in Poly (ℂ)) \to X^{p} \times_{f} * \in Poly (ℂ)$
53	51 52	mpan	$⊢ * \in Poly (ℂ) \to X^{p} \times_{f} * \in Poly (ℂ)$
54		plyaddcl	$⊢ (ℂ \times \{1\} \in Poly (ℂ) \land X^{p} \times_{f} * \in Poly (ℂ)) \to (ℂ \times \{1\}) +_{f} (X^{p} \times_{f} *) \in Poly (ℂ)$
55	49 53 54	sylancr	$⊢ * \in Poly (ℂ) \to (ℂ \times \{1\}) +_{f} (X^{p} \times_{f} *) \in Poly (ℂ)$
56		dgrcl	$⊢ * \in Poly (ℂ) \to \deg (*) \in ℕ_{0}$
57		nn0p1nn	$⊢ \deg () \in ℕ_{0} \to \deg () + 1 \in ℕ$
58		nn0cn	$⊢ \deg () \in ℕ_{0} \to \deg () \in ℂ$
59		1cnd	$⊢ \deg (*) \in ℕ_{0} \to 1 \in ℂ$
60	58 59	addcomd	$⊢ \deg () \in ℕ_{0} \to \deg () + 1 = 1 + \deg (*)$
61	60	eleq1d	$⊢ \deg () \in ℕ_{0} \to (\deg () + 1 \in ℕ \leftrightarrow 1 + \deg (*) \in ℕ)$
62	57 61	mpbid	$⊢ \deg () \in ℕ_{0} \to 1 + \deg () \in ℕ$
63	56 62	syl	$⊢ * \in Poly (ℂ) \to 1 + \deg (*) \in ℕ$
64		1re	$⊢ 1 \in ℝ$
65		cjre	$⊢ 1 \in ℝ \to \overline{1} = 1$
66	64 65	ax-mp	$⊢ \overline{1} = 1$
67		ax-1ne0	$⊢ 1 \neq 0$
68	66 67	eqnetri	$⊢ \overline{1} \neq 0$
69		ne0p	$⊢ (1 \in ℂ \land \overline{1} \neq 0) \to * \neq 0_{𝑝}$
70	47 68 69	mp2an	$⊢ * \neq 0_{𝑝}$
71	6	fveq1i	$⊢ X^{p} (1) = ({I ↾}_{ℂ}) (1)$
72		fvres	$⊢ 1 \in ℂ \to ({I ↾}_{ℂ}) (1) = I (1)$
73	47 72	ax-mp	$⊢ ({I ↾}_{ℂ}) (1) = I (1)$
74	71 73	eqtri	$⊢ X^{p} (1) = I (1)$
75		fvi	$⊢ 1 \in V \to I (1) = 1$
76	2 75	ax-mp	$⊢ I (1) = 1$
77	74 76	eqtri	$⊢ X^{p} (1) = 1$
78	77 67	eqnetri	$⊢ X^{p} (1) \neq 0$
79		ne0p	$⊢ (1 \in ℂ \land X^{p} (1) \neq 0) \to X^{p} \neq 0_{𝑝}$
80	47 78 79	mp2an	$⊢ X^{p} \neq 0_{𝑝}$
81	51 80	pm3.2i	$⊢ (X^{p} \in Poly (ℂ) \land X^{p} \neq 0_{𝑝})$
82		dgrid	$⊢ \deg (X^{p}) = 1$
83	82	eqcomi	$⊢ 1 = \deg (X^{p})$
84		eqid	$⊢ \deg () = \deg ()$
85	83 84	dgrmul	$⊢ ((X^{p} \in Poly (ℂ) \land X^{p} \neq 0_{𝑝}) \land (* \in Poly (ℂ) \land * \neq 0_{𝑝})) \to \deg (X^{p} \times_{f} ) = 1 + \deg ()$
86	81 85	mpan	$⊢ (* \in Poly (ℂ) \land * \neq 0_{𝑝}) \to \deg (X^{p} \times_{f} ) = 1 + \deg ()$
87	70 86	mpan2	$⊢ * \in Poly (ℂ) \to \deg (X^{p} \times_{f} ) = 1 + \deg ()$
88	87	eleq1d	$⊢ * \in Poly (ℂ) \to (\deg (X^{p} \times_{f} ) \in ℕ \leftrightarrow 1 + \deg () \in ℕ)$
89	63 88	mpbird	$⊢ * \in Poly (ℂ) \to \deg (X^{p} \times_{f} *) \in ℕ$
90	49	a1i	$⊢ * \in Poly (ℂ) \to ℂ \times \{1\} \in Poly (ℂ)$
91	89	nngt0d	$⊢ * \in Poly (ℂ) \to 0 < \deg (X^{p} \times_{f} *)$
92		0dgr	$⊢ 1 \in ℂ \to \deg (ℂ \times \{1\}) = 0$
93	47 92	ax-mp	$⊢ \deg (ℂ \times \{1\}) = 0$
94	93	eqcomi	$⊢ 0 = \deg (ℂ \times \{1\})$
95		eqid	$⊢ \deg (X^{p} \times_{f} ) = \deg (X^{p} \times_{f} )$
96	94 95	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} *)$
97	90 53 91 96	syl3anc	$⊢ * \in Poly (ℂ) \to \deg ((ℂ \times \{1\}) +_{f} (X^{p} \times_{f} )) = \deg (X^{p} \times_{f} )$
98	97	eleq1d	$⊢ * \in Poly (ℂ) \to (\deg ((ℂ \times \{1\}) +_{f} (X^{p} \times_{f} )) \in ℕ \leftrightarrow \deg (X^{p} \times_{f} ) \in ℕ)$
99	98	biimprd	$⊢ * \in Poly (ℂ) \to (\deg (X^{p} \times_{f} ) \in ℕ \to \deg ((ℂ \times \{1\}) +_{f} (X^{p} \times_{f} )) \in ℕ)$
100	89 99	mpd	$⊢ * \in Poly (ℂ) \to \deg ((ℂ \times \{1\}) +_{f} (X^{p} \times_{f} *)) \in ℕ$
101		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$
102	55 100 101	syl2anc	$⊢ * \in Poly (ℂ) \to \exists x \in ℂ ((ℂ \times \{1\}) +_{f} (X^{p} \times_{f} *)) (x) = 0$
103	45 102	mto	$⊢ \neg * \in Poly (ℂ)$

Metamath Proof Explorer

Theorem cjnpoly

Proof