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	⊢ 𝑅 = { 1 , ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) , ( ( - 1 − ( i · ( √ ‘ 3 ) ) ) / 2 ) }
	cubic.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	cubic.z	⊢ ( 𝜑 → 𝐴 ≠ 0 )
	cubic.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	cubic.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
	cubic.d	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
	cubic.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
	cubic.t	⊢ ( 𝜑 → 𝑇 = ( ( ( 𝑁 + ( √ ‘ 𝐺 ) ) / 2 ) ↑𝑐 ( 1 / 3 ) ) )
	cubic.g	⊢ ( 𝜑 → 𝐺 = ( ( 𝑁 ↑ 2 ) − ( 4 · ( 𝑀 ↑ 3 ) ) ) )
	cubic.m	⊢ ( 𝜑 → 𝑀 = ( ( 𝐵 ↑ 2 ) − ( 3 · ( 𝐴 · 𝐶 ) ) ) )
	cubic.n	⊢ ( 𝜑 → 𝑁 = ( ( ( 2 · ( 𝐵 ↑ 3 ) ) − ( ( 9 · 𝐴 ) · ( 𝐵 · 𝐶 ) ) ) + ( ; 2 7 · ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) ) )
	cubic.0	⊢ ( 𝜑 → 𝑀 ≠ 0 )
Assertion	cubic	⊢ ( 𝜑 → ( ( ( ( 𝐴 · ( 𝑋 ↑ 3 ) ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) = 0 ↔ ∃ 𝑟 ∈ 𝑅 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / ( 3 · 𝐴 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cubic.r	⊢ 𝑅 = { 1 , ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) , ( ( - 1 − ( i · ( √ ‘ 3 ) ) ) / 2 ) }
2		cubic.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
3		cubic.z	⊢ ( 𝜑 → 𝐴 ≠ 0 )
4		cubic.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
5		cubic.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
6		cubic.d	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
7		cubic.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
8		cubic.t	⊢ ( 𝜑 → 𝑇 = ( ( ( 𝑁 + ( √ ‘ 𝐺 ) ) / 2 ) ↑𝑐 ( 1 / 3 ) ) )
9		cubic.g	⊢ ( 𝜑 → 𝐺 = ( ( 𝑁 ↑ 2 ) − ( 4 · ( 𝑀 ↑ 3 ) ) ) )
10		cubic.m	⊢ ( 𝜑 → 𝑀 = ( ( 𝐵 ↑ 2 ) − ( 3 · ( 𝐴 · 𝐶 ) ) ) )
11		cubic.n	⊢ ( 𝜑 → 𝑁 = ( ( ( 2 · ( 𝐵 ↑ 3 ) ) − ( ( 9 · 𝐴 ) · ( 𝐵 · 𝐶 ) ) ) + ( ; 2 7 · ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) ) )
12		cubic.0	⊢ ( 𝜑 → 𝑀 ≠ 0 )
13		2cn	⊢ 2 ∈ ℂ
14		3nn0	⊢ 3 ∈ ℕ0
15		expcl	⊢ ( ( 𝐵 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝐵 ↑ 3 ) ∈ ℂ )
16	4 14 15	sylancl	⊢ ( 𝜑 → ( 𝐵 ↑ 3 ) ∈ ℂ )
17		mulcl	⊢ ( ( 2 ∈ ℂ ∧ ( 𝐵 ↑ 3 ) ∈ ℂ ) → ( 2 · ( 𝐵 ↑ 3 ) ) ∈ ℂ )
18	13 16 17	sylancr	⊢ ( 𝜑 → ( 2 · ( 𝐵 ↑ 3 ) ) ∈ ℂ )
19		9cn	⊢ 9 ∈ ℂ
20		mulcl	⊢ ( ( 9 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 9 · 𝐴 ) ∈ ℂ )
21	19 2 20	sylancr	⊢ ( 𝜑 → ( 9 · 𝐴 ) ∈ ℂ )
22	4 5	mulcld	⊢ ( 𝜑 → ( 𝐵 · 𝐶 ) ∈ ℂ )
23	21 22	mulcld	⊢ ( 𝜑 → ( ( 9 · 𝐴 ) · ( 𝐵 · 𝐶 ) ) ∈ ℂ )
24	18 23	subcld	⊢ ( 𝜑 → ( ( 2 · ( 𝐵 ↑ 3 ) ) − ( ( 9 · 𝐴 ) · ( 𝐵 · 𝐶 ) ) ) ∈ ℂ )
25		2nn0	⊢ 2 ∈ ℕ0
26		7nn	⊢ 7 ∈ ℕ
27	25 26	decnncl	⊢ ; 2 7 ∈ ℕ
28	27	nncni	⊢ ; 2 7 ∈ ℂ
29	2	sqcld	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℂ )
30	29 6	mulcld	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) · 𝐷 ) ∈ ℂ )
31		mulcl	⊢ ( ( ; 2 7 ∈ ℂ ∧ ( ( 𝐴 ↑ 2 ) · 𝐷 ) ∈ ℂ ) → ( ; 2 7 · ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) ∈ ℂ )
32	28 30 31	sylancr	⊢ ( 𝜑 → ( ; 2 7 · ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) ∈ ℂ )
33	24 32	addcld	⊢ ( 𝜑 → ( ( ( 2 · ( 𝐵 ↑ 3 ) ) − ( ( 9 · 𝐴 ) · ( 𝐵 · 𝐶 ) ) ) + ( ; 2 7 · ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) ) ∈ ℂ )
34	11 33	eqeltrd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
35	34	sqcld	⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) ∈ ℂ )
36		4cn	⊢ 4 ∈ ℂ
37	4	sqcld	⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℂ )
38		3cn	⊢ 3 ∈ ℂ
39	2 5	mulcld	⊢ ( 𝜑 → ( 𝐴 · 𝐶 ) ∈ ℂ )
40		mulcl	⊢ ( ( 3 ∈ ℂ ∧ ( 𝐴 · 𝐶 ) ∈ ℂ ) → ( 3 · ( 𝐴 · 𝐶 ) ) ∈ ℂ )
41	38 39 40	sylancr	⊢ ( 𝜑 → ( 3 · ( 𝐴 · 𝐶 ) ) ∈ ℂ )
42	37 41	subcld	⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) − ( 3 · ( 𝐴 · 𝐶 ) ) ) ∈ ℂ )
43	10 42	eqeltrd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
44		expcl	⊢ ( ( 𝑀 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝑀 ↑ 3 ) ∈ ℂ )
45	43 14 44	sylancl	⊢ ( 𝜑 → ( 𝑀 ↑ 3 ) ∈ ℂ )
46		mulcl	⊢ ( ( 4 ∈ ℂ ∧ ( 𝑀 ↑ 3 ) ∈ ℂ ) → ( 4 · ( 𝑀 ↑ 3 ) ) ∈ ℂ )
47	36 45 46	sylancr	⊢ ( 𝜑 → ( 4 · ( 𝑀 ↑ 3 ) ) ∈ ℂ )
48	35 47	subcld	⊢ ( 𝜑 → ( ( 𝑁 ↑ 2 ) − ( 4 · ( 𝑀 ↑ 3 ) ) ) ∈ ℂ )
49	9 48	eqeltrd	⊢ ( 𝜑 → 𝐺 ∈ ℂ )
50	49	sqrtcld	⊢ ( 𝜑 → ( √ ‘ 𝐺 ) ∈ ℂ )
51	34 50	addcld	⊢ ( 𝜑 → ( 𝑁 + ( √ ‘ 𝐺 ) ) ∈ ℂ )
52	51	halfcld	⊢ ( 𝜑 → ( ( 𝑁 + ( √ ‘ 𝐺 ) ) / 2 ) ∈ ℂ )
53		3ne0	⊢ 3 ≠ 0
54	38 53	reccli	⊢ ( 1 / 3 ) ∈ ℂ
55		cxpcl	⊢ ( ( ( ( 𝑁 + ( √ ‘ 𝐺 ) ) / 2 ) ∈ ℂ ∧ ( 1 / 3 ) ∈ ℂ ) → ( ( ( 𝑁 + ( √ ‘ 𝐺 ) ) / 2 ) ↑𝑐 ( 1 / 3 ) ) ∈ ℂ )
56	52 54 55	sylancl	⊢ ( 𝜑 → ( ( ( 𝑁 + ( √ ‘ 𝐺 ) ) / 2 ) ↑𝑐 ( 1 / 3 ) ) ∈ ℂ )
57	8 56	eqeltrd	⊢ ( 𝜑 → 𝑇 ∈ ℂ )
58	8	oveq1d	⊢ ( 𝜑 → ( 𝑇 ↑ 3 ) = ( ( ( ( 𝑁 + ( √ ‘ 𝐺 ) ) / 2 ) ↑𝑐 ( 1 / 3 ) ) ↑ 3 ) )
59		3nn	⊢ 3 ∈ ℕ
60		cxproot	⊢ ( ( ( ( 𝑁 + ( √ ‘ 𝐺 ) ) / 2 ) ∈ ℂ ∧ 3 ∈ ℕ ) → ( ( ( ( 𝑁 + ( √ ‘ 𝐺 ) ) / 2 ) ↑𝑐 ( 1 / 3 ) ) ↑ 3 ) = ( ( 𝑁 + ( √ ‘ 𝐺 ) ) / 2 ) )
61	52 59 60	sylancl	⊢ ( 𝜑 → ( ( ( ( 𝑁 + ( √ ‘ 𝐺 ) ) / 2 ) ↑𝑐 ( 1 / 3 ) ) ↑ 3 ) = ( ( 𝑁 + ( √ ‘ 𝐺 ) ) / 2 ) )
62	58 61	eqtrd	⊢ ( 𝜑 → ( 𝑇 ↑ 3 ) = ( ( 𝑁 + ( √ ‘ 𝐺 ) ) / 2 ) )
63	49	sqsqrtd	⊢ ( 𝜑 → ( ( √ ‘ 𝐺 ) ↑ 2 ) = 𝐺 )
64	63 9	eqtrd	⊢ ( 𝜑 → ( ( √ ‘ 𝐺 ) ↑ 2 ) = ( ( 𝑁 ↑ 2 ) − ( 4 · ( 𝑀 ↑ 3 ) ) ) )
65	13	a1i	⊢ ( 𝜑 → 2 ∈ ℂ )
66	36	a1i	⊢ ( 𝜑 → 4 ∈ ℂ )
67		4ne0	⊢ 4 ≠ 0
68	67	a1i	⊢ ( 𝜑 → 4 ≠ 0 )
69		3z	⊢ 3 ∈ ℤ
70	69	a1i	⊢ ( 𝜑 → 3 ∈ ℤ )
71	43 12 70	expne0d	⊢ ( 𝜑 → ( 𝑀 ↑ 3 ) ≠ 0 )
72	66 45 68 71	mulne0d	⊢ ( 𝜑 → ( 4 · ( 𝑀 ↑ 3 ) ) ≠ 0 )
73	64	oveq2d	⊢ ( 𝜑 → ( ( 𝑁 ↑ 2 ) − ( ( √ ‘ 𝐺 ) ↑ 2 ) ) = ( ( 𝑁 ↑ 2 ) − ( ( 𝑁 ↑ 2 ) − ( 4 · ( 𝑀 ↑ 3 ) ) ) ) )
74		subsq	⊢ ( ( 𝑁 ∈ ℂ ∧ ( √ ‘ 𝐺 ) ∈ ℂ ) → ( ( 𝑁 ↑ 2 ) − ( ( √ ‘ 𝐺 ) ↑ 2 ) ) = ( ( 𝑁 + ( √ ‘ 𝐺 ) ) · ( 𝑁 − ( √ ‘ 𝐺 ) ) ) )
75	34 50 74	syl2anc	⊢ ( 𝜑 → ( ( 𝑁 ↑ 2 ) − ( ( √ ‘ 𝐺 ) ↑ 2 ) ) = ( ( 𝑁 + ( √ ‘ 𝐺 ) ) · ( 𝑁 − ( √ ‘ 𝐺 ) ) ) )
76	35 47	nncand	⊢ ( 𝜑 → ( ( 𝑁 ↑ 2 ) − ( ( 𝑁 ↑ 2 ) − ( 4 · ( 𝑀 ↑ 3 ) ) ) ) = ( 4 · ( 𝑀 ↑ 3 ) ) )
77	73 75 76	3eqtr3d	⊢ ( 𝜑 → ( ( 𝑁 + ( √ ‘ 𝐺 ) ) · ( 𝑁 − ( √ ‘ 𝐺 ) ) ) = ( 4 · ( 𝑀 ↑ 3 ) ) )
78	34 50	subcld	⊢ ( 𝜑 → ( 𝑁 − ( √ ‘ 𝐺 ) ) ∈ ℂ )
79	78	mul02d	⊢ ( 𝜑 → ( 0 · ( 𝑁 − ( √ ‘ 𝐺 ) ) ) = 0 )
80	72 77 79	3netr4d	⊢ ( 𝜑 → ( ( 𝑁 + ( √ ‘ 𝐺 ) ) · ( 𝑁 − ( √ ‘ 𝐺 ) ) ) ≠ ( 0 · ( 𝑁 − ( √ ‘ 𝐺 ) ) ) )
81		oveq1	⊢ ( ( 𝑁 + ( √ ‘ 𝐺 ) ) = 0 → ( ( 𝑁 + ( √ ‘ 𝐺 ) ) · ( 𝑁 − ( √ ‘ 𝐺 ) ) ) = ( 0 · ( 𝑁 − ( √ ‘ 𝐺 ) ) ) )
82	81	necon3i	⊢ ( ( ( 𝑁 + ( √ ‘ 𝐺 ) ) · ( 𝑁 − ( √ ‘ 𝐺 ) ) ) ≠ ( 0 · ( 𝑁 − ( √ ‘ 𝐺 ) ) ) → ( 𝑁 + ( √ ‘ 𝐺 ) ) ≠ 0 )
83	80 82	syl	⊢ ( 𝜑 → ( 𝑁 + ( √ ‘ 𝐺 ) ) ≠ 0 )
84		2ne0	⊢ 2 ≠ 0
85	84	a1i	⊢ ( 𝜑 → 2 ≠ 0 )
86	51 65 83 85	divne0d	⊢ ( 𝜑 → ( ( 𝑁 + ( √ ‘ 𝐺 ) ) / 2 ) ≠ 0 )
87	54	a1i	⊢ ( 𝜑 → ( 1 / 3 ) ∈ ℂ )
88	52 86 87	cxpne0d	⊢ ( 𝜑 → ( ( ( 𝑁 + ( √ ‘ 𝐺 ) ) / 2 ) ↑𝑐 ( 1 / 3 ) ) ≠ 0 )
89	8 88	eqnetrd	⊢ ( 𝜑 → 𝑇 ≠ 0 )
90	2 3 4 5 6 7 57 62 50 64 10 11 89	cubic2	⊢ ( 𝜑 → ( ( ( ( 𝐴 · ( 𝑋 ↑ 3 ) ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) = 0 ↔ ∃ 𝑟 ∈ ℂ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / ( 3 · 𝐴 ) ) ) ) )
91	1	1cubr	⊢ ( 𝑟 ∈ 𝑅 ↔ ( 𝑟 ∈ ℂ ∧ ( 𝑟 ↑ 3 ) = 1 ) )
92	91	anbi1i	⊢ ( ( 𝑟 ∈ 𝑅 ∧ 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / ( 3 · 𝐴 ) ) ) ↔ ( ( 𝑟 ∈ ℂ ∧ ( 𝑟 ↑ 3 ) = 1 ) ∧ 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / ( 3 · 𝐴 ) ) ) )
93		anass	⊢ ( ( ( 𝑟 ∈ ℂ ∧ ( 𝑟 ↑ 3 ) = 1 ) ∧ 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / ( 3 · 𝐴 ) ) ) ↔ ( 𝑟 ∈ ℂ ∧ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / ( 3 · 𝐴 ) ) ) ) )
94	92 93	bitri	⊢ ( ( 𝑟 ∈ 𝑅 ∧ 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / ( 3 · 𝐴 ) ) ) ↔ ( 𝑟 ∈ ℂ ∧ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / ( 3 · 𝐴 ) ) ) ) )
95	94	rexbii2	⊢ ( ∃ 𝑟 ∈ 𝑅 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / ( 3 · 𝐴 ) ) ↔ ∃ 𝑟 ∈ ℂ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / ( 3 · 𝐴 ) ) ) )
96	90 95	bitr4di	⊢ ( 𝜑 → ( ( ( ( 𝐴 · ( 𝑋 ↑ 3 ) ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) = 0 ↔ ∃ 𝑟 ∈ 𝑅 𝑋 = - ( ( ( 𝐵 + ( 𝑟 · 𝑇 ) ) + ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) / ( 3 · 𝐴 ) ) ) )