| Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > Mathboxes > constrext2chn | Structured version Visualization version GIF version | ||
| Description: If a constructible number generates some subfield 𝐿 of ℂ, then the degree of the extension of 𝐿 over ℚ is a power of two. Theorem 7.12 of [Stewart] p. 98. (Contributed by Thierry Arnoux, 26-Oct-2025.) |
| Ref | Expression |
|---|---|
| constrext2chn.q | ⊢ 𝑄 = (ℂfld ↾s ℚ) |
| constrext2chn.l | ⊢ 𝐿 = (ℂfld ↾s 𝑆) |
| constrext2chn.s | ⊢ 𝑆 = (ℂfld fldGen (ℚ ∪ {𝐴})) |
| constrext2chn.a | ⊢ (𝜑 → 𝐴 ∈ Constr) |
| Ref | Expression |
|---|---|
| constrext2chn | ⊢ (𝜑 → ∃𝑛 ∈ ℕ0 (𝐿[:]𝑄) = (2↑𝑛)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | constrcbvlem 34057 | . 2 ⊢ rec((𝑧 ∈ V ↦ {𝑦 ∈ ℂ ∣ (∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑜 ∈ ℝ ∃𝑝 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 ∃𝑜 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞))) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞))))}), {0, 1}) = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1}) | |
| 2 | eqid 2765 | . 2 ⊢ (ℂfld ↾s 𝑒) = (ℂfld ↾s 𝑒) | |
| 3 | eqid 2765 | . 2 ⊢ (ℂfld ↾s 𝑓) = (ℂfld ↾s 𝑓) | |
| 4 | oveq2 7408 | . . . . . 6 ⊢ (ℎ = 𝑒 → (ℂfld ↾s ℎ) = (ℂfld ↾s 𝑒)) | |
| 5 | 4 | adantl 486 | . . . . 5 ⊢ ((𝑔 = 𝑓 ∧ ℎ = 𝑒) → (ℂfld ↾s ℎ) = (ℂfld ↾s 𝑒)) |
| 6 | oveq2 7408 | . . . . . 6 ⊢ (𝑔 = 𝑓 → (ℂfld ↾s 𝑔) = (ℂfld ↾s 𝑓)) | |
| 7 | 6 | adantr 485 | . . . . 5 ⊢ ((𝑔 = 𝑓 ∧ ℎ = 𝑒) → (ℂfld ↾s 𝑔) = (ℂfld ↾s 𝑓)) |
| 8 | 5, 7 | breq12d 5117 | . . . 4 ⊢ ((𝑔 = 𝑓 ∧ ℎ = 𝑒) → ((ℂfld ↾s ℎ)/FldExt(ℂfld ↾s 𝑔) ↔ (ℂfld ↾s 𝑒)/FldExt(ℂfld ↾s 𝑓))) |
| 9 | 5, 7 | oveq12d 7418 | . . . . 5 ⊢ ((𝑔 = 𝑓 ∧ ℎ = 𝑒) → ((ℂfld ↾s ℎ)[:](ℂfld ↾s 𝑔)) = ((ℂfld ↾s 𝑒)[:](ℂfld ↾s 𝑓))) |
| 10 | 9 | eqeq1d 2767 | . . . 4 ⊢ ((𝑔 = 𝑓 ∧ ℎ = 𝑒) → (((ℂfld ↾s ℎ)[:](ℂfld ↾s 𝑔)) = 2 ↔ ((ℂfld ↾s 𝑒)[:](ℂfld ↾s 𝑓)) = 2)) |
| 11 | 8, 10 | anbi12d 643 | . . 3 ⊢ ((𝑔 = 𝑓 ∧ ℎ = 𝑒) → (((ℂfld ↾s ℎ)/FldExt(ℂfld ↾s 𝑔) ∧ ((ℂfld ↾s ℎ)[:](ℂfld ↾s 𝑔)) = 2) ↔ ((ℂfld ↾s 𝑒)/FldExt(ℂfld ↾s 𝑓) ∧ ((ℂfld ↾s 𝑒)[:](ℂfld ↾s 𝑓)) = 2))) |
| 12 | 11 | cbvopabv 5177 | . 2 ⊢ {〈𝑔, ℎ〉 ∣ ((ℂfld ↾s ℎ)/FldExt(ℂfld ↾s 𝑔) ∧ ((ℂfld ↾s ℎ)[:](ℂfld ↾s 𝑔)) = 2)} = {〈𝑓, 𝑒〉 ∣ ((ℂfld ↾s 𝑒)/FldExt(ℂfld ↾s 𝑓) ∧ ((ℂfld ↾s 𝑒)[:](ℂfld ↾s 𝑓)) = 2)} |
| 13 | peano1 7873 | . . 3 ⊢ ∅ ∈ ω | |
| 14 | 13 | a1i 11 | . 2 ⊢ (𝜑 → ∅ ∈ ω) |
| 15 | constrext2chn.q | . 2 ⊢ 𝑄 = (ℂfld ↾s ℚ) | |
| 16 | constrext2chn.l | . . 3 ⊢ 𝐿 = (ℂfld ↾s 𝑆) | |
| 17 | constrext2chn.s | . . . 4 ⊢ 𝑆 = (ℂfld fldGen (ℚ ∪ {𝐴})) | |
| 18 | 17 | oveq2i 7411 | . . 3 ⊢ (ℂfld ↾s 𝑆) = (ℂfld ↾s (ℂfld fldGen (ℚ ∪ {𝐴}))) |
| 19 | 16, 18 | eqtri 2788 | . 2 ⊢ 𝐿 = (ℂfld ↾s (ℂfld fldGen (ℚ ∪ {𝐴}))) |
| 20 | constrext2chn.a | . 2 ⊢ (𝜑 → 𝐴 ∈ Constr) | |
| 21 | 1, 2, 3, 12, 14, 15, 19, 20 | constrext2chnlem 34052 | 1 ⊢ (𝜑 → ∃𝑛 ∈ ℕ0 (𝐿[:]𝑄) = (2↑𝑛)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 400 ∨ w3o 1100 ∧ w3a 1101 = wceq 1563 ∈ wcel 2145 ≠ wne 2960 ∃wrex 3089 {crab 3417 Vcvv 3457 ∪ cun 3905 ∅c0 4288 {csn 4585 {cpr 4587 class class class wbr 5104 {copab 5166 ↦ cmpt 5185 ‘cfv 6525 (class class class)co 7400 ωcom 7850 reccrdg 8384 ℂcc 11086 ℝcr 11087 0cc0 11088 1c1 11089 + caddc 11091 · cmul 11093 − cmin 11429 2c2 12283 ℕ0cn0 12492 ℚcq 12960 ↑cexp 14085 ∗ccj 15135 ℑcim 15137 abscabs 15273 ↾s cress 17278 ℂfldccnfld 21479 fldGen cfldgen 33541 /FldExtcfldext 33940 [:]cextdg 33942 Constrcconstr 34031 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-rep 5231 ax-sep 5250 ax-nul 5260 ax-pow 5326 ax-pr 5394 ax-un 7722 ax-reg 9542 ax-inf2 9598 ax-ac2 10435 ax-cnex 11144 ax-resscn 11145 ax-1cn 11146 ax-icn 11147 ax-addcl 11148 ax-addrcl 11149 ax-mulcl 11150 ax-mulrcl 11151 ax-mulcom 11152 ax-addass 11153 ax-mulass 11154 ax-distr 11155 ax-i2m1 11156 ax-1ne0 11157 ax-1rid 11158 ax-rnegex 11159 ax-rrecex 11160 ax-cnre 11161 ax-pre-lttri 11162 ax-pre-lttrn 11163 ax-pre-ltadd 11164 ax-pre-mulgt0 11165 ax-pre-sup 11166 ax-addf 11167 ax-mulf 11168 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3370 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-pss 3927 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5105 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6291 df-ord 6352 df-on 6353 df-lim 6354 df-suc 6355 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-isom 6534 df-riota 7357 df-ov 7403 df-oprab 7404 df-mpo 7405 df-of 7664 df-ofr 7665 df-rpss 7710 df-om 7851 df-1st 7974 df-2nd 7975 df-supp 8145 df-tpos 8210 df-frecs 8266 df-wrecs 8297 df-recs 8346 df-rdg 8385 df-1o 8441 df-2o 8442 df-oadd 8445 df-er 8682 df-ec 8684 df-qs 8688 df-map 8814 df-pm 8815 df-ixp 8884 df-en 8932 df-dom 8933 df-sdom 8934 df-fin 8935 df-fsupp 9310 df-sup 9390 df-inf 9391 df-oi 9460 df-r1 9724 df-rank 9725 df-dju 9875 df-card 9913 df-acn 9916 df-ac 10088 df-pnf 11233 df-mnf 11234 df-xr 11235 df-ltxr 11236 df-le 11237 df-sub 11431 df-neg 11432 df-div 11860 df-nn 12222 df-2 12291 df-3 12292 df-4 12293 df-5 12294 df-6 12295 df-7 12296 df-8 12297 df-9 12298 df-n0 12493 df-xnn0 12566 df-z 12580 df-dec 12700 df-uz 12851 df-q 12961 df-rp 13005 df-xneg 13125 df-xmul 13127 df-ico 13366 df-fz 13524 df-fzo 13671 df-fl 13813 df-mod 13891 df-seq 14026 df-exp 14086 df-hash 14355 df-word 14539 df-lsw 14588 df-concat 14596 df-s1 14622 df-substr 14667 df-pfx 14697 df-cj 15138 df-re 15139 df-im 15140 df-sqrt 15274 df-abs 15275 df-dvds 16299 df-gcd 16541 df-prm 16718 df-pc 16885 df-struct 17195 df-sets 17212 df-slot 17230 df-ndx 17242 df-base 17258 df-ress 17279 df-plusg 17311 df-mulr 17312 df-starv 17313 df-sca 17314 df-vsca 17315 df-ip 17316 df-tset 17317 df-ple 17318 df-ocomp 17319 df-ds 17320 df-unif 17321 df-hom 17322 df-cco 17323 df-0g 17482 df-gsum 17483 df-prds 17488 df-pws 17490 df-imas 17550 df-qus 17551 df-mre 17626 df-mrc 17627 df-mri 17628 df-acs 17629 df-proset 18338 df-drs 18339 df-poset 18357 df-ipo 18572 df-chn 18650 df-mgm 18686 df-sgrp 18765 df-mnd 18781 df-mhm 18829 df-submnd 18830 df-grp 18991 df-minusg 18992 df-sbg 18993 df-mulg 19122 df-subg 19177 df-nsg 19178 df-eqg 19179 df-ghm 19272 df-gim 19317 df-cntz 19375 df-oppg 19404 df-lsm 19694 df-cmn 19840 df-abl 19841 df-mgp 20205 df-rng 20219 df-ur 20252 df-srg 20257 df-ring 20305 df-cring 20306 df-oppr 20407 df-dvdsr 20427 df-unit 20428 df-irred 20429 df-invr 20458 df-dvr 20471 df-rhm 20542 df-nzr 20584 df-subrng 20619 df-subrg 20643 df-rlreg 20767 df-domn 20768 df-idom 20769 df-drng 20803 df-field 20804 df-sdrg 20856 df-lmod 20949 df-lss 21019 df-lsp 21059 df-lmhm 21109 df-lmim 21110 df-lmic 21111 df-lbs 21162 df-lvec 21190 df-sra 21260 df-rgmod 21261 df-lidl 21298 df-rsp 21299 df-2idl 21348 df-lpidl 21447 df-lpir 21448 df-pid 21462 df-cnfld 21480 df-dsmm 21839 df-frlm 21854 df-uvc 21890 df-lindf 21913 df-linds 21914 df-assa 21960 df-asp 21961 df-ascl 21962 df-psr 22016 df-mvr 22017 df-mpl 22018 df-opsr 22020 df-evls 22182 df-evl 22183 df-psr1 22297 df-vr1 22298 df-ply1 22299 df-coe1 22300 df-evls1 22432 df-evl1 22433 df-mdeg 26169 df-deg1 26170 df-mon1 26245 df-uc1p 26246 df-q1p 26247 df-r1p 26248 df-ig1p 26249 df-fldgen 33542 df-mxidl 33655 df-dim 33902 df-fldext 33943 df-extdg 33944 df-irng 33986 df-minply 34002 df-constr 34032 |
| This theorem is referenced by: constrcon 34076 |
| Copyright terms: Public domain | W3C validator |