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		fnfvof	⊢ ( ( ( Xp Fn ℂ ∧ ∗ Fn ℂ ) ∧ ( ℂ ∈ V ∧ 𝑥 ∈ ℂ ) ) → ( ( Xp ∘f · ∗ ) ‘ 𝑥 ) = ( ( Xp ‘ 𝑥 ) · ( ∗ ‘ 𝑥 ) ) )
24	8 12 23	mpanl12	⊢ ( ( ℂ ∈ V ∧ 𝑥 ∈ ℂ ) → ( ( Xp ∘f · ∗ ) ‘ 𝑥 ) = ( ( Xp ‘ 𝑥 ) · ( ∗ ‘ 𝑥 ) ) )
25	1 24	mpan	⊢ ( 𝑥 ∈ ℂ → ( ( Xp ∘f · ∗ ) ‘ 𝑥 ) = ( ( Xp ‘ 𝑥 ) · ( ∗ ‘ 𝑥 ) ) )
26	6	fveq1i	⊢ ( Xp ‘ 𝑥 ) = ( ( I ↾ ℂ ) ‘ 𝑥 )
27		fvres	⊢ ( 𝑥 ∈ ℂ → ( ( I ↾ ℂ ) ‘ 𝑥 ) = ( I ‘ 𝑥 ) )
28	26 27	eqtrid	⊢ ( 𝑥 ∈ ℂ → ( Xp ‘ 𝑥 ) = ( I ‘ 𝑥 ) )
29		fvi	⊢ ( 𝑥 ∈ ℂ → ( I ‘ 𝑥 ) = 𝑥 )
30	28 29	eqtrd	⊢ ( 𝑥 ∈ ℂ → ( Xp ‘ 𝑥 ) = 𝑥 )
31	30	oveq1d	⊢ ( 𝑥 ∈ ℂ → ( ( Xp ‘ 𝑥 ) · ( ∗ ‘ 𝑥 ) ) = ( 𝑥 · ( ∗ ‘ 𝑥 ) ) )
32	25 31	eqtrd	⊢ ( 𝑥 ∈ ℂ → ( ( Xp ∘f · ∗ ) ‘ 𝑥 ) = ( 𝑥 · ( ∗ ‘ 𝑥 ) ) )
33	32	oveq2d	⊢ ( 𝑥 ∈ ℂ → ( 1 + ( ( Xp ∘f · ∗ ) ‘ 𝑥 ) ) = ( 1 + ( 𝑥 · ( ∗ ‘ 𝑥 ) ) ) )
34	20 22 33	3eqtrd	⊢ ( 𝑥 ∈ ℂ → ( ( ( ℂ × { 1 } ) ∘f + ( Xp ∘f · ∗ ) ) ‘ 𝑥 ) = ( 1 + ( 𝑥 · ( ∗ ‘ 𝑥 ) ) ) )
35		1red	⊢ ( 𝑥 ∈ ℂ → 1 ∈ ℝ )
36		cjmulrcl	⊢ ( 𝑥 ∈ ℂ → ( 𝑥 · ( ∗ ‘ 𝑥 ) ) ∈ ℝ )
37		0lt1	⊢ 0 < 1
38	37	a1i	⊢ ( 𝑥 ∈ ℂ → 0 < 1 )
39		cjmulge0	⊢ ( 𝑥 ∈ ℂ → 0 ≤ ( 𝑥 · ( ∗ ‘ 𝑥 ) ) )
40	35 36 38 39	addgtge0d	⊢ ( 𝑥 ∈ ℂ → 0 < ( 1 + ( 𝑥 · ( ∗ ‘ 𝑥 ) ) ) )
41	40	gt0ne0d	⊢ ( 𝑥 ∈ ℂ → ( 1 + ( 𝑥 · ( ∗ ‘ 𝑥 ) ) ) ≠ 0 )
42	34 41	eqnetrd	⊢ ( 𝑥 ∈ ℂ → ( ( ( ℂ × { 1 } ) ∘f + ( Xp ∘f · ∗ ) ) ‘ 𝑥 ) ≠ 0 )
43	42	neneqd	⊢ ( 𝑥 ∈ ℂ → ¬ ( ( ( ℂ × { 1 } ) ∘f + ( Xp ∘f · ∗ ) ) ‘ 𝑥 ) = 0 )
44	43	nrex	⊢ ¬ ∃ 𝑥 ∈ ℂ ( ( ( ℂ × { 1 } ) ∘f + ( Xp ∘f · ∗ ) ) ‘ 𝑥 ) = 0
45		ssid	⊢ ℂ ⊆ ℂ
46		ax-1cn	⊢ 1 ∈ ℂ
47		plyconst	⊢ ( ( ℂ ⊆ ℂ ∧ 1 ∈ ℂ ) → ( ℂ × { 1 } ) ∈ ( Poly ‘ ℂ ) )
48	45 46 47	mp2an	⊢ ( ℂ × { 1 } ) ∈ ( Poly ‘ ℂ )
49		plyid	⊢ ( ( ℂ ⊆ ℂ ∧ 1 ∈ ℂ ) → Xp ∈ ( Poly ‘ ℂ ) )
50	45 46 49	mp2an	⊢ Xp ∈ ( Poly ‘ ℂ )
51		plymulcl	⊢ ( ( Xp ∈ ( Poly ‘ ℂ ) ∧ ∗ ∈ ( Poly ‘ ℂ ) ) → ( Xp ∘f · ∗ ) ∈ ( Poly ‘ ℂ ) )
52	50 51	mpan	⊢ ( ∗ ∈ ( Poly ‘ ℂ ) → ( Xp ∘f · ∗ ) ∈ ( Poly ‘ ℂ ) )
53		plyaddcl	⊢ ( ( ( ℂ × { 1 } ) ∈ ( Poly ‘ ℂ ) ∧ ( Xp ∘f · ∗ ) ∈ ( Poly ‘ ℂ ) ) → ( ( ℂ × { 1 } ) ∘f + ( Xp ∘f · ∗ ) ) ∈ ( Poly ‘ ℂ ) )
54	48 52 53	sylancr	⊢ ( ∗ ∈ ( Poly ‘ ℂ ) → ( ( ℂ × { 1 } ) ∘f + ( Xp ∘f · ∗ ) ) ∈ ( Poly ‘ ℂ ) )
55		1re	⊢ 1 ∈ ℝ
56		cjre	⊢ ( 1 ∈ ℝ → ( ∗ ‘ 1 ) = 1 )
57	55 56	ax-mp	⊢ ( ∗ ‘ 1 ) = 1
58		ax-1ne0	⊢ 1 ≠ 0
59	57 58	eqnetri	⊢ ( ∗ ‘ 1 ) ≠ 0
60		ne0p	⊢ ( ( 1 ∈ ℂ ∧ ( ∗ ‘ 1 ) ≠ 0 ) → ∗ ≠ 0𝑝 )
61	46 59 60	mp2an	⊢ ∗ ≠ 0𝑝
62	6	fveq1i	⊢ ( Xp ‘ 1 ) = ( ( I ↾ ℂ ) ‘ 1 )
63		fvres	⊢ ( 1 ∈ ℂ → ( ( I ↾ ℂ ) ‘ 1 ) = ( I ‘ 1 ) )
64	46 63	ax-mp	⊢ ( ( I ↾ ℂ ) ‘ 1 ) = ( I ‘ 1 )
65		fvi	⊢ ( 1 ∈ V → ( I ‘ 1 ) = 1 )
66	2 65	ax-mp	⊢ ( I ‘ 1 ) = 1
67	62 64 66	3eqtri	⊢ ( Xp ‘ 1 ) = 1
68	67 58	eqnetri	⊢ ( Xp ‘ 1 ) ≠ 0
69		ne0p	⊢ ( ( 1 ∈ ℂ ∧ ( Xp ‘ 1 ) ≠ 0 ) → Xp ≠ 0𝑝 )
70	46 68 69	mp2an	⊢ Xp ≠ 0𝑝
71		dgrid	⊢ ( deg ‘ Xp ) = 1
72	71	eqcomi	⊢ 1 = ( deg ‘ Xp )
73		eqid	⊢ ( deg ‘ ∗ ) = ( deg ‘ ∗ )
74	72 73	dgrmul	⊢ ( ( ( Xp ∈ ( Poly ‘ ℂ ) ∧ Xp ≠ 0𝑝 ) ∧ ( ∗ ∈ ( Poly ‘ ℂ ) ∧ ∗ ≠ 0𝑝 ) ) → ( deg ‘ ( Xp ∘f · ∗ ) ) = ( 1 + ( deg ‘ ∗ ) ) )
75	50 70 74	mpanl12	⊢ ( ( ∗ ∈ ( Poly ‘ ℂ ) ∧ ∗ ≠ 0𝑝 ) → ( deg ‘ ( Xp ∘f · ∗ ) ) = ( 1 + ( deg ‘ ∗ ) ) )
76	61 75	mpan2	⊢ ( ∗ ∈ ( Poly ‘ ℂ ) → ( deg ‘ ( Xp ∘f · ∗ ) ) = ( 1 + ( deg ‘ ∗ ) ) )
77		dgrcl	⊢ ( ∗ ∈ ( Poly ‘ ℂ ) → ( deg ‘ ∗ ) ∈ ℕ0 )
78		nn0cn	⊢ ( ( deg ‘ ∗ ) ∈ ℕ0 → ( deg ‘ ∗ ) ∈ ℂ )
79		1cnd	⊢ ( ( deg ‘ ∗ ) ∈ ℕ0 → 1 ∈ ℂ )
80	78 79	addcomd	⊢ ( ( deg ‘ ∗ ) ∈ ℕ0 → ( ( deg ‘ ∗ ) + 1 ) = ( 1 + ( deg ‘ ∗ ) ) )
81		nn0p1nn	⊢ ( ( deg ‘ ∗ ) ∈ ℕ0 → ( ( deg ‘ ∗ ) + 1 ) ∈ ℕ )
82	80 81	eqeltrrd	⊢ ( ( deg ‘ ∗ ) ∈ ℕ0 → ( 1 + ( deg ‘ ∗ ) ) ∈ ℕ )
83	77 82	syl	⊢ ( ∗ ∈ ( Poly ‘ ℂ ) → ( 1 + ( deg ‘ ∗ ) ) ∈ ℕ )
84	76 83	eqeltrd	⊢ ( ∗ ∈ ( Poly ‘ ℂ ) → ( deg ‘ ( Xp ∘f · ∗ ) ) ∈ ℕ )
85	84	nngt0d	⊢ ( ∗ ∈ ( Poly ‘ ℂ ) → 0 < ( deg ‘ ( Xp ∘f · ∗ ) ) )
86		0dgr	⊢ ( 1 ∈ ℂ → ( deg ‘ ( ℂ × { 1 } ) ) = 0 )
87	46 86	ax-mp	⊢ ( deg ‘ ( ℂ × { 1 } ) ) = 0
88	87	eqcomi	⊢ 0 = ( deg ‘ ( ℂ × { 1 } ) )
89		eqid	⊢ ( deg ‘ ( Xp ∘f · ∗ ) ) = ( deg ‘ ( Xp ∘f · ∗ ) )
90	88 89	dgradd2	⊢ ( ( ( ℂ × { 1 } ) ∈ ( Poly ‘ ℂ ) ∧ ( Xp ∘f · ∗ ) ∈ ( Poly ‘ ℂ ) ∧ 0 < ( deg ‘ ( Xp ∘f · ∗ ) ) ) → ( deg ‘ ( ( ℂ × { 1 } ) ∘f + ( Xp ∘f · ∗ ) ) ) = ( deg ‘ ( Xp ∘f · ∗ ) ) )
91	48 52 85 90	mp3an2i	⊢ ( ∗ ∈ ( Poly ‘ ℂ ) → ( deg ‘ ( ( ℂ × { 1 } ) ∘f + ( Xp ∘f · ∗ ) ) ) = ( deg ‘ ( Xp ∘f · ∗ ) ) )
92	91 84	eqeltrd	⊢ ( ∗ ∈ ( Poly ‘ ℂ ) → ( deg ‘ ( ( ℂ × { 1 } ) ∘f + ( Xp ∘f · ∗ ) ) ) ∈ ℕ )
93		fta	⊢ ( ( ( ( ℂ × { 1 } ) ∘f + ( Xp ∘f · ∗ ) ) ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ ( ( ℂ × { 1 } ) ∘f + ( Xp ∘f · ∗ ) ) ) ∈ ℕ ) → ∃ 𝑥 ∈ ℂ ( ( ( ℂ × { 1 } ) ∘f + ( Xp ∘f · ∗ ) ) ‘ 𝑥 ) = 0 )
94	54 92 93	syl2anc	⊢ ( ∗ ∈ ( Poly ‘ ℂ ) → ∃ 𝑥 ∈ ℂ ( ( ( ℂ × { 1 } ) ∘f + ( Xp ∘f · ∗ ) ) ‘ 𝑥 ) = 0 )
95	44 94	mto	⊢ ¬ ∗ ∈ ( Poly ‘ ℂ )