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 ↑𝑐 ( 1 / 3 ) ) ∉ Constr

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( deg1 ‘ ( ℂfld ↾s ℚ ) ) = ( deg1 ‘ ( ℂfld ↾s ℚ ) )
2		eqid	⊢ ( ℂfld minPoly ℚ ) = ( ℂfld minPoly ℚ )
3		2cnd	⊢ ( ⊤ → 2 ∈ ℂ )
4		3cn	⊢ 3 ∈ ℂ
5		3ne0	⊢ 3 ≠ 0
6	4 5	reccli	⊢ ( 1 / 3 ) ∈ ℂ
7	6	a1i	⊢ ( ⊤ → ( 1 / 3 ) ∈ ℂ )
8	3 7	cxpcld	⊢ ( ⊤ → ( 2 ↑𝑐 ( 1 / 3 ) ) ∈ ℂ )
9		eqidd	⊢ ( ⊤ → ( ( ℂfld minPoly ℚ ) ‘ ( 2 ↑𝑐 ( 1 / 3 ) ) ) = ( ( ℂfld minPoly ℚ ) ‘ ( 2 ↑𝑐 ( 1 / 3 ) ) ) )
10		eqid	⊢ ( ℂfld ↾s ℚ ) = ( ℂfld ↾s ℚ )
11		eqid	⊢ ( -g ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) = ( -g ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) )
12		eqid	⊢ ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ) = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) )
13		eqid	⊢ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) = ( Poly1 ‘ ( ℂfld ↾s ℚ ) )
14		eqid	⊢ ( algSc ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) = ( algSc ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) )
15		eqid	⊢ ( var1 ‘ ( ℂfld ↾s ℚ ) ) = ( var1 ‘ ( ℂfld ↾s ℚ ) )
16		eqid	⊢ ( ( 3 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ) ( var1 ‘ ( ℂfld ↾s ℚ ) ) ) ( -g ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ‘ 2 ) ) = ( ( 3 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ) ( var1 ‘ ( ℂfld ↾s ℚ ) ) ) ( -g ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ‘ 2 ) )
17		eqid	⊢ ( 2 ↑𝑐 ( 1 / 3 ) ) = ( 2 ↑𝑐 ( 1 / 3 ) )
18	10 11 12 13 14 15 1 16 17 2	2sqr3minply	⊢ ( ( ( 3 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ) ( var1 ‘ ( ℂfld ↾s ℚ ) ) ) ( -g ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ‘ 2 ) ) = ( ( ℂfld minPoly ℚ ) ‘ ( 2 ↑𝑐 ( 1 / 3 ) ) ) ∧ ( ( deg1 ‘ ( ℂfld ↾s ℚ ) ) ‘ ( ( 3 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ) ( var1 ‘ ( ℂfld ↾s ℚ ) ) ) ( -g ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ‘ 2 ) ) ) = 3 )
19	18	simpli	⊢ ( ( 3 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ) ( var1 ‘ ( ℂfld ↾s ℚ ) ) ) ( -g ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ‘ 2 ) ) = ( ( ℂfld minPoly ℚ ) ‘ ( 2 ↑𝑐 ( 1 / 3 ) ) )
20	19	fveq2i	⊢ ( ( deg1 ‘ ( ℂfld ↾s ℚ ) ) ‘ ( ( 3 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ) ( var1 ‘ ( ℂfld ↾s ℚ ) ) ) ( -g ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ‘ 2 ) ) ) = ( ( deg1 ‘ ( ℂfld ↾s ℚ ) ) ‘ ( ( ℂfld minPoly ℚ ) ‘ ( 2 ↑𝑐 ( 1 / 3 ) ) ) )
21	18	simpri	⊢ ( ( deg1 ‘ ( ℂfld ↾s ℚ ) ) ‘ ( ( 3 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ) ( var1 ‘ ( ℂfld ↾s ℚ ) ) ) ( -g ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ‘ 2 ) ) ) = 3
22	20 21	eqtr3i	⊢ ( ( deg1 ‘ ( ℂfld ↾s ℚ ) ) ‘ ( ( ℂfld minPoly ℚ ) ‘ ( 2 ↑𝑐 ( 1 / 3 ) ) ) ) = 3
23		3nn0	⊢ 3 ∈ ℕ0
24	22 23	eqeltri	⊢ ( ( deg1 ‘ ( ℂfld ↾s ℚ ) ) ‘ ( ( ℂfld minPoly ℚ ) ‘ ( 2 ↑𝑐 ( 1 / 3 ) ) ) ) ∈ ℕ0
25	24	a1i	⊢ ( ⊤ → ( ( deg1 ‘ ( ℂfld ↾s ℚ ) ) ‘ ( ( ℂfld minPoly ℚ ) ‘ ( 2 ↑𝑐 ( 1 / 3 ) ) ) ) ∈ ℕ0 )
26	22	a1i	⊢ ( 𝑛 ∈ ℕ0 → ( ( deg1 ‘ ( ℂfld ↾s ℚ ) ) ‘ ( ( ℂfld minPoly ℚ ) ‘ ( 2 ↑𝑐 ( 1 / 3 ) ) ) ) = 3 )
27		3z	⊢ 3 ∈ ℤ
28		iddvds	⊢ ( 3 ∈ ℤ → 3 ∥ 3 )
29	27 28	ax-mp	⊢ 3 ∥ 3
30		simpr	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 3 = ( 2 ↑ 𝑛 ) ) → 3 = ( 2 ↑ 𝑛 ) )
31	29 30	breqtrid	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 3 = ( 2 ↑ 𝑛 ) ) → 3 ∥ ( 2 ↑ 𝑛 ) )
32		3prm	⊢ 3 ∈ ℙ
33		2prm	⊢ 2 ∈ ℙ
34		prmdvdsexpr	⊢ ( ( 3 ∈ ℙ ∧ 2 ∈ ℙ ∧ 𝑛 ∈ ℕ0 ) → ( 3 ∥ ( 2 ↑ 𝑛 ) → 3 = 2 ) )
35	32 33 34	mp3an12	⊢ ( 𝑛 ∈ ℕ0 → ( 3 ∥ ( 2 ↑ 𝑛 ) → 3 = 2 ) )
36	35	imp	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 3 ∥ ( 2 ↑ 𝑛 ) ) → 3 = 2 )
37	31 36	syldan	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 3 = ( 2 ↑ 𝑛 ) ) → 3 = 2 )
38		2re	⊢ 2 ∈ ℝ
39		2lt3	⊢ 2 < 3
40	38 39	gtneii	⊢ 3 ≠ 2
41	40	neii	⊢ ¬ 3 = 2
42	41	a1i	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 3 = ( 2 ↑ 𝑛 ) ) → ¬ 3 = 2 )
43	37 42	pm2.65da	⊢ ( 𝑛 ∈ ℕ0 → ¬ 3 = ( 2 ↑ 𝑛 ) )
44	43	neqned	⊢ ( 𝑛 ∈ ℕ0 → 3 ≠ ( 2 ↑ 𝑛 ) )
45	26 44	eqnetrd	⊢ ( 𝑛 ∈ ℕ0 → ( ( deg1 ‘ ( ℂfld ↾s ℚ ) ) ‘ ( ( ℂfld minPoly ℚ ) ‘ ( 2 ↑𝑐 ( 1 / 3 ) ) ) ) ≠ ( 2 ↑ 𝑛 ) )
46	45	adantl	⊢ ( ( ⊤ ∧ 𝑛 ∈ ℕ0 ) → ( ( deg1 ‘ ( ℂfld ↾s ℚ ) ) ‘ ( ( ℂfld minPoly ℚ ) ‘ ( 2 ↑𝑐 ( 1 / 3 ) ) ) ) ≠ ( 2 ↑ 𝑛 ) )
47	1 2 8 9 25 46	constrcon	⊢ ( ⊤ → ¬ ( 2 ↑𝑐 ( 1 / 3 ) ) ∈ Constr )
48	47	mptru	⊢ ¬ ( 2 ↑𝑐 ( 1 / 3 ) ) ∈ Constr
49	48	nelir	⊢ ( 2 ↑𝑐 ( 1 / 3 ) ) ∉ Constr