Metamath Proof Explorer

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. (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