Metamath Proof Explorer

Theorem cubic2

Description: The solution to the general cubic equation, for arbitrary choices G and T of the square and cube roots. (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Hypotheses cubic2.a 
|- ( ph -> A e. CC )
cubic2.z 
|- ( ph -> A =/= 0 )
cubic2.b 
|- ( ph -> B e. CC )
cubic2.c 
|- ( ph -> C e. CC )
cubic2.d 
|- ( ph -> D e. CC )
cubic2.x 
|- ( ph -> X e. CC )
cubic2.t 
|- ( ph -> T e. CC )
cubic2.3 
|- ( ph -> ( T ^ 3 ) = ( ( N + G ) / 2 ) )
cubic2.g 
|- ( ph -> G e. CC )
cubic2.2 
|- ( ph -> ( G ^ 2 ) = ( ( N ^ 2 ) - ( 4 x. ( M ^ 3 ) ) ) )
cubic2.m 
|- ( ph -> M = ( ( B ^ 2 ) - ( 3 x. ( A x. C ) ) ) )
cubic2.n 
|- ( ph -> N = ( ( ( 2 x. ( B ^ 3 ) ) - ( ( 9 x. A ) x. ( B x. C ) ) ) + ( ; 2 7 x. ( ( A ^ 2 ) x. D ) ) ) )
cubic2.0 
|- ( ph -> T =/= 0 )
Assertion 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 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cubic2.a 
 |-  ( ph -> A e. CC )
2 cubic2.z 
 |-  ( ph -> A =/= 0 )
3 cubic2.b 
 |-  ( ph -> B e. CC )
4 cubic2.c 
 |-  ( ph -> C e. CC )
5 cubic2.d 
 |-  ( ph -> D e. CC )
6 cubic2.x 
 |-  ( ph -> X e. CC )
7 cubic2.t 
 |-  ( ph -> T e. CC )
8 cubic2.3 
 |-  ( ph -> ( T ^ 3 ) = ( ( N + G ) / 2 ) )
9 cubic2.g 
 |-  ( ph -> G e. CC )
10 cubic2.2 
 |-  ( ph -> ( G ^ 2 ) = ( ( N ^ 2 ) - ( 4 x. ( M ^ 3 ) ) ) )
11 cubic2.m 
 |-  ( ph -> M = ( ( B ^ 2 ) - ( 3 x. ( A x. C ) ) ) )
12 cubic2.n 
 |-  ( ph -> N = ( ( ( 2 x. ( B ^ 3 ) ) - ( ( 9 x. A ) x. ( B x. C ) ) ) + ( ; 2 7 x. ( ( A ^ 2 ) x. D ) ) ) )
13 cubic2.0 
 |-  ( ph -> T =/= 0 )
14 3nn0 
 |-  3 e. NN0
15 expcl 
 |-  ( ( X e. CC /\ 3 e. NN0 ) -> ( X ^ 3 ) e. CC )
16 6 14 15 sylancl 
 |-  ( ph -> ( X ^ 3 ) e. CC )
17 1 16 mulcld 
 |-  ( ph -> ( A x. ( X ^ 3 ) ) e. CC )
18 6 sqcld 
 |-  ( ph -> ( X ^ 2 ) e. CC )
19 3 18 mulcld 
 |-  ( ph -> ( B x. ( X ^ 2 ) ) e. CC )
20 17 19 addcld 
 |-  ( ph -> ( ( A x. ( X ^ 3 ) ) + ( B x. ( X ^ 2 ) ) ) e. CC )
21 4 6 mulcld 
 |-  ( ph -> ( C x. X ) e. CC )
22 21 5 addcld 
 |-  ( ph -> ( ( C x. X ) + D ) e. CC )
23 20 22 addcld 
 |-  ( ph -> ( ( ( A x. ( X ^ 3 ) ) + ( B x. ( X ^ 2 ) ) ) + ( ( C x. X ) + D ) ) e. CC )
24 23 1 2 diveq0ad 
 |-  ( ph -> ( ( ( ( ( A x. ( X ^ 3 ) ) + ( B x. ( X ^ 2 ) ) ) + ( ( C x. X ) + D ) ) / A ) = 0 <-> ( ( ( A x. ( X ^ 3 ) ) + ( B x. ( X ^ 2 ) ) ) + ( ( C x. X ) + D ) ) = 0 ) )
25 20 22 1 2 divdird 
 |-  ( ph -> ( ( ( ( A x. ( X ^ 3 ) ) + ( B x. ( X ^ 2 ) ) ) + ( ( C x. X ) + D ) ) / A ) = ( ( ( ( A x. ( X ^ 3 ) ) + ( B x. ( X ^ 2 ) ) ) / A ) + ( ( ( C x. X ) + D ) / A ) ) )
26 17 19 1 2 divdird 
 |-  ( ph -> ( ( ( A x. ( X ^ 3 ) ) + ( B x. ( X ^ 2 ) ) ) / A ) = ( ( ( A x. ( X ^ 3 ) ) / A ) + ( ( B x. ( X ^ 2 ) ) / A ) ) )
27 16 1 2 divcan3d 
 |-  ( ph -> ( ( A x. ( X ^ 3 ) ) / A ) = ( X ^ 3 ) )
28 3 18 1 2 div23d 
 |-  ( ph -> ( ( B x. ( X ^ 2 ) ) / A ) = ( ( B / A ) x. ( X ^ 2 ) ) )
29 27 28 oveq12d 
 |-  ( ph -> ( ( ( A x. ( X ^ 3 ) ) / A ) + ( ( B x. ( X ^ 2 ) ) / A ) ) = ( ( X ^ 3 ) + ( ( B / A ) x. ( X ^ 2 ) ) ) )
30 26 29 eqtrd 
 |-  ( ph -> ( ( ( A x. ( X ^ 3 ) ) + ( B x. ( X ^ 2 ) ) ) / A ) = ( ( X ^ 3 ) + ( ( B / A ) x. ( X ^ 2 ) ) ) )
31 21 5 1 2 divdird 
 |-  ( ph -> ( ( ( C x. X ) + D ) / A ) = ( ( ( C x. X ) / A ) + ( D / A ) ) )
32 4 6 1 2 div23d 
 |-  ( ph -> ( ( C x. X ) / A ) = ( ( C / A ) x. X ) )
33 32 oveq1d 
 |-  ( ph -> ( ( ( C x. X ) / A ) + ( D / A ) ) = ( ( ( C / A ) x. X ) + ( D / A ) ) )
34 31 33 eqtrd 
 |-  ( ph -> ( ( ( C x. X ) + D ) / A ) = ( ( ( C / A ) x. X ) + ( D / A ) ) )
35 30 34 oveq12d 
 |-  ( ph -> ( ( ( ( A x. ( X ^ 3 ) ) + ( B x. ( X ^ 2 ) ) ) / A ) + ( ( ( C x. X ) + D ) / A ) ) = ( ( ( X ^ 3 ) + ( ( B / A ) x. ( X ^ 2 ) ) ) + ( ( ( C / A ) x. X ) + ( D / A ) ) ) )
36 25 35 eqtrd 
 |-  ( ph -> ( ( ( ( A x. ( X ^ 3 ) ) + ( B x. ( X ^ 2 ) ) ) + ( ( C x. X ) + D ) ) / A ) = ( ( ( X ^ 3 ) + ( ( B / A ) x. ( X ^ 2 ) ) ) + ( ( ( C / A ) x. X ) + ( D / A ) ) ) )
37 36 eqeq1d 
 |-  ( ph -> ( ( ( ( ( A x. ( X ^ 3 ) ) + ( B x. ( X ^ 2 ) ) ) + ( ( C x. X ) + D ) ) / A ) = 0 <-> ( ( ( X ^ 3 ) + ( ( B / A ) x. ( X ^ 2 ) ) ) + ( ( ( C / A ) x. X ) + ( D / A ) ) ) = 0 ) )
38 24 37 bitr3d 
 |-  ( ph -> ( ( ( ( A x. ( X ^ 3 ) ) + ( B x. ( X ^ 2 ) ) ) + ( ( C x. X ) + D ) ) = 0 <-> ( ( ( X ^ 3 ) + ( ( B / A ) x. ( X ^ 2 ) ) ) + ( ( ( C / A ) x. X ) + ( D / A ) ) ) = 0 ) )
39 3 1 2 divcld 
 |-  ( ph -> ( B / A ) e. CC )
40 4 1 2 divcld 
 |-  ( ph -> ( C / A ) e. CC )
41 5 1 2 divcld 
 |-  ( ph -> ( D / A ) e. CC )
42 7 1 2 divcld 
 |-  ( ph -> ( T / A ) e. CC )
43 14 a1i 
 |-  ( ph -> 3 e. NN0 )
44 7 1 2 43 expdivd 
 |-  ( ph -> ( ( T / A ) ^ 3 ) = ( ( T ^ 3 ) / ( A ^ 3 ) ) )
45 8 oveq1d 
 |-  ( ph -> ( ( T ^ 3 ) / ( A ^ 3 ) ) = ( ( ( N + G ) / 2 ) / ( A ^ 3 ) ) )
46 2cn 
 |-  2 e. CC
47 expcl 
 |-  ( ( B e. CC /\ 3 e. NN0 ) -> ( B ^ 3 ) e. CC )
48 3 14 47 sylancl 
 |-  ( ph -> ( B ^ 3 ) e. CC )
49 mulcl 
 |-  ( ( 2 e. CC /\ ( B ^ 3 ) e. CC ) -> ( 2 x. ( B ^ 3 ) ) e. CC )
50 46 48 49 sylancr 
 |-  ( ph -> ( 2 x. ( B ^ 3 ) ) e. CC )
51 9cn 
 |-  9 e. CC
52 mulcl 
 |-  ( ( 9 e. CC /\ A e. CC ) -> ( 9 x. A ) e. CC )
53 51 1 52 sylancr 
 |-  ( ph -> ( 9 x. A ) e. CC )
54 3 4 mulcld 
 |-  ( ph -> ( B x. C ) e. CC )
55 53 54 mulcld 
 |-  ( ph -> ( ( 9 x. A ) x. ( B x. C ) ) e. CC )
56 50 55 subcld 
 |-  ( ph -> ( ( 2 x. ( B ^ 3 ) ) - ( ( 9 x. A ) x. ( B x. C ) ) ) e. CC )
57 2nn0 
 |-  2 e. NN0
58 7nn 
 |-  7 e. NN
59 57 58 decnncl 
 |-  ; 2 7 e. NN
60 59 nncni 
 |-  ; 2 7 e. CC
61 1 sqcld 
 |-  ( ph -> ( A ^ 2 ) e. CC )
62 61 5 mulcld 
 |-  ( ph -> ( ( A ^ 2 ) x. D ) e. CC )
63 mulcl 
 |-  ( ( ; 2 7 e. CC /\ ( ( A ^ 2 ) x. D ) e. CC ) -> ( ; 2 7 x. ( ( A ^ 2 ) x. D ) ) e. CC )
64 60 62 63 sylancr 
 |-  ( ph -> ( ; 2 7 x. ( ( A ^ 2 ) x. D ) ) e. CC )
65 56 64 addcld 
 |-  ( ph -> ( ( ( 2 x. ( B ^ 3 ) ) - ( ( 9 x. A ) x. ( B x. C ) ) ) + ( ; 2 7 x. ( ( A ^ 2 ) x. D ) ) ) e. CC )
66 12 65 eqeltrd 
 |-  ( ph -> N e. CC )
67 66 9 addcld 
 |-  ( ph -> ( N + G ) e. CC )
68 2cnd 
 |-  ( ph -> 2 e. CC )
69 expcl 
 |-  ( ( A e. CC /\ 3 e. NN0 ) -> ( A ^ 3 ) e. CC )
70 1 14 69 sylancl 
 |-  ( ph -> ( A ^ 3 ) e. CC )
71 2ne0 
 |-  2 =/= 0
72 71 a1i 
 |-  ( ph -> 2 =/= 0 )
73 3z 
 |-  3 e. ZZ
74 73 a1i 
 |-  ( ph -> 3 e. ZZ )
75 1 2 74 expne0d 
 |-  ( ph -> ( A ^ 3 ) =/= 0 )
76 67 68 70 72 75 divdiv32d 
 |-  ( ph -> ( ( ( N + G ) / 2 ) / ( A ^ 3 ) ) = ( ( ( N + G ) / ( A ^ 3 ) ) / 2 ) )
77 66 9 70 75 divdird 
 |-  ( ph -> ( ( N + G ) / ( A ^ 3 ) ) = ( ( N / ( A ^ 3 ) ) + ( G / ( A ^ 3 ) ) ) )
78 77 oveq1d 
 |-  ( ph -> ( ( ( N + G ) / ( A ^ 3 ) ) / 2 ) = ( ( ( N / ( A ^ 3 ) ) + ( G / ( A ^ 3 ) ) ) / 2 ) )
79 76 78 eqtrd 
 |-  ( ph -> ( ( ( N + G ) / 2 ) / ( A ^ 3 ) ) = ( ( ( N / ( A ^ 3 ) ) + ( G / ( A ^ 3 ) ) ) / 2 ) )
80 44 45 79 3eqtrd 
 |-  ( ph -> ( ( T / A ) ^ 3 ) = ( ( ( N / ( A ^ 3 ) ) + ( G / ( A ^ 3 ) ) ) / 2 ) )
81 9 70 75 divcld 
 |-  ( ph -> ( G / ( A ^ 3 ) ) e. CC )
82 9 70 75 sqdivd 
 |-  ( ph -> ( ( G / ( A ^ 3 ) ) ^ 2 ) = ( ( G ^ 2 ) / ( ( A ^ 3 ) ^ 2 ) ) )
83 10 oveq1d 
 |-  ( ph -> ( ( G ^ 2 ) / ( ( A ^ 3 ) ^ 2 ) ) = ( ( ( N ^ 2 ) - ( 4 x. ( M ^ 3 ) ) ) / ( ( A ^ 3 ) ^ 2 ) ) )
84 66 sqcld 
 |-  ( ph -> ( N ^ 2 ) e. CC )
85 4cn 
 |-  4 e. CC
86 3 sqcld 
 |-  ( ph -> ( B ^ 2 ) e. CC )
87 3cn 
 |-  3 e. CC
88 1 4 mulcld 
 |-  ( ph -> ( A x. C ) e. CC )
89 mulcl 
 |-  ( ( 3 e. CC /\ ( A x. C ) e. CC ) -> ( 3 x. ( A x. C ) ) e. CC )
90 87 88 89 sylancr 
 |-  ( ph -> ( 3 x. ( A x. C ) ) e. CC )
91 86 90 subcld 
 |-  ( ph -> ( ( B ^ 2 ) - ( 3 x. ( A x. C ) ) ) e. CC )
92 11 91 eqeltrd 
 |-  ( ph -> M e. CC )
93 expcl 
 |-  ( ( M e. CC /\ 3 e. NN0 ) -> ( M ^ 3 ) e. CC )
94 92 14 93 sylancl 
 |-  ( ph -> ( M ^ 3 ) e. CC )
95 mulcl 
 |-  ( ( 4 e. CC /\ ( M ^ 3 ) e. CC ) -> ( 4 x. ( M ^ 3 ) ) e. CC )
96 85 94 95 sylancr 
 |-  ( ph -> ( 4 x. ( M ^ 3 ) ) e. CC )
97 70 sqcld 
 |-  ( ph -> ( ( A ^ 3 ) ^ 2 ) e. CC )
98 sqne0 
 |-  ( ( A ^ 3 ) e. CC -> ( ( ( A ^ 3 ) ^ 2 ) =/= 0 <-> ( A ^ 3 ) =/= 0 ) )
99 70 98 syl 
 |-  ( ph -> ( ( ( A ^ 3 ) ^ 2 ) =/= 0 <-> ( A ^ 3 ) =/= 0 ) )
100 75 99 mpbird 
 |-  ( ph -> ( ( A ^ 3 ) ^ 2 ) =/= 0 )
101 84 96 97 100 divsubdird 
 |-  ( ph -> ( ( ( N ^ 2 ) - ( 4 x. ( M ^ 3 ) ) ) / ( ( A ^ 3 ) ^ 2 ) ) = ( ( ( N ^ 2 ) / ( ( A ^ 3 ) ^ 2 ) ) - ( ( 4 x. ( M ^ 3 ) ) / ( ( A ^ 3 ) ^ 2 ) ) ) )
102 66 70 75 sqdivd 
 |-  ( ph -> ( ( N / ( A ^ 3 ) ) ^ 2 ) = ( ( N ^ 2 ) / ( ( A ^ 3 ) ^ 2 ) ) )
103 2z 
 |-  2 e. ZZ
104 103 a1i 
 |-  ( ph -> 2 e. ZZ )
105 1 2 104 expne0d 
 |-  ( ph -> ( A ^ 2 ) =/= 0 )
106 92 61 105 43 expdivd 
 |-  ( ph -> ( ( M / ( A ^ 2 ) ) ^ 3 ) = ( ( M ^ 3 ) / ( ( A ^ 2 ) ^ 3 ) ) )
107 46 87 mulcomi 
 |-  ( 2 x. 3 ) = ( 3 x. 2 )
108 107 oveq2i 
 |-  ( A ^ ( 2 x. 3 ) ) = ( A ^ ( 3 x. 2 ) )
109 57 a1i 
 |-  ( ph -> 2 e. NN0 )
110 1 43 109 expmuld 
 |-  ( ph -> ( A ^ ( 2 x. 3 ) ) = ( ( A ^ 2 ) ^ 3 ) )
111 1 109 43 expmuld 
 |-  ( ph -> ( A ^ ( 3 x. 2 ) ) = ( ( A ^ 3 ) ^ 2 ) )
112 108 110 111 3eqtr3a 
 |-  ( ph -> ( ( A ^ 2 ) ^ 3 ) = ( ( A ^ 3 ) ^ 2 ) )
113 112 oveq2d 
 |-  ( ph -> ( ( M ^ 3 ) / ( ( A ^ 2 ) ^ 3 ) ) = ( ( M ^ 3 ) / ( ( A ^ 3 ) ^ 2 ) ) )
114 106 113 eqtrd 
 |-  ( ph -> ( ( M / ( A ^ 2 ) ) ^ 3 ) = ( ( M ^ 3 ) / ( ( A ^ 3 ) ^ 2 ) ) )
115 114 oveq2d 
 |-  ( ph -> ( 4 x. ( ( M / ( A ^ 2 ) ) ^ 3 ) ) = ( 4 x. ( ( M ^ 3 ) / ( ( A ^ 3 ) ^ 2 ) ) ) )
116 85 a1i 
 |-  ( ph -> 4 e. CC )
117 116 94 97 100 divassd 
 |-  ( ph -> ( ( 4 x. ( M ^ 3 ) ) / ( ( A ^ 3 ) ^ 2 ) ) = ( 4 x. ( ( M ^ 3 ) / ( ( A ^ 3 ) ^ 2 ) ) ) )
118 115 117 eqtr4d 
 |-  ( ph -> ( 4 x. ( ( M / ( A ^ 2 ) ) ^ 3 ) ) = ( ( 4 x. ( M ^ 3 ) ) / ( ( A ^ 3 ) ^ 2 ) ) )
119 102 118 oveq12d 
 |-  ( ph -> ( ( ( N / ( A ^ 3 ) ) ^ 2 ) - ( 4 x. ( ( M / ( A ^ 2 ) ) ^ 3 ) ) ) = ( ( ( N ^ 2 ) / ( ( A ^ 3 ) ^ 2 ) ) - ( ( 4 x. ( M ^ 3 ) ) / ( ( A ^ 3 ) ^ 2 ) ) ) )
120 101 119 eqtr4d 
 |-  ( ph -> ( ( ( N ^ 2 ) - ( 4 x. ( M ^ 3 ) ) ) / ( ( A ^ 3 ) ^ 2 ) ) = ( ( ( N / ( A ^ 3 ) ) ^ 2 ) - ( 4 x. ( ( M / ( A ^ 2 ) ) ^ 3 ) ) ) )
121 82 83 120 3eqtrd 
 |-  ( ph -> ( ( G / ( A ^ 3 ) ) ^ 2 ) = ( ( ( N / ( A ^ 3 ) ) ^ 2 ) - ( 4 x. ( ( M / ( A ^ 2 ) ) ^ 3 ) ) ) )
122 86 90 61 105 divsubdird 
 |-  ( ph -> ( ( ( B ^ 2 ) - ( 3 x. ( A x. C ) ) ) / ( A ^ 2 ) ) = ( ( ( B ^ 2 ) / ( A ^ 2 ) ) - ( ( 3 x. ( A x. C ) ) / ( A ^ 2 ) ) ) )
123 11 oveq1d 
 |-  ( ph -> ( M / ( A ^ 2 ) ) = ( ( ( B ^ 2 ) - ( 3 x. ( A x. C ) ) ) / ( A ^ 2 ) ) )
124 3 1 2 sqdivd 
 |-  ( ph -> ( ( B / A ) ^ 2 ) = ( ( B ^ 2 ) / ( A ^ 2 ) ) )
125 1 sqvald 
 |-  ( ph -> ( A ^ 2 ) = ( A x. A ) )
126 125 oveq2d 
 |-  ( ph -> ( ( A x. C ) / ( A ^ 2 ) ) = ( ( A x. C ) / ( A x. A ) ) )
127 4 1 1 2 2 divcan5d 
 |-  ( ph -> ( ( A x. C ) / ( A x. A ) ) = ( C / A ) )
128 126 127 eqtr2d 
 |-  ( ph -> ( C / A ) = ( ( A x. C ) / ( A ^ 2 ) ) )
129 128 oveq2d 
 |-  ( ph -> ( 3 x. ( C / A ) ) = ( 3 x. ( ( A x. C ) / ( A ^ 2 ) ) ) )
130 87 a1i 
 |-  ( ph -> 3 e. CC )
131 130 88 61 105 divassd 
 |-  ( ph -> ( ( 3 x. ( A x. C ) ) / ( A ^ 2 ) ) = ( 3 x. ( ( A x. C ) / ( A ^ 2 ) ) ) )
132 129 131 eqtr4d 
 |-  ( ph -> ( 3 x. ( C / A ) ) = ( ( 3 x. ( A x. C ) ) / ( A ^ 2 ) ) )
133 124 132 oveq12d 
 |-  ( ph -> ( ( ( B / A ) ^ 2 ) - ( 3 x. ( C / A ) ) ) = ( ( ( B ^ 2 ) / ( A ^ 2 ) ) - ( ( 3 x. ( A x. C ) ) / ( A ^ 2 ) ) ) )
134 122 123 133 3eqtr4d 
 |-  ( ph -> ( M / ( A ^ 2 ) ) = ( ( ( B / A ) ^ 2 ) - ( 3 x. ( C / A ) ) ) )
135 56 64 70 75 divdird 
 |-  ( ph -> ( ( ( ( 2 x. ( B ^ 3 ) ) - ( ( 9 x. A ) x. ( B x. C ) ) ) + ( ; 2 7 x. ( ( A ^ 2 ) x. D ) ) ) / ( A ^ 3 ) ) = ( ( ( ( 2 x. ( B ^ 3 ) ) - ( ( 9 x. A ) x. ( B x. C ) ) ) / ( A ^ 3 ) ) + ( ( ; 2 7 x. ( ( A ^ 2 ) x. D ) ) / ( A ^ 3 ) ) ) )
136 12 oveq1d 
 |-  ( ph -> ( N / ( A ^ 3 ) ) = ( ( ( ( 2 x. ( B ^ 3 ) ) - ( ( 9 x. A ) x. ( B x. C ) ) ) + ( ; 2 7 x. ( ( A ^ 2 ) x. D ) ) ) / ( A ^ 3 ) ) )
137 3 1 2 43 expdivd 
 |-  ( ph -> ( ( B / A ) ^ 3 ) = ( ( B ^ 3 ) / ( A ^ 3 ) ) )
138 137 oveq2d 
 |-  ( ph -> ( 2 x. ( ( B / A ) ^ 3 ) ) = ( 2 x. ( ( B ^ 3 ) / ( A ^ 3 ) ) ) )
139 68 48 70 75 divassd 
 |-  ( ph -> ( ( 2 x. ( B ^ 3 ) ) / ( A ^ 3 ) ) = ( 2 x. ( ( B ^ 3 ) / ( A ^ 3 ) ) ) )
140 138 139 eqtr4d 
 |-  ( ph -> ( 2 x. ( ( B / A ) ^ 3 ) ) = ( ( 2 x. ( B ^ 3 ) ) / ( A ^ 3 ) ) )
141 51 a1i 
 |-  ( ph -> 9 e. CC )
142 1 54 mulcld 
 |-  ( ph -> ( A x. ( B x. C ) ) e. CC )
143 141 142 70 75 divassd 
 |-  ( ph -> ( ( 9 x. ( A x. ( B x. C ) ) ) / ( A ^ 3 ) ) = ( 9 x. ( ( A x. ( B x. C ) ) / ( A ^ 3 ) ) ) )
144 141 1 54 mulassd 
 |-  ( ph -> ( ( 9 x. A ) x. ( B x. C ) ) = ( 9 x. ( A x. ( B x. C ) ) ) )
145 144 oveq1d 
 |-  ( ph -> ( ( ( 9 x. A ) x. ( B x. C ) ) / ( A ^ 3 ) ) = ( ( 9 x. ( A x. ( B x. C ) ) ) / ( A ^ 3 ) ) )
146 54 61 1 105 2 divcan5d 
 |-  ( ph -> ( ( A x. ( B x. C ) ) / ( A x. ( A ^ 2 ) ) ) = ( ( B x. C ) / ( A ^ 2 ) ) )
147 df-3 
 |-  3 = ( 2 + 1 )
148 147 oveq2i 
 |-  ( A ^ 3 ) = ( A ^ ( 2 + 1 ) )
149 expp1 
 |-  ( ( A e. CC /\ 2 e. NN0 ) -> ( A ^ ( 2 + 1 ) ) = ( ( A ^ 2 ) x. A ) )
150 1 57 149 sylancl 
 |-  ( ph -> ( A ^ ( 2 + 1 ) ) = ( ( A ^ 2 ) x. A ) )
151 148 150 eqtrid 
 |-  ( ph -> ( A ^ 3 ) = ( ( A ^ 2 ) x. A ) )
152 61 1 mulcomd 
 |-  ( ph -> ( ( A ^ 2 ) x. A ) = ( A x. ( A ^ 2 ) ) )
153 151 152 eqtrd 
 |-  ( ph -> ( A ^ 3 ) = ( A x. ( A ^ 2 ) ) )
154 153 oveq2d 
 |-  ( ph -> ( ( A x. ( B x. C ) ) / ( A ^ 3 ) ) = ( ( A x. ( B x. C ) ) / ( A x. ( A ^ 2 ) ) ) )
155 3 1 4 1 2 2 divmuldivd 
 |-  ( ph -> ( ( B / A ) x. ( C / A ) ) = ( ( B x. C ) / ( A x. A ) ) )
156 125 oveq2d 
 |-  ( ph -> ( ( B x. C ) / ( A ^ 2 ) ) = ( ( B x. C ) / ( A x. A ) ) )
157 155 156 eqtr4d 
 |-  ( ph -> ( ( B / A ) x. ( C / A ) ) = ( ( B x. C ) / ( A ^ 2 ) ) )
158 146 154 157 3eqtr4rd 
 |-  ( ph -> ( ( B / A ) x. ( C / A ) ) = ( ( A x. ( B x. C ) ) / ( A ^ 3 ) ) )
159 158 oveq2d 
 |-  ( ph -> ( 9 x. ( ( B / A ) x. ( C / A ) ) ) = ( 9 x. ( ( A x. ( B x. C ) ) / ( A ^ 3 ) ) ) )
160 143 145 159 3eqtr4rd 
 |-  ( ph -> ( 9 x. ( ( B / A ) x. ( C / A ) ) ) = ( ( ( 9 x. A ) x. ( B x. C ) ) / ( A ^ 3 ) ) )
161 140 160 oveq12d 
 |-  ( ph -> ( ( 2 x. ( ( B / A ) ^ 3 ) ) - ( 9 x. ( ( B / A ) x. ( C / A ) ) ) ) = ( ( ( 2 x. ( B ^ 3 ) ) / ( A ^ 3 ) ) - ( ( ( 9 x. A ) x. ( B x. C ) ) / ( A ^ 3 ) ) ) )
162 50 55 70 75 divsubdird 
 |-  ( ph -> ( ( ( 2 x. ( B ^ 3 ) ) - ( ( 9 x. A ) x. ( B x. C ) ) ) / ( A ^ 3 ) ) = ( ( ( 2 x. ( B ^ 3 ) ) / ( A ^ 3 ) ) - ( ( ( 9 x. A ) x. ( B x. C ) ) / ( A ^ 3 ) ) ) )
163 161 162 eqtr4d 
 |-  ( ph -> ( ( 2 x. ( ( B / A ) ^ 3 ) ) - ( 9 x. ( ( B / A ) x. ( C / A ) ) ) ) = ( ( ( 2 x. ( B ^ 3 ) ) - ( ( 9 x. A ) x. ( B x. C ) ) ) / ( A ^ 3 ) ) )
164 151 oveq2d 
 |-  ( ph -> ( ( ( A ^ 2 ) x. D ) / ( A ^ 3 ) ) = ( ( ( A ^ 2 ) x. D ) / ( ( A ^ 2 ) x. A ) ) )
165 5 1 61 2 105 divcan5d 
 |-  ( ph -> ( ( ( A ^ 2 ) x. D ) / ( ( A ^ 2 ) x. A ) ) = ( D / A ) )
166 164 165 eqtr2d 
 |-  ( ph -> ( D / A ) = ( ( ( A ^ 2 ) x. D ) / ( A ^ 3 ) ) )
167 166 oveq2d 
 |-  ( ph -> ( ; 2 7 x. ( D / A ) ) = ( ; 2 7 x. ( ( ( A ^ 2 ) x. D ) / ( A ^ 3 ) ) ) )
168 60 a1i 
 |-  ( ph -> ; 2 7 e. CC )
169 168 62 70 75 divassd 
 |-  ( ph -> ( ( ; 2 7 x. ( ( A ^ 2 ) x. D ) ) / ( A ^ 3 ) ) = ( ; 2 7 x. ( ( ( A ^ 2 ) x. D ) / ( A ^ 3 ) ) ) )
170 167 169 eqtr4d 
 |-  ( ph -> ( ; 2 7 x. ( D / A ) ) = ( ( ; 2 7 x. ( ( A ^ 2 ) x. D ) ) / ( A ^ 3 ) ) )
171 163 170 oveq12d 
 |-  ( ph -> ( ( ( 2 x. ( ( B / A ) ^ 3 ) ) - ( 9 x. ( ( B / A ) x. ( C / A ) ) ) ) + ( ; 2 7 x. ( D / A ) ) ) = ( ( ( ( 2 x. ( B ^ 3 ) ) - ( ( 9 x. A ) x. ( B x. C ) ) ) / ( A ^ 3 ) ) + ( ( ; 2 7 x. ( ( A ^ 2 ) x. D ) ) / ( A ^ 3 ) ) ) )
172 135 136 171 3eqtr4d 
 |-  ( ph -> ( N / ( A ^ 3 ) ) = ( ( ( 2 x. ( ( B / A ) ^ 3 ) ) - ( 9 x. ( ( B / A ) x. ( C / A ) ) ) ) + ( ; 2 7 x. ( D / A ) ) ) )
173 7 1 13 2 divne0d 
 |-  ( ph -> ( T / A ) =/= 0 )
174 39 40 41 6 42 80 81 121 134 172 173 mcubic 
 |-  ( ph -> ( ( ( ( X ^ 3 ) + ( ( B / A ) x. ( X ^ 2 ) ) ) + ( ( ( C / A ) x. X ) + ( D / A ) ) ) = 0 <-> E. r e. CC ( ( r ^ 3 ) = 1 /\ X = -u ( ( ( ( B / A ) + ( r x. ( T / A ) ) ) + ( ( M / ( A ^ 2 ) ) / ( r x. ( T / A ) ) ) ) / 3 ) ) ) )
175 oveq1 
 |-  ( r = 0 -> ( r ^ 3 ) = ( 0 ^ 3 ) )
176 3nn 
 |-  3 e. NN
177 0exp 
 |-  ( 3 e. NN -> ( 0 ^ 3 ) = 0 )
178 176 177 ax-mp 
 |-  ( 0 ^ 3 ) = 0
179 175 178 eqtrdi 
 |-  ( r = 0 -> ( r ^ 3 ) = 0 )
180 0ne1 
 |-  0 =/= 1
181 180 a1i 
 |-  ( r = 0 -> 0 =/= 1 )
182 179 181 eqnetrd 
 |-  ( r = 0 -> ( r ^ 3 ) =/= 1 )
183 182 necon2i 
 |-  ( ( r ^ 3 ) = 1 -> r =/= 0 )
184 simprl 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> r e. CC )
185 7 adantr 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> T e. CC )
186 1 adantr 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> A e. CC )
187 2 adantr 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> A =/= 0 )
188 184 185 186 187 divassd 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( r x. T ) / A ) = ( r x. ( T / A ) ) )
189 188 eqcomd 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( r x. ( T / A ) ) = ( ( r x. T ) / A ) )
190 189 oveq2d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( B / A ) + ( r x. ( T / A ) ) ) = ( ( B / A ) + ( ( r x. T ) / A ) ) )
191 3 adantr 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> B e. CC )
192 184 185 mulcld 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( r x. T ) e. CC )
193 191 192 186 187 divdird 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( B + ( r x. T ) ) / A ) = ( ( B / A ) + ( ( r x. T ) / A ) ) )
194 190 193 eqtr4d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( B / A ) + ( r x. ( T / A ) ) ) = ( ( B + ( r x. T ) ) / A ) )
195 92 adantr 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> M e. CC )
196 195 186 187 divcld 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( M / A ) e. CC )
197 simprr 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> r =/= 0 )
198 13 adantr 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> T =/= 0 )
199 184 185 197 198 mulne0d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( r x. T ) =/= 0 )
200 196 192 186 199 187 divcan7d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( ( M / A ) / A ) / ( ( r x. T ) / A ) ) = ( ( M / A ) / ( r x. T ) ) )
201 195 186 186 187 187 divdiv1d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( M / A ) / A ) = ( M / ( A x. A ) ) )
202 186 sqvald 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( A ^ 2 ) = ( A x. A ) )
203 202 oveq2d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( M / ( A ^ 2 ) ) = ( M / ( A x. A ) ) )
204 201 203 eqtr4d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( M / A ) / A ) = ( M / ( A ^ 2 ) ) )
205 204 188 oveq12d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( ( M / A ) / A ) / ( ( r x. T ) / A ) ) = ( ( M / ( A ^ 2 ) ) / ( r x. ( T / A ) ) ) )
206 195 186 192 187 199 divdiv32d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( M / A ) / ( r x. T ) ) = ( ( M / ( r x. T ) ) / A ) )
207 200 205 206 3eqtr3d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( M / ( A ^ 2 ) ) / ( r x. ( T / A ) ) ) = ( ( M / ( r x. T ) ) / A ) )
208 194 207 oveq12d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( ( B / A ) + ( r x. ( T / A ) ) ) + ( ( M / ( A ^ 2 ) ) / ( r x. ( T / A ) ) ) ) = ( ( ( B + ( r x. T ) ) / A ) + ( ( M / ( r x. T ) ) / A ) ) )
209 191 192 addcld 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( B + ( r x. T ) ) e. CC )
210 195 192 199 divcld 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( M / ( r x. T ) ) e. CC )
211 209 210 186 187 divdird 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / A ) = ( ( ( B + ( r x. T ) ) / A ) + ( ( M / ( r x. T ) ) / A ) ) )
212 208 211 eqtr4d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( ( B / A ) + ( r x. ( T / A ) ) ) + ( ( M / ( A ^ 2 ) ) / ( r x. ( T / A ) ) ) ) = ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / A ) )
213 212 oveq1d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( ( ( B / A ) + ( r x. ( T / A ) ) ) + ( ( M / ( A ^ 2 ) ) / ( r x. ( T / A ) ) ) ) / 3 ) = ( ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / A ) / 3 ) )
214 209 210 addcld 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) e. CC )
215 87 a1i 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> 3 e. CC )
216 3ne0 
 |-  3 =/= 0
217 216 a1i 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> 3 =/= 0 )
218 214 186 215 187 217 divdiv1d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / A ) / 3 ) = ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / ( A x. 3 ) ) )
219 mulcom 
 |-  ( ( A e. CC /\ 3 e. CC ) -> ( A x. 3 ) = ( 3 x. A ) )
220 186 87 219 sylancl 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( A x. 3 ) = ( 3 x. A ) )
221 220 oveq2d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / ( A x. 3 ) ) = ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / ( 3 x. A ) ) )
222 213 218 221 3eqtrd 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( ( ( B / A ) + ( r x. ( T / A ) ) ) + ( ( M / ( A ^ 2 ) ) / ( r x. ( T / A ) ) ) ) / 3 ) = ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / ( 3 x. A ) ) )
223 222 negeqd 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> -u ( ( ( ( B / A ) + ( r x. ( T / A ) ) ) + ( ( M / ( A ^ 2 ) ) / ( r x. ( T / A ) ) ) ) / 3 ) = -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / ( 3 x. A ) ) )
224 223 eqeq2d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( X = -u ( ( ( ( B / A ) + ( r x. ( T / A ) ) ) + ( ( M / ( A ^ 2 ) ) / ( r x. ( T / A ) ) ) ) / 3 ) <-> X = -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / ( 3 x. A ) ) ) )
225 224 anassrs 
 |-  ( ( ( ph /\ r e. CC ) /\ r =/= 0 ) -> ( X = -u ( ( ( ( B / A ) + ( r x. ( T / A ) ) ) + ( ( M / ( A ^ 2 ) ) / ( r x. ( T / A ) ) ) ) / 3 ) <-> X = -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / ( 3 x. A ) ) ) )
226 183 225 sylan2 
 |-  ( ( ( ph /\ r e. CC ) /\ ( r ^ 3 ) = 1 ) -> ( X = -u ( ( ( ( B / A ) + ( r x. ( T / A ) ) ) + ( ( M / ( A ^ 2 ) ) / ( r x. ( T / A ) ) ) ) / 3 ) <-> X = -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / ( 3 x. A ) ) ) )
227 226 pm5.32da 
 |-  ( ( ph /\ r e. CC ) -> ( ( ( r ^ 3 ) = 1 /\ X = -u ( ( ( ( B / A ) + ( r x. ( T / A ) ) ) + ( ( M / ( A ^ 2 ) ) / ( r x. ( T / A ) ) ) ) / 3 ) ) <-> ( ( r ^ 3 ) = 1 /\ X = -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / ( 3 x. A ) ) ) ) )
228 227 rexbidva 
 |-  ( ph -> ( E. r e. CC ( ( r ^ 3 ) = 1 /\ X = -u ( ( ( ( B / A ) + ( r x. ( T / A ) ) ) + ( ( M / ( A ^ 2 ) ) / ( r x. ( T / A ) ) ) ) / 3 ) ) <-> E. r e. CC ( ( r ^ 3 ) = 1 /\ X = -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / ( 3 x. A ) ) ) ) )
229 38 174 228 3bitrd 
 |-  ( 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 ) ) ) ) )