Theorem quart1cl

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

	Ref	Expression
Hypotheses	quart1.a	$$⊢\phi \to A\in ℂ$$
	quart1.b	$$⊢\phi \to B\in ℂ$$
	quart1.c	$$⊢\phi \to C\in ℂ$$
	quart1.d	$$⊢\phi \to D\in ℂ$$
	quart1.p	$$⊢\phi \to P=B-\left(\frac{3}{8}\right)A^2$$
	quart1.q	$$⊢\phi \to Q=C-\left(\frac{AB}{2}\right)+\left(\frac{A^3}{8}\right)$$
	quart1.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$$
Assertion	quart1cl	$$⊢\phi \to \left(P\in ℂ\wedge Q\in ℂ\wedge R\in ℂ\right)$$

Proof

Step	Hyp	Ref	Expression
1		quart1.a	$$⊢\phi \to A\in ℂ$$
2		quart1.b	$$⊢\phi \to B\in ℂ$$
3		quart1.c	$$⊢\phi \to C\in ℂ$$
4		quart1.d	$$⊢\phi \to D\in ℂ$$
5		quart1.p	$$⊢\phi \to P=B-\left(\frac{3}{8}\right)A^2$$
6		quart1.q	$$⊢\phi \to Q=C-\left(\frac{AB}{2}\right)+\left(\frac{A^3}{8}\right)$$
7		quart1.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$$
8		3cn	$$⊢3\in ℂ$$
9		8cn	$$⊢8\in ℂ$$
10		8nn	$$⊢8\in \mathbb{N}$$
11	10	nnne0i	$$⊢8\ne 0$$
12	8 9 11	divcli	$$⊢\frac{3}{8}\in ℂ$$
13	1	sqcld	$$⊢\phi \to A^2\in ℂ$$
14		mulcl	$$⊢\left(\frac{3}{8}\in ℂ\wedge A^2\in ℂ\right)\to \left(\frac{3}{8}\right)A^2\in ℂ$$
15	12 13 14	sylancr	$$⊢\phi \to \left(\frac{3}{8}\right)A^2\in ℂ$$
16	2 15	subcld	$$⊢\phi \to B-\left(\frac{3}{8}\right)A^2\in ℂ$$
17	5 16	eqeltrd	$$⊢\phi \to P\in ℂ$$
18	1 2	mulcld	$$⊢\phi \to AB\in ℂ$$
19	18	halfcld	$$⊢\phi \to \frac{AB}{2}\in ℂ$$
20	3 19	subcld	$$⊢\phi \to C-\left(\frac{AB}{2}\right)\in ℂ$$
21		3nn0	$$⊢3\in {\mathbb{N}}_0$$
22		expcl	$$⊢\left(A\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to A^3\in ℂ$$
23	1 21 22	sylancl	$$⊢\phi \to A^3\in ℂ$$
24	9	a1i	$$⊢\phi \to 8\in ℂ$$
25	11	a1i	$$⊢\phi \to 8\ne 0$$
26	23 24 25	divcld	$$⊢\phi \to \frac{A^3}{8}\in ℂ$$
27	20 26	addcld	$$⊢\phi \to C-\left(\frac{AB}{2}\right)+\left(\frac{A^3}{8}\right)\in ℂ$$
28	6 27	eqeltrd	$$⊢\phi \to Q\in ℂ$$
29	3 1	mulcld	$$⊢\phi \to CA\in ℂ$$
30		4cn	$$⊢4\in ℂ$$
31	30	a1i	$$⊢\phi \to 4\in ℂ$$
32		4ne0	$$⊢4\ne 0$$
33	32	a1i	$$⊢\phi \to 4\ne 0$$
34	29 31 33	divcld	$$⊢\phi \to \frac{CA}{4}\in ℂ$$
35	4 34	subcld	$$⊢\phi \to D-\left(\frac{CA}{4}\right)\in ℂ$$
36	13 2	mulcld	$$⊢\phi \to A^{2}B\in ℂ$$
37		1nn0	$$⊢1\in {\mathbb{N}}_0$$
38		6nn	$$⊢6\in \mathbb{N}$$
39	37 38	decnncl	$$⊢16\in \mathbb{N}$$
40	39	nncni	$$⊢16\in ℂ$$
41	40	a1i	$$⊢\phi \to 16\in ℂ$$
42	39	nnne0i	$$⊢16\ne 0$$
43	42	a1i	$$⊢\phi \to 16\ne 0$$
44	36 41 43	divcld	$$⊢\phi \to \frac{A^{2}B}{16}\in ℂ$$
45		25nn0	$$⊢25\in {\mathbb{N}}_0$$
46	45 38	decnncl	$$⊢256\in \mathbb{N}$$
47	46	nncni	$$⊢256\in ℂ$$
48	46	nnne0i	$$⊢256\ne 0$$
49	8 47 48	divcli	$$⊢\frac{3}{256}\in ℂ$$
50		4nn0	$$⊢4\in {\mathbb{N}}_0$$
51		expcl	$$⊢\left(A\in ℂ\wedge 4\in {\mathbb{N}}_0\right)\to A^4\in ℂ$$
52	1 50 51	sylancl	$$⊢\phi \to A^4\in ℂ$$
53		mulcl	$$⊢\left(\frac{3}{256}\in ℂ\wedge A^4\in ℂ\right)\to \left(\frac{3}{256}\right)A^4\in ℂ$$
54	49 52 53	sylancr	$$⊢\phi \to \left(\frac{3}{256}\right)A^4\in ℂ$$
55	44 54	subcld	$$⊢\phi \to \left(\frac{A^{2}B}{16}\right)-\left(\frac{3}{256}\right)A^4\in ℂ$$
56	35 55	addcld	$$⊢\phi \to \left(D-\left(\frac{CA}{4}\right)\right)+\left(\frac{A^{2}B}{16}\right)-\left(\frac{3}{256}\right)A^4\in ℂ$$
57	7 56	eqeltrd	$$⊢\phi \to R\in ℂ$$
58	17 28 57	3jca	$$⊢\phi \to \left(P\in ℂ\wedge Q\in ℂ\wedge R\in ℂ\right)$$