Theorem quartlem3

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

	Ref	Expression
Hypotheses	quart.a	$$⊢\phi \to A\in ℂ$$
	quart.b	$$⊢\phi \to B\in ℂ$$
	quart.c	$$⊢\phi \to C\in ℂ$$
	quart.d	$$⊢\phi \to D\in ℂ$$
	quart.x	$$⊢\phi \to X\in ℂ$$
	quart.e	$$⊢\phi \to E=-\frac{A}{4}$$
	quart.p	$$⊢\phi \to P=B-\left(\frac{3}{8}\right)A^2$$
	quart.q	$$⊢\phi \to Q=C-\left(\frac{AB}{2}\right)+\left(\frac{A^3}{8}\right)$$
	quart.r	$$⊢\phi \to R=\left(D-\left(\frac{CA}{4}\right)\right)+\left(\frac{A^{2}B}{16}\right)-\left(\frac{3}{256}\right)A^4$$
	quart.u	$$⊢\phi \to U=P^2+12R$$
	quart.v	$$⊢\phi \to V=\left(-2P^3\right)-27Q^2+72PR$$
	quart.w	$$⊢\phi \to W=\sqrt{V^2-4U^3}$$
	quart.s	$$⊢\phi \to S=\frac{\sqrt{M}}{2}$$
	quart.m	$$⊢\phi \to M=-\frac{2P+T+\left(\frac{U}{T}\right)}{3}$$
	quart.t	$$⊢\phi \to T={\left(\frac{V+W}{2}\right)}^{\frac{1}{3}}$$
	quart.t0	$$⊢\phi \to T\ne 0$$
Assertion	quartlem3	$$⊢\phi \to \left(S\in ℂ\wedge M\in ℂ\wedge T\in ℂ\right)$$

Proof

Step	Hyp	Ref	Expression
1		quart.a	$$⊢\phi \to A\in ℂ$$
2		quart.b	$$⊢\phi \to B\in ℂ$$
3		quart.c	$$⊢\phi \to C\in ℂ$$
4		quart.d	$$⊢\phi \to D\in ℂ$$
5		quart.x	$$⊢\phi \to X\in ℂ$$
6		quart.e	$$⊢\phi \to E=-\frac{A}{4}$$
7		quart.p	$$⊢\phi \to P=B-\left(\frac{3}{8}\right)A^2$$
8		quart.q	$$⊢\phi \to Q=C-\left(\frac{AB}{2}\right)+\left(\frac{A^3}{8}\right)$$
9		quart.r	$$⊢\phi \to R=\left(D-\left(\frac{CA}{4}\right)\right)+\left(\frac{A^{2}B}{16}\right)-\left(\frac{3}{256}\right)A^4$$
10		quart.u	$$⊢\phi \to U=P^2+12R$$
11		quart.v	$$⊢\phi \to V=\left(-2P^3\right)-27Q^2+72PR$$
12		quart.w	$$⊢\phi \to W=\sqrt{V^2-4U^3}$$
13		quart.s	$$⊢\phi \to S=\frac{\sqrt{M}}{2}$$
14		quart.m	$$⊢\phi \to M=-\frac{2P+T+\left(\frac{U}{T}\right)}{3}$$
15		quart.t	$$⊢\phi \to T={\left(\frac{V+W}{2}\right)}^{\frac{1}{3}}$$
16		quart.t0	$$⊢\phi \to T\ne 0$$
17		2cn	$$⊢2\in ℂ$$
18	1 2 3 4 7 8 9	quart1cl	$$⊢\phi \to \left(P\in ℂ\wedge Q\in ℂ\wedge R\in ℂ\right)$$
19	18	simp1d	$$⊢\phi \to P\in ℂ$$
20		mulcl	$$⊢\left(2\in ℂ\wedge P\in ℂ\right)\to 2P\in ℂ$$
21	17 19 20	sylancr	$$⊢\phi \to 2P\in ℂ$$
22	1 2 3 4 1 6 7 8 9 10 11 12	quartlem2	$$⊢\phi \to \left(U\in ℂ\wedge V\in ℂ\wedge W\in ℂ\right)$$
23	22	simp2d	$$⊢\phi \to V\in ℂ$$
24	22	simp3d	$$⊢\phi \to W\in ℂ$$
25	23 24	addcld	$$⊢\phi \to V+W\in ℂ$$
26	25	halfcld	$$⊢\phi \to \frac{V+W}{2}\in ℂ$$
27		3nn	$$⊢3\in \mathbb{N}$$
28		nnrecre	$$⊢3\in \mathbb{N}\to \frac{1}{3}\in ℝ$$
29	27 28	ax-mp	$$⊢\frac{1}{3}\in ℝ$$
30	29	recni	$$⊢\frac{1}{3}\in ℂ$$
31		cxpcl	$$⊢\left(\frac{V+W}{2}\in ℂ\wedge \frac{1}{3}\in ℂ\right)\to {\left(\frac{V+W}{2}\right)}^{\frac{1}{3}}\in ℂ$$
32	26 30 31	sylancl	$$⊢\phi \to {\left(\frac{V+W}{2}\right)}^{\frac{1}{3}}\in ℂ$$
33	15 32	eqeltrd	$$⊢\phi \to T\in ℂ$$
34	21 33	addcld	$$⊢\phi \to 2P+T\in ℂ$$
35	22	simp1d	$$⊢\phi \to U\in ℂ$$
36	35 33 16	divcld	$$⊢\phi \to \frac{U}{T}\in ℂ$$
37	34 36	addcld	$$⊢\phi \to 2P+T+\left(\frac{U}{T}\right)\in ℂ$$
38		3cn	$$⊢3\in ℂ$$
39	38	a1i	$$⊢\phi \to 3\in ℂ$$
40		3ne0	$$⊢3\ne 0$$
41	40	a1i	$$⊢\phi \to 3\ne 0$$
42	37 39 41	divcld	$$⊢\phi \to \frac{2P+T+\left(\frac{U}{T}\right)}{3}\in ℂ$$
43	42	negcld	$$⊢\phi \to -\frac{2P+T+\left(\frac{U}{T}\right)}{3}\in ℂ$$
44	14 43	eqeltrd	$$⊢\phi \to M\in ℂ$$
45	44	sqrtcld	$$⊢\phi \to \sqrt{M}\in ℂ$$
46	45	halfcld	$$⊢\phi \to \frac{\sqrt{M}}{2}\in ℂ$$
47	13 46	eqeltrd	$$⊢\phi \to S\in ℂ$$
48	47 44 33	3jca	$$⊢\phi \to \left(S\in ℂ\wedge M\in ℂ\wedge T\in ℂ\right)$$