Theorem dcubic1

Description: Forward direction of dcubic : the claimed formula produces solutions to the cubic equation. (Contributed by Mario Carneiro, 25-Apr-2015)

	Ref	Expression
Hypotheses	dcubic.c	$$⊢\phi \to P\in ℂ$$
	dcubic.d	$$⊢\phi \to Q\in ℂ$$
	dcubic.x	$$⊢\phi \to X\in ℂ$$
	dcubic.t	$$⊢\phi \to T\in ℂ$$
	dcubic.3	$$⊢\phi \to T^3=G-N$$
	dcubic.g	$$⊢\phi \to G\in ℂ$$
	dcubic.2	$$⊢\phi \to G^2=N^2+M^3$$
	dcubic.m	$$⊢\phi \to M=\frac{P}{3}$$
	dcubic.n	$$⊢\phi \to N=\frac{Q}{2}$$
	dcubic.0	$$⊢\phi \to T\ne 0$$
	dcubic1.x	$$⊢\phi \to X=T-\left(\frac{M}{T}\right)$$
Assertion	dcubic1	$$⊢\phi \to X^3+PX+Q=0$$

Proof

Step	Hyp	Ref	Expression
1		dcubic.c	$$⊢\phi \to P\in ℂ$$
2		dcubic.d	$$⊢\phi \to Q\in ℂ$$
3		dcubic.x	$$⊢\phi \to X\in ℂ$$
4		dcubic.t	$$⊢\phi \to T\in ℂ$$
5		dcubic.3	$$⊢\phi \to T^3=G-N$$
6		dcubic.g	$$⊢\phi \to G\in ℂ$$
7		dcubic.2	$$⊢\phi \to G^2=N^2+M^3$$
8		dcubic.m	$$⊢\phi \to M=\frac{P}{3}$$
9		dcubic.n	$$⊢\phi \to N=\frac{Q}{2}$$
10		dcubic.0	$$⊢\phi \to T\ne 0$$
11		dcubic1.x	$$⊢\phi \to X=T-\left(\frac{M}{T}\right)$$
12	5	oveq1d	$$⊢\phi \to {\left(T^3\right)}^2={\left(G-N\right)}^2$$
13	2	halfcld	$$⊢\phi \to \frac{Q}{2}\in ℂ$$
14	9 13	eqeltrd	$$⊢\phi \to N\in ℂ$$
15		binom2sub	$$⊢\left(G\in ℂ\wedge N\in ℂ\right)\to {\left(G-N\right)}^2=G^2-2G\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+N^2$$
16	6 14 15	syl2anc	$$⊢\phi \to {\left(G-N\right)}^2=G^2-2G\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+N^2$$
17		2cnd	$$⊢\phi \to 2\in ℂ$$
18	17 6 14	mul12d	$$⊢\phi \to 2G\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=G2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
19	9	oveq2d	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=2\left(\frac{Q}{2}\right)$$
20		2ne0	$$⊢2\ne 0$$
21	20	a1i	$$⊢\phi \to 2\ne 0$$
22	2 17 21	divcan2d	$$⊢\phi \to 2\left(\frac{Q}{2}\right)=Q$$
23	19 22	eqtrd	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=Q$$
24	23	oveq2d	$$⊢\phi \to G2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=GQ$$
25	6 2	mulcomd	$$⊢\phi \to GQ=QG$$
26	18 24 25	3eqtrd	$$⊢\phi \to 2G\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=QG$$
27	7 26	oveq12d	$$⊢\phi \to G^2-2G\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=N^2+M^3-QG$$
28	27	oveq1d	$$⊢\phi \to G^2-2G\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+N^2=\left(N^2+M^3\right)-QG+N^2$$
29	12 16 28	3eqtrd	$$⊢\phi \to {\left(T^3\right)}^2=\left(N^2+M^3\right)-QG+N^2$$
30	14	sqcld	$$⊢\phi \to N^2\in ℂ$$
31		3cn	$$⊢3\in ℂ$$
32	31	a1i	$$⊢\phi \to 3\in ℂ$$
33		3ne0	$$⊢3\ne 0$$
34	33	a1i	$$⊢\phi \to 3\ne 0$$
35	1 32 34	divcld	$$⊢\phi \to \frac{P}{3}\in ℂ$$
36	8 35	eqeltrd	$$⊢\phi \to M\in ℂ$$
37		3nn0	$$⊢3\in {\mathbb{N}}_0$$
38		expcl	$$⊢\left(M\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to M^3\in ℂ$$
39	36 37 38	sylancl	$$⊢\phi \to M^3\in ℂ$$
40	30 39	addcld	$$⊢\phi \to N^2+M^3\in ℂ$$
41	2 6	mulcld	$$⊢\phi \to QG\in ℂ$$
42	40 30 41	addsubd	$$⊢\phi \to \left(N^2+M^3\right)+N^2-QG=\left(N^2+M^3\right)-QG+N^2$$
43	30 39 30	add32d	$$⊢\phi \to N^2+M^3+N^2=N^2+N^2+M^3$$
44	30	2timesd	$$⊢\phi \to 2N^2=N^2+N^2$$
45	44	oveq1d	$$⊢\phi \to 2N^2+M^3=N^2+N^2+M^3$$
46	43 45	eqtr4d	$$⊢\phi \to N^2+M^3+N^2=2N^2+M^3$$
47	46	oveq1d	$$⊢\phi \to \left(N^2+M^3\right)+N^2-QG=2N^2+M^3-QG$$
48	29 42 47	3eqtr2d	$$⊢\phi \to {\left(T^3\right)}^2=2N^2+M^3-QG$$
49	2 6 14	subdid	$$⊢\phi \to Q\left(G-N\right)=QG-Q\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
50	5	oveq2d	$$⊢\phi \to Q{T}^3=Q\left(G-N\right)$$
51	14	sqvald	$$⊢\phi \to N^2=\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
52	51	oveq2d	$$⊢\phi \to 2N^2=2\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
53	17 14 14	mulassd	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=2\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
54	23	oveq1d	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=Q\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
55	52 53 54	3eqtr2d	$$⊢\phi \to 2N^2=Q\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
56	55	oveq2d	$$⊢\phi \to QG-2N^2=QG-Q\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
57	49 50 56	3eqtr4d	$$⊢\phi \to Q{T}^3=QG-2N^2$$
58	57	oveq1d	$$⊢\phi \to Q{T}^3-M^3=QG-2N^2-M^3$$
59		2cn	$$⊢2\in ℂ$$
60		mulcl	$$⊢\left(2\in ℂ\wedge N^2\in ℂ\right)\to 2N^2\in ℂ$$
61	59 30 60	sylancr	$$⊢\phi \to 2N^2\in ℂ$$
62	41 61 39	subsub4d	$$⊢\phi \to QG-2N^2-M^3=QG-\left(2N^2+M^3\right)$$
63	58 62	eqtrd	$$⊢\phi \to Q{T}^3-M^3=QG-\left(2N^2+M^3\right)$$
64	48 63	oveq12d	$$⊢\phi \to {\left(T^3\right)}^2+Q{T}^3-M^3=\left(2N^2+M^3-QG\right)+QG-\left(2N^2+M^3\right)$$
65	61 39	addcld	$$⊢\phi \to 2N^2+M^3\in ℂ$$
66		npncan2	$$⊢\left(2N^2+M^3\in ℂ\wedge QG\in ℂ\right)\to \left(2N^2+M^3-QG\right)+QG-\left(2N^2+M^3\right)=0$$
67	65 41 66	syl2anc	$$⊢\phi \to \left(2N^2+M^3-QG\right)+QG-\left(2N^2+M^3\right)=0$$
68	64 67	eqtrd	$$⊢\phi \to {\left(T^3\right)}^2+Q{T}^3-M^3=0$$
69	1 2 3 4 5 6 7 8 9 10 4 10 11	dcubic1lem	$$⊢\phi \to \left(X^3+PX+Q=0\leftrightarrow {\left(T^3\right)}^2+Q{T}^3-M^3=0\right)$$
70	68 69	mpbird	$$⊢\phi \to X^3+PX+Q=0$$