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 = \{1, \frac{- 1 + i \sqrt{3}}{2}, \frac{- 1 - i \sqrt{3}}{2}\}$
	cubic.a	$⊢ φ \to A \in ℂ$
	cubic.z	$⊢ φ \to A \neq 0$
	cubic.b	$⊢ φ \to B \in ℂ$
	cubic.c	$⊢ φ \to C \in ℂ$
	cubic.d	$⊢ φ \to D \in ℂ$
	cubic.x	$⊢ φ \to X \in ℂ$
	cubic.t	$⊢ φ \to T = {(\frac{N + \sqrt{G}}{2})}^{\frac{1}{3}}$
	cubic.g	$⊢ φ \to G = N^{2} - 4 M^{3}$
	cubic.m	$⊢ φ \to M = B^{2} - 3 A C$
	cubic.n	$⊢ φ \to N = 2 B^{3} - 9 A B C + 27 A^{2} D$
	cubic.0	$⊢ φ \to M \neq 0$
Assertion	cubic	$⊢ φ \to (A X^{3} + B X^{2} + C X + D = 0 \leftrightarrow \exists r \in R X = - \frac{B + r T + (\frac{M}{r T})}{3 A})$

Proof

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

Metamath Proof Explorer

Theorem cubic

Proof