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 ^c ( 1 / 3 ) ) e/ Constr

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( deg1 ` ( CCfld |`s QQ ) ) = ( deg1 ` ( CCfld |`s QQ ) )
2 eqid 
 |-  ( CCfld minPoly QQ ) = ( CCfld minPoly QQ )
3 2cnd 
 |-  ( T. -> 2 e. CC )
4 3cn 
 |-  3 e. CC
5 3ne0 
 |-  3 =/= 0
6 4 5 reccli 
 |-  ( 1 / 3 ) e. CC
7 6 a1i 
 |-  ( T. -> ( 1 / 3 ) e. CC )
8 3 7 cxpcld 
 |-  ( T. -> ( 2 ^c ( 1 / 3 ) ) e. CC )
9 eqidd 
 |-  ( T. -> ( ( CCfld minPoly QQ ) ` ( 2 ^c ( 1 / 3 ) ) ) = ( ( CCfld minPoly QQ ) ` ( 2 ^c ( 1 / 3 ) ) ) )
10 eqid 
 |-  ( CCfld |`s QQ ) = ( CCfld |`s QQ )
11 eqid 
 |-  ( -g ` ( Poly1 ` ( CCfld |`s QQ ) ) ) = ( -g ` ( Poly1 ` ( CCfld |`s QQ ) ) )
12 eqid 
 |-  ( .g ` ( mulGrp ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ) = ( .g ` ( mulGrp ` ( Poly1 ` ( CCfld |`s QQ ) ) ) )
13 eqid 
 |-  ( Poly1 ` ( CCfld |`s QQ ) ) = ( Poly1 ` ( CCfld |`s QQ ) )
14 eqid 
 |-  ( algSc ` ( Poly1 ` ( CCfld |`s QQ ) ) ) = ( algSc ` ( Poly1 ` ( CCfld |`s QQ ) ) )
15 eqid 
 |-  ( var1 ` ( CCfld |`s QQ ) ) = ( var1 ` ( CCfld |`s QQ ) )
16 eqid 
 |-  ( ( 3 ( .g ` ( mulGrp ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ) ( var1 ` ( CCfld |`s QQ ) ) ) ( -g ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ( ( algSc ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ` 2 ) ) = ( ( 3 ( .g ` ( mulGrp ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ) ( var1 ` ( CCfld |`s QQ ) ) ) ( -g ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ( ( algSc ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ` 2 ) )
17 eqid 
 |-  ( 2 ^c ( 1 / 3 ) ) = ( 2 ^c ( 1 / 3 ) )
18 10 11 12 13 14 15 1 16 17 2 2sqr3minply 
 |-  ( ( ( 3 ( .g ` ( mulGrp ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ) ( var1 ` ( CCfld |`s QQ ) ) ) ( -g ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ( ( algSc ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ` 2 ) ) = ( ( CCfld minPoly QQ ) ` ( 2 ^c ( 1 / 3 ) ) ) /\ ( ( deg1 ` ( CCfld |`s QQ ) ) ` ( ( 3 ( .g ` ( mulGrp ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ) ( var1 ` ( CCfld |`s QQ ) ) ) ( -g ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ( ( algSc ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ` 2 ) ) ) = 3 )
19 18 simpli 
 |-  ( ( 3 ( .g ` ( mulGrp ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ) ( var1 ` ( CCfld |`s QQ ) ) ) ( -g ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ( ( algSc ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ` 2 ) ) = ( ( CCfld minPoly QQ ) ` ( 2 ^c ( 1 / 3 ) ) )
20 19 fveq2i 
 |-  ( ( deg1 ` ( CCfld |`s QQ ) ) ` ( ( 3 ( .g ` ( mulGrp ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ) ( var1 ` ( CCfld |`s QQ ) ) ) ( -g ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ( ( algSc ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ` 2 ) ) ) = ( ( deg1 ` ( CCfld |`s QQ ) ) ` ( ( CCfld minPoly QQ ) ` ( 2 ^c ( 1 / 3 ) ) ) )
21 18 simpri 
 |-  ( ( deg1 ` ( CCfld |`s QQ ) ) ` ( ( 3 ( .g ` ( mulGrp ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ) ( var1 ` ( CCfld |`s QQ ) ) ) ( -g ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ( ( algSc ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ` 2 ) ) ) = 3
22 20 21 eqtr3i 
 |-  ( ( deg1 ` ( CCfld |`s QQ ) ) ` ( ( CCfld minPoly QQ ) ` ( 2 ^c ( 1 / 3 ) ) ) ) = 3
23 3nn0 
 |-  3 e. NN0
24 22 23 eqeltri 
 |-  ( ( deg1 ` ( CCfld |`s QQ ) ) ` ( ( CCfld minPoly QQ ) ` ( 2 ^c ( 1 / 3 ) ) ) ) e. NN0
25 24 a1i 
 |-  ( T. -> ( ( deg1 ` ( CCfld |`s QQ ) ) ` ( ( CCfld minPoly QQ ) ` ( 2 ^c ( 1 / 3 ) ) ) ) e. NN0 )
26 22 a1i 
 |-  ( n e. NN0 -> ( ( deg1 ` ( CCfld |`s QQ ) ) ` ( ( CCfld minPoly QQ ) ` ( 2 ^c ( 1 / 3 ) ) ) ) = 3 )
27 3z 
 |-  3 e. ZZ
28 iddvds 
 |-  ( 3 e. ZZ -> 3 || 3 )
29 27 28 ax-mp 
 |-  3 || 3
30 simpr 
 |-  ( ( n e. NN0 /\ 3 = ( 2 ^ n ) ) -> 3 = ( 2 ^ n ) )
31 29 30 breqtrid 
 |-  ( ( n e. NN0 /\ 3 = ( 2 ^ n ) ) -> 3 || ( 2 ^ n ) )
32 3prm 
 |-  3 e. Prime
33 2prm 
 |-  2 e. Prime
34 prmdvdsexpr 
 |-  ( ( 3 e. Prime /\ 2 e. Prime /\ n e. NN0 ) -> ( 3 || ( 2 ^ n ) -> 3 = 2 ) )
35 32 33 34 mp3an12 
 |-  ( n e. NN0 -> ( 3 || ( 2 ^ n ) -> 3 = 2 ) )
36 35 imp 
 |-  ( ( n e. NN0 /\ 3 || ( 2 ^ n ) ) -> 3 = 2 )
37 31 36 syldan 
 |-  ( ( n e. NN0 /\ 3 = ( 2 ^ n ) ) -> 3 = 2 )
38 2re 
 |-  2 e. RR
39 2lt3 
 |-  2 < 3
40 38 39 gtneii 
 |-  3 =/= 2
41 40 neii 
 |-  -. 3 = 2
42 41 a1i 
 |-  ( ( n e. NN0 /\ 3 = ( 2 ^ n ) ) -> -. 3 = 2 )
43 37 42 pm2.65da 
 |-  ( n e. NN0 -> -. 3 = ( 2 ^ n ) )
44 43 neqned 
 |-  ( n e. NN0 -> 3 =/= ( 2 ^ n ) )
45 26 44 eqnetrd 
 |-  ( n e. NN0 -> ( ( deg1 ` ( CCfld |`s QQ ) ) ` ( ( CCfld minPoly QQ ) ` ( 2 ^c ( 1 / 3 ) ) ) ) =/= ( 2 ^ n ) )
46 45 adantl 
 |-  ( ( T. /\ n e. NN0 ) -> ( ( deg1 ` ( CCfld |`s QQ ) ) ` ( ( CCfld minPoly QQ ) ` ( 2 ^c ( 1 / 3 ) ) ) ) =/= ( 2 ^ n ) )
47 1 2 8 9 25 46 constrcon 
 |-  ( T. -> -. ( 2 ^c ( 1 / 3 ) ) e. Constr )
48 47 mptru 
 |-  -. ( 2 ^c ( 1 / 3 ) ) e. Constr
49 48 nelir 
 |-  ( 2 ^c ( 1 / 3 ) ) e/ Constr