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. Theorem 7.13 of [Stewart] p. 99. (Contributed by Thierry Arnoux and Saveliy Skresanov, 26-Oct-2025.) |
| Ref | Expression |
|---|---|
| 2sqr3nconstr | ⊢ (2↑𝑐(1 / 3)) ∉ Constr |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqid 2729 | . . . 4 ⊢ (deg1‘(ℂfld ↾s ℚ)) = (deg1‘(ℂfld ↾s ℚ)) | |
| 2 | eqid 2729 | . . . 4 ⊢ (ℂfld minPoly ℚ) = (ℂfld minPoly ℚ) | |
| 3 | 2cnd 12224 | . . . . 5 ⊢ (⊤ → 2 ∈ ℂ) | |
| 4 | 3cn 12227 | . . . . . . 7 ⊢ 3 ∈ ℂ | |
| 5 | 3ne0 12252 | . . . . . . 7 ⊢ 3 ≠ 0 | |
| 6 | 4, 5 | reccli 11872 | . . . . . 6 ⊢ (1 / 3) ∈ ℂ |
| 7 | 6 | a1i 11 | . . . . 5 ⊢ (⊤ → (1 / 3) ∈ ℂ) |
| 8 | 3, 7 | cxpcld 26633 | . . . 4 ⊢ (⊤ → (2↑𝑐(1 / 3)) ∈ ℂ) |
| 9 | eqidd 2730 | . . . 4 ⊢ (⊤ → ((ℂfld minPoly ℚ)‘(2↑𝑐(1 / 3))) = ((ℂfld minPoly ℚ)‘(2↑𝑐(1 / 3)))) | |
| 10 | eqid 2729 | . . . . . . . . . 10 ⊢ (ℂfld ↾s ℚ) = (ℂfld ↾s ℚ) | |
| 11 | eqid 2729 | . . . . . . . . . 10 ⊢ (-g‘(Poly1‘(ℂfld ↾s ℚ))) = (-g‘(Poly1‘(ℂfld ↾s ℚ))) | |
| 12 | eqid 2729 | . . . . . . . . . 10 ⊢ (.g‘(mulGrp‘(Poly1‘(ℂfld ↾s ℚ)))) = (.g‘(mulGrp‘(Poly1‘(ℂfld ↾s ℚ)))) | |
| 13 | eqid 2729 | . . . . . . . . . 10 ⊢ (Poly1‘(ℂfld ↾s ℚ)) = (Poly1‘(ℂfld ↾s ℚ)) | |
| 14 | eqid 2729 | . . . . . . . . . 10 ⊢ (algSc‘(Poly1‘(ℂfld ↾s ℚ))) = (algSc‘(Poly1‘(ℂfld ↾s ℚ))) | |
| 15 | eqid 2729 | . . . . . . . . . 10 ⊢ (var1‘(ℂfld ↾s ℚ)) = (var1‘(ℂfld ↾s ℚ)) | |
| 16 | eqid 2729 | . . . . . . . . . 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 2729 | . . . . . . . . . 10 ⊢ (2↑𝑐(1 / 3)) = (2↑𝑐(1 / 3)) | |
| 18 | 10, 11, 12, 13, 14, 15, 1, 16, 17, 2 | 2sqr3minply 33746 | . . . . . . . . 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 6829 | . . . . . . 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 2754 | . . . . . 6 ⊢ ((deg1‘(ℂfld ↾s ℚ))‘((ℂfld minPoly ℚ)‘(2↑𝑐(1 / 3)))) = 3 |
| 23 | 3nn0 12420 | . . . . . 6 ⊢ 3 ∈ ℕ0 | |
| 24 | 22, 23 | eqeltri 2824 | . . . . 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 12526 | . . . . . . . . . . 11 ⊢ 3 ∈ ℤ | |
| 28 | iddvds 16198 | . . . . . . . . . . 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 5132 | . . . . . . . . 9 ⊢ ((𝑛 ∈ ℕ0 ∧ 3 = (2↑𝑛)) → 3 ∥ (2↑𝑛)) |
| 32 | 3prm 16623 | . . . . . . . . . . 11 ⊢ 3 ∈ ℙ | |
| 33 | 2prm 16621 | . . . . . . . . . . 11 ⊢ 2 ∈ ℙ | |
| 34 | prmdvdsexpr 16646 | . . . . . . . . . . 11 ⊢ ((3 ∈ ℙ ∧ 2 ∈ ℙ ∧ 𝑛 ∈ ℕ0) → (3 ∥ (2↑𝑛) → 3 = 2)) | |
| 35 | 32, 33, 34 | mp3an12 1453 | . . . . . . . . . 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 12220 | . . . . . . . . . . 11 ⊢ 2 ∈ ℝ | |
| 39 | 2lt3 12313 | . . . . . . . . . . 11 ⊢ 2 < 3 | |
| 40 | 38, 39 | gtneii 11246 | . . . . . . . . . 10 ⊢ 3 ≠ 2 |
| 41 | 40 | neii 2927 | . . . . . . . . 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 2932 | . . . . . 6 ⊢ (𝑛 ∈ ℕ0 → 3 ≠ (2↑𝑛)) |
| 45 | 26, 44 | eqnetrd 2992 | . . . . 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 33740 | . . 3 ⊢ (⊤ → ¬ (2↑𝑐(1 / 3)) ∈ Constr) |
| 48 | 47 | mptru 1547 | . 2 ⊢ ¬ (2↑𝑐(1 / 3)) ∈ Constr |
| 49 | 48 | nelir 3032 | 1 ⊢ (2↑𝑐(1 / 3)) ∉ Constr |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 = wceq 1540 ⊤wtru 1541 ∈ wcel 2109 ≠ wne 2925 ∉ wnel 3029 class class class wbr 5095 ‘cfv 6486 (class class class)co 7353 ℂcc 11026 1c1 11029 / cdiv 11795 2c2 12201 3c3 12202 ℕ0cn0 12402 ℤcz 12489 ℚcq 12867 ↑cexp 13986 ∥ cdvds 16181 ℙcprime 16600 ↾s cress 17159 -gcsg 18832 .gcmg 18964 mulGrpcmgp 20043 ℂfldccnfld 21279 algSccascl 21777 var1cv1 22076 Poly1cpl1 22077 deg1cdg1 25975 ↑𝑐ccxp 26480 minPoly cminply 33665 Constrcconstr 33695 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7675 ax-reg 9503 ax-inf2 9556 ax-ac2 10376 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105 ax-pre-sup 11106 ax-addf 11107 ax-mulf 11108 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3345 df-reu 3346 df-rab 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-tp 4584 df-op 4586 df-uni 4862 df-int 4900 df-iun 4946 df-iin 4947 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5518 df-eprel 5523 df-po 5531 df-so 5532 df-fr 5576 df-se 5577 df-we 5578 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-isom 6495 df-riota 7310 df-ov 7356 df-oprab 7357 df-mpo 7358 df-of 7617 df-ofr 7618 df-rpss 7663 df-om 7807 df-1st 7931 df-2nd 7932 df-supp 8101 df-tpos 8166 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-2o 8396 df-oadd 8399 df-er 8632 df-ec 8634 df-qs 8638 df-map 8762 df-pm 8763 df-ixp 8832 df-en 8880 df-dom 8881 df-sdom 8882 df-fin 8883 df-fsupp 9271 df-fi 9320 df-sup 9351 df-inf 9352 df-oi 9421 df-r1 9679 df-rank 9680 df-dju 9816 df-card 9854 df-acn 9857 df-ac 10029 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11367 df-neg 11368 df-div 11796 df-nn 12147 df-2 12209 df-3 12210 df-4 12211 df-5 12212 df-6 12213 df-7 12214 df-8 12215 df-9 12216 df-n0 12403 df-xnn0 12476 df-z 12490 df-dec 12610 df-uz 12754 df-q 12868 df-rp 12912 df-xneg 13032 df-xadd 13033 df-xmul 13034 df-ioo 13270 df-ioc 13271 df-ico 13272 df-icc 13273 df-fz 13429 df-fzo 13576 df-fl 13714 df-mod 13792 df-seq 13927 df-exp 13987 df-fac 14199 df-bc 14228 df-hash 14256 df-word 14439 df-lsw 14488 df-concat 14496 df-s1 14521 df-substr 14566 df-pfx 14596 df-shft 14992 df-cj 15024 df-re 15025 df-im 15026 df-sqrt 15160 df-abs 15161 df-limsup 15396 df-clim 15413 df-rlim 15414 df-sum 15612 df-ef 15992 df-sin 15994 df-cos 15995 df-pi 15997 df-dvds 16182 df-gcd 16424 df-prm 16601 df-numer 16664 df-denom 16665 df-pc 16767 df-struct 17076 df-sets 17093 df-slot 17111 df-ndx 17123 df-base 17139 df-ress 17160 df-plusg 17192 df-mulr 17193 df-starv 17194 df-sca 17195 df-vsca 17196 df-ip 17197 df-tset 17198 df-ple 17199 df-ocomp 17200 df-ds 17201 df-unif 17202 df-hom 17203 df-cco 17204 df-rest 17344 df-topn 17345 df-0g 17363 df-gsum 17364 df-topgen 17365 df-pt 17366 df-prds 17369 df-pws 17371 df-xrs 17424 df-qtop 17429 df-imas 17430 df-qus 17431 df-xps 17432 df-mre 17506 df-mrc 17507 df-mri 17508 df-acs 17509 df-proset 18218 df-drs 18219 df-poset 18237 df-ipo 18452 df-mgm 18532 df-sgrp 18611 df-mnd 18627 df-mhm 18675 df-submnd 18676 df-grp 18833 df-minusg 18834 df-sbg 18835 df-mulg 18965 df-subg 19020 df-nsg 19021 df-eqg 19022 df-ghm 19110 df-gim 19156 df-cntz 19214 df-oppg 19243 df-lsm 19533 df-cmn 19679 df-abl 19680 df-mgp 20044 df-rng 20056 df-ur 20085 df-srg 20090 df-ring 20138 df-cring 20139 df-oppr 20240 df-dvdsr 20260 df-unit 20261 df-irred 20262 df-invr 20291 df-dvr 20304 df-rhm 20375 df-nzr 20416 df-subrng 20449 df-subrg 20473 df-rlreg 20597 df-domn 20598 df-idom 20599 df-drng 20634 df-field 20635 df-sdrg 20690 df-lmod 20783 df-lss 20853 df-lsp 20893 df-lmhm 20944 df-lmim 20945 df-lmic 20946 df-lbs 20997 df-lvec 21025 df-sra 21095 df-rgmod 21096 df-lidl 21133 df-rsp 21134 df-2idl 21175 df-lpidl 21247 df-lpir 21248 df-pid 21262 df-psmet 21271 df-xmet 21272 df-met 21273 df-bl 21274 df-mopn 21275 df-fbas 21276 df-fg 21277 df-cnfld 21280 df-dsmm 21657 df-frlm 21672 df-uvc 21708 df-lindf 21731 df-linds 21732 df-assa 21778 df-asp 21779 df-ascl 21780 df-psr 21834 df-mvr 21835 df-mpl 21836 df-opsr 21838 df-evls 21997 df-evl 21998 df-psr1 22080 df-vr1 22081 df-ply1 22082 df-coe1 22083 df-evls1 22218 df-evl1 22219 df-top 22797 df-topon 22814 df-topsp 22836 df-bases 22849 df-cld 22922 df-ntr 22923 df-cls 22924 df-nei 23001 df-lp 23039 df-perf 23040 df-cn 23130 df-cnp 23131 df-haus 23218 df-tx 23465 df-hmeo 23658 df-fil 23749 df-fm 23841 df-flim 23842 df-flf 23843 df-xms 24224 df-ms 24225 df-tms 24226 df-cncf 24787 df-limc 25783 df-dv 25784 df-mdeg 25976 df-deg1 25977 df-mon1 26052 df-uc1p 26053 df-q1p 26054 df-r1p 26055 df-ig1p 26056 df-log 26481 df-cxp 26482 df-chn 32960 df-fldgen 33260 df-mxidl 33407 df-dim 33571 df-fldext 33613 df-extdg 33614 df-irng 33655 df-minply 33666 df-constr 33696 |
| This theorem is referenced by: (None) |
| Copyright terms: Public domain | W3C validator |