Metamath Proof Explorer

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 = { 1 , ( ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) / 2 ) , ( ( -u 1 - ( _i x. ( sqrt ` 3 ) ) ) / 2 ) }
cubic.a 
|- ( ph -> A e. CC )
cubic.z 
|- ( ph -> A =/= 0 )
cubic.b 
|- ( ph -> B e. CC )
cubic.c 
|- ( ph -> C e. CC )
cubic.d 
|- ( ph -> D e. CC )
cubic.x 
|- ( ph -> X e. CC )
cubic.t 
|- ( ph -> T = ( ( ( N + ( sqrt ` G ) ) / 2 ) ^c ( 1 / 3 ) ) )
cubic.g 
|- ( ph -> G = ( ( N ^ 2 ) - ( 4 x. ( M ^ 3 ) ) ) )
cubic.m 
|- ( ph -> M = ( ( B ^ 2 ) - ( 3 x. ( A x. C ) ) ) )
cubic.n 
|- ( ph -> N = ( ( ( 2 x. ( B ^ 3 ) ) - ( ( 9 x. A ) x. ( B x. C ) ) ) + ( ; 2 7 x. ( ( A ^ 2 ) x. D ) ) ) )
cubic.0 
|- ( ph -> M =/= 0 )
Assertion cubic 
|- ( ph -> ( ( ( ( A x. ( X ^ 3 ) ) + ( B x. ( X ^ 2 ) ) ) + ( ( C x. X ) + D ) ) = 0 <-> E. r e. R X = -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / ( 3 x. A ) ) ) )

Proof

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