Theorem quartlem1

Description: Lemma for quart . (Contributed by Mario Carneiro, 6-May-2015)

	Ref	Expression
Hypotheses	quartlem1.p	$$⊢\phi \to P\in ℂ$$
	quartlem1.q	$$⊢\phi \to Q\in ℂ$$
	quartlem1.r	$$⊢\phi \to R\in ℂ$$
	quartlem1.u	$$⊢\phi \to U=P^2+12R$$
	quartlem1.v	$$⊢\phi \to V=\left(-2P^3\right)-27Q^2+72PR$$
Assertion	quartlem1	$$⊢\phi \to \left(U={2P}^2-3\left(P^2-4R\right)\wedge V=2{2P}^3-92P\left(P^2-4R\right)+27\left(-Q^2\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		quartlem1.p	$$⊢\phi \to P\in ℂ$$
2		quartlem1.q	$$⊢\phi \to Q\in ℂ$$
3		quartlem1.r	$$⊢\phi \to R\in ℂ$$
4		quartlem1.u	$$⊢\phi \to U=P^2+12R$$
5		quartlem1.v	$$⊢\phi \to V=\left(-2P^3\right)-27Q^2+72PR$$
6		2cn	$$⊢2\in ℂ$$
7		sqmul	$$⊢\left(2\in ℂ\wedge P\in ℂ\right)\to {2P}^2=2^2{P}^2$$
8	6 1 7	sylancr	$$⊢\phi \to {2P}^2=2^2{P}^2$$
9		sq2	$$⊢2^2=4$$
10	9	oveq1i	$$⊢2^2{P}^2=4P^2$$
11	8 10	eqtrdi	$$⊢\phi \to {2P}^2=4P^2$$
12	11	oveq1d	$$⊢\phi \to {2P}^2-3P^2=4P^2-3P^2$$
13		4cn	$$⊢4\in ℂ$$
14	13	a1i	$$⊢\phi \to 4\in ℂ$$
15		3cn	$$⊢3\in ℂ$$
16	15	a1i	$$⊢\phi \to 3\in ℂ$$
17	1	sqcld	$$⊢\phi \to P^2\in ℂ$$
18	14 16 17	subdird	$$⊢\phi \to \left(4-3\right)P^2=4P^2-3P^2$$
19	12 18	eqtr4d	$$⊢\phi \to {2P}^2-3P^2=\left(4-3\right)P^2$$
20		ax-1cn	$$⊢1\in ℂ$$
21		3p1e4	$$⊢3+1=4$$
22	13 15 20 21	subaddrii	$$⊢4-3=1$$
23	22	oveq1i	$$⊢\left(4-3\right)P^2=1P^2$$
24		mullid	$$⊢P^2\in ℂ\to 1P^2=P^2$$
25	23 24	eqtrid	$$⊢P^2\in ℂ\to \left(4-3\right)P^2=P^2$$
26	17 25	syl	$$⊢\phi \to \left(4-3\right)P^2=P^2$$
27	19 26	eqtr2d	$$⊢\phi \to P^2={2P}^2-3P^2$$
28	27	oveq1d	$$⊢\phi \to P^2+12R={2P}^2-3P^2+12R$$
29		mulcl	$$⊢\left(2\in ℂ\wedge P\in ℂ\right)\to 2P\in ℂ$$
30	6 1 29	sylancr	$$⊢\phi \to 2P\in ℂ$$
31	30	sqcld	$$⊢\phi \to {2P}^2\in ℂ$$
32		mulcl	$$⊢\left(3\in ℂ\wedge P^2\in ℂ\right)\to 3P^2\in ℂ$$
33	15 17 32	sylancr	$$⊢\phi \to 3P^2\in ℂ$$
34		1nn0	$$⊢1\in {\mathbb{N}}_0$$
35		2nn	$$⊢2\in \mathbb{N}$$
36	34 35	decnncl	$$⊢12\in \mathbb{N}$$
37	36	nncni	$$⊢12\in ℂ$$
38		mulcl	$$⊢\left(12\in ℂ\wedge R\in ℂ\right)\to 12R\in ℂ$$
39	37 3 38	sylancr	$$⊢\phi \to 12R\in ℂ$$
40	31 33 39	subsubd	$$⊢\phi \to {2P}^2-\left(3P^2-12R\right)={2P}^2-3P^2+12R$$
41	28 40	eqtr4d	$$⊢\phi \to P^2+12R={2P}^2-\left(3P^2-12R\right)$$
42		mulcl	$$⊢\left(4\in ℂ\wedge R\in ℂ\right)\to 4R\in ℂ$$
43	13 3 42	sylancr	$$⊢\phi \to 4R\in ℂ$$
44	16 17 43	subdid	$$⊢\phi \to 3\left(P^2-4R\right)=3P^2-34R$$
45		4t3e12	$$⊢4\cdot 3=12$$
46	13 15 45	mulcomli	$$⊢3\cdot 4=12$$
47	46	oveq1i	$$⊢3\cdot 4R=12R$$
48	16 14 3	mulassd	$$⊢\phi \to 3\cdot 4R=34R$$
49	47 48	eqtr3id	$$⊢\phi \to 12R=34R$$
50	49	oveq2d	$$⊢\phi \to 3P^2-12R=3P^2-34R$$
51	44 50	eqtr4d	$$⊢\phi \to 3\left(P^2-4R\right)=3P^2-12R$$
52	51	oveq2d	$$⊢\phi \to {2P}^2-3\left(P^2-4R\right)={2P}^2-\left(3P^2-12R\right)$$
53	41 4 52	3eqtr4d	$$⊢\phi \to U={2P}^2-3\left(P^2-4R\right)$$
54	6	a1i	$$⊢\phi \to 2\in ℂ$$
55		3nn0	$$⊢3\in {\mathbb{N}}_0$$
56	55	a1i	$$⊢\phi \to 3\in {\mathbb{N}}_0$$
57	54 1 56	mulexpd	$$⊢\phi \to {2P}^3=2^3{P}^3$$
58		cu2	$$⊢2^3=8$$
59	58	oveq1i	$$⊢2^3{P}^3=8P^3$$
60	57 59	eqtrdi	$$⊢\phi \to {2P}^3=8P^3$$
61	60	oveq2d	$$⊢\phi \to 2{2P}^3=28P^3$$
62		8cn	$$⊢8\in ℂ$$
63	62	a1i	$$⊢\phi \to 8\in ℂ$$
64		expcl	$$⊢\left(P\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to P^3\in ℂ$$
65	1 55 64	sylancl	$$⊢\phi \to P^3\in ℂ$$
66	54 63 65	mul12d	$$⊢\phi \to 28P^3=82P^3$$
67	61 66	eqtrd	$$⊢\phi \to 2{2P}^3=82P^3$$
68		9cn	$$⊢9\in ℂ$$
69	68	a1i	$$⊢\phi \to 9\in ℂ$$
70		mulcl	$$⊢\left(2\in ℂ\wedge P^3\in ℂ\right)\to 2P^3\in ℂ$$
71	6 65 70	sylancr	$$⊢\phi \to 2P^3\in ℂ$$
72	1 3	mulcld	$$⊢\phi \to PR\in ℂ$$
73		mulcl	$$⊢\left(8\in ℂ\wedge PR\in ℂ\right)\to 8PR\in ℂ$$
74	62 72 73	sylancr	$$⊢\phi \to 8PR\in ℂ$$
75	69 71 74	subdid	$$⊢\phi \to 9\left(2P^3-8PR\right)=92P^3-98PR$$
76	30 17 43	subdid	$$⊢\phi \to 2P\left(P^2-4R\right)=2P{P}^2-2P4R$$
77	54 1 17	mulassd	$$⊢\phi \to 2P{P}^2=2P{P}^2$$
78	1 17	mulcomd	$$⊢\phi \to P{P}^2=P^{2}P$$
79		df-3	$$⊢3=2+1$$
80	79	oveq2i	$$⊢P^3=P^{2+1}$$
81		2nn0	$$⊢2\in {\mathbb{N}}_0$$
82		expp1	$$⊢\left(P\in ℂ\wedge 2\in {\mathbb{N}}_0\right)\to P^{2+1}=P^{2}P$$
83	1 81 82	sylancl	$$⊢\phi \to P^{2+1}=P^{2}P$$
84	80 83	eqtrid	$$⊢\phi \to P^3=P^{2}P$$
85	78 84	eqtr4d	$$⊢\phi \to P{P}^2=P^3$$
86	85	oveq2d	$$⊢\phi \to 2P{P}^2=2P^3$$
87	77 86	eqtrd	$$⊢\phi \to 2P{P}^2=2P^3$$
88	54 1 14 3	mul4d	$$⊢\phi \to 2P4R=2\cdot 4PR$$
89		2t4e8	$$⊢2\cdot 4=8$$
90	89	oveq1i	$$⊢2\cdot 4PR=8PR$$
91	88 90	eqtrdi	$$⊢\phi \to 2P4R=8PR$$
92	87 91	oveq12d	$$⊢\phi \to 2P{P}^2-2P4R=2P^3-8PR$$
93	76 92	eqtrd	$$⊢\phi \to 2P\left(P^2-4R\right)=2P^3-8PR$$
94	93	oveq2d	$$⊢\phi \to 92P\left(P^2-4R\right)=9\left(2P^3-8PR\right)$$
95		9t8e72	$$⊢9\cdot 8=72$$
96	95	oveq1i	$$⊢9\cdot 8PR=72PR$$
97	69 63 72	mulassd	$$⊢\phi \to 9\cdot 8PR=98PR$$
98	96 97	eqtr3id	$$⊢\phi \to 72PR=98PR$$
99	98	oveq2d	$$⊢\phi \to 92P^3-72PR=92P^3-98PR$$
100	75 94 99	3eqtr4d	$$⊢\phi \to 92P\left(P^2-4R\right)=92P^3-72PR$$
101	67 100	oveq12d	$$⊢\phi \to 2{2P}^3-92P\left(P^2-4R\right)=82P^3-\left(92P^3-72PR\right)$$
102		mulcl	$$⊢\left(8\in ℂ\wedge 2P^3\in ℂ\right)\to 82P^3\in ℂ$$
103	62 71 102	sylancr	$$⊢\phi \to 82P^3\in ℂ$$
104		mulcl	$$⊢\left(9\in ℂ\wedge 2P^3\in ℂ\right)\to 92P^3\in ℂ$$
105	68 71 104	sylancr	$$⊢\phi \to 92P^3\in ℂ$$
106		7nn0	$$⊢7\in {\mathbb{N}}_0$$
107	106 35	decnncl	$$⊢72\in \mathbb{N}$$
108	107	nncni	$$⊢72\in ℂ$$
109		mulcl	$$⊢\left(72\in ℂ\wedge PR\in ℂ\right)\to 72PR\in ℂ$$
110	108 72 109	sylancr	$$⊢\phi \to 72PR\in ℂ$$
111	103 105 110	subsubd	$$⊢\phi \to 82P^3-\left(92P^3-72PR\right)=82P^3-92P^3+72PR$$
112	105 103	negsubdi2d	$$⊢\phi \to -\left(92P^3-82P^3\right)=82P^3-92P^3$$
113	69 63 71	subdird	$$⊢\phi \to \left(9-8\right)2P^3=92P^3-82P^3$$
114		8p1e9	$$⊢8+1=9$$
115	68 62 20 114	subaddrii	$$⊢9-8=1$$
116	115	oveq1i	$$⊢\left(9-8\right)2P^3=12P^3$$
117	71	mullidd	$$⊢\phi \to 12P^3=2P^3$$
118	116 117	eqtrid	$$⊢\phi \to \left(9-8\right)2P^3=2P^3$$
119	113 118	eqtr3d	$$⊢\phi \to 92P^3-82P^3=2P^3$$
120	119	negeqd	$$⊢\phi \to -\left(92P^3-82P^3\right)=-2P^3$$
121	112 120	eqtr3d	$$⊢\phi \to 82P^3-92P^3=-2P^3$$
122	121	oveq1d	$$⊢\phi \to 82P^3-92P^3+72PR=-2P^3+72PR$$
123	101 111 122	3eqtrd	$$⊢\phi \to 2{2P}^3-92P\left(P^2-4R\right)=-2P^3+72PR$$
124		7nn	$$⊢7\in \mathbb{N}$$
125	81 124	decnncl	$$⊢27\in \mathbb{N}$$
126	125	nncni	$$⊢27\in ℂ$$
127	2	sqcld	$$⊢\phi \to Q^2\in ℂ$$
128		mulneg2	$$⊢\left(27\in ℂ\wedge Q^2\in ℂ\right)\to 27\left(-Q^2\right)=-27Q^2$$
129	126 127 128	sylancr	$$⊢\phi \to 27\left(-Q^2\right)=-27Q^2$$
130	123 129	oveq12d	$$⊢\phi \to 2{2P}^3-92P\left(P^2-4R\right)+27\left(-Q^2\right)=\left(-2P^3\right)+72PR+\left(-27Q^2\right)$$
131	71	negcld	$$⊢\phi \to -2P^3\in ℂ$$
132		mulcl	$$⊢\left(27\in ℂ\wedge Q^2\in ℂ\right)\to 27Q^2\in ℂ$$
133	126 127 132	sylancr	$$⊢\phi \to 27Q^2\in ℂ$$
134	131 110 133	addsubd	$$⊢\phi \to \left(-2P^3\right)+72PR-27Q^2=\left(-2P^3\right)-27Q^2+72PR$$
135	131 110	addcld	$$⊢\phi \to -2P^3+72PR\in ℂ$$
136	135 133	negsubd	$$⊢\phi \to \left(-2P^3\right)+72PR+\left(-27Q^2\right)=\left(-2P^3\right)+72PR-27Q^2$$
137	134 136 5	3eqtr4d	$$⊢\phi \to \left(-2P^3\right)+72PR+\left(-27Q^2\right)=V$$
138	130 137	eqtr2d	$$⊢\phi \to V=2{2P}^3-92P\left(P^2-4R\right)+27\left(-Q^2\right)$$
139	53 138	jca	$$⊢\phi \to \left(U={2P}^2-3\left(P^2-4R\right)\wedge V=2{2P}^3-92P\left(P^2-4R\right)+27\left(-Q^2\right)\right)$$