Theorem 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	⊢ ¬ ∗ ∈ ( Poly ‘ ℂ )

Proof

Step	Hyp	Ref	Expression
1		cnex	⊢ ℂ ∈ V
2		1ex	⊢ 1 ∈ V
3		fconstmpt	⊢ ( ℂ × { 1 } ) = ( 𝑥 ∈ ℂ ↦ 1 )
4	2 3	fnmpti	⊢ ( ℂ × { 1 } ) Fn ℂ
5		fnresi	⊢ ( I ↾ ℂ ) Fn ℂ
6		df-idp	⊢ Xp = ( I ↾ ℂ )
7	6	fneq1i	⊢ ( Xp Fn ℂ ↔ ( I ↾ ℂ ) Fn ℂ )
8	5 7	mpbir	⊢ Xp Fn ℂ
9	8	a1i	⊢ ( ⊤ → Xp Fn ℂ )
10		cjf	⊢ ∗ : ℂ ⟶ ℂ
11		ffn	⊢ ( ∗ : ℂ ⟶ ℂ → ∗ Fn ℂ )
12	10 11	ax-mp	⊢ ∗ Fn ℂ
13	12	a1i	⊢ ( ⊤ → ∗ Fn ℂ )
14	1	a1i	⊢ ( ⊤ → ℂ ∈ V )
15		inidm	⊢ ( ℂ ∩ ℂ ) = ℂ
16	9 13 14 14 15	offn	⊢ ( ⊤ → ( Xp ∘f · ∗ ) Fn ℂ )
17	16	mptru	⊢ ( Xp ∘f · ∗ ) Fn ℂ
18		fnfvof	⊢ ( ( ( ( ℂ × { 1 } ) Fn ℂ ∧ ( Xp ∘f · ∗ ) Fn ℂ ) ∧ ( ℂ ∈ V ∧ 𝑥 ∈ ℂ ) ) → ( ( ( ℂ × { 1 } ) ∘f + ( Xp ∘f · ∗ ) ) ‘ 𝑥 ) = ( ( ( ℂ × { 1 } ) ‘ 𝑥 ) + ( ( Xp ∘f · ∗ ) ‘ 𝑥 ) ) )
19	4 17 18	mpanl12	⊢ ( ( ℂ ∈ V ∧ 𝑥 ∈ ℂ ) → ( ( ( ℂ × { 1 } ) ∘f + ( Xp ∘f · ∗ ) ) ‘ 𝑥 ) = ( ( ( ℂ × { 1 } ) ‘ 𝑥 ) + ( ( Xp ∘f · ∗ ) ‘ 𝑥 ) ) )
20	1 19	mpan	⊢ ( 𝑥 ∈ ℂ → ( ( ( ℂ × { 1 } ) ∘f + ( Xp ∘f · ∗ ) ) ‘ 𝑥 ) = ( ( ( ℂ × { 1 } ) ‘ 𝑥 ) + ( ( Xp ∘f · ∗ ) ‘ 𝑥 ) ) )
21	2	fvconst2	⊢ ( 𝑥 ∈ ℂ → ( ( ℂ × { 1 } ) ‘ 𝑥 ) = 1 )
22	21	oveq1d	⊢ ( 𝑥 ∈ ℂ → ( ( ( ℂ × { 1 } ) ‘ 𝑥 ) + ( ( Xp ∘f · ∗ ) ‘ 𝑥 ) ) = ( 1 + ( ( Xp ∘f · ∗ ) ‘ 𝑥 ) ) )
23	20 22	eqtrd	⊢ ( 𝑥 ∈ ℂ → ( ( ( ℂ × { 1 } ) ∘f + ( Xp ∘f · ∗ ) ) ‘ 𝑥 ) = ( 1 + ( ( Xp ∘f · ∗ ) ‘ 𝑥 ) ) )
24		fnfvof	⊢ ( ( ( Xp Fn ℂ ∧ ∗ Fn ℂ ) ∧ ( ℂ ∈ V ∧ 𝑥 ∈ ℂ ) ) → ( ( Xp ∘f · ∗ ) ‘ 𝑥 ) = ( ( Xp ‘ 𝑥 ) · ( ∗ ‘ 𝑥 ) ) )
25	8 12 24	mpanl12	⊢ ( ( ℂ ∈ V ∧ 𝑥 ∈ ℂ ) → ( ( Xp ∘f · ∗ ) ‘ 𝑥 ) = ( ( Xp ‘ 𝑥 ) · ( ∗ ‘ 𝑥 ) ) )
26	1 25	mpan	⊢ ( 𝑥 ∈ ℂ → ( ( Xp ∘f · ∗ ) ‘ 𝑥 ) = ( ( Xp ‘ 𝑥 ) · ( ∗ ‘ 𝑥 ) ) )
27	6	fveq1i	⊢ ( Xp ‘ 𝑥 ) = ( ( I ↾ ℂ ) ‘ 𝑥 )
28		fvres	⊢ ( 𝑥 ∈ ℂ → ( ( I ↾ ℂ ) ‘ 𝑥 ) = ( I ‘ 𝑥 ) )
29	27 28	eqtrid	⊢ ( 𝑥 ∈ ℂ → ( Xp ‘ 𝑥 ) = ( I ‘ 𝑥 ) )
30		fvi	⊢ ( 𝑥 ∈ ℂ → ( I ‘ 𝑥 ) = 𝑥 )
31	29 30	eqtrd	⊢ ( 𝑥 ∈ ℂ → ( Xp ‘ 𝑥 ) = 𝑥 )
32	31	oveq1d	⊢ ( 𝑥 ∈ ℂ → ( ( Xp ‘ 𝑥 ) · ( ∗ ‘ 𝑥 ) ) = ( 𝑥 · ( ∗ ‘ 𝑥 ) ) )
33	26 32	eqtrd	⊢ ( 𝑥 ∈ ℂ → ( ( Xp ∘f · ∗ ) ‘ 𝑥 ) = ( 𝑥 · ( ∗ ‘ 𝑥 ) ) )
34	33	oveq2d	⊢ ( 𝑥 ∈ ℂ → ( 1 + ( ( Xp ∘f · ∗ ) ‘ 𝑥 ) ) = ( 1 + ( 𝑥 · ( ∗ ‘ 𝑥 ) ) ) )
35	23 34	eqtrd	⊢ ( 𝑥 ∈ ℂ → ( ( ( ℂ × { 1 } ) ∘f + ( Xp ∘f · ∗ ) ) ‘ 𝑥 ) = ( 1 + ( 𝑥 · ( ∗ ‘ 𝑥 ) ) ) )
36		1red	⊢ ( 𝑥 ∈ ℂ → 1 ∈ ℝ )
37		cjmulrcl	⊢ ( 𝑥 ∈ ℂ → ( 𝑥 · ( ∗ ‘ 𝑥 ) ) ∈ ℝ )
38		0lt1	⊢ 0 < 1
39	38	a1i	⊢ ( 𝑥 ∈ ℂ → 0 < 1 )
40		cjmulge0	⊢ ( 𝑥 ∈ ℂ → 0 ≤ ( 𝑥 · ( ∗ ‘ 𝑥 ) ) )
41	36 37 39 40	addgtge0d	⊢ ( 𝑥 ∈ ℂ → 0 < ( 1 + ( 𝑥 · ( ∗ ‘ 𝑥 ) ) ) )
42	41	gt0ne0d	⊢ ( 𝑥 ∈ ℂ → ( 1 + ( 𝑥 · ( ∗ ‘ 𝑥 ) ) ) ≠ 0 )
43	35 42	eqnetrd	⊢ ( 𝑥 ∈ ℂ → ( ( ( ℂ × { 1 } ) ∘f + ( Xp ∘f · ∗ ) ) ‘ 𝑥 ) ≠ 0 )
44	43	neneqd	⊢ ( 𝑥 ∈ ℂ → ¬ ( ( ( ℂ × { 1 } ) ∘f + ( Xp ∘f · ∗ ) ) ‘ 𝑥 ) = 0 )
45	44	nrex	⊢ ¬ ∃ 𝑥 ∈ ℂ ( ( ( ℂ × { 1 } ) ∘f + ( Xp ∘f · ∗ ) ) ‘ 𝑥 ) = 0
46		ssid	⊢ ℂ ⊆ ℂ
47		ax-1cn	⊢ 1 ∈ ℂ
48		plyconst	⊢ ( ( ℂ ⊆ ℂ ∧ 1 ∈ ℂ ) → ( ℂ × { 1 } ) ∈ ( Poly ‘ ℂ ) )
49	46 47 48	mp2an	⊢ ( ℂ × { 1 } ) ∈ ( Poly ‘ ℂ )
50		plyid	⊢ ( ( ℂ ⊆ ℂ ∧ 1 ∈ ℂ ) → Xp ∈ ( Poly ‘ ℂ ) )
51	46 47 50	mp2an	⊢ Xp ∈ ( Poly ‘ ℂ )
52		plymulcl	⊢ ( ( Xp ∈ ( Poly ‘ ℂ ) ∧ ∗ ∈ ( Poly ‘ ℂ ) ) → ( Xp ∘f · ∗ ) ∈ ( Poly ‘ ℂ ) )
53	51 52	mpan	⊢ ( ∗ ∈ ( Poly ‘ ℂ ) → ( Xp ∘f · ∗ ) ∈ ( Poly ‘ ℂ ) )
54		plyaddcl	⊢ ( ( ( ℂ × { 1 } ) ∈ ( Poly ‘ ℂ ) ∧ ( Xp ∘f · ∗ ) ∈ ( Poly ‘ ℂ ) ) → ( ( ℂ × { 1 } ) ∘f + ( Xp ∘f · ∗ ) ) ∈ ( Poly ‘ ℂ ) )
55	49 53 54	sylancr	⊢ ( ∗ ∈ ( Poly ‘ ℂ ) → ( ( ℂ × { 1 } ) ∘f + ( Xp ∘f · ∗ ) ) ∈ ( Poly ‘ ℂ ) )
56		dgrcl	⊢ ( ∗ ∈ ( Poly ‘ ℂ ) → ( deg ‘ ∗ ) ∈ ℕ0 )
57		nn0p1nn	⊢ ( ( deg ‘ ∗ ) ∈ ℕ0 → ( ( deg ‘ ∗ ) + 1 ) ∈ ℕ )
58		nn0cn	⊢ ( ( deg ‘ ∗ ) ∈ ℕ0 → ( deg ‘ ∗ ) ∈ ℂ )
59		1cnd	⊢ ( ( deg ‘ ∗ ) ∈ ℕ0 → 1 ∈ ℂ )
60	58 59	addcomd	⊢ ( ( deg ‘ ∗ ) ∈ ℕ0 → ( ( deg ‘ ∗ ) + 1 ) = ( 1 + ( deg ‘ ∗ ) ) )
61	60	eleq1d	⊢ ( ( deg ‘ ∗ ) ∈ ℕ0 → ( ( ( deg ‘ ∗ ) + 1 ) ∈ ℕ ↔ ( 1 + ( deg ‘ ∗ ) ) ∈ ℕ ) )
62	57 61	mpbid	⊢ ( ( deg ‘ ∗ ) ∈ ℕ0 → ( 1 + ( deg ‘ ∗ ) ) ∈ ℕ )
63	56 62	syl	⊢ ( ∗ ∈ ( Poly ‘ ℂ ) → ( 1 + ( deg ‘ ∗ ) ) ∈ ℕ )
64		1re	⊢ 1 ∈ ℝ
65		cjre	⊢ ( 1 ∈ ℝ → ( ∗ ‘ 1 ) = 1 )
66	64 65	ax-mp	⊢ ( ∗ ‘ 1 ) = 1
67		ax-1ne0	⊢ 1 ≠ 0
68	66 67	eqnetri	⊢ ( ∗ ‘ 1 ) ≠ 0
69		ne0p	⊢ ( ( 1 ∈ ℂ ∧ ( ∗ ‘ 1 ) ≠ 0 ) → ∗ ≠ 0𝑝 )
70	47 68 69	mp2an	⊢ ∗ ≠ 0𝑝
71	6	fveq1i	⊢ ( Xp ‘ 1 ) = ( ( I ↾ ℂ ) ‘ 1 )
72		fvres	⊢ ( 1 ∈ ℂ → ( ( I ↾ ℂ ) ‘ 1 ) = ( I ‘ 1 ) )
73	47 72	ax-mp	⊢ ( ( I ↾ ℂ ) ‘ 1 ) = ( I ‘ 1 )
74	71 73	eqtri	⊢ ( Xp ‘ 1 ) = ( I ‘ 1 )
75		fvi	⊢ ( 1 ∈ V → ( I ‘ 1 ) = 1 )
76	2 75	ax-mp	⊢ ( I ‘ 1 ) = 1
77	74 76	eqtri	⊢ ( Xp ‘ 1 ) = 1
78	77 67	eqnetri	⊢ ( Xp ‘ 1 ) ≠ 0
79		ne0p	⊢ ( ( 1 ∈ ℂ ∧ ( Xp ‘ 1 ) ≠ 0 ) → Xp ≠ 0𝑝 )
80	47 78 79	mp2an	⊢ Xp ≠ 0𝑝
81	51 80	pm3.2i	⊢ ( Xp ∈ ( Poly ‘ ℂ ) ∧ Xp ≠ 0𝑝 )
82		dgrid	⊢ ( deg ‘ Xp ) = 1
83	82	eqcomi	⊢ 1 = ( deg ‘ Xp )
84		eqid	⊢ ( deg ‘ ∗ ) = ( deg ‘ ∗ )
85	83 84	dgrmul	⊢ ( ( ( Xp ∈ ( Poly ‘ ℂ ) ∧ Xp ≠ 0𝑝 ) ∧ ( ∗ ∈ ( Poly ‘ ℂ ) ∧ ∗ ≠ 0𝑝 ) ) → ( deg ‘ ( Xp ∘f · ∗ ) ) = ( 1 + ( deg ‘ ∗ ) ) )
86	81 85	mpan	⊢ ( ( ∗ ∈ ( Poly ‘ ℂ ) ∧ ∗ ≠ 0𝑝 ) → ( deg ‘ ( Xp ∘f · ∗ ) ) = ( 1 + ( deg ‘ ∗ ) ) )
87	70 86	mpan2	⊢ ( ∗ ∈ ( Poly ‘ ℂ ) → ( deg ‘ ( Xp ∘f · ∗ ) ) = ( 1 + ( deg ‘ ∗ ) ) )
88	87	eleq1d	⊢ ( ∗ ∈ ( Poly ‘ ℂ ) → ( ( deg ‘ ( Xp ∘f · ∗ ) ) ∈ ℕ ↔ ( 1 + ( deg ‘ ∗ ) ) ∈ ℕ ) )
89	63 88	mpbird	⊢ ( ∗ ∈ ( Poly ‘ ℂ ) → ( deg ‘ ( Xp ∘f · ∗ ) ) ∈ ℕ )
90	49	a1i	⊢ ( ∗ ∈ ( Poly ‘ ℂ ) → ( ℂ × { 1 } ) ∈ ( Poly ‘ ℂ ) )
91	89	nngt0d	⊢ ( ∗ ∈ ( Poly ‘ ℂ ) → 0 < ( deg ‘ ( Xp ∘f · ∗ ) ) )
92		0dgr	⊢ ( 1 ∈ ℂ → ( deg ‘ ( ℂ × { 1 } ) ) = 0 )
93	47 92	ax-mp	⊢ ( deg ‘ ( ℂ × { 1 } ) ) = 0
94	93	eqcomi	⊢ 0 = ( deg ‘ ( ℂ × { 1 } ) )
95		eqid	⊢ ( deg ‘ ( Xp ∘f · ∗ ) ) = ( deg ‘ ( Xp ∘f · ∗ ) )
96	94 95	dgradd2	⊢ ( ( ( ℂ × { 1 } ) ∈ ( Poly ‘ ℂ ) ∧ ( Xp ∘f · ∗ ) ∈ ( Poly ‘ ℂ ) ∧ 0 < ( deg ‘ ( Xp ∘f · ∗ ) ) ) → ( deg ‘ ( ( ℂ × { 1 } ) ∘f + ( Xp ∘f · ∗ ) ) ) = ( deg ‘ ( Xp ∘f · ∗ ) ) )
97	90 53 91 96	syl3anc	⊢ ( ∗ ∈ ( Poly ‘ ℂ ) → ( deg ‘ ( ( ℂ × { 1 } ) ∘f + ( Xp ∘f · ∗ ) ) ) = ( deg ‘ ( Xp ∘f · ∗ ) ) )
98	97	eleq1d	⊢ ( ∗ ∈ ( Poly ‘ ℂ ) → ( ( deg ‘ ( ( ℂ × { 1 } ) ∘f + ( Xp ∘f · ∗ ) ) ) ∈ ℕ ↔ ( deg ‘ ( Xp ∘f · ∗ ) ) ∈ ℕ ) )
99	98	biimprd	⊢ ( ∗ ∈ ( Poly ‘ ℂ ) → ( ( deg ‘ ( Xp ∘f · ∗ ) ) ∈ ℕ → ( deg ‘ ( ( ℂ × { 1 } ) ∘f + ( Xp ∘f · ∗ ) ) ) ∈ ℕ ) )
100	89 99	mpd	⊢ ( ∗ ∈ ( Poly ‘ ℂ ) → ( deg ‘ ( ( ℂ × { 1 } ) ∘f + ( Xp ∘f · ∗ ) ) ) ∈ ℕ )
101		fta	⊢ ( ( ( ( ℂ × { 1 } ) ∘f + ( Xp ∘f · ∗ ) ) ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ ( ( ℂ × { 1 } ) ∘f + ( Xp ∘f · ∗ ) ) ) ∈ ℕ ) → ∃ 𝑥 ∈ ℂ ( ( ( ℂ × { 1 } ) ∘f + ( Xp ∘f · ∗ ) ) ‘ 𝑥 ) = 0 )
102	55 100 101	syl2anc	⊢ ( ∗ ∈ ( Poly ‘ ℂ ) → ∃ 𝑥 ∈ ℂ ( ( ( ℂ × { 1 } ) ∘f + ( Xp ∘f · ∗ ) ) ‘ 𝑥 ) = 0 )
103	45 102	mto	⊢ ¬ ∗ ∈ ( Poly ‘ ℂ )