Theorem quartlem2

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}$$
Assertion	quartlem2	$$⊢\phi \to \left(U\in ℂ\wedge V\in ℂ\wedge W\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	1 2 3 4 7 8 9	quart1cl	$$⊢\phi \to \left(P\in ℂ\wedge Q\in ℂ\wedge R\in ℂ\right)$$
14	13	simp1d	$$⊢\phi \to P\in ℂ$$
15	14	sqcld	$$⊢\phi \to P^2\in ℂ$$
16		1nn0	$$⊢1\in {\mathbb{N}}_0$$
17		2nn	$$⊢2\in \mathbb{N}$$
18	16 17	decnncl	$$⊢12\in \mathbb{N}$$
19	18	nncni	$$⊢12\in ℂ$$
20	13	simp3d	$$⊢\phi \to R\in ℂ$$
21		mulcl	$$⊢\left(12\in ℂ\wedge R\in ℂ\right)\to 12R\in ℂ$$
22	19 20 21	sylancr	$$⊢\phi \to 12R\in ℂ$$
23	15 22	addcld	$$⊢\phi \to P^2+12R\in ℂ$$
24	10 23	eqeltrd	$$⊢\phi \to U\in ℂ$$
25		2cn	$$⊢2\in ℂ$$
26		3nn0	$$⊢3\in {\mathbb{N}}_0$$
27		expcl	$$⊢\left(P\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to P^3\in ℂ$$
28	14 26 27	sylancl	$$⊢\phi \to P^3\in ℂ$$
29		mulcl	$$⊢\left(2\in ℂ\wedge P^3\in ℂ\right)\to 2P^3\in ℂ$$
30	25 28 29	sylancr	$$⊢\phi \to 2P^3\in ℂ$$
31	30	negcld	$$⊢\phi \to -2P^3\in ℂ$$
32		2nn0	$$⊢2\in {\mathbb{N}}_0$$
33		7nn	$$⊢7\in \mathbb{N}$$
34	32 33	decnncl	$$⊢27\in \mathbb{N}$$
35	34	nncni	$$⊢27\in ℂ$$
36	13	simp2d	$$⊢\phi \to Q\in ℂ$$
37	36	sqcld	$$⊢\phi \to Q^2\in ℂ$$
38		mulcl	$$⊢\left(27\in ℂ\wedge Q^2\in ℂ\right)\to 27Q^2\in ℂ$$
39	35 37 38	sylancr	$$⊢\phi \to 27Q^2\in ℂ$$
40	31 39	subcld	$$⊢\phi \to -2P^3-27Q^2\in ℂ$$
41		7nn0	$$⊢7\in {\mathbb{N}}_0$$
42	41 17	decnncl	$$⊢72\in \mathbb{N}$$
43	42	nncni	$$⊢72\in ℂ$$
44	14 20	mulcld	$$⊢\phi \to PR\in ℂ$$
45		mulcl	$$⊢\left(72\in ℂ\wedge PR\in ℂ\right)\to 72PR\in ℂ$$
46	43 44 45	sylancr	$$⊢\phi \to 72PR\in ℂ$$
47	40 46	addcld	$$⊢\phi \to \left(-2P^3\right)-27Q^2+72PR\in ℂ$$
48	11 47	eqeltrd	$$⊢\phi \to V\in ℂ$$
49	48	sqcld	$$⊢\phi \to V^2\in ℂ$$
50		4cn	$$⊢4\in ℂ$$
51		expcl	$$⊢\left(U\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to U^3\in ℂ$$
52	24 26 51	sylancl	$$⊢\phi \to U^3\in ℂ$$
53		mulcl	$$⊢\left(4\in ℂ\wedge U^3\in ℂ\right)\to 4U^3\in ℂ$$
54	50 52 53	sylancr	$$⊢\phi \to 4U^3\in ℂ$$
55	49 54	subcld	$$⊢\phi \to V^2-4U^3\in ℂ$$
56	55	sqrtcld	$$⊢\phi \to \sqrt{V^2-4U^3}\in ℂ$$
57	12 56	eqeltrd	$$⊢\phi \to W\in ℂ$$
58	24 48 57	3jca	$$⊢\phi \to \left(U\in ℂ\wedge V\in ℂ\wedge W\in ℂ\right)$$