Nearby theorems
|
|
Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > Mathboxes > 2sqr3nconstr | Structured version Visualization version GIF version | ||
| 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↑𝑐(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 |
|---|---|
| 2sqr3nconstr | ⊢ (2↑𝑐(1 / 3)) ∉ Constr |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqid 2734 | . . . 4 ⊢ (deg1‘(ℂfld ↾s ℚ)) = (deg1‘(ℂfld ↾s ℚ)) | |
| 2 | eqid 2734 | . . . 4 ⊢ (ℂfld minPoly ℚ) = (ℂfld minPoly ℚ) | |
| 3 | 2cnd 12325 | . . . . 5 ⊢ (⊤ → 2 ∈ ℂ) | |
| 4 | 3cn 12328 | . . . . . . 7 ⊢ 3 ∈ ℂ | |
| 5 | 3ne0 12353 | . . . . . . 7 ⊢ 3 ≠ 0 | |
| 6 | 4, 5 | reccli 11978 | . . . . . 6 ⊢ (1 / 3) ∈ ℂ |
| 7 | 6 | a1i 11 | . . . . 5 ⊢ (⊤ → (1 / 3) ∈ ℂ) |
| 8 | 3, 7 | cxpcld 26685 | . . . 4 ⊢ (⊤ → (2↑𝑐(1 / 3)) ∈ ℂ) |
| 9 | eqidd 2735 | . . . 4 ⊢ (⊤ → ((ℂfld minPoly ℚ)‘(2↑𝑐(1 / 3))) = ((ℂfld minPoly ℚ)‘(2↑𝑐(1 / 3)))) | |
| 10 | eqid 2734 | . . . . . . . . . 10 ⊢ (ℂfld ↾s ℚ) = (ℂfld ↾s ℚ) | |
| 11 | eqid 2734 | . . . . . . . . . 10 ⊢ (-g‘(Poly1‘(ℂfld ↾s ℚ))) = (-g‘(Poly1‘(ℂfld ↾s ℚ))) | |
| 12 | eqid 2734 | . . . . . . . . . 10 ⊢ (.g‘(mulGrp‘(Poly1‘(ℂfld ↾s ℚ)))) = (.g‘(mulGrp‘(Poly1‘(ℂfld ↾s ℚ)))) | |
| 13 | eqid 2734 | . . . . . . . . . 10 ⊢ (Poly1‘(ℂfld ↾s ℚ)) = (Poly1‘(ℂfld ↾s ℚ)) | |
| 14 | eqid 2734 | . . . . . . . . . 10 ⊢ (algSc‘(Poly1‘(ℂfld ↾s ℚ))) = (algSc‘(Poly1‘(ℂfld ↾s ℚ))) | |
| 15 | eqid 2734 | . . . . . . . . . 10 ⊢ (var1‘(ℂfld ↾s ℚ)) = (var1‘(ℂfld ↾s ℚ)) | |
| 16 | eqid 2734 | . . . . . . . . . 10 ⊢ ((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 2734 | . . . . . . . . . 10 ⊢ (2↑𝑐(1 / 3)) = (2↑𝑐(1 / 3)) | |
| 18 | 10, 11, 12, 13, 14, 15, 1, 16, 17, 2 | 2sqr3minply 33724 | . . . . . . . . 9 ⊢ (((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 483 | . . . . . . . 8 ⊢ ((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 6888 | . . . . . . 7 ⊢ ((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 485 | . . . . . . 7 ⊢ ((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 2759 | . . . . . 6 ⊢ ((deg1‘(ℂfld ↾s ℚ))‘((ℂfld minPoly ℚ)‘(2↑𝑐(1 / 3)))) = 3 |
| 23 | 3nn0 12526 | . . . . . 6 ⊢ 3 ∈ ℕ0 | |
| 24 | 22, 23 | eqeltri 2829 | . . . . 5 ⊢ ((deg1‘(ℂfld ↾s ℚ))‘((ℂfld minPoly ℚ)‘(2↑𝑐(1 / 3)))) ∈ ℕ0 |
| 25 | 24 | a1i 11 | . . . 4 ⊢ (⊤ → ((deg1‘(ℂfld ↾s ℚ))‘((ℂfld minPoly ℚ)‘(2↑𝑐(1 / 3)))) ∈ ℕ0) |
| 26 | 22 | a1i 11 | . . . . . 6 ⊢ (𝑛 ∈ ℕ0 → ((deg1‘(ℂfld ↾s ℚ))‘((ℂfld minPoly ℚ)‘(2↑𝑐(1 / 3)))) = 3) |
| 27 | 3z 12632 | . . . . . . . . . . 11 ⊢ 3 ∈ ℤ | |
| 28 | iddvds 16288 | . . . . . . . . . . 11 ⊢ (3 ∈ ℤ → 3 ∥ 3) | |
| 29 | 27, 28 | ax-mp 5 | . . . . . . . . . 10 ⊢ 3 ∥ 3 |
| 30 | simpr 484 | . . . . . . . . . 10 ⊢ ((𝑛 ∈ ℕ0 ∧ 3 = (2↑𝑛)) → 3 = (2↑𝑛)) | |
| 31 | 29, 30 | breqtrid 5160 | . . . . . . . . 9 ⊢ ((𝑛 ∈ ℕ0 ∧ 3 = (2↑𝑛)) → 3 ∥ (2↑𝑛)) |
| 32 | 3prm 16712 | . . . . . . . . . . 11 ⊢ 3 ∈ ℙ | |
| 33 | 2prm 16710 | . . . . . . . . . . 11 ⊢ 2 ∈ ℙ | |
| 34 | prmdvdsexpr 16735 | . . . . . . . . . . 11 ⊢ ((3 ∈ ℙ ∧ 2 ∈ ℙ ∧ 𝑛 ∈ ℕ0) → (3 ∥ (2↑𝑛) → 3 = 2)) | |
| 35 | 32, 33, 34 | mp3an12 1452 | . . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ0 → (3 ∥ (2↑𝑛) → 3 = 2)) |
| 36 | 35 | imp 406 | . . . . . . . . 9 ⊢ ((𝑛 ∈ ℕ0 ∧ 3 ∥ (2↑𝑛)) → 3 = 2) |
| 37 | 31, 36 | syldan 591 | . . . . . . . 8 ⊢ ((𝑛 ∈ ℕ0 ∧ 3 = (2↑𝑛)) → 3 = 2) |
| 38 | 2re 12321 | . . . . . . . . . . 11 ⊢ 2 ∈ ℝ | |
| 39 | 2lt3 12419 | . . . . . . . . . . 11 ⊢ 2 < 3 | |
| 40 | 38, 39 | gtneii 11354 | . . . . . . . . . 10 ⊢ 3 ≠ 2 |
| 41 | 40 | neii 2933 | . . . . . . . . 9 ⊢ ¬ 3 = 2 |
| 42 | 41 | a1i 11 | . . . . . . . 8 ⊢ ((𝑛 ∈ ℕ0 ∧ 3 = (2↑𝑛)) → ¬ 3 = 2) |
| 43 | 37, 42 | pm2.65da 816 | . . . . . . 7 ⊢ (𝑛 ∈ ℕ0 → ¬ 3 = (2↑𝑛)) |
| 44 | 43 | neqned 2938 | . . . . . 6 ⊢ (𝑛 ∈ ℕ0 → 3 ≠ (2↑𝑛)) |
| 45 | 26, 44 | eqnetrd 2998 | . . . . 5 ⊢ (𝑛 ∈ ℕ0 → ((deg1‘(ℂfld ↾s ℚ))‘((ℂfld minPoly ℚ)‘(2↑𝑐(1 / 3)))) ≠ (2↑𝑛)) |
| 46 | 45 | adantl 481 | . . . 4 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ0) → ((deg1‘(ℂfld ↾s ℚ))‘((ℂfld minPoly ℚ)‘(2↑𝑐(1 / 3)))) ≠ (2↑𝑛)) |
| 47 | 1, 2, 8, 9, 25, 46 | constrcon 33723 | . . 3 ⊢ (⊤ → ¬ (2↑𝑐(1 / 3)) ∈ Constr) |
| 48 | 47 | mptru 1546 | . 2 ⊢ ¬ (2↑𝑐(1 / 3)) ∈ Constr |
| 49 | 48 | nelir 3038 | 1 ⊢ (2↑𝑐(1 / 3)) ∉ Constr |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 = wceq 1539 ⊤wtru 1540 ∈ wcel 2107 ≠ wne 2931 ∉ wnel 3035 class class class wbr 5123 ‘cfv 6540 (class class class)co 7412 ℂcc 11134 1c1 11137 / cdiv 11901 2c2 12302 3c3 12303 ℕ0cn0 12508 ℤcz 12595 ℚcq 12971 ↑cexp 14083 ∥ cdvds 16271 ℙcprime 16689 ↾s cress 17251 -gcsg 18921 .gcmg 19053 mulGrpcmgp 20104 ℂfldccnfld 21325 algSccascl 21825 var1cv1 22124 Poly1cpl1 22125 deg1cdg1 26028 ↑𝑐ccxp 26532 minPoly cminply 33670 Constrcconstr 33700 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2706 ax-rep 5259 ax-sep 5276 ax-nul 5286 ax-pow 5345 ax-pr 5412 ax-un 7736 ax-reg 9613 ax-inf2 9662 ax-ac2 10484 ax-cnex 11192 ax-resscn 11193 ax-1cn 11194 ax-icn 11195 ax-addcl 11196 ax-addrcl 11197 ax-mulcl 11198 ax-mulrcl 11199 ax-mulcom 11200 ax-addass 11201 ax-mulass 11202 ax-distr 11203 ax-i2m1 11204 ax-1ne0 11205 ax-1rid 11206 ax-rnegex 11207 ax-rrecex 11208 ax-cnre 11209 ax-pre-lttri 11210 ax-pre-lttrn 11211 ax-pre-ltadd 11212 ax-pre-mulgt0 11213 ax-pre-sup 11214 ax-addf 11215 ax-mulf 11216 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2808 df-nfc 2884 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3060 df-rmo 3363 df-reu 3364 df-rab 3420 df-v 3465 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-tp 4611 df-op 4613 df-uni 4888 df-int 4927 df-iun 4973 df-iin 4974 df-br 5124 df-opab 5186 df-mpt 5206 df-tr 5240 df-id 5558 df-eprel 5564 df-po 5572 df-so 5573 df-fr 5617 df-se 5618 df-we 5619 df-xp 5671 df-rel 5672 df-cnv 5673 df-co 5674 df-dm 5675 df-rn 5676 df-res 5677 df-ima 5678 df-pred 6301 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6493 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-of 7678 df-ofr 7679 df-rpss 7724 df-om 7869 df-1st 7995 df-2nd 7996 df-supp 8167 df-tpos 8232 df-frecs 8287 df-wrecs 8318 df-recs 8392 df-rdg 8431 df-1o 8487 df-2o 8488 df-oadd 8491 df-er 8726 df-ec 8728 df-qs 8732 df-map 8849 df-pm 8850 df-ixp 8919 df-en 8967 df-dom 8968 df-sdom 8969 df-fin 8970 df-fsupp 9383 df-fi 9432 df-sup 9463 df-inf 9464 df-oi 9531 df-r1 9785 df-rank 9786 df-dju 9922 df-card 9960 df-acn 9963 df-ac 10137 df-pnf 11278 df-mnf 11279 df-xr 11280 df-ltxr 11281 df-le 11282 df-sub 11475 df-neg 11476 df-div 11902 df-nn 12248 df-2 12310 df-3 12311 df-4 12312 df-5 12313 df-6 12314 df-7 12315 df-8 12316 df-9 12317 df-n0 12509 df-xnn0 12582 df-z 12596 df-dec 12716 df-uz 12860 df-q 12972 df-rp 13016 df-xneg 13135 df-xadd 13136 df-xmul 13137 df-ioo 13372 df-ioc 13373 df-ico 13374 df-icc 13375 df-fz 13529 df-fzo 13676 df-fl 13813 df-mod 13891 df-seq 14024 df-exp 14084 df-fac 14294 df-bc 14323 df-hash 14351 df-word 14534 df-lsw 14582 df-concat 14590 df-s1 14615 df-substr 14660 df-pfx 14690 df-shft 15087 df-cj 15119 df-re 15120 df-im 15121 df-sqrt 15255 df-abs 15256 df-limsup 15488 df-clim 15505 df-rlim 15506 df-sum 15704 df-ef 16084 df-sin 16086 df-cos 16087 df-pi 16089 df-dvds 16272 df-gcd 16513 df-prm 16690 df-numer 16753 df-denom 16754 df-pc 16856 df-struct 17165 df-sets 17182 df-slot 17200 df-ndx 17212 df-base 17229 df-ress 17252 df-plusg 17285 df-mulr 17286 df-starv 17287 df-sca 17288 df-vsca 17289 df-ip 17290 df-tset 17291 df-ple 17292 df-ocomp 17293 df-ds 17294 df-unif 17295 df-hom 17296 df-cco 17297 df-rest 17437 df-topn 17438 df-0g 17456 df-gsum 17457 df-topgen 17458 df-pt 17459 df-prds 17462 df-pws 17464 df-xrs 17517 df-qtop 17522 df-imas 17523 df-qus 17524 df-xps 17525 df-mre 17599 df-mrc 17600 df-mri 17601 df-acs 17602 df-proset 18309 df-drs 18310 df-poset 18328 df-ipo 18541 df-mgm 18621 df-sgrp 18700 df-mnd 18716 df-mhm 18764 df-submnd 18765 df-grp 18922 df-minusg 18923 df-sbg 18924 df-mulg 19054 df-subg 19109 df-nsg 19110 df-eqg 19111 df-ghm 19199 df-gim 19245 df-cntz 19303 df-oppg 19332 df-lsm 19621 df-cmn 19767 df-abl 19768 df-mgp 20105 df-rng 20117 df-ur 20146 df-srg 20151 df-ring 20199 df-cring 20200 df-oppr 20301 df-dvdsr 20324 df-unit 20325 df-irred 20326 df-invr 20355 df-dvr 20368 df-rhm 20439 df-nzr 20480 df-subrng 20513 df-subrg 20537 df-rlreg 20661 df-domn 20662 df-idom 20663 df-drng 20698 df-field 20699 df-sdrg 20755 df-lmod 20827 df-lss 20897 df-lsp 20937 df-lmhm 20988 df-lmim 20989 df-lmic 20990 df-lbs 21041 df-lvec 21069 df-sra 21139 df-rgmod 21140 df-lidl 21179 df-rsp 21180 df-2idl 21221 df-lpidl 21293 df-lpir 21294 df-pid 21308 df-psmet 21317 df-xmet 21318 df-met 21319 df-bl 21320 df-mopn 21321 df-fbas 21322 df-fg 21323 df-cnfld 21326 df-dsmm 21705 df-frlm 21720 df-uvc 21756 df-lindf 21779 df-linds 21780 df-assa 21826 df-asp 21827 df-ascl 21828 df-psr 21882 df-mvr 21883 df-mpl 21884 df-opsr 21886 df-evls 22045 df-evl 22046 df-psr1 22128 df-vr1 22129 df-ply1 22130 df-coe1 22131 df-evls1 22266 df-evl1 22267 df-top 22847 df-topon 22864 df-topsp 22886 df-bases 22899 df-cld 22972 df-ntr 22973 df-cls 22974 df-nei 23051 df-lp 23089 df-perf 23090 df-cn 23180 df-cnp 23181 df-haus 23268 df-tx 23515 df-hmeo 23708 df-fil 23799 df-fm 23891 df-flim 23892 df-flf 23893 df-xms 24274 df-ms 24275 df-tms 24276 df-cncf 24839 df-limc 25836 df-dv 25837 df-mdeg 26029 df-deg1 26030 df-mon1 26105 df-uc1p 26106 df-q1p 26107 df-r1p 26108 df-ig1p 26109 df-log 26533 df-cxp 26534 df-chn 32925 df-fldgen 33244 df-mxidl 33414 df-dim 33576 df-fldext 33619 df-extdg 33620 df-irng 33662 df-minply 33671 df-constr 33701 |
| This theorem is referenced by: (None) |
| Copyright terms: Public domain | W3C validator |