Theorem 2sqr3nconstr

Description: Doubling the cube is an impossible construction, i.e. the cube root of 2 is not constructible with straightedge and compass. Given a cube of edge of length one, a cube of double volume would have an edge of length ( 2 ^c ( 1 / 3 ) ) , however that number is not constructible. This is the first part of Metamath 100 proof #8. Theorem 7.13 of Stewart p. 99. (Contributed by Thierry Arnoux and Saveliy Skresanov, 26-Oct-2025)

	Ref	Expression
Assertion	2sqr3nconstr	$$⊢2^{\frac{1}{3}}\notin \mathrm{Constr}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)={\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)$$
2		eqid	$$⊢{ℂ}_{\mathrm{fld}}\mathrm{minPoly}\mathbb{Q}={ℂ}_{\mathrm{fld}}\mathrm{minPoly}\mathbb{Q}$$
3		2cnd	$$⊢\top \to 2\in ℂ$$
4		3cn	$$⊢3\in ℂ$$
5		3ne0	$$⊢3\ne 0$$
6	4 5	reccli	$$⊢\frac{1}{3}\in ℂ$$
7	6	a1i	$$⊢\top \to \frac{1}{3}\in ℂ$$
8	3 7	cxpcld	$$⊢\top \to 2^{\frac{1}{3}}\in ℂ$$
9		eqidd	$$⊢\top \to \left({ℂ}_{\mathrm{fld}}\mathrm{minPoly}\mathbb{Q}\right)\left(2^{\frac{1}{3}}\right)=\left({ℂ}_{\mathrm{fld}}\mathrm{minPoly}\mathbb{Q}\right)\left(2^{\frac{1}{3}}\right)$$
10		eqid	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
11		eqid	$$⊢{-}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}={-}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}$$
12		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}}={\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}}$$
13		eqid	$$⊢{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)={\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)$$
14		eqid	$$⊢\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)=\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)$$
15		eqid	$$⊢{\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)={\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)$$
16		eqid	$$⊢\left(3{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}}{\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right){-}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)\left(2\right)=\left(3{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}}{\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right){-}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)\left(2\right)$$
17		eqid	$$⊢2^{\frac{1}{3}}=2^{\frac{1}{3}}$$
18	10 11 12 13 14 15 1 16 17 2	2sqr3minply	$$⊢\left(\left(3{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}}{\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right){-}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)\left(2\right)=\left({ℂ}_{\mathrm{fld}}\mathrm{minPoly}\mathbb{Q}\right)\left(2^{\frac{1}{3}}\right)\wedge {\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\left(\left(3{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}}{\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right){-}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)\left(2\right)\right)=3\right)$$
19	18	simpli	$$⊢\left(3{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}}{\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right){-}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)\left(2\right)=\left({ℂ}_{\mathrm{fld}}\mathrm{minPoly}\mathbb{Q}\right)\left(2^{\frac{1}{3}}\right)$$
20	19	fveq2i	$$⊢{\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\left(\left(3{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}}{\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right){-}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)\left(2\right)\right)={\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\left(\left({ℂ}_{\mathrm{fld}}\mathrm{minPoly}\mathbb{Q}\right)\left(2^{\frac{1}{3}}\right)\right)$$
21	18	simpri	$$⊢{\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\left(\left(3{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}}{\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right){-}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)\left(2\right)\right)=3$$
22	20 21	eqtr3i	$$⊢{\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\left(\left({ℂ}_{\mathrm{fld}}\mathrm{minPoly}\mathbb{Q}\right)\left(2^{\frac{1}{3}}\right)\right)=3$$
23		3nn0	$$⊢3\in {\mathbb{N}}_0$$
24	22 23	eqeltri	$$⊢{\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\left(\left({ℂ}_{\mathrm{fld}}\mathrm{minPoly}\mathbb{Q}\right)\left(2^{\frac{1}{3}}\right)\right)\in {\mathbb{N}}_0$$
25	24	a1i	$$⊢\top \to {\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\left(\left({ℂ}_{\mathrm{fld}}\mathrm{minPoly}\mathbb{Q}\right)\left(2^{\frac{1}{3}}\right)\right)\in {\mathbb{N}}_0$$
26	22	a1i	$$⊢n\in {\mathbb{N}}_0\to {\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\left(\left({ℂ}_{\mathrm{fld}}\mathrm{minPoly}\mathbb{Q}\right)\left(2^{\frac{1}{3}}\right)\right)=3$$
27		3z	$$⊢3\in \mathbb{Z}$$
28		iddvds	$$⊢3\in \mathbb{Z}\to 3\parallel 3$$
29	27 28	ax-mp	$$⊢3\parallel 3$$
30		simpr	$$⊢\left(n\in {\mathbb{N}}_0\wedge 3=2^n\right)\to 3=2^n$$
31	29 30	breqtrid	$$⊢\left(n\in {\mathbb{N}}_0\wedge 3=2^n\right)\to 3\parallel 2^n$$
32		3prm	$$⊢3\in \mathbb{P}$$
33		2prm	$$⊢2\in \mathbb{P}$$
34		prmdvdsexpr	$$⊢\left(3\in \mathbb{P}\wedge 2\in \mathbb{P}\wedge n\in {\mathbb{N}}_0\right)\to \left(3\parallel 2^n\to 3=2\right)$$
35	32 33 34	mp3an12	$$⊢n\in {\mathbb{N}}_0\to \left(3\parallel 2^n\to 3=2\right)$$
36	35	imp	$$⊢\left(n\in {\mathbb{N}}_0\wedge 3\parallel 2^n\right)\to 3=2$$
37	31 36	syldan	$$⊢\left(n\in {\mathbb{N}}_0\wedge 3=2^n\right)\to 3=2$$
38		2re	$$⊢2\in ℝ$$
39		2lt3	$$⊢2<3$$
40	38 39	gtneii	$$⊢3\ne 2$$
41	40	neii	$$⊢\neg 3=2$$
42	41	a1i	$$⊢\left(n\in {\mathbb{N}}_0\wedge 3=2^n\right)\to \neg 3=2$$
43	37 42	pm2.65da	$$⊢n\in {\mathbb{N}}_0\to \neg 3=2^n$$
44	43	neqned	$$⊢n\in {\mathbb{N}}_0\to 3\ne 2^n$$
45	26 44	eqnetrd	$$⊢n\in {\mathbb{N}}_0\to {\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\left(\left({ℂ}_{\mathrm{fld}}\mathrm{minPoly}\mathbb{Q}\right)\left(2^{\frac{1}{3}}\right)\right)\ne 2^n$$
46	45	adantl	$$⊢\left(\top \wedge n\in {\mathbb{N}}_0\right)\to {\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\left(\left({ℂ}_{\mathrm{fld}}\mathrm{minPoly}\mathbb{Q}\right)\left(2^{\frac{1}{3}}\right)\right)\ne 2^n$$
47	1 2 8 9 25 46	constrcon	$$⊢\top \to \neg 2^{\frac{1}{3}}\in \mathrm{Constr}$$
48	47	mptru	$$⊢\neg 2^{\frac{1}{3}}\in \mathrm{Constr}$$
49	48	nelir	$$⊢2^{\frac{1}{3}}\notin \mathrm{Constr}$$