Theorem trisecnconstr

Description: Not all angles can be trisected. (Contributed by Thierry Arnoux, 15-Nov-2025)

	Ref	Expression
Assertion	trisecnconstr	$$⊢\neg \forall o\in \mathrm{Constr}{o}^{\frac{1}{3}}\in \mathrm{Constr}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}={\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}$$
2		eqid	$$⊢{{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}}^{\frac{1}{3}}={{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}}^{\frac{1}{3}}$$
3	1 2	cos9thpinconstr	$$⊢\left({\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}\in \mathrm{Constr}\wedge {{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}}^{\frac{1}{3}}\notin \mathrm{Constr}\right)$$
4	3	simpri	$$⊢{{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}}^{\frac{1}{3}}\notin \mathrm{Constr}$$
5	4	neli	$$⊢\neg {{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}}^{\frac{1}{3}}\in \mathrm{Constr}$$
6	3	simpli	$$⊢{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}\in \mathrm{Constr}$$
7		oveq1	$$⊢o={\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}\to o^{\frac{1}{3}}={{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}}^{\frac{1}{3}}$$
8	7	eleq1d	$$⊢o={\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}\to \left(o^{\frac{1}{3}}\in \mathrm{Constr}\leftrightarrow {{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}}^{\frac{1}{3}}\in \mathrm{Constr}\right)$$
9	8	rspcv	$$⊢{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}\in \mathrm{Constr}\to \left(\forall o\in \mathrm{Constr}{o}^{\frac{1}{3}}\in \mathrm{Constr}\to {{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}}^{\frac{1}{3}}\in \mathrm{Constr}\right)$$
10	6 9	ax-mp	$$⊢\forall o\in \mathrm{Constr}{o}^{\frac{1}{3}}\in \mathrm{Constr}\to {{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}}^{\frac{1}{3}}\in \mathrm{Constr}$$
11	5 10	mto	$$⊢\neg \forall o\in \mathrm{Constr}{o}^{\frac{1}{3}}\in \mathrm{Constr}$$