quartlem4

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

	Ref	Expression
Hypotheses	quart.a	$⊢ φ \to A \in ℂ$
	quart.b	$⊢ φ \to B \in ℂ$
	quart.c	$⊢ φ \to C \in ℂ$
	quart.d	$⊢ φ \to D \in ℂ$
	quart.x	$⊢ φ \to X \in ℂ$
	quart.e	$⊢ φ \to E = - \frac{A}{4}$
	quart.p	$⊢ φ \to P = B - (\frac{3}{8}) A^{2}$
	quart.q	$⊢ φ \to Q = C - (\frac{A B}{2}) + (\frac{A^{3}}{8})$
	quart.r	$⊢ φ \to R = (D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}$
	quart.u	$⊢ φ \to U = P^{2} + 12 R$
	quart.v	$⊢ φ \to V = (- 2 P^{3}) - 27 Q^{2} + 72 P R$
	quart.w	$⊢ φ \to W = \sqrt{V^{2} - 4 U^{3}}$
	quart.s	$⊢ φ \to S = \frac{\sqrt{M}}{2}$
	quart.m	$⊢ φ \to M = - \frac{2 P + T + (\frac{U}{T})}{3}$
	quart.t	$⊢ φ \to T = {(\frac{V + W}{2})}^{\frac{1}{3}}$
	quart.t0	$⊢ φ \to T \neq 0$
	quart.m0	$⊢ φ \to M \neq 0$
	quart.i	$⊢ φ \to I = \sqrt{(- S^{2}) - (\frac{P}{2}) + (\frac{\frac{Q}{4}}{S})}$
	quart.j	$⊢ φ \to J = \sqrt{(- S^{2}) - (\frac{P}{2}) - (\frac{\frac{Q}{4}}{S})}$
Assertion	quartlem4	$⊢ φ \to (S \neq 0 \land I \in ℂ \land J \in ℂ)$

Proof

Step	Hyp	Ref	Expression
1		quart.a	$⊢ φ \to A \in ℂ$
2		quart.b	$⊢ φ \to B \in ℂ$
3		quart.c	$⊢ φ \to C \in ℂ$
4		quart.d	$⊢ φ \to D \in ℂ$
5		quart.x	$⊢ φ \to X \in ℂ$
6		quart.e	$⊢ φ \to E = - \frac{A}{4}$
7		quart.p	$⊢ φ \to P = B - (\frac{3}{8}) A^{2}$
8		quart.q	$⊢ φ \to Q = C - (\frac{A B}{2}) + (\frac{A^{3}}{8})$
9		quart.r	$⊢ φ \to R = (D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}$
10		quart.u	$⊢ φ \to U = P^{2} + 12 R$
11		quart.v	$⊢ φ \to V = (- 2 P^{3}) - 27 Q^{2} + 72 P R$
12		quart.w	$⊢ φ \to W = \sqrt{V^{2} - 4 U^{3}}$
13		quart.s	$⊢ φ \to S = \frac{\sqrt{M}}{2}$
14		quart.m	$⊢ φ \to M = - \frac{2 P + T + (\frac{U}{T})}{3}$
15		quart.t	$⊢ φ \to T = {(\frac{V + W}{2})}^{\frac{1}{3}}$
16		quart.t0	$⊢ φ \to T \neq 0$
17		quart.m0	$⊢ φ \to M \neq 0$
18		quart.i	$⊢ φ \to I = \sqrt{(- S^{2}) - (\frac{P}{2}) + (\frac{\frac{Q}{4}}{S})}$
19		quart.j	$⊢ φ \to J = \sqrt{(- S^{2}) - (\frac{P}{2}) - (\frac{\frac{Q}{4}}{S})}$
20	1 2 3 4 1 6 7 8 9 10 11 12 13 14 15 16	quartlem3	$⊢ φ \to (S \in ℂ \land M \in ℂ \land T \in ℂ)$
21	20	simp2d	$⊢ φ \to M \in ℂ$
22	21	sqrtcld	$⊢ φ \to \sqrt{M} \in ℂ$
23		2cnd	$⊢ φ \to 2 \in ℂ$
24	21	sqsqrtd	$⊢ φ \to {\sqrt{M}}^{2} = M$
25	24 17	eqnetrd	$⊢ φ \to {\sqrt{M}}^{2} \neq 0$
26		sqne0	$⊢ \sqrt{M} \in ℂ \to ({\sqrt{M}}^{2} \neq 0 \leftrightarrow \sqrt{M} \neq 0)$
27	22 26	syl	$⊢ φ \to ({\sqrt{M}}^{2} \neq 0 \leftrightarrow \sqrt{M} \neq 0)$
28	25 27	mpbid	$⊢ φ \to \sqrt{M} \neq 0$
29		2ne0	$⊢ 2 \neq 0$
30	29	a1i	$⊢ φ \to 2 \neq 0$
31	22 23 28 30	divne0d	$⊢ φ \to \frac{\sqrt{M}}{2} \neq 0$
32	13 31	eqnetrd	$⊢ φ \to S \neq 0$
33	20	simp1d	$⊢ φ \to S \in ℂ$
34	33	sqcld	$⊢ φ \to S^{2} \in ℂ$
35	34	negcld	$⊢ φ \to - S^{2} \in ℂ$
36	1 2 3 4 7 8 9	quart1cl	$⊢ φ \to (P \in ℂ \land Q \in ℂ \land R \in ℂ)$
37	36	simp1d	$⊢ φ \to P \in ℂ$
38	37	halfcld	$⊢ φ \to \frac{P}{2} \in ℂ$
39	35 38	subcld	$⊢ φ \to - S^{2} - (\frac{P}{2}) \in ℂ$
40	36	simp2d	$⊢ φ \to Q \in ℂ$
41		4cn	$⊢ 4 \in ℂ$
42	41	a1i	$⊢ φ \to 4 \in ℂ$
43		4ne0	$⊢ 4 \neq 0$
44	43	a1i	$⊢ φ \to 4 \neq 0$
45	40 42 44	divcld	$⊢ φ \to \frac{Q}{4} \in ℂ$
46	45 33 32	divcld	$⊢ φ \to \frac{\frac{Q}{4}}{S} \in ℂ$
47	39 46	addcld	$⊢ φ \to (- S^{2}) - (\frac{P}{2}) + (\frac{\frac{Q}{4}}{S}) \in ℂ$
48	47	sqrtcld	$⊢ φ \to \sqrt{(- S^{2}) - (\frac{P}{2}) + (\frac{\frac{Q}{4}}{S})} \in ℂ$
49	18 48	eqeltrd	$⊢ φ \to I \in ℂ$
50	39 46	subcld	$⊢ φ \to (- S^{2}) - (\frac{P}{2}) - (\frac{\frac{Q}{4}}{S}) \in ℂ$
51	50	sqrtcld	$⊢ φ \to \sqrt{(- S^{2}) - (\frac{P}{2}) - (\frac{\frac{Q}{4}}{S})} \in ℂ$
52	19 51	eqeltrd	$⊢ φ \to J \in ℂ$
53	32 49 52	3jca	$⊢ φ \to (S \neq 0 \land I \in ℂ \land J \in ℂ)$

Metamath Proof Explorer

Theorem quartlem4

Proof