quartlem4 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > quartlem4		Structured version Visualization version GIF version

Theorem quartlem4 27221

Description: Closure lemmas for quart 27222. (Contributed by Mario Carneiro, 7-May-2015.)

**Hypotheses**
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)
quart.m0	⊢ (𝜑 → 𝑀 ≠ 0)
quart.i	⊢ (𝜑 → 𝐼 = (√‘(( -(𝑆↑2) − (𝑃 / 2)) + ((𝑄 / 4) / 𝑆))))
quart.j	⊢ (𝜑 → 𝐽 = (√‘(( -(𝑆↑2) − (𝑃 / 2)) − ((𝑄 / 4) / 𝑆))))

**Assertion**
Ref	Expression
quartlem4	⊢ (𝜑 → (𝑆 ≠ 0 ∧ 𝐼 ∈ ℂ ∧ 𝐽 ∈ ℂ))

**Proof of Theorem quartlem4**
Step	Hyp	Ref	Expression
1		quart.s	. . 3 ⊢ (𝜑 → 𝑆 = ((√‘𝑀) / 2))
2		quart.a	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
3		quart.b	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
4		quart.c	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ ℂ)
5		quart.d	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ ℂ)
6		quart.e	. . . . . . 7 ⊢ (𝜑 → 𝐸 = -(𝐴 / 4))
7		quart.p	. . . . . . 7 ⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2))))
8		quart.q	. . . . . . 7 ⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)))
9		quart.r	. . . . . . 7 ⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))
10		quart.u	. . . . . . 7 ⊢ (𝜑 → 𝑈 = ((𝑃↑2) + (;12 · 𝑅)))
11		quart.v	. . . . . . 7 ⊢ (𝜑 → 𝑉 = (( -(2 · (𝑃↑3)) − (;27 · (𝑄↑2))) + (;72 · (𝑃 · 𝑅))))
12		quart.w	. . . . . . 7 ⊢ (𝜑 → 𝑊 = (√‘((𝑉↑2) − (4 · (𝑈↑3)))))
13		quart.m	. . . . . . 7 ⊢ (𝜑 → 𝑀 = -((((2 · 𝑃) + 𝑇) + (𝑈 / 𝑇)) / 3))
14		quart.t	. . . . . . 7 ⊢ (𝜑 → 𝑇 = (((𝑉 + 𝑊) / 2)↑_𝑐(1 / 3)))
15		quart.t0	. . . . . . 7 ⊢ (𝜑 → 𝑇 ≠ 0)
16	2, 3, 4, 5, 2, 6, 7, 8, 9, 10, 11, 12, 1, 13, 14, 15	quartlem3 27220	. . . . . 6 ⊢ (𝜑 → (𝑆 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑇 ∈ ℂ))
17	16	simp2d 1161	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ ℂ)
18	17	sqrtcld 15639	. . . 4 ⊢ (𝜑 → (√‘𝑀) ∈ ℂ)
19		2cnd 12451	. . . 4 ⊢ (𝜑 → 2 ∈ ℂ)
20	17	sqsqrtd 15641	. . . . . 6 ⊢ (𝜑 → ((√‘𝑀)↑2) = 𝑀)
21		quart.m0	. . . . . 6 ⊢ (𝜑 → 𝑀 ≠ 0)
22	20, 21	eqnetrd 3026	. . . . 5 ⊢ (𝜑 → ((√‘𝑀)↑2) ≠ 0)
23		sqne0 14296	. . . . . 6 ⊢ ((√‘𝑀) ∈ ℂ → (((√‘𝑀)↑2) ≠ 0 ↔ (√‘𝑀) ≠ 0))
24	18, 23	syl 18	. . . . 5 ⊢ (𝜑 → (((√‘𝑀)↑2) ≠ 0 ↔ (√‘𝑀) ≠ 0))
25	22, 24	mpbid 235	. . . 4 ⊢ (𝜑 → (√‘𝑀) ≠ 0)
26		2ne0 12479	. . . . 5 ⊢ 2 ≠ 0
27	26	a1i 11	. . . 4 ⊢ (𝜑 → 2 ≠ 0)
28	18, 19, 25, 27	divne0d 12139	. . 3 ⊢ (𝜑 → ((√‘𝑀) / 2) ≠ 0)
29	1, 28	eqnetrd 3026	. 2 ⊢ (𝜑 → 𝑆 ≠ 0)
30		quart.i	. . 3 ⊢ (𝜑 → 𝐼 = (√‘(( -(𝑆↑2) − (𝑃 / 2)) + ((𝑄 / 4) / 𝑆))))
31	16	simp1d 1160	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ∈ ℂ)
32	31	sqcld 14317	. . . . . . 7 ⊢ (𝜑 → (𝑆↑2) ∈ ℂ)
33	32	negcld 11686	. . . . . 6 ⊢ (𝜑 → -(𝑆↑2) ∈ ℂ)
34	2, 3, 4, 5, 7, 8, 9	quart1cl 27215	. . . . . . . 8 ⊢ (𝜑 → (𝑃 ∈ ℂ ∧ 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ))
35	34	simp1d 1160	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ ℂ)
36	35	halfcld 12621	. . . . . 6 ⊢ (𝜑 → (𝑃 / 2) ∈ ℂ)
37	33, 36	subcld 11699	. . . . 5 ⊢ (𝜑 → ( -(𝑆↑2) − (𝑃 / 2)) ∈ ℂ)
38	34	simp2d 1161	. . . . . . 7 ⊢ (𝜑 → 𝑄 ∈ ℂ)
39		4cn 12458	. . . . . . . 8 ⊢ 4 ∈ ℂ
40	39	a1i 11	. . . . . . 7 ⊢ (𝜑 → 4 ∈ ℂ)
41		4ne0 12484	. . . . . . . 8 ⊢ 4 ≠ 0
42	41	a1i 11	. . . . . . 7 ⊢ (𝜑 → 4 ≠ 0)
43	38, 40, 42	divcld 12123	. . . . . 6 ⊢ (𝜑 → (𝑄 / 4) ∈ ℂ)
44	43, 31, 29	divcld 12123	. . . . 5 ⊢ (𝜑 → ((𝑄 / 4) / 𝑆) ∈ ℂ)
45	37, 44	addcld 11358	. . . 4 ⊢ (𝜑 → (( -(𝑆↑2) − (𝑃 / 2)) + ((𝑄 / 4) / 𝑆)) ∈ ℂ)
46	45	sqrtcld 15639	. . 3 ⊢ (𝜑 → (√‘(( -(𝑆↑2) − (𝑃 / 2)) + ((𝑄 / 4) / 𝑆))) ∈ ℂ)
47	30, 46	eqeltrd 2864	. 2 ⊢ (𝜑 → 𝐼 ∈ ℂ)
48		quart.j	. . 3 ⊢ (𝜑 → 𝐽 = (√‘(( -(𝑆↑2) − (𝑃 / 2)) − ((𝑄 / 4) / 𝑆))))
49	37, 44	subcld 11699	. . . 4 ⊢ (𝜑 → (( -(𝑆↑2) − (𝑃 / 2)) − ((𝑄 / 4) / 𝑆)) ∈ ℂ)
50	49	sqrtcld 15639	. . 3 ⊢ (𝜑 → (√‘(( -(𝑆↑2) − (𝑃 / 2)) − ((𝑄 / 4) / 𝑆))) ∈ ℂ)
51	48, 50	eqeltrd 2864	. 2 ⊢ (𝜑 → 𝐽 ∈ ℂ)
52	29, 47, 51	3jca 1146	1 ⊢ (𝜑 → (𝑆 ≠ 0 ∧ 𝐼 ∈ ℂ ∧ 𝐽 ∈ ℂ))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ w3a 1103 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ‘cfv 6561 (class class class)co 7446 ℂcc 11228 0cc0 11230 1c1 11231 + caddc 11233 · cmul 11235 − cmin 11571 -cneg 11572 / cdiv 12003 2c2 12427 3c3 12428 4c4 12429 5c5 12430 6c6 12431 7c7 12432 8c8 12433 cdc 12844 ↑cexp 14234 √csqrt 15432 ↑_𝑐ccxp 26916

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5236 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7778 ax-inf2 9672 ax-cnex 11286 ax-resscn 11287 ax-1cn 11288 ax-icn 11289 ax-addcl 11290 ax-addrcl 11291 ax-mulcl 11292 ax-mulrcl 11293 ax-mulcom 11294 ax-addass 11295 ax-mulass 11296 ax-distr 11297 ax-i2m1 11298 ax-1ne0 11299 ax-1rid 11300 ax-rnegex 11301 ax-rrecex 11302 ax-cnre 11303 ax-pre-lttri 11304 ax-pre-lttrn 11305 ax-pre-ltadd 11306 ax-pre-mulgt0 11307 ax-pre-sup 11308 ax-addf 11309

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-se 5610 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-pred 6325 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6515 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-isom 6570 df-riota 7403 df-ov 7449 df-oprab 7450 df-mpo 7451 df-of 7720 df-om 7905 df-1st 8028 df-2nd 8029 df-supp 8208 df-frecs 8330 df-wrecs 8361 df-recs 8410 df-rdg 8449 df-1o 8507 df-2o 8508 df-er 8748 df-map 8880 df-pm 8881 df-ixp 8957 df-en 9005 df-dom 9006 df-sdom 9007 df-fin 9008 df-fsupp 9385 df-fi 9433 df-sup 9464 df-inf 9465 df-oi 9534 df-card 10050 df-pnf 11375 df-mnf 11376 df-xr 11377 df-ltxr 11378 df-le 11379 df-sub 11573 df-neg 11574 df-div 12004 df-nn 12366 df-2 12435 df-3 12436 df-4 12437 df-5 12438 df-6 12439 df-7 12440 df-8 12441 df-9 12442 df-n0 12637 df-z 12724 df-dec 12845 df-uz 12996 df-q 13106 df-rp 13151 df-xneg 13271 df-xadd 13272 df-xmul 13273 df-ioo 13510 df-ioc 13511 df-ico 13512 df-icc 13513 df-fz 13670 df-fzo 13819 df-fl 13962 df-mod 14040 df-seq 14175 df-exp 14235 df-fac 14448 df-bc 14477 df-hash 14505 df-shft 15252 df-cj 15298 df-re 15299 df-im 15300 df-sqrt 15434 df-abs 15435 df-limsup 15670 df-clim 15687 df-rlim 15688 df-sum 15886 df-ef 16265 df-sin 16267 df-cos 16268 df-pi 16270 df-struct 17357 df-sets 17374 df-slot 17392 df-ndx 17404 df-base 17420 df-ress 17441 df-plusg 17473 df-mulr 17474 df-starv 17475 df-sca 17476 df-vsca 17477 df-ip 17478 df-tset 17479 df-ple 17480 df-ds 17482 df-unif 17483 df-hom 17484 df-cco 17485 df-rest 17625 df-topn 17626 df-0g 17644 df-gsum 17645 df-topgen 17646 df-pt 17647 df-prds 17650 df-xrs 17706 df-qtop 17711 df-imas 17712 df-xps 17714 df-mre 17788 df-mrc 17789 df-acs 17791 df-mgm 18848 df-sgrp 18940 df-mnd 18956 df-submnd 19011 df-mulg 19310 df-cntz 19564 df-cmn 20029 df-psmet 21703 df-xmet 21704 df-met 21705 df-bl 21706 df-mopn 21707 df-fbas 21708 df-fg 21709 df-cnfld 21712 df-top 23245 df-topon 23262 df-topsp 23284 df-bases 23297 df-cld 23370 df-ntr 23371 df-cls 23372 df-nei 23449 df-lp 23487 df-perf 23488 df-cn 23578 df-cnp 23579 df-haus 23666 df-tx 23914 df-hmeo 24107 df-fil 24198 df-fm 24290 df-flim 24291 df-flf 24292 df-xms 24672 df-ms 24673 df-tms 24674 df-cncf 25232 df-limc 26219 df-dv 26220 df-log 26917 df-cxp 26918

This theorem is used by: quart 27222

W3C validator