Theorem cubic

Description: The cubic equation, which gives the roots of an arbitrary (nondegenerate) cubic function. Use rextp to convert the existential quantifier to a triple disjunction. This is Metamath 100 proof #37. (Contributed by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Hypotheses	cubic.r	$$⊢R=\left\{1,\frac{-1+\mathrm{i}\sqrt{3}}{2},\frac{-1-\mathrm{i}\sqrt{3}}{2}\right\}$$
	cubic.a	$$⊢\phi \to A\in ℂ$$
	cubic.z	$$⊢\phi \to A\ne 0$$
	cubic.b	$$⊢\phi \to B\in ℂ$$
	cubic.c	$$⊢\phi \to C\in ℂ$$
	cubic.d	$$⊢\phi \to D\in ℂ$$
	cubic.x	$$⊢\phi \to X\in ℂ$$
	cubic.t	$$⊢\phi \to T={\left(\frac{N+\sqrt{G}}{2}\right)}^{\frac{1}{3}}$$
	cubic.g	$$⊢\phi \to G=N^2-4M^3$$
	cubic.m	$$⊢\phi \to M=B^2-3AC$$
	cubic.n	$$⊢\phi \to N=2B^3-9ABC+27A^{2}D$$
	cubic.0	$$⊢\phi \to M\ne 0$$
Assertion	cubic	$$⊢\phi \to \left(A{X}^3+B{X}^2+CX+D=0\leftrightarrow \exists r\in RX=-\frac{B+rT+\left(\frac{M}{rT}\right)}{3A}\right)$$

Proof

Step	Hyp	Ref	Expression
1		cubic.r	$$⊢R=\left\{1,\frac{-1+\mathrm{i}\sqrt{3}}{2},\frac{-1-\mathrm{i}\sqrt{3}}{2}\right\}$$
2		cubic.a	$$⊢\phi \to A\in ℂ$$
3		cubic.z	$$⊢\phi \to A\ne 0$$
4		cubic.b	$$⊢\phi \to B\in ℂ$$
5		cubic.c	$$⊢\phi \to C\in ℂ$$
6		cubic.d	$$⊢\phi \to D\in ℂ$$
7		cubic.x	$$⊢\phi \to X\in ℂ$$
8		cubic.t	$$⊢\phi \to T={\left(\frac{N+\sqrt{G}}{2}\right)}^{\frac{1}{3}}$$
9		cubic.g	$$⊢\phi \to G=N^2-4M^3$$
10		cubic.m	$$⊢\phi \to M=B^2-3AC$$
11		cubic.n	$$⊢\phi \to N=2B^3-9ABC+27A^{2}D$$
12		cubic.0	$$⊢\phi \to M\ne 0$$
13		2cn	$$⊢2\in ℂ$$
14		3nn0	$$⊢3\in {\mathbb{N}}_0$$
15		expcl	$$⊢\left(B\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to B^3\in ℂ$$
16	4 14 15	sylancl	$$⊢\phi \to B^3\in ℂ$$
17		mulcl	$$⊢\left(2\in ℂ\wedge B^3\in ℂ\right)\to 2B^3\in ℂ$$
18	13 16 17	sylancr	$$⊢\phi \to 2B^3\in ℂ$$
19		9cn	$$⊢9\in ℂ$$
20		mulcl	$$⊢\left(9\in ℂ\wedge A\in ℂ\right)\to 9A\in ℂ$$
21	19 2 20	sylancr	$$⊢\phi \to 9A\in ℂ$$
22	4 5	mulcld	$$⊢\phi \to BC\in ℂ$$
23	21 22	mulcld	$$⊢\phi \to 9ABC\in ℂ$$
24	18 23	subcld	$$⊢\phi \to 2B^3-9ABC\in ℂ$$
25		2nn0	$$⊢2\in {\mathbb{N}}_0$$
26		7nn	$$⊢7\in \mathbb{N}$$
27	25 26	decnncl	$$⊢27\in \mathbb{N}$$
28	27	nncni	$$⊢27\in ℂ$$
29	2	sqcld	$$⊢\phi \to A^2\in ℂ$$
30	29 6	mulcld	$$⊢\phi \to A^{2}D\in ℂ$$
31		mulcl	$$⊢\left(27\in ℂ\wedge A^{2}D\in ℂ\right)\to 27A^{2}D\in ℂ$$
32	28 30 31	sylancr	$$⊢\phi \to 27A^{2}D\in ℂ$$
33	24 32	addcld	$$⊢\phi \to 2B^3-9ABC+27A^{2}D\in ℂ$$
34	11 33	eqeltrd	$$⊢\phi \to N\in ℂ$$
35	34	sqcld	$$⊢\phi \to N^2\in ℂ$$
36		4cn	$$⊢4\in ℂ$$
37	4	sqcld	$$⊢\phi \to B^2\in ℂ$$
38		3cn	$$⊢3\in ℂ$$
39	2 5	mulcld	$$⊢\phi \to AC\in ℂ$$
40		mulcl	$$⊢\left(3\in ℂ\wedge AC\in ℂ\right)\to 3AC\in ℂ$$
41	38 39 40	sylancr	$$⊢\phi \to 3AC\in ℂ$$
42	37 41	subcld	$$⊢\phi \to B^2-3AC\in ℂ$$
43	10 42	eqeltrd	$$⊢\phi \to M\in ℂ$$
44		expcl	$$⊢\left(M\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to M^3\in ℂ$$
45	43 14 44	sylancl	$$⊢\phi \to M^3\in ℂ$$
46		mulcl	$$⊢\left(4\in ℂ\wedge M^3\in ℂ\right)\to 4M^3\in ℂ$$
47	36 45 46	sylancr	$$⊢\phi \to 4M^3\in ℂ$$
48	35 47	subcld	$$⊢\phi \to N^2-4M^3\in ℂ$$
49	9 48	eqeltrd	$$⊢\phi \to G\in ℂ$$
50	49	sqrtcld	$$⊢\phi \to \sqrt{G}\in ℂ$$
51	34 50	addcld	$$⊢\phi \to N+\sqrt{G}\in ℂ$$
52	51	halfcld	$$⊢\phi \to \frac{N+\sqrt{G}}{2}\in ℂ$$
53		3ne0	$$⊢3\ne 0$$
54	38 53	reccli	$$⊢\frac{1}{3}\in ℂ$$
55		cxpcl	$$⊢\left(\frac{N+\sqrt{G}}{2}\in ℂ\wedge \frac{1}{3}\in ℂ\right)\to {\left(\frac{N+\sqrt{G}}{2}\right)}^{\frac{1}{3}}\in ℂ$$
56	52 54 55	sylancl	$$⊢\phi \to {\left(\frac{N+\sqrt{G}}{2}\right)}^{\frac{1}{3}}\in ℂ$$
57	8 56	eqeltrd	$$⊢\phi \to T\in ℂ$$
58	8	oveq1d	$$⊢\phi \to T^3={\left({\left(\frac{N+\sqrt{G}}{2}\right)}^{\frac{1}{3}}\right)}^3$$
59		3nn	$$⊢3\in \mathbb{N}$$
60		cxproot	$$⊢\left(\frac{N+\sqrt{G}}{2}\in ℂ\wedge 3\in \mathbb{N}\right)\to {\left({\left(\frac{N+\sqrt{G}}{2}\right)}^{\frac{1}{3}}\right)}^3=\frac{N+\sqrt{G}}{2}$$
61	52 59 60	sylancl	$$⊢\phi \to {\left({\left(\frac{N+\sqrt{G}}{2}\right)}^{\frac{1}{3}}\right)}^3=\frac{N+\sqrt{G}}{2}$$
62	58 61	eqtrd	$$⊢\phi \to T^3=\frac{N+\sqrt{G}}{2}$$
63	49	sqsqrtd	$$⊢\phi \to {\sqrt{G}}^2=G$$
64	63 9	eqtrd	$$⊢\phi \to {\sqrt{G}}^2=N^2-4M^3$$
65	13	a1i	$$⊢\phi \to 2\in ℂ$$
66	36	a1i	$$⊢\phi \to 4\in ℂ$$
67		4ne0	$$⊢4\ne 0$$
68	67	a1i	$$⊢\phi \to 4\ne 0$$
69		3z	$$⊢3\in \mathbb{Z}$$
70	69	a1i	$$⊢\phi \to 3\in \mathbb{Z}$$
71	43 12 70	expne0d	$$⊢\phi \to M^3\ne 0$$
72	66 45 68 71	mulne0d	$$⊢\phi \to 4M^3\ne 0$$
73	64	oveq2d	$$⊢\phi \to N^2-{\sqrt{G}}^2=N^2-\left(N^2-4M^3\right)$$
74		subsq	$$⊢\left(N\in ℂ\wedge \sqrt{G}\in ℂ\right)\to N^2-{\sqrt{G}}^2=\left(N+\sqrt{G}\right)\left(N-\sqrt{G}\right)$$
75	34 50 74	syl2anc	$$⊢\phi \to N^2-{\sqrt{G}}^2=\left(N+\sqrt{G}\right)\left(N-\sqrt{G}\right)$$
76	35 47	nncand	$$⊢\phi \to N^2-\left(N^2-4M^3\right)=4M^3$$
77	73 75 76	3eqtr3d	$$⊢\phi \to \left(N+\sqrt{G}\right)\left(N-\sqrt{G}\right)=4M^3$$
78	34 50	subcld	$$⊢\phi \to N-\sqrt{G}\in ℂ$$
79	78	mul02d	$$⊢\phi \to 0\cdot \left(N-\sqrt{G}\right)=0$$
80	72 77 79	3netr4d	$$⊢\phi \to \left(N+\sqrt{G}\right)\left(N-\sqrt{G}\right)\ne 0\cdot \left(N-\sqrt{G}\right)$$
81		oveq1	$$⊢N+\sqrt{G}=0\to \left(N+\sqrt{G}\right)\left(N-\sqrt{G}\right)=0\cdot \left(N-\sqrt{G}\right)$$
82	81	necon3i	$$⊢\left(N+\sqrt{G}\right)\left(N-\sqrt{G}\right)\ne 0\cdot \left(N-\sqrt{G}\right)\to N+\sqrt{G}\ne 0$$
83	80 82	syl	$$⊢\phi \to N+\sqrt{G}\ne 0$$
84		2ne0	$$⊢2\ne 0$$
85	84	a1i	$$⊢\phi \to 2\ne 0$$
86	51 65 83 85	divne0d	$$⊢\phi \to \frac{N+\sqrt{G}}{2}\ne 0$$
87	54	a1i	$$⊢\phi \to \frac{1}{3}\in ℂ$$
88	52 86 87	cxpne0d	$$⊢\phi \to {\left(\frac{N+\sqrt{G}}{2}\right)}^{\frac{1}{3}}\ne 0$$
89	8 88	eqnetrd	$$⊢\phi \to T\ne 0$$
90	2 3 4 5 6 7 57 62 50 64 10 11 89	cubic2	$$⊢\phi \to \left(A{X}^3+B{X}^2+CX+D=0\leftrightarrow \exists r\in ℂ\left(r^3=1\wedge X=-\frac{B+rT+\left(\frac{M}{rT}\right)}{3A}\right)\right)$$
91	1	1cubr	$$⊢r\in R\leftrightarrow \left(r\in ℂ\wedge r^3=1\right)$$
92	91	anbi1i	$$⊢\left(r\in R\wedge X=-\frac{B+rT+\left(\frac{M}{rT}\right)}{3A}\right)\leftrightarrow \left(\left(r\in ℂ\wedge r^3=1\right)\wedge X=-\frac{B+rT+\left(\frac{M}{rT}\right)}{3A}\right)$$
93		anass	$$⊢\left(\left(r\in ℂ\wedge r^3=1\right)\wedge X=-\frac{B+rT+\left(\frac{M}{rT}\right)}{3A}\right)\leftrightarrow \left(r\in ℂ\wedge \left(r^3=1\wedge X=-\frac{B+rT+\left(\frac{M}{rT}\right)}{3A}\right)\right)$$
94	92 93	bitri	$$⊢\left(r\in R\wedge X=-\frac{B+rT+\left(\frac{M}{rT}\right)}{3A}\right)\leftrightarrow \left(r\in ℂ\wedge \left(r^3=1\wedge X=-\frac{B+rT+\left(\frac{M}{rT}\right)}{3A}\right)\right)$$
95	94	rexbii2	$$⊢\exists r\in RX=-\frac{B+rT+\left(\frac{M}{rT}\right)}{3A}\leftrightarrow \exists r\in ℂ\left(r^3=1\wedge X=-\frac{B+rT+\left(\frac{M}{rT}\right)}{3A}\right)$$
96	90 95	bitr4di	$$⊢\phi \to \left(A{X}^3+B{X}^2+CX+D=0\leftrightarrow \exists r\in RX=-\frac{B+rT+\left(\frac{M}{rT}\right)}{3A}\right)$$