Metamath Proof Explorer

Theorem mcubic

Description: Solutions to a monic cubic equation, a special case of cubic . (Contributed by Mario Carneiro, 24-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 mcubic.b 
 |-  ( ph -> B e. CC )
2 mcubic.c 
 |-  ( ph -> C e. CC )
3 mcubic.d 
 |-  ( ph -> D e. CC )
4 mcubic.x 
 |-  ( ph -> X e. CC )
5 mcubic.t 
 |-  ( ph -> T e. CC )
6 mcubic.3 
 |-  ( ph -> ( T ^ 3 ) = ( ( N + G ) / 2 ) )
7 mcubic.g 
 |-  ( ph -> G e. CC )
8 mcubic.2 
 |-  ( ph -> ( G ^ 2 ) = ( ( N ^ 2 ) - ( 4 x. ( M ^ 3 ) ) ) )
9 mcubic.m 
 |-  ( ph -> M = ( ( B ^ 2 ) - ( 3 x. C ) ) )
10 mcubic.n 
 |-  ( ph -> N = ( ( ( 2 x. ( B ^ 3 ) ) - ( 9 x. ( B x. C ) ) ) + ( ; 2 7 x. D ) ) )
11 mcubic.0 
 |-  ( ph -> T =/= 0 )
12 1 sqcld 
 |-  ( ph -> ( B ^ 2 ) e. CC )
13 3cn 
 |-  3 e. CC
14 mulcl 
 |-  ( ( 3 e. CC /\ C e. CC ) -> ( 3 x. C ) e. CC )
15 13 2 14 sylancr 
 |-  ( ph -> ( 3 x. C ) e. CC )
16 12 15 subcld 
 |-  ( ph -> ( ( B ^ 2 ) - ( 3 x. C ) ) e. CC )
17 9 16 eqeltrd 
 |-  ( ph -> M e. CC )
18 13 a1i 
 |-  ( ph -> 3 e. CC )
19 3ne0 
 |-  3 =/= 0
20 19 a1i 
 |-  ( ph -> 3 =/= 0 )
21 17 18 20 divcld 
 |-  ( ph -> ( M / 3 ) e. CC )
22 21 negcld 
 |-  ( ph -> -u ( M / 3 ) e. CC )
23 2cn 
 |-  2 e. CC
24 3nn0 
 |-  3 e. NN0
25 expcl 
 |-  ( ( B e. CC /\ 3 e. NN0 ) -> ( B ^ 3 ) e. CC )
26 1 24 25 sylancl 
 |-  ( ph -> ( B ^ 3 ) e. CC )
27 mulcl 
 |-  ( ( 2 e. CC /\ ( B ^ 3 ) e. CC ) -> ( 2 x. ( B ^ 3 ) ) e. CC )
28 23 26 27 sylancr 
 |-  ( ph -> ( 2 x. ( B ^ 3 ) ) e. CC )
29 9cn 
 |-  9 e. CC
30 1 2 mulcld 
 |-  ( ph -> ( B x. C ) e. CC )
31 mulcl 
 |-  ( ( 9 e. CC /\ ( B x. C ) e. CC ) -> ( 9 x. ( B x. C ) ) e. CC )
32 29 30 31 sylancr 
 |-  ( ph -> ( 9 x. ( B x. C ) ) e. CC )
33 28 32 subcld 
 |-  ( ph -> ( ( 2 x. ( B ^ 3 ) ) - ( 9 x. ( B x. C ) ) ) e. CC )
34 2nn0 
 |-  2 e. NN0
35 7nn 
 |-  7 e. NN
36 34 35 decnncl 
 |-  ; 2 7 e. NN
37 36 nncni 
 |-  ; 2 7 e. CC
38 mulcl 
 |-  ( ( ; 2 7 e. CC /\ D e. CC ) -> ( ; 2 7 x. D ) e. CC )
39 37 3 38 sylancr 
 |-  ( ph -> ( ; 2 7 x. D ) e. CC )
40 33 39 addcld 
 |-  ( ph -> ( ( ( 2 x. ( B ^ 3 ) ) - ( 9 x. ( B x. C ) ) ) + ( ; 2 7 x. D ) ) e. CC )
41 10 40 eqeltrd 
 |-  ( ph -> N e. CC )
42 37 a1i 
 |-  ( ph -> ; 2 7 e. CC )
43 36 nnne0i 
 |-  ; 2 7 =/= 0
44 43 a1i 
 |-  ( ph -> ; 2 7 =/= 0 )
45 41 42 44 divcld 
 |-  ( ph -> ( N / ; 2 7 ) e. CC )
46 1 18 20 divcld 
 |-  ( ph -> ( B / 3 ) e. CC )
47 4 46 addcld 
 |-  ( ph -> ( X + ( B / 3 ) ) e. CC )
48 5 18 20 divcld 
 |-  ( ph -> ( T / 3 ) e. CC )
49 48 negcld 
 |-  ( ph -> -u ( T / 3 ) e. CC )
50 3nn 
 |-  3 e. NN
51 50 a1i 
 |-  ( ph -> 3 e. NN )
52 n2dvds3 
 |-  -. 2 || 3
53 52 a1i 
 |-  ( ph -> -. 2 || 3 )
54 oexpneg 
 |-  ( ( ( T / 3 ) e. CC /\ 3 e. NN /\ -. 2 || 3 ) -> ( -u ( T / 3 ) ^ 3 ) = -u ( ( T / 3 ) ^ 3 ) )
55 48 51 53 54 syl3anc 
 |-  ( ph -> ( -u ( T / 3 ) ^ 3 ) = -u ( ( T / 3 ) ^ 3 ) )
56 24 a1i 
 |-  ( ph -> 3 e. NN0 )
57 5 18 20 56 expdivd 
 |-  ( ph -> ( ( T / 3 ) ^ 3 ) = ( ( T ^ 3 ) / ( 3 ^ 3 ) ) )
58 3exp3 
 |-  ( 3 ^ 3 ) = ; 2 7
59 58 a1i 
 |-  ( ph -> ( 3 ^ 3 ) = ; 2 7 )
60 6 59 oveq12d 
 |-  ( ph -> ( ( T ^ 3 ) / ( 3 ^ 3 ) ) = ( ( ( N + G ) / 2 ) / ; 2 7 ) )
61 41 7 addcld 
 |-  ( ph -> ( N + G ) e. CC )
62 2cnd 
 |-  ( ph -> 2 e. CC )
63 2ne0 
 |-  2 =/= 0
64 63 a1i 
 |-  ( ph -> 2 =/= 0 )
65 61 62 42 64 44 divdiv32d 
 |-  ( ph -> ( ( ( N + G ) / 2 ) / ; 2 7 ) = ( ( ( N + G ) / ; 2 7 ) / 2 ) )
66 41 7 addcomd 
 |-  ( ph -> ( N + G ) = ( G + N ) )
67 66 oveq1d 
 |-  ( ph -> ( ( N + G ) / ; 2 7 ) = ( ( G + N ) / ; 2 7 ) )
68 7 41 42 44 divdird 
 |-  ( ph -> ( ( G + N ) / ; 2 7 ) = ( ( G / ; 2 7 ) + ( N / ; 2 7 ) ) )
69 67 68 eqtrd 
 |-  ( ph -> ( ( N + G ) / ; 2 7 ) = ( ( G / ; 2 7 ) + ( N / ; 2 7 ) ) )
70 69 oveq1d 
 |-  ( ph -> ( ( ( N + G ) / ; 2 7 ) / 2 ) = ( ( ( G / ; 2 7 ) + ( N / ; 2 7 ) ) / 2 ) )
71 7 42 44 divcld 
 |-  ( ph -> ( G / ; 2 7 ) e. CC )
72 71 45 62 64 divdird 
 |-  ( ph -> ( ( ( G / ; 2 7 ) + ( N / ; 2 7 ) ) / 2 ) = ( ( ( G / ; 2 7 ) / 2 ) + ( ( N / ; 2 7 ) / 2 ) ) )
73 65 70 72 3eqtrd 
 |-  ( ph -> ( ( ( N + G ) / 2 ) / ; 2 7 ) = ( ( ( G / ; 2 7 ) / 2 ) + ( ( N / ; 2 7 ) / 2 ) ) )
74 57 60 73 3eqtrd 
 |-  ( ph -> ( ( T / 3 ) ^ 3 ) = ( ( ( G / ; 2 7 ) / 2 ) + ( ( N / ; 2 7 ) / 2 ) ) )
75 74 negeqd 
 |-  ( ph -> -u ( ( T / 3 ) ^ 3 ) = -u ( ( ( G / ; 2 7 ) / 2 ) + ( ( N / ; 2 7 ) / 2 ) ) )
76 71 halfcld 
 |-  ( ph -> ( ( G / ; 2 7 ) / 2 ) e. CC )
77 45 halfcld 
 |-  ( ph -> ( ( N / ; 2 7 ) / 2 ) e. CC )
78 76 77 negdi2d 
 |-  ( ph -> -u ( ( ( G / ; 2 7 ) / 2 ) + ( ( N / ; 2 7 ) / 2 ) ) = ( -u ( ( G / ; 2 7 ) / 2 ) - ( ( N / ; 2 7 ) / 2 ) ) )
79 55 75 78 3eqtrd 
 |-  ( ph -> ( -u ( T / 3 ) ^ 3 ) = ( -u ( ( G / ; 2 7 ) / 2 ) - ( ( N / ; 2 7 ) / 2 ) ) )
80 76 negcld 
 |-  ( ph -> -u ( ( G / ; 2 7 ) / 2 ) e. CC )
81 sqneg 
 |-  ( ( ( G / ; 2 7 ) / 2 ) e. CC -> ( -u ( ( G / ; 2 7 ) / 2 ) ^ 2 ) = ( ( ( G / ; 2 7 ) / 2 ) ^ 2 ) )
82 76 81 syl 
 |-  ( ph -> ( -u ( ( G / ; 2 7 ) / 2 ) ^ 2 ) = ( ( ( G / ; 2 7 ) / 2 ) ^ 2 ) )
83 71 62 64 sqdivd 
 |-  ( ph -> ( ( ( G / ; 2 7 ) / 2 ) ^ 2 ) = ( ( ( G / ; 2 7 ) ^ 2 ) / ( 2 ^ 2 ) ) )
84 45 62 64 sqdivd 
 |-  ( ph -> ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) = ( ( ( N / ; 2 7 ) ^ 2 ) / ( 2 ^ 2 ) ) )
85 41 42 44 sqdivd 
 |-  ( ph -> ( ( N / ; 2 7 ) ^ 2 ) = ( ( N ^ 2 ) / ( ; 2 7 ^ 2 ) ) )
86 85 oveq1d 
 |-  ( ph -> ( ( ( N / ; 2 7 ) ^ 2 ) / ( 2 ^ 2 ) ) = ( ( ( N ^ 2 ) / ( ; 2 7 ^ 2 ) ) / ( 2 ^ 2 ) ) )
87 84 86 eqtr2d 
 |-  ( ph -> ( ( ( N ^ 2 ) / ( ; 2 7 ^ 2 ) ) / ( 2 ^ 2 ) ) = ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) )
88 4cn 
 |-  4 e. CC
89 88 a1i 
 |-  ( ph -> 4 e. CC )
90 expcl 
 |-  ( ( M e. CC /\ 3 e. NN0 ) -> ( M ^ 3 ) e. CC )
91 17 24 90 sylancl 
 |-  ( ph -> ( M ^ 3 ) e. CC )
92 37 sqcli 
 |-  ( ; 2 7 ^ 2 ) e. CC
93 92 a1i 
 |-  ( ph -> ( ; 2 7 ^ 2 ) e. CC )
94 sqne0 
 |-  ( ; 2 7 e. CC -> ( ( ; 2 7 ^ 2 ) =/= 0 <-> ; 2 7 =/= 0 ) )
95 42 94 syl 
 |-  ( ph -> ( ( ; 2 7 ^ 2 ) =/= 0 <-> ; 2 7 =/= 0 ) )
96 44 95 mpbird 
 |-  ( ph -> ( ; 2 7 ^ 2 ) =/= 0 )
97 89 91 93 96 divassd 
 |-  ( ph -> ( ( 4 x. ( M ^ 3 ) ) / ( ; 2 7 ^ 2 ) ) = ( 4 x. ( ( M ^ 3 ) / ( ; 2 7 ^ 2 ) ) ) )
98 29 a1i 
 |-  ( ph -> 9 e. CC )
99 9nn 
 |-  9 e. NN
100 99 nnne0i 
 |-  9 =/= 0
101 100 a1i 
 |-  ( ph -> 9 =/= 0 )
102 17 98 101 56 expdivd 
 |-  ( ph -> ( ( M / 9 ) ^ 3 ) = ( ( M ^ 3 ) / ( 9 ^ 3 ) ) )
103 23 13 mulcomi 
 |-  ( 2 x. 3 ) = ( 3 x. 2 )
104 103 oveq2i 
 |-  ( 3 ^ ( 2 x. 3 ) ) = ( 3 ^ ( 3 x. 2 ) )
105 expmul 
 |-  ( ( 3 e. CC /\ 2 e. NN0 /\ 3 e. NN0 ) -> ( 3 ^ ( 2 x. 3 ) ) = ( ( 3 ^ 2 ) ^ 3 ) )
106 13 34 24 105 mp3an 
 |-  ( 3 ^ ( 2 x. 3 ) ) = ( ( 3 ^ 2 ) ^ 3 )
107 expmul 
 |-  ( ( 3 e. CC /\ 3 e. NN0 /\ 2 e. NN0 ) -> ( 3 ^ ( 3 x. 2 ) ) = ( ( 3 ^ 3 ) ^ 2 ) )
108 13 24 34 107 mp3an 
 |-  ( 3 ^ ( 3 x. 2 ) ) = ( ( 3 ^ 3 ) ^ 2 )
109 104 106 108 3eqtr3i 
 |-  ( ( 3 ^ 2 ) ^ 3 ) = ( ( 3 ^ 3 ) ^ 2 )
110 sq3 
 |-  ( 3 ^ 2 ) = 9
111 110 oveq1i 
 |-  ( ( 3 ^ 2 ) ^ 3 ) = ( 9 ^ 3 )
112 58 oveq1i 
 |-  ( ( 3 ^ 3 ) ^ 2 ) = ( ; 2 7 ^ 2 )
113 109 111 112 3eqtr3i 
 |-  ( 9 ^ 3 ) = ( ; 2 7 ^ 2 )
114 113 oveq2i 
 |-  ( ( M ^ 3 ) / ( 9 ^ 3 ) ) = ( ( M ^ 3 ) / ( ; 2 7 ^ 2 ) )
115 102 114 eqtrdi 
 |-  ( ph -> ( ( M / 9 ) ^ 3 ) = ( ( M ^ 3 ) / ( ; 2 7 ^ 2 ) ) )
116 115 oveq2d 
 |-  ( ph -> ( 4 x. ( ( M / 9 ) ^ 3 ) ) = ( 4 x. ( ( M ^ 3 ) / ( ; 2 7 ^ 2 ) ) ) )
117 97 116 eqtr4d 
 |-  ( ph -> ( ( 4 x. ( M ^ 3 ) ) / ( ; 2 7 ^ 2 ) ) = ( 4 x. ( ( M / 9 ) ^ 3 ) ) )
118 117 oveq1d 
 |-  ( ph -> ( ( ( 4 x. ( M ^ 3 ) ) / ( ; 2 7 ^ 2 ) ) / ( 2 ^ 2 ) ) = ( ( 4 x. ( ( M / 9 ) ^ 3 ) ) / ( 2 ^ 2 ) ) )
119 sq2 
 |-  ( 2 ^ 2 ) = 4
120 119 oveq2i 
 |-  ( ( 4 x. ( ( M / 9 ) ^ 3 ) ) / ( 2 ^ 2 ) ) = ( ( 4 x. ( ( M / 9 ) ^ 3 ) ) / 4 )
121 17 98 101 divcld 
 |-  ( ph -> ( M / 9 ) e. CC )
122 expcl 
 |-  ( ( ( M / 9 ) e. CC /\ 3 e. NN0 ) -> ( ( M / 9 ) ^ 3 ) e. CC )
123 121 24 122 sylancl 
 |-  ( ph -> ( ( M / 9 ) ^ 3 ) e. CC )
124 4ne0 
 |-  4 =/= 0
125 124 a1i 
 |-  ( ph -> 4 =/= 0 )
126 123 89 125 divcan3d 
 |-  ( ph -> ( ( 4 x. ( ( M / 9 ) ^ 3 ) ) / 4 ) = ( ( M / 9 ) ^ 3 ) )
127 120 126 eqtrid 
 |-  ( ph -> ( ( 4 x. ( ( M / 9 ) ^ 3 ) ) / ( 2 ^ 2 ) ) = ( ( M / 9 ) ^ 3 ) )
128 118 127 eqtrd 
 |-  ( ph -> ( ( ( 4 x. ( M ^ 3 ) ) / ( ; 2 7 ^ 2 ) ) / ( 2 ^ 2 ) ) = ( ( M / 9 ) ^ 3 ) )
129 87 128 oveq12d 
 |-  ( ph -> ( ( ( ( N ^ 2 ) / ( ; 2 7 ^ 2 ) ) / ( 2 ^ 2 ) ) - ( ( ( 4 x. ( M ^ 3 ) ) / ( ; 2 7 ^ 2 ) ) / ( 2 ^ 2 ) ) ) = ( ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) - ( ( M / 9 ) ^ 3 ) ) )
130 41 sqcld 
 |-  ( ph -> ( N ^ 2 ) e. CC )
131 130 93 96 divcld 
 |-  ( ph -> ( ( N ^ 2 ) / ( ; 2 7 ^ 2 ) ) e. CC )
132 mulcl 
 |-  ( ( 4 e. CC /\ ( M ^ 3 ) e. CC ) -> ( 4 x. ( M ^ 3 ) ) e. CC )
133 88 91 132 sylancr 
 |-  ( ph -> ( 4 x. ( M ^ 3 ) ) e. CC )
134 133 93 96 divcld 
 |-  ( ph -> ( ( 4 x. ( M ^ 3 ) ) / ( ; 2 7 ^ 2 ) ) e. CC )
135 23 sqcli 
 |-  ( 2 ^ 2 ) e. CC
136 135 a1i 
 |-  ( ph -> ( 2 ^ 2 ) e. CC )
137 119 124 eqnetri 
 |-  ( 2 ^ 2 ) =/= 0
138 137 a1i 
 |-  ( ph -> ( 2 ^ 2 ) =/= 0 )
139 131 134 136 138 divsubdird 
 |-  ( ph -> ( ( ( ( N ^ 2 ) / ( ; 2 7 ^ 2 ) ) - ( ( 4 x. ( M ^ 3 ) ) / ( ; 2 7 ^ 2 ) ) ) / ( 2 ^ 2 ) ) = ( ( ( ( N ^ 2 ) / ( ; 2 7 ^ 2 ) ) / ( 2 ^ 2 ) ) - ( ( ( 4 x. ( M ^ 3 ) ) / ( ; 2 7 ^ 2 ) ) / ( 2 ^ 2 ) ) ) )
140 77 sqcld 
 |-  ( ph -> ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) e. CC )
141 140 123 negsubd 
 |-  ( ph -> ( ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) + -u ( ( M / 9 ) ^ 3 ) ) = ( ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) - ( ( M / 9 ) ^ 3 ) ) )
142 129 139 141 3eqtr4d 
 |-  ( ph -> ( ( ( ( N ^ 2 ) / ( ; 2 7 ^ 2 ) ) - ( ( 4 x. ( M ^ 3 ) ) / ( ; 2 7 ^ 2 ) ) ) / ( 2 ^ 2 ) ) = ( ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) + -u ( ( M / 9 ) ^ 3 ) ) )
143 7 42 44 sqdivd 
 |-  ( ph -> ( ( G / ; 2 7 ) ^ 2 ) = ( ( G ^ 2 ) / ( ; 2 7 ^ 2 ) ) )
144 8 oveq1d 
 |-  ( ph -> ( ( G ^ 2 ) / ( ; 2 7 ^ 2 ) ) = ( ( ( N ^ 2 ) - ( 4 x. ( M ^ 3 ) ) ) / ( ; 2 7 ^ 2 ) ) )
145 130 133 93 96 divsubdird 
 |-  ( ph -> ( ( ( N ^ 2 ) - ( 4 x. ( M ^ 3 ) ) ) / ( ; 2 7 ^ 2 ) ) = ( ( ( N ^ 2 ) / ( ; 2 7 ^ 2 ) ) - ( ( 4 x. ( M ^ 3 ) ) / ( ; 2 7 ^ 2 ) ) ) )
146 143 144 145 3eqtrd 
 |-  ( ph -> ( ( G / ; 2 7 ) ^ 2 ) = ( ( ( N ^ 2 ) / ( ; 2 7 ^ 2 ) ) - ( ( 4 x. ( M ^ 3 ) ) / ( ; 2 7 ^ 2 ) ) ) )
147 146 oveq1d 
 |-  ( ph -> ( ( ( G / ; 2 7 ) ^ 2 ) / ( 2 ^ 2 ) ) = ( ( ( ( N ^ 2 ) / ( ; 2 7 ^ 2 ) ) - ( ( 4 x. ( M ^ 3 ) ) / ( ; 2 7 ^ 2 ) ) ) / ( 2 ^ 2 ) ) )
148 oexpneg 
 |-  ( ( ( M / 9 ) e. CC /\ 3 e. NN /\ -. 2 || 3 ) -> ( -u ( M / 9 ) ^ 3 ) = -u ( ( M / 9 ) ^ 3 ) )
149 121 51 53 148 syl3anc 
 |-  ( ph -> ( -u ( M / 9 ) ^ 3 ) = -u ( ( M / 9 ) ^ 3 ) )
150 149 oveq2d 
 |-  ( ph -> ( ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) + ( -u ( M / 9 ) ^ 3 ) ) = ( ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) + -u ( ( M / 9 ) ^ 3 ) ) )
151 142 147 150 3eqtr4d 
 |-  ( ph -> ( ( ( G / ; 2 7 ) ^ 2 ) / ( 2 ^ 2 ) ) = ( ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) + ( -u ( M / 9 ) ^ 3 ) ) )
152 82 83 151 3eqtrd 
 |-  ( ph -> ( -u ( ( G / ; 2 7 ) / 2 ) ^ 2 ) = ( ( ( ( N / ; 2 7 ) / 2 ) ^ 2 ) + ( -u ( M / 9 ) ^ 3 ) ) )
153 17 18 18 20 20 divdiv1d 
 |-  ( ph -> ( ( M / 3 ) / 3 ) = ( M / ( 3 x. 3 ) ) )
154 3t3e9 
 |-  ( 3 x. 3 ) = 9
155 154 oveq2i 
 |-  ( M / ( 3 x. 3 ) ) = ( M / 9 )
156 153 155 eqtrdi 
 |-  ( ph -> ( ( M / 3 ) / 3 ) = ( M / 9 ) )
157 156 negeqd 
 |-  ( ph -> -u ( ( M / 3 ) / 3 ) = -u ( M / 9 ) )
158 21 18 20 divnegd 
 |-  ( ph -> -u ( ( M / 3 ) / 3 ) = ( -u ( M / 3 ) / 3 ) )
159 157 158 eqtr3d 
 |-  ( ph -> -u ( M / 9 ) = ( -u ( M / 3 ) / 3 ) )
160 eqidd 
 |-  ( ph -> ( ( N / ; 2 7 ) / 2 ) = ( ( N / ; 2 7 ) / 2 ) )
161 5 18 11 20 divne0d 
 |-  ( ph -> ( T / 3 ) =/= 0 )
162 48 161 negne0d 
 |-  ( ph -> -u ( T / 3 ) =/= 0 )
163 22 45 47 49 79 80 152 159 160 162 dcubic 
 |-  ( ph -> ( ( ( ( X + ( B / 3 ) ) ^ 3 ) + ( ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) + ( N / ; 2 7 ) ) ) = 0 <-> E. r e. CC ( ( r ^ 3 ) = 1 /\ ( X + ( B / 3 ) ) = ( ( r x. -u ( T / 3 ) ) - ( -u ( M / 9 ) / ( r x. -u ( T / 3 ) ) ) ) ) ) )
164 binom3 
 |-  ( ( X e. CC /\ ( B / 3 ) e. CC ) -> ( ( X + ( B / 3 ) ) ^ 3 ) = ( ( ( X ^ 3 ) + ( 3 x. ( ( X ^ 2 ) x. ( B / 3 ) ) ) ) + ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) ) )
165 4 46 164 syl2anc 
 |-  ( ph -> ( ( X + ( B / 3 ) ) ^ 3 ) = ( ( ( X ^ 3 ) + ( 3 x. ( ( X ^ 2 ) x. ( B / 3 ) ) ) ) + ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) ) )
166 4 sqcld 
 |-  ( ph -> ( X ^ 2 ) e. CC )
167 18 166 46 mul12d 
 |-  ( ph -> ( 3 x. ( ( X ^ 2 ) x. ( B / 3 ) ) ) = ( ( X ^ 2 ) x. ( 3 x. ( B / 3 ) ) ) )
168 1 18 20 divcan2d 
 |-  ( ph -> ( 3 x. ( B / 3 ) ) = B )
169 168 oveq2d 
 |-  ( ph -> ( ( X ^ 2 ) x. ( 3 x. ( B / 3 ) ) ) = ( ( X ^ 2 ) x. B ) )
170 166 1 mulcomd 
 |-  ( ph -> ( ( X ^ 2 ) x. B ) = ( B x. ( X ^ 2 ) ) )
171 167 169 170 3eqtrd 
 |-  ( ph -> ( 3 x. ( ( X ^ 2 ) x. ( B / 3 ) ) ) = ( B x. ( X ^ 2 ) ) )
172 171 oveq2d 
 |-  ( ph -> ( ( X ^ 3 ) + ( 3 x. ( ( X ^ 2 ) x. ( B / 3 ) ) ) ) = ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) )
173 172 oveq1d 
 |-  ( ph -> ( ( ( X ^ 3 ) + ( 3 x. ( ( X ^ 2 ) x. ( B / 3 ) ) ) ) + ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) ) = ( ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) + ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) ) )
174 165 173 eqtrd 
 |-  ( ph -> ( ( X + ( B / 3 ) ) ^ 3 ) = ( ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) + ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) ) )
175 174 oveq1d 
 |-  ( ph -> ( ( ( X + ( B / 3 ) ) ^ 3 ) + ( ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) + ( N / ; 2 7 ) ) ) = ( ( ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) + ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) ) + ( ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) + ( N / ; 2 7 ) ) ) )
176 expcl 
 |-  ( ( X e. CC /\ 3 e. NN0 ) -> ( X ^ 3 ) e. CC )
177 4 24 176 sylancl 
 |-  ( ph -> ( X ^ 3 ) e. CC )
178 1 166 mulcld 
 |-  ( ph -> ( B x. ( X ^ 2 ) ) e. CC )
179 177 178 addcld 
 |-  ( ph -> ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) e. CC )
180 46 sqcld 
 |-  ( ph -> ( ( B / 3 ) ^ 2 ) e. CC )
181 4 180 mulcld 
 |-  ( ph -> ( X x. ( ( B / 3 ) ^ 2 ) ) e. CC )
182 18 181 mulcld 
 |-  ( ph -> ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) e. CC )
183 expcl 
 |-  ( ( ( B / 3 ) e. CC /\ 3 e. NN0 ) -> ( ( B / 3 ) ^ 3 ) e. CC )
184 46 24 183 sylancl 
 |-  ( ph -> ( ( B / 3 ) ^ 3 ) e. CC )
185 182 184 addcld 
 |-  ( ph -> ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) e. CC )
186 22 47 mulcld 
 |-  ( ph -> ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) e. CC )
187 186 45 addcld 
 |-  ( ph -> ( ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) + ( N / ; 2 7 ) ) e. CC )
188 179 185 187 addassd 
 |-  ( ph -> ( ( ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) + ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) ) + ( ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) + ( N / ; 2 7 ) ) ) = ( ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) + ( ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) + ( ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) + ( N / ; 2 7 ) ) ) ) )
189 22 4 46 adddid 
 |-  ( ph -> ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) = ( ( -u ( M / 3 ) x. X ) + ( -u ( M / 3 ) x. ( B / 3 ) ) ) )
190 189 oveq1d 
 |-  ( ph -> ( ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) + ( N / ; 2 7 ) ) = ( ( ( -u ( M / 3 ) x. X ) + ( -u ( M / 3 ) x. ( B / 3 ) ) ) + ( N / ; 2 7 ) ) )
191 22 4 mulcld 
 |-  ( ph -> ( -u ( M / 3 ) x. X ) e. CC )
192 22 46 mulcld 
 |-  ( ph -> ( -u ( M / 3 ) x. ( B / 3 ) ) e. CC )
193 191 192 45 addassd 
 |-  ( ph -> ( ( ( -u ( M / 3 ) x. X ) + ( -u ( M / 3 ) x. ( B / 3 ) ) ) + ( N / ; 2 7 ) ) = ( ( -u ( M / 3 ) x. X ) + ( ( -u ( M / 3 ) x. ( B / 3 ) ) + ( N / ; 2 7 ) ) ) )
194 9 oveq1d 
 |-  ( ph -> ( M / 3 ) = ( ( ( B ^ 2 ) - ( 3 x. C ) ) / 3 ) )
195 12 15 18 20 divsubdird 
 |-  ( ph -> ( ( ( B ^ 2 ) - ( 3 x. C ) ) / 3 ) = ( ( ( B ^ 2 ) / 3 ) - ( ( 3 x. C ) / 3 ) ) )
196 2 18 20 divcan3d 
 |-  ( ph -> ( ( 3 x. C ) / 3 ) = C )
197 196 oveq2d 
 |-  ( ph -> ( ( ( B ^ 2 ) / 3 ) - ( ( 3 x. C ) / 3 ) ) = ( ( ( B ^ 2 ) / 3 ) - C ) )
198 194 195 197 3eqtrd 
 |-  ( ph -> ( M / 3 ) = ( ( ( B ^ 2 ) / 3 ) - C ) )
199 198 negeqd 
 |-  ( ph -> -u ( M / 3 ) = -u ( ( ( B ^ 2 ) / 3 ) - C ) )
200 12 18 20 divcld 
 |-  ( ph -> ( ( B ^ 2 ) / 3 ) e. CC )
201 200 2 negsubdi2d 
 |-  ( ph -> -u ( ( ( B ^ 2 ) / 3 ) - C ) = ( C - ( ( B ^ 2 ) / 3 ) ) )
202 199 201 eqtrd 
 |-  ( ph -> -u ( M / 3 ) = ( C - ( ( B ^ 2 ) / 3 ) ) )
203 202 oveq1d 
 |-  ( ph -> ( -u ( M / 3 ) x. X ) = ( ( C - ( ( B ^ 2 ) / 3 ) ) x. X ) )
204 2 200 4 subdird 
 |-  ( ph -> ( ( C - ( ( B ^ 2 ) / 3 ) ) x. X ) = ( ( C x. X ) - ( ( ( B ^ 2 ) / 3 ) x. X ) ) )
205 200 4 mulcomd 
 |-  ( ph -> ( ( ( B ^ 2 ) / 3 ) x. X ) = ( X x. ( ( B ^ 2 ) / 3 ) ) )
206 13 sqvali 
 |-  ( 3 ^ 2 ) = ( 3 x. 3 )
207 206 oveq2i 
 |-  ( ( B ^ 2 ) / ( 3 ^ 2 ) ) = ( ( B ^ 2 ) / ( 3 x. 3 ) )
208 1 18 20 sqdivd 
 |-  ( ph -> ( ( B / 3 ) ^ 2 ) = ( ( B ^ 2 ) / ( 3 ^ 2 ) ) )
209 12 18 18 20 20 divdiv1d 
 |-  ( ph -> ( ( ( B ^ 2 ) / 3 ) / 3 ) = ( ( B ^ 2 ) / ( 3 x. 3 ) ) )
210 207 208 209 3eqtr4a 
 |-  ( ph -> ( ( B / 3 ) ^ 2 ) = ( ( ( B ^ 2 ) / 3 ) / 3 ) )
211 210 oveq2d 
 |-  ( ph -> ( 3 x. ( ( B / 3 ) ^ 2 ) ) = ( 3 x. ( ( ( B ^ 2 ) / 3 ) / 3 ) ) )
212 200 18 20 divcan2d 
 |-  ( ph -> ( 3 x. ( ( ( B ^ 2 ) / 3 ) / 3 ) ) = ( ( B ^ 2 ) / 3 ) )
213 211 212 eqtrd 
 |-  ( ph -> ( 3 x. ( ( B / 3 ) ^ 2 ) ) = ( ( B ^ 2 ) / 3 ) )
214 213 oveq2d 
 |-  ( ph -> ( X x. ( 3 x. ( ( B / 3 ) ^ 2 ) ) ) = ( X x. ( ( B ^ 2 ) / 3 ) ) )
215 4 18 180 mul12d 
 |-  ( ph -> ( X x. ( 3 x. ( ( B / 3 ) ^ 2 ) ) ) = ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) )
216 205 214 215 3eqtr2d 
 |-  ( ph -> ( ( ( B ^ 2 ) / 3 ) x. X ) = ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) )
217 216 oveq2d 
 |-  ( ph -> ( ( C x. X ) - ( ( ( B ^ 2 ) / 3 ) x. X ) ) = ( ( C x. X ) - ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) ) )
218 203 204 217 3eqtrd 
 |-  ( ph -> ( -u ( M / 3 ) x. X ) = ( ( C x. X ) - ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) ) )
219 202 oveq1d 
 |-  ( ph -> ( -u ( M / 3 ) x. ( B / 3 ) ) = ( ( C - ( ( B ^ 2 ) / 3 ) ) x. ( B / 3 ) ) )
220 2 200 46 subdird 
 |-  ( ph -> ( ( C - ( ( B ^ 2 ) / 3 ) ) x. ( B / 3 ) ) = ( ( C x. ( B / 3 ) ) - ( ( ( B ^ 2 ) / 3 ) x. ( B / 3 ) ) ) )
221 2 1 18 20 divassd 
 |-  ( ph -> ( ( C x. B ) / 3 ) = ( C x. ( B / 3 ) ) )
222 2 1 mulcomd 
 |-  ( ph -> ( C x. B ) = ( B x. C ) )
223 222 oveq1d 
 |-  ( ph -> ( ( C x. B ) / 3 ) = ( ( B x. C ) / 3 ) )
224 221 223 eqtr3d 
 |-  ( ph -> ( C x. ( B / 3 ) ) = ( ( B x. C ) / 3 ) )
225 12 18 1 18 20 20 divmuldivd 
 |-  ( ph -> ( ( ( B ^ 2 ) / 3 ) x. ( B / 3 ) ) = ( ( ( B ^ 2 ) x. B ) / ( 3 x. 3 ) ) )
226 df-3 
 |-  3 = ( 2 + 1 )
227 226 oveq2i 
 |-  ( B ^ 3 ) = ( B ^ ( 2 + 1 ) )
228 expp1 
 |-  ( ( B e. CC /\ 2 e. NN0 ) -> ( B ^ ( 2 + 1 ) ) = ( ( B ^ 2 ) x. B ) )
229 1 34 228 sylancl 
 |-  ( ph -> ( B ^ ( 2 + 1 ) ) = ( ( B ^ 2 ) x. B ) )
230 227 229 eqtr2id 
 |-  ( ph -> ( ( B ^ 2 ) x. B ) = ( B ^ 3 ) )
231 154 a1i 
 |-  ( ph -> ( 3 x. 3 ) = 9 )
232 230 231 oveq12d 
 |-  ( ph -> ( ( ( B ^ 2 ) x. B ) / ( 3 x. 3 ) ) = ( ( B ^ 3 ) / 9 ) )
233 225 232 eqtrd 
 |-  ( ph -> ( ( ( B ^ 2 ) / 3 ) x. ( B / 3 ) ) = ( ( B ^ 3 ) / 9 ) )
234 224 233 oveq12d 
 |-  ( ph -> ( ( C x. ( B / 3 ) ) - ( ( ( B ^ 2 ) / 3 ) x. ( B / 3 ) ) ) = ( ( ( B x. C ) / 3 ) - ( ( B ^ 3 ) / 9 ) ) )
235 219 220 234 3eqtrd 
 |-  ( ph -> ( -u ( M / 3 ) x. ( B / 3 ) ) = ( ( ( B x. C ) / 3 ) - ( ( B ^ 3 ) / 9 ) ) )
236 10 oveq1d 
 |-  ( ph -> ( N / ; 2 7 ) = ( ( ( ( 2 x. ( B ^ 3 ) ) - ( 9 x. ( B x. C ) ) ) + ( ; 2 7 x. D ) ) / ; 2 7 ) )
237 33 39 42 44 divdird 
 |-  ( ph -> ( ( ( ( 2 x. ( B ^ 3 ) ) - ( 9 x. ( B x. C ) ) ) + ( ; 2 7 x. D ) ) / ; 2 7 ) = ( ( ( ( 2 x. ( B ^ 3 ) ) - ( 9 x. ( B x. C ) ) ) / ; 2 7 ) + ( ( ; 2 7 x. D ) / ; 2 7 ) ) )
238 28 32 42 44 divsubdird 
 |-  ( ph -> ( ( ( 2 x. ( B ^ 3 ) ) - ( 9 x. ( B x. C ) ) ) / ; 2 7 ) = ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( 9 x. ( B x. C ) ) / ; 2 7 ) ) )
239 9t3e27 
 |-  ( 9 x. 3 ) = ; 2 7
240 239 oveq2i 
 |-  ( ( 9 x. ( B x. C ) ) / ( 9 x. 3 ) ) = ( ( 9 x. ( B x. C ) ) / ; 2 7 )
241 30 18 98 20 101 divcan5d 
 |-  ( ph -> ( ( 9 x. ( B x. C ) ) / ( 9 x. 3 ) ) = ( ( B x. C ) / 3 ) )
242 240 241 eqtr3id 
 |-  ( ph -> ( ( 9 x. ( B x. C ) ) / ; 2 7 ) = ( ( B x. C ) / 3 ) )
243 242 oveq2d 
 |-  ( ph -> ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( 9 x. ( B x. C ) ) / ; 2 7 ) ) = ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B x. C ) / 3 ) ) )
244 238 243 eqtrd 
 |-  ( ph -> ( ( ( 2 x. ( B ^ 3 ) ) - ( 9 x. ( B x. C ) ) ) / ; 2 7 ) = ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B x. C ) / 3 ) ) )
245 3 42 44 divcan3d 
 |-  ( ph -> ( ( ; 2 7 x. D ) / ; 2 7 ) = D )
246 244 245 oveq12d 
 |-  ( ph -> ( ( ( ( 2 x. ( B ^ 3 ) ) - ( 9 x. ( B x. C ) ) ) / ; 2 7 ) + ( ( ; 2 7 x. D ) / ; 2 7 ) ) = ( ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B x. C ) / 3 ) ) + D ) )
247 236 237 246 3eqtrd 
 |-  ( ph -> ( N / ; 2 7 ) = ( ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B x. C ) / 3 ) ) + D ) )
248 235 247 oveq12d 
 |-  ( ph -> ( ( -u ( M / 3 ) x. ( B / 3 ) ) + ( N / ; 2 7 ) ) = ( ( ( ( B x. C ) / 3 ) - ( ( B ^ 3 ) / 9 ) ) + ( ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B x. C ) / 3 ) ) + D ) ) )
249 26 98 101 divcld 
 |-  ( ph -> ( ( B ^ 3 ) / 9 ) e. CC )
250 28 42 44 divcld 
 |-  ( ph -> ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) e. CC )
251 249 250 negsubdi2d 
 |-  ( ph -> -u ( ( ( B ^ 3 ) / 9 ) - ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) ) = ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B ^ 3 ) / 9 ) ) )
252 1 18 20 56 expdivd 
 |-  ( ph -> ( ( B / 3 ) ^ 3 ) = ( ( B ^ 3 ) / ( 3 ^ 3 ) ) )
253 58 oveq2i 
 |-  ( ( B ^ 3 ) / ( 3 ^ 3 ) ) = ( ( B ^ 3 ) / ; 2 7 )
254 ax-1cn 
 |-  1 e. CC
255 2p1e3 
 |-  ( 2 + 1 ) = 3
256 13 23 254 255 subaddrii 
 |-  ( 3 - 2 ) = 1
257 256 oveq1i 
 |-  ( ( 3 - 2 ) x. ( B ^ 3 ) ) = ( 1 x. ( B ^ 3 ) )
258 26 mullidd 
 |-  ( ph -> ( 1 x. ( B ^ 3 ) ) = ( B ^ 3 ) )
259 257 258 eqtrid 
 |-  ( ph -> ( ( 3 - 2 ) x. ( B ^ 3 ) ) = ( B ^ 3 ) )
260 18 62 26 subdird 
 |-  ( ph -> ( ( 3 - 2 ) x. ( B ^ 3 ) ) = ( ( 3 x. ( B ^ 3 ) ) - ( 2 x. ( B ^ 3 ) ) ) )
261 259 260 eqtr3d 
 |-  ( ph -> ( B ^ 3 ) = ( ( 3 x. ( B ^ 3 ) ) - ( 2 x. ( B ^ 3 ) ) ) )
262 261 oveq1d 
 |-  ( ph -> ( ( B ^ 3 ) / ; 2 7 ) = ( ( ( 3 x. ( B ^ 3 ) ) - ( 2 x. ( B ^ 3 ) ) ) / ; 2 7 ) )
263 mulcl 
 |-  ( ( 3 e. CC /\ ( B ^ 3 ) e. CC ) -> ( 3 x. ( B ^ 3 ) ) e. CC )
264 13 26 263 sylancr 
 |-  ( ph -> ( 3 x. ( B ^ 3 ) ) e. CC )
265 264 28 42 44 divsubdird 
 |-  ( ph -> ( ( ( 3 x. ( B ^ 3 ) ) - ( 2 x. ( B ^ 3 ) ) ) / ; 2 7 ) = ( ( ( 3 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) ) )
266 262 265 eqtrd 
 |-  ( ph -> ( ( B ^ 3 ) / ; 2 7 ) = ( ( ( 3 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) ) )
267 253 266 eqtrid 
 |-  ( ph -> ( ( B ^ 3 ) / ( 3 ^ 3 ) ) = ( ( ( 3 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) ) )
268 29 13 239 mulcomli 
 |-  ( 3 x. 9 ) = ; 2 7
269 268 oveq2i 
 |-  ( ( 3 x. ( B ^ 3 ) ) / ( 3 x. 9 ) ) = ( ( 3 x. ( B ^ 3 ) ) / ; 2 7 )
270 26 98 18 101 20 divcan5d 
 |-  ( ph -> ( ( 3 x. ( B ^ 3 ) ) / ( 3 x. 9 ) ) = ( ( B ^ 3 ) / 9 ) )
271 269 270 eqtr3id 
 |-  ( ph -> ( ( 3 x. ( B ^ 3 ) ) / ; 2 7 ) = ( ( B ^ 3 ) / 9 ) )
272 271 oveq1d 
 |-  ( ph -> ( ( ( 3 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) ) = ( ( ( B ^ 3 ) / 9 ) - ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) ) )
273 252 267 272 3eqtrd 
 |-  ( ph -> ( ( B / 3 ) ^ 3 ) = ( ( ( B ^ 3 ) / 9 ) - ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) ) )
274 273 negeqd 
 |-  ( ph -> -u ( ( B / 3 ) ^ 3 ) = -u ( ( ( B ^ 3 ) / 9 ) - ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) ) )
275 30 18 20 divcld 
 |-  ( ph -> ( ( B x. C ) / 3 ) e. CC )
276 275 249 250 npncan3d 
 |-  ( ph -> ( ( ( ( B x. C ) / 3 ) - ( ( B ^ 3 ) / 9 ) ) + ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B x. C ) / 3 ) ) ) = ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B ^ 3 ) / 9 ) ) )
277 251 274 276 3eqtr4d 
 |-  ( ph -> -u ( ( B / 3 ) ^ 3 ) = ( ( ( ( B x. C ) / 3 ) - ( ( B ^ 3 ) / 9 ) ) + ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B x. C ) / 3 ) ) ) )
278 277 oveq1d 
 |-  ( ph -> ( -u ( ( B / 3 ) ^ 3 ) + D ) = ( ( ( ( ( B x. C ) / 3 ) - ( ( B ^ 3 ) / 9 ) ) + ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B x. C ) / 3 ) ) ) + D ) )
279 184 negcld 
 |-  ( ph -> -u ( ( B / 3 ) ^ 3 ) e. CC )
280 279 3 addcomd 
 |-  ( ph -> ( -u ( ( B / 3 ) ^ 3 ) + D ) = ( D + -u ( ( B / 3 ) ^ 3 ) ) )
281 235 192 eqeltrrd 
 |-  ( ph -> ( ( ( B x. C ) / 3 ) - ( ( B ^ 3 ) / 9 ) ) e. CC )
282 250 275 subcld 
 |-  ( ph -> ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B x. C ) / 3 ) ) e. CC )
283 281 282 3 addassd 
 |-  ( ph -> ( ( ( ( ( B x. C ) / 3 ) - ( ( B ^ 3 ) / 9 ) ) + ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B x. C ) / 3 ) ) ) + D ) = ( ( ( ( B x. C ) / 3 ) - ( ( B ^ 3 ) / 9 ) ) + ( ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B x. C ) / 3 ) ) + D ) ) )
284 278 280 283 3eqtr3d 
 |-  ( ph -> ( D + -u ( ( B / 3 ) ^ 3 ) ) = ( ( ( ( B x. C ) / 3 ) - ( ( B ^ 3 ) / 9 ) ) + ( ( ( ( 2 x. ( B ^ 3 ) ) / ; 2 7 ) - ( ( B x. C ) / 3 ) ) + D ) ) )
285 3 184 negsubd 
 |-  ( ph -> ( D + -u ( ( B / 3 ) ^ 3 ) ) = ( D - ( ( B / 3 ) ^ 3 ) ) )
286 248 284 285 3eqtr2d 
 |-  ( ph -> ( ( -u ( M / 3 ) x. ( B / 3 ) ) + ( N / ; 2 7 ) ) = ( D - ( ( B / 3 ) ^ 3 ) ) )
287 218 286 oveq12d 
 |-  ( ph -> ( ( -u ( M / 3 ) x. X ) + ( ( -u ( M / 3 ) x. ( B / 3 ) ) + ( N / ; 2 7 ) ) ) = ( ( ( C x. X ) - ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) ) + ( D - ( ( B / 3 ) ^ 3 ) ) ) )
288 190 193 287 3eqtrd 
 |-  ( ph -> ( ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) + ( N / ; 2 7 ) ) = ( ( ( C x. X ) - ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) ) + ( D - ( ( B / 3 ) ^ 3 ) ) ) )
289 2 4 mulcld 
 |-  ( ph -> ( C x. X ) e. CC )
290 289 3 182 184 addsub4d 
 |-  ( ph -> ( ( ( C x. X ) + D ) - ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) ) = ( ( ( C x. X ) - ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) ) + ( D - ( ( B / 3 ) ^ 3 ) ) ) )
291 288 290 eqtr4d 
 |-  ( ph -> ( ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) + ( N / ; 2 7 ) ) = ( ( ( C x. X ) + D ) - ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) ) )
292 291 oveq2d 
 |-  ( ph -> ( ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) + ( ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) + ( N / ; 2 7 ) ) ) = ( ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) + ( ( ( C x. X ) + D ) - ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) ) ) )
293 289 3 addcld 
 |-  ( ph -> ( ( C x. X ) + D ) e. CC )
294 185 293 pncan3d 
 |-  ( ph -> ( ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) + ( ( ( C x. X ) + D ) - ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) ) ) = ( ( C x. X ) + D ) )
295 292 294 eqtrd 
 |-  ( ph -> ( ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) + ( ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) + ( N / ; 2 7 ) ) ) = ( ( C x. X ) + D ) )
296 295 oveq2d 
 |-  ( ph -> ( ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) + ( ( ( 3 x. ( X x. ( ( B / 3 ) ^ 2 ) ) ) + ( ( B / 3 ) ^ 3 ) ) + ( ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) + ( N / ; 2 7 ) ) ) ) = ( ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) + ( ( C x. X ) + D ) ) )
297 175 188 296 3eqtrd 
 |-  ( ph -> ( ( ( X + ( B / 3 ) ) ^ 3 ) + ( ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) + ( N / ; 2 7 ) ) ) = ( ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) + ( ( C x. X ) + D ) ) )
298 297 eqeq1d 
 |-  ( ph -> ( ( ( ( X + ( B / 3 ) ) ^ 3 ) + ( ( -u ( M / 3 ) x. ( X + ( B / 3 ) ) ) + ( N / ; 2 7 ) ) ) = 0 <-> ( ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) + ( ( C x. X ) + D ) ) = 0 ) )
299 oveq1 
 |-  ( r = 0 -> ( r ^ 3 ) = ( 0 ^ 3 ) )
300 0exp 
 |-  ( 3 e. NN -> ( 0 ^ 3 ) = 0 )
301 50 300 ax-mp 
 |-  ( 0 ^ 3 ) = 0
302 299 301 eqtrdi 
 |-  ( r = 0 -> ( r ^ 3 ) = 0 )
303 0ne1 
 |-  0 =/= 1
304 303 a1i 
 |-  ( r = 0 -> 0 =/= 1 )
305 302 304 eqnetrd 
 |-  ( r = 0 -> ( r ^ 3 ) =/= 1 )
306 305 necon2i 
 |-  ( ( r ^ 3 ) = 1 -> r =/= 0 )
307 eqcom 
 |-  ( X = -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) <-> -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) = X )
308 1 adantr 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> B e. CC )
309 simprl 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> r e. CC )
310 5 adantr 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> T e. CC )
311 309 310 mulcld 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( r x. T ) e. CC )
312 17 adantr 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> M e. CC )
313 simprr 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> r =/= 0 )
314 11 adantr 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> T =/= 0 )
315 309 310 313 314 mulne0d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( r x. T ) =/= 0 )
316 312 311 315 divcld 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( M / ( r x. T ) ) e. CC )
317 311 316 addcld 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( r x. T ) + ( M / ( r x. T ) ) ) e. CC )
318 13 a1i 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> 3 e. CC )
319 19 a1i 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> 3 =/= 0 )
320 308 317 318 319 divdird 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( B + ( ( r x. T ) + ( M / ( r x. T ) ) ) ) / 3 ) = ( ( B / 3 ) + ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) ) )
321 308 311 316 addassd 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) = ( B + ( ( r x. T ) + ( M / ( r x. T ) ) ) ) )
322 321 oveq1d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) = ( ( B + ( ( r x. T ) + ( M / ( r x. T ) ) ) ) / 3 ) )
323 46 adantr 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( B / 3 ) e. CC )
324 317 318 319 divcld 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) e. CC )
325 323 324 subnegd 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( B / 3 ) - -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) ) = ( ( B / 3 ) + ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) ) )
326 320 322 325 3eqtr4d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) = ( ( B / 3 ) - -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) ) )
327 326 negeqd 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) = -u ( ( B / 3 ) - -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) ) )
328 324 negcld 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) e. CC )
329 323 328 negsubdi2d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> -u ( ( B / 3 ) - -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) ) = ( -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) - ( B / 3 ) ) )
330 327 329 eqtrd 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) = ( -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) - ( B / 3 ) ) )
331 330 eqeq1d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) = X <-> ( -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) - ( B / 3 ) ) = X ) )
332 307 331 bitrid 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( X = -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) <-> ( -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) - ( B / 3 ) ) = X ) )
333 4 adantr 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> X e. CC )
334 328 323 333 subadd2d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) - ( B / 3 ) ) = X <-> ( X + ( B / 3 ) ) = -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) ) )
335 311 316 318 319 divdird 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) = ( ( ( r x. T ) / 3 ) + ( ( M / ( r x. T ) ) / 3 ) ) )
336 335 negeqd 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) = -u ( ( ( r x. T ) / 3 ) + ( ( M / ( r x. T ) ) / 3 ) ) )
337 311 318 319 divcld 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( r x. T ) / 3 ) e. CC )
338 316 318 319 divcld 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( M / ( r x. T ) ) / 3 ) e. CC )
339 337 338 negdi2d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> -u ( ( ( r x. T ) / 3 ) + ( ( M / ( r x. T ) ) / 3 ) ) = ( -u ( ( r x. T ) / 3 ) - ( ( M / ( r x. T ) ) / 3 ) ) )
340 309 310 318 319 divassd 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( r x. T ) / 3 ) = ( r x. ( T / 3 ) ) )
341 340 negeqd 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> -u ( ( r x. T ) / 3 ) = -u ( r x. ( T / 3 ) ) )
342 48 adantr 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( T / 3 ) e. CC )
343 309 342 mulneg2d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( r x. -u ( T / 3 ) ) = -u ( r x. ( T / 3 ) ) )
344 341 343 eqtr4d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> -u ( ( r x. T ) / 3 ) = ( r x. -u ( T / 3 ) ) )
345 312 311 318 315 319 divdiv32d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( M / ( r x. T ) ) / 3 ) = ( ( M / 3 ) / ( r x. T ) ) )
346 21 adantr 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( M / 3 ) e. CC )
347 346 311 318 315 319 divcan7d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( ( M / 3 ) / 3 ) / ( ( r x. T ) / 3 ) ) = ( ( M / 3 ) / ( r x. T ) ) )
348 156 oveq1d 
 |-  ( ph -> ( ( ( M / 3 ) / 3 ) / ( ( r x. T ) / 3 ) ) = ( ( M / 9 ) / ( ( r x. T ) / 3 ) ) )
349 348 adantr 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( ( M / 3 ) / 3 ) / ( ( r x. T ) / 3 ) ) = ( ( M / 9 ) / ( ( r x. T ) / 3 ) ) )
350 345 347 349 3eqtr2d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( M / ( r x. T ) ) / 3 ) = ( ( M / 9 ) / ( ( r x. T ) / 3 ) ) )
351 121 adantr 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( M / 9 ) e. CC )
352 311 318 315 319 divne0d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( r x. T ) / 3 ) =/= 0 )
353 351 337 352 div2negd 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( -u ( M / 9 ) / -u ( ( r x. T ) / 3 ) ) = ( ( M / 9 ) / ( ( r x. T ) / 3 ) ) )
354 344 oveq2d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( -u ( M / 9 ) / -u ( ( r x. T ) / 3 ) ) = ( -u ( M / 9 ) / ( r x. -u ( T / 3 ) ) ) )
355 350 353 354 3eqtr2d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( M / ( r x. T ) ) / 3 ) = ( -u ( M / 9 ) / ( r x. -u ( T / 3 ) ) ) )
356 344 355 oveq12d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( -u ( ( r x. T ) / 3 ) - ( ( M / ( r x. T ) ) / 3 ) ) = ( ( r x. -u ( T / 3 ) ) - ( -u ( M / 9 ) / ( r x. -u ( T / 3 ) ) ) ) )
357 336 339 356 3eqtrd 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) = ( ( r x. -u ( T / 3 ) ) - ( -u ( M / 9 ) / ( r x. -u ( T / 3 ) ) ) ) )
358 357 eqeq2d 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( X + ( B / 3 ) ) = -u ( ( ( r x. T ) + ( M / ( r x. T ) ) ) / 3 ) <-> ( X + ( B / 3 ) ) = ( ( r x. -u ( T / 3 ) ) - ( -u ( M / 9 ) / ( r x. -u ( T / 3 ) ) ) ) ) )
359 332 334 358 3bitrrd 
 |-  ( ( ph /\ ( r e. CC /\ r =/= 0 ) ) -> ( ( X + ( B / 3 ) ) = ( ( r x. -u ( T / 3 ) ) - ( -u ( M / 9 ) / ( r x. -u ( T / 3 ) ) ) ) <-> X = -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) ) )
360 359 anassrs 
 |-  ( ( ( ph /\ r e. CC ) /\ r =/= 0 ) -> ( ( X + ( B / 3 ) ) = ( ( r x. -u ( T / 3 ) ) - ( -u ( M / 9 ) / ( r x. -u ( T / 3 ) ) ) ) <-> X = -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) ) )
361 306 360 sylan2 
 |-  ( ( ( ph /\ r e. CC ) /\ ( r ^ 3 ) = 1 ) -> ( ( X + ( B / 3 ) ) = ( ( r x. -u ( T / 3 ) ) - ( -u ( M / 9 ) / ( r x. -u ( T / 3 ) ) ) ) <-> X = -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) ) )
362 361 pm5.32da 
 |-  ( ( ph /\ r e. CC ) -> ( ( ( r ^ 3 ) = 1 /\ ( X + ( B / 3 ) ) = ( ( r x. -u ( T / 3 ) ) - ( -u ( M / 9 ) / ( r x. -u ( T / 3 ) ) ) ) ) <-> ( ( r ^ 3 ) = 1 /\ X = -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) ) ) )
363 362 rexbidva 
 |-  ( ph -> ( E. r e. CC ( ( r ^ 3 ) = 1 /\ ( X + ( B / 3 ) ) = ( ( r x. -u ( T / 3 ) ) - ( -u ( M / 9 ) / ( r x. -u ( T / 3 ) ) ) ) ) <-> E. r e. CC ( ( r ^ 3 ) = 1 /\ X = -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) ) ) )
364 163 298 363 3bitr3d 
 |-  ( ph -> ( ( ( ( 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 ) ) ) )