Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > quartlem3 | Structured version Visualization version GIF version |
Description: Closure lemmas for quart 25716. (Contributed by Mario Carneiro, 7-May-2015.) |
Ref | Expression |
---|---|
quart.a | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
quart.b | ⊢ (𝜑 → 𝐵 ∈ ℂ) |
quart.c | ⊢ (𝜑 → 𝐶 ∈ ℂ) |
quart.d | ⊢ (𝜑 → 𝐷 ∈ ℂ) |
quart.x | ⊢ (𝜑 → 𝑋 ∈ ℂ) |
quart.e | ⊢ (𝜑 → 𝐸 = -(𝐴 / 4)) |
quart.p | ⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2)))) |
quart.q | ⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))) |
quart.r | ⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))) |
quart.u | ⊢ (𝜑 → 𝑈 = ((𝑃↑2) + (;12 · 𝑅))) |
quart.v | ⊢ (𝜑 → 𝑉 = ((-(2 · (𝑃↑3)) − (;27 · (𝑄↑2))) + (;72 · (𝑃 · 𝑅)))) |
quart.w | ⊢ (𝜑 → 𝑊 = (√‘((𝑉↑2) − (4 · (𝑈↑3))))) |
quart.s | ⊢ (𝜑 → 𝑆 = ((√‘𝑀) / 2)) |
quart.m | ⊢ (𝜑 → 𝑀 = -((((2 · 𝑃) + 𝑇) + (𝑈 / 𝑇)) / 3)) |
quart.t | ⊢ (𝜑 → 𝑇 = (((𝑉 + 𝑊) / 2)↑𝑐(1 / 3))) |
quart.t0 | ⊢ (𝜑 → 𝑇 ≠ 0) |
Ref | Expression |
---|---|
quartlem3 | ⊢ (𝜑 → (𝑆 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑇 ∈ ℂ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | quart.s | . . 3 ⊢ (𝜑 → 𝑆 = ((√‘𝑀) / 2)) | |
2 | quart.m | . . . . . 6 ⊢ (𝜑 → 𝑀 = -((((2 · 𝑃) + 𝑇) + (𝑈 / 𝑇)) / 3)) | |
3 | 2cn 11888 | . . . . . . . . . . 11 ⊢ 2 ∈ ℂ | |
4 | quart.a | . . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
5 | quart.b | . . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ ℂ) | |
6 | quart.c | . . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ ℂ) | |
7 | quart.d | . . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐷 ∈ ℂ) | |
8 | quart.p | . . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2)))) | |
9 | quart.q | . . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))) | |
10 | quart.r | . . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))) | |
11 | 4, 5, 6, 7, 8, 9, 10 | quart1cl 25709 | . . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃 ∈ ℂ ∧ 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ)) |
12 | 11 | simp1d 1144 | . . . . . . . . . . 11 ⊢ (𝜑 → 𝑃 ∈ ℂ) |
13 | mulcl 10796 | . . . . . . . . . . 11 ⊢ ((2 ∈ ℂ ∧ 𝑃 ∈ ℂ) → (2 · 𝑃) ∈ ℂ) | |
14 | 3, 12, 13 | sylancr 590 | . . . . . . . . . 10 ⊢ (𝜑 → (2 · 𝑃) ∈ ℂ) |
15 | quart.t | . . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 = (((𝑉 + 𝑊) / 2)↑𝑐(1 / 3))) | |
16 | quart.e | . . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐸 = -(𝐴 / 4)) | |
17 | quart.u | . . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑈 = ((𝑃↑2) + (;12 · 𝑅))) | |
18 | quart.v | . . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑉 = ((-(2 · (𝑃↑3)) − (;27 · (𝑄↑2))) + (;72 · (𝑃 · 𝑅)))) | |
19 | quart.w | . . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑊 = (√‘((𝑉↑2) − (4 · (𝑈↑3))))) | |
20 | 4, 5, 6, 7, 4, 16, 8, 9, 10, 17, 18, 19 | quartlem2 25713 | . . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 ∈ ℂ ∧ 𝑉 ∈ ℂ ∧ 𝑊 ∈ ℂ)) |
21 | 20 | simp2d 1145 | . . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ∈ ℂ) |
22 | 20 | simp3d 1146 | . . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑊 ∈ ℂ) |
23 | 21, 22 | addcld 10835 | . . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑉 + 𝑊) ∈ ℂ) |
24 | 23 | halfcld 12058 | . . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑉 + 𝑊) / 2) ∈ ℂ) |
25 | 3nn 11892 | . . . . . . . . . . . . . 14 ⊢ 3 ∈ ℕ | |
26 | nnrecre 11855 | . . . . . . . . . . . . . 14 ⊢ (3 ∈ ℕ → (1 / 3) ∈ ℝ) | |
27 | 25, 26 | ax-mp 5 | . . . . . . . . . . . . 13 ⊢ (1 / 3) ∈ ℝ |
28 | 27 | recni 10830 | . . . . . . . . . . . 12 ⊢ (1 / 3) ∈ ℂ |
29 | cxpcl 25534 | . . . . . . . . . . . 12 ⊢ ((((𝑉 + 𝑊) / 2) ∈ ℂ ∧ (1 / 3) ∈ ℂ) → (((𝑉 + 𝑊) / 2)↑𝑐(1 / 3)) ∈ ℂ) | |
30 | 24, 28, 29 | sylancl 589 | . . . . . . . . . . 11 ⊢ (𝜑 → (((𝑉 + 𝑊) / 2)↑𝑐(1 / 3)) ∈ ℂ) |
31 | 15, 30 | eqeltrd 2834 | . . . . . . . . . 10 ⊢ (𝜑 → 𝑇 ∈ ℂ) |
32 | 14, 31 | addcld 10835 | . . . . . . . . 9 ⊢ (𝜑 → ((2 · 𝑃) + 𝑇) ∈ ℂ) |
33 | 20 | simp1d 1144 | . . . . . . . . . 10 ⊢ (𝜑 → 𝑈 ∈ ℂ) |
34 | quart.t0 | . . . . . . . . . 10 ⊢ (𝜑 → 𝑇 ≠ 0) | |
35 | 33, 31, 34 | divcld 11591 | . . . . . . . . 9 ⊢ (𝜑 → (𝑈 / 𝑇) ∈ ℂ) |
36 | 32, 35 | addcld 10835 | . . . . . . . 8 ⊢ (𝜑 → (((2 · 𝑃) + 𝑇) + (𝑈 / 𝑇)) ∈ ℂ) |
37 | 3cn 11894 | . . . . . . . . 9 ⊢ 3 ∈ ℂ | |
38 | 37 | a1i 11 | . . . . . . . 8 ⊢ (𝜑 → 3 ∈ ℂ) |
39 | 3ne0 11919 | . . . . . . . . 9 ⊢ 3 ≠ 0 | |
40 | 39 | a1i 11 | . . . . . . . 8 ⊢ (𝜑 → 3 ≠ 0) |
41 | 36, 38, 40 | divcld 11591 | . . . . . . 7 ⊢ (𝜑 → ((((2 · 𝑃) + 𝑇) + (𝑈 / 𝑇)) / 3) ∈ ℂ) |
42 | 41 | negcld 11159 | . . . . . 6 ⊢ (𝜑 → -((((2 · 𝑃) + 𝑇) + (𝑈 / 𝑇)) / 3) ∈ ℂ) |
43 | 2, 42 | eqeltrd 2834 | . . . . 5 ⊢ (𝜑 → 𝑀 ∈ ℂ) |
44 | 43 | sqrtcld 14984 | . . . 4 ⊢ (𝜑 → (√‘𝑀) ∈ ℂ) |
45 | 44 | halfcld 12058 | . . 3 ⊢ (𝜑 → ((√‘𝑀) / 2) ∈ ℂ) |
46 | 1, 45 | eqeltrd 2834 | . 2 ⊢ (𝜑 → 𝑆 ∈ ℂ) |
47 | 46, 43, 31 | 3jca 1130 | 1 ⊢ (𝜑 → (𝑆 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑇 ∈ ℂ)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1089 = wceq 1543 ∈ wcel 2110 ≠ wne 2935 ‘cfv 6369 (class class class)co 7202 ℂcc 10710 ℝcr 10711 0cc0 10712 1c1 10713 + caddc 10715 · cmul 10717 − cmin 11045 -cneg 11046 / cdiv 11472 ℕcn 11813 2c2 11868 3c3 11869 4c4 11870 5c5 11871 6c6 11872 7c7 11873 8c8 11874 ;cdc 12276 ↑cexp 13618 √csqrt 14779 ↑𝑐ccxp 25416 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2706 ax-rep 5168 ax-sep 5181 ax-nul 5188 ax-pow 5247 ax-pr 5311 ax-un 7512 ax-inf2 9245 ax-cnex 10768 ax-resscn 10769 ax-1cn 10770 ax-icn 10771 ax-addcl 10772 ax-addrcl 10773 ax-mulcl 10774 ax-mulrcl 10775 ax-mulcom 10776 ax-addass 10777 ax-mulass 10778 ax-distr 10779 ax-i2m1 10780 ax-1ne0 10781 ax-1rid 10782 ax-rnegex 10783 ax-rrecex 10784 ax-cnre 10785 ax-pre-lttri 10786 ax-pre-lttrn 10787 ax-pre-ltadd 10788 ax-pre-mulgt0 10789 ax-pre-sup 10790 ax-addf 10791 ax-mulf 10792 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2537 df-eu 2566 df-clab 2713 df-cleq 2726 df-clel 2812 df-nfc 2882 df-ne 2936 df-nel 3040 df-ral 3059 df-rex 3060 df-reu 3061 df-rmo 3062 df-rab 3063 df-v 3403 df-sbc 3688 df-csb 3803 df-dif 3860 df-un 3862 df-in 3864 df-ss 3874 df-pss 3876 df-nul 4228 df-if 4430 df-pw 4505 df-sn 4532 df-pr 4534 df-tp 4536 df-op 4538 df-uni 4810 df-int 4850 df-iun 4896 df-iin 4897 df-br 5044 df-opab 5106 df-mpt 5125 df-tr 5151 df-id 5444 df-eprel 5449 df-po 5457 df-so 5458 df-fr 5498 df-se 5499 df-we 5500 df-xp 5546 df-rel 5547 df-cnv 5548 df-co 5549 df-dm 5550 df-rn 5551 df-res 5552 df-ima 5553 df-pred 6149 df-ord 6205 df-on 6206 df-lim 6207 df-suc 6208 df-iota 6327 df-fun 6371 df-fn 6372 df-f 6373 df-f1 6374 df-fo 6375 df-f1o 6376 df-fv 6377 df-isom 6378 df-riota 7159 df-ov 7205 df-oprab 7206 df-mpo 7207 df-of 7458 df-om 7634 df-1st 7750 df-2nd 7751 df-supp 7893 df-wrecs 8036 df-recs 8097 df-rdg 8135 df-1o 8191 df-2o 8192 df-er 8380 df-map 8499 df-pm 8500 df-ixp 8568 df-en 8616 df-dom 8617 df-sdom 8618 df-fin 8619 df-fsupp 8975 df-fi 9016 df-sup 9047 df-inf 9048 df-oi 9115 df-card 9538 df-pnf 10852 df-mnf 10853 df-xr 10854 df-ltxr 10855 df-le 10856 df-sub 11047 df-neg 11048 df-div 11473 df-nn 11814 df-2 11876 df-3 11877 df-4 11878 df-5 11879 df-6 11880 df-7 11881 df-8 11882 df-9 11883 df-n0 12074 df-z 12160 df-dec 12277 df-uz 12422 df-q 12528 df-rp 12570 df-xneg 12687 df-xadd 12688 df-xmul 12689 df-ioo 12922 df-ioc 12923 df-ico 12924 df-icc 12925 df-fz 13079 df-fzo 13222 df-fl 13350 df-mod 13426 df-seq 13558 df-exp 13619 df-fac 13823 df-bc 13852 df-hash 13880 df-shft 14613 df-cj 14645 df-re 14646 df-im 14647 df-sqrt 14781 df-abs 14782 df-limsup 15015 df-clim 15032 df-rlim 15033 df-sum 15233 df-ef 15610 df-sin 15612 df-cos 15613 df-pi 15615 df-struct 16686 df-ndx 16687 df-slot 16688 df-base 16690 df-sets 16691 df-ress 16692 df-plusg 16780 df-mulr 16781 df-starv 16782 df-sca 16783 df-vsca 16784 df-ip 16785 df-tset 16786 df-ple 16787 df-ds 16789 df-unif 16790 df-hom 16791 df-cco 16792 df-rest 16899 df-topn 16900 df-0g 16918 df-gsum 16919 df-topgen 16920 df-pt 16921 df-prds 16924 df-xrs 16979 df-qtop 16984 df-imas 16985 df-xps 16987 df-mre 17061 df-mrc 17062 df-acs 17064 df-mgm 18086 df-sgrp 18135 df-mnd 18146 df-submnd 18191 df-mulg 18461 df-cntz 18683 df-cmn 19144 df-psmet 20327 df-xmet 20328 df-met 20329 df-bl 20330 df-mopn 20331 df-fbas 20332 df-fg 20333 df-cnfld 20336 df-top 21763 df-topon 21780 df-topsp 21802 df-bases 21815 df-cld 21888 df-ntr 21889 df-cls 21890 df-nei 21967 df-lp 22005 df-perf 22006 df-cn 22096 df-cnp 22097 df-haus 22184 df-tx 22431 df-hmeo 22624 df-fil 22715 df-fm 22807 df-flim 22808 df-flf 22809 df-xms 23190 df-ms 23191 df-tms 23192 df-cncf 23747 df-limc 24735 df-dv 24736 df-log 25417 df-cxp 25418 |
This theorem is referenced by: quartlem4 25715 quart 25716 |
Copyright terms: Public domain | W3C validator |