Metamath Proof Explorer

Theorem dcubic1lem

Description: Lemma for dcubic1 and dcubic2 : simplify the cubic equation under the substitution X = U - M / U . (Contributed by Mario Carneiro, 26-Apr-2015)

Ref Expression
Hypotheses dcubic.c 
|- ( ph -> P e. CC )
dcubic.d 
|- ( ph -> Q e. CC )
dcubic.x 
|- ( ph -> X e. CC )
dcubic.t 
|- ( ph -> T e. CC )
dcubic.3 
|- ( ph -> ( T ^ 3 ) = ( G - N ) )
dcubic.g 
|- ( ph -> G e. CC )
dcubic.2 
|- ( ph -> ( G ^ 2 ) = ( ( N ^ 2 ) + ( M ^ 3 ) ) )
dcubic.m 
|- ( ph -> M = ( P / 3 ) )
dcubic.n 
|- ( ph -> N = ( Q / 2 ) )
dcubic.0 
|- ( ph -> T =/= 0 )
dcubic2.u 
|- ( ph -> U e. CC )
dcubic2.z 
|- ( ph -> U =/= 0 )
dcubic2.2 
|- ( ph -> X = ( U - ( M / U ) ) )
Assertion dcubic1lem 
|- ( ph -> ( ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 <-> ( ( ( U ^ 3 ) ^ 2 ) + ( ( Q x. ( U ^ 3 ) ) - ( M ^ 3 ) ) ) = 0 ) )

Proof

Step Hyp Ref Expression
1 dcubic.c 
 |-  ( ph -> P e. CC )
2 dcubic.d 
 |-  ( ph -> Q e. CC )
3 dcubic.x 
 |-  ( ph -> X e. CC )
4 dcubic.t 
 |-  ( ph -> T e. CC )
5 dcubic.3 
 |-  ( ph -> ( T ^ 3 ) = ( G - N ) )
6 dcubic.g 
 |-  ( ph -> G e. CC )
7 dcubic.2 
 |-  ( ph -> ( G ^ 2 ) = ( ( N ^ 2 ) + ( M ^ 3 ) ) )
8 dcubic.m 
 |-  ( ph -> M = ( P / 3 ) )
9 dcubic.n 
 |-  ( ph -> N = ( Q / 2 ) )
10 dcubic.0 
 |-  ( ph -> T =/= 0 )
11 dcubic2.u 
 |-  ( ph -> U e. CC )
12 dcubic2.z 
 |-  ( ph -> U =/= 0 )
13 dcubic2.2 
 |-  ( ph -> X = ( U - ( M / U ) ) )
14 3nn0 
 |-  3 e. NN0
15 expcl 
 |-  ( ( U e. CC /\ 3 e. NN0 ) -> ( U ^ 3 ) e. CC )
16 11 14 15 sylancl 
 |-  ( ph -> ( U ^ 3 ) e. CC )
17 16 sqvald 
 |-  ( ph -> ( ( U ^ 3 ) ^ 2 ) = ( ( U ^ 3 ) x. ( U ^ 3 ) ) )
18 17 oveq1d 
 |-  ( ph -> ( ( ( U ^ 3 ) ^ 2 ) / ( U ^ 3 ) ) = ( ( ( U ^ 3 ) x. ( U ^ 3 ) ) / ( U ^ 3 ) ) )
19 3z 
 |-  3 e. ZZ
20 19 a1i 
 |-  ( ph -> 3 e. ZZ )
21 11 12 20 expne0d 
 |-  ( ph -> ( U ^ 3 ) =/= 0 )
22 16 16 21 divcan4d 
 |-  ( ph -> ( ( ( U ^ 3 ) x. ( U ^ 3 ) ) / ( U ^ 3 ) ) = ( U ^ 3 ) )
23 18 22 eqtr2d 
 |-  ( ph -> ( U ^ 3 ) = ( ( ( U ^ 3 ) ^ 2 ) / ( U ^ 3 ) ) )
24 3cn 
 |-  3 e. CC
25 24 a1i 
 |-  ( ph -> 3 e. CC )
26 3ne0 
 |-  3 =/= 0
27 26 a1i 
 |-  ( ph -> 3 =/= 0 )
28 1 25 27 divcld 
 |-  ( ph -> ( P / 3 ) e. CC )
29 8 28 eqeltrd 
 |-  ( ph -> M e. CC )
30 expcl 
 |-  ( ( M e. CC /\ 3 e. NN0 ) -> ( M ^ 3 ) e. CC )
31 29 14 30 sylancl 
 |-  ( ph -> ( M ^ 3 ) e. CC )
32 31 16 21 divcld 
 |-  ( ph -> ( ( M ^ 3 ) / ( U ^ 3 ) ) e. CC )
33 2 32 negsubd 
 |-  ( ph -> ( Q + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) = ( Q - ( ( M ^ 3 ) / ( U ^ 3 ) ) ) )
34 2 16 21 divcan4d 
 |-  ( ph -> ( ( Q x. ( U ^ 3 ) ) / ( U ^ 3 ) ) = Q )
35 34 oveq1d 
 |-  ( ph -> ( ( ( Q x. ( U ^ 3 ) ) / ( U ^ 3 ) ) - ( ( M ^ 3 ) / ( U ^ 3 ) ) ) = ( Q - ( ( M ^ 3 ) / ( U ^ 3 ) ) ) )
36 33 35 eqtr4d 
 |-  ( ph -> ( Q + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) = ( ( ( Q x. ( U ^ 3 ) ) / ( U ^ 3 ) ) - ( ( M ^ 3 ) / ( U ^ 3 ) ) ) )
37 1 3 mulcld 
 |-  ( ph -> ( P x. X ) e. CC )
38 37 negcld 
 |-  ( ph -> -u ( P x. X ) e. CC )
39 32 negcld 
 |-  ( ph -> -u ( ( M ^ 3 ) / ( U ^ 3 ) ) e. CC )
40 38 39 37 2 add42d 
 |-  ( ph -> ( ( -u ( P x. X ) + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) + ( ( P x. X ) + Q ) ) = ( ( -u ( P x. X ) + ( P x. X ) ) + ( Q + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) ) )
41 1 3 mulneg2d 
 |-  ( ph -> ( P x. -u X ) = -u ( P x. X ) )
42 13 negeqd 
 |-  ( ph -> -u X = -u ( U - ( M / U ) ) )
43 29 11 12 divcld 
 |-  ( ph -> ( M / U ) e. CC )
44 11 43 negsubdid 
 |-  ( ph -> -u ( U - ( M / U ) ) = ( -u U + ( M / U ) ) )
45 42 44 eqtrd 
 |-  ( ph -> -u X = ( -u U + ( M / U ) ) )
46 45 oveq2d 
 |-  ( ph -> ( P x. -u X ) = ( P x. ( -u U + ( M / U ) ) ) )
47 41 46 eqtr3d 
 |-  ( ph -> -u ( P x. X ) = ( P x. ( -u U + ( M / U ) ) ) )
48 11 negcld 
 |-  ( ph -> -u U e. CC )
49 1 48 43 adddid 
 |-  ( ph -> ( P x. ( -u U + ( M / U ) ) ) = ( ( P x. -u U ) + ( P x. ( M / U ) ) ) )
50 1 11 mulneg2d 
 |-  ( ph -> ( P x. -u U ) = -u ( P x. U ) )
51 50 oveq1d 
 |-  ( ph -> ( ( P x. -u U ) + ( P x. ( M / U ) ) ) = ( -u ( P x. U ) + ( P x. ( M / U ) ) ) )
52 47 49 51 3eqtrd 
 |-  ( ph -> -u ( P x. X ) = ( -u ( P x. U ) + ( P x. ( M / U ) ) ) )
53 52 oveq1d 
 |-  ( ph -> ( -u ( P x. X ) + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) = ( ( -u ( P x. U ) + ( P x. ( M / U ) ) ) + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) )
54 1 11 mulcld 
 |-  ( ph -> ( P x. U ) e. CC )
55 54 negcld 
 |-  ( ph -> -u ( P x. U ) e. CC )
56 1 43 mulcld 
 |-  ( ph -> ( P x. ( M / U ) ) e. CC )
57 55 56 39 addassd 
 |-  ( ph -> ( ( -u ( P x. U ) + ( P x. ( M / U ) ) ) + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) = ( -u ( P x. U ) + ( ( P x. ( M / U ) ) + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) ) )
58 53 57 eqtrd 
 |-  ( ph -> ( -u ( P x. X ) + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) = ( -u ( P x. U ) + ( ( P x. ( M / U ) ) + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) ) )
59 58 oveq1d 
 |-  ( ph -> ( ( -u ( P x. X ) + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) + ( ( P x. X ) + Q ) ) = ( ( -u ( P x. U ) + ( ( P x. ( M / U ) ) + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) ) + ( ( P x. X ) + Q ) ) )
60 38 37 addcomd 
 |-  ( ph -> ( -u ( P x. X ) + ( P x. X ) ) = ( ( P x. X ) + -u ( P x. X ) ) )
61 37 negidd 
 |-  ( ph -> ( ( P x. X ) + -u ( P x. X ) ) = 0 )
62 60 61 eqtrd 
 |-  ( ph -> ( -u ( P x. X ) + ( P x. X ) ) = 0 )
63 62 oveq1d 
 |-  ( ph -> ( ( -u ( P x. X ) + ( P x. X ) ) + ( Q + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) ) = ( 0 + ( Q + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) ) )
64 2 39 addcld 
 |-  ( ph -> ( Q + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) e. CC )
65 64 addlidd 
 |-  ( ph -> ( 0 + ( Q + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) ) = ( Q + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) )
66 63 65 eqtrd 
 |-  ( ph -> ( ( -u ( P x. X ) + ( P x. X ) ) + ( Q + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) ) = ( Q + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) )
67 40 59 66 3eqtr3d 
 |-  ( ph -> ( ( -u ( P x. U ) + ( ( P x. ( M / U ) ) + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) ) + ( ( P x. X ) + Q ) ) = ( Q + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) )
68 2 16 mulcld 
 |-  ( ph -> ( Q x. ( U ^ 3 ) ) e. CC )
69 68 31 16 21 divsubdird 
 |-  ( ph -> ( ( ( Q x. ( U ^ 3 ) ) - ( M ^ 3 ) ) / ( U ^ 3 ) ) = ( ( ( Q x. ( U ^ 3 ) ) / ( U ^ 3 ) ) - ( ( M ^ 3 ) / ( U ^ 3 ) ) ) )
70 36 67 69 3eqtr4d 
 |-  ( ph -> ( ( -u ( P x. U ) + ( ( P x. ( M / U ) ) + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) ) + ( ( P x. X ) + Q ) ) = ( ( ( Q x. ( U ^ 3 ) ) - ( M ^ 3 ) ) / ( U ^ 3 ) ) )
71 23 70 oveq12d 
 |-  ( ph -> ( ( U ^ 3 ) + ( ( -u ( P x. U ) + ( ( P x. ( M / U ) ) + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) ) + ( ( P x. X ) + Q ) ) ) = ( ( ( ( U ^ 3 ) ^ 2 ) / ( U ^ 3 ) ) + ( ( ( Q x. ( U ^ 3 ) ) - ( M ^ 3 ) ) / ( U ^ 3 ) ) ) )
72 11 43 negsubd 
 |-  ( ph -> ( U + -u ( M / U ) ) = ( U - ( M / U ) ) )
73 13 72 eqtr4d 
 |-  ( ph -> X = ( U + -u ( M / U ) ) )
74 73 oveq1d 
 |-  ( ph -> ( X ^ 3 ) = ( ( U + -u ( M / U ) ) ^ 3 ) )
75 43 negcld 
 |-  ( ph -> -u ( M / U ) e. CC )
76 binom3 
 |-  ( ( U e. CC /\ -u ( M / U ) e. CC ) -> ( ( U + -u ( M / U ) ) ^ 3 ) = ( ( ( U ^ 3 ) + ( 3 x. ( ( U ^ 2 ) x. -u ( M / U ) ) ) ) + ( ( 3 x. ( U x. ( -u ( M / U ) ^ 2 ) ) ) + ( -u ( M / U ) ^ 3 ) ) ) )
77 11 75 76 syl2anc 
 |-  ( ph -> ( ( U + -u ( M / U ) ) ^ 3 ) = ( ( ( U ^ 3 ) + ( 3 x. ( ( U ^ 2 ) x. -u ( M / U ) ) ) ) + ( ( 3 x. ( U x. ( -u ( M / U ) ^ 2 ) ) ) + ( -u ( M / U ) ^ 3 ) ) ) )
78 11 sqcld 
 |-  ( ph -> ( U ^ 2 ) e. CC )
79 78 43 mulneg2d 
 |-  ( ph -> ( ( U ^ 2 ) x. -u ( M / U ) ) = -u ( ( U ^ 2 ) x. ( M / U ) ) )
80 78 29 11 12 div12d 
 |-  ( ph -> ( ( U ^ 2 ) x. ( M / U ) ) = ( M x. ( ( U ^ 2 ) / U ) ) )
81 11 sqvald 
 |-  ( ph -> ( U ^ 2 ) = ( U x. U ) )
82 81 oveq1d 
 |-  ( ph -> ( ( U ^ 2 ) / U ) = ( ( U x. U ) / U ) )
83 11 11 12 divcan4d 
 |-  ( ph -> ( ( U x. U ) / U ) = U )
84 82 83 eqtrd 
 |-  ( ph -> ( ( U ^ 2 ) / U ) = U )
85 84 oveq2d 
 |-  ( ph -> ( M x. ( ( U ^ 2 ) / U ) ) = ( M x. U ) )
86 80 85 eqtrd 
 |-  ( ph -> ( ( U ^ 2 ) x. ( M / U ) ) = ( M x. U ) )
87 86 negeqd 
 |-  ( ph -> -u ( ( U ^ 2 ) x. ( M / U ) ) = -u ( M x. U ) )
88 79 87 eqtrd 
 |-  ( ph -> ( ( U ^ 2 ) x. -u ( M / U ) ) = -u ( M x. U ) )
89 88 oveq2d 
 |-  ( ph -> ( 3 x. ( ( U ^ 2 ) x. -u ( M / U ) ) ) = ( 3 x. -u ( M x. U ) ) )
90 29 11 mulcld 
 |-  ( ph -> ( M x. U ) e. CC )
91 25 90 mulneg2d 
 |-  ( ph -> ( 3 x. -u ( M x. U ) ) = -u ( 3 x. ( M x. U ) ) )
92 25 29 11 mulassd 
 |-  ( ph -> ( ( 3 x. M ) x. U ) = ( 3 x. ( M x. U ) ) )
93 8 oveq2d 
 |-  ( ph -> ( 3 x. M ) = ( 3 x. ( P / 3 ) ) )
94 1 25 27 divcan2d 
 |-  ( ph -> ( 3 x. ( P / 3 ) ) = P )
95 93 94 eqtrd 
 |-  ( ph -> ( 3 x. M ) = P )
96 95 oveq1d 
 |-  ( ph -> ( ( 3 x. M ) x. U ) = ( P x. U ) )
97 92 96 eqtr3d 
 |-  ( ph -> ( 3 x. ( M x. U ) ) = ( P x. U ) )
98 97 negeqd 
 |-  ( ph -> -u ( 3 x. ( M x. U ) ) = -u ( P x. U ) )
99 89 91 98 3eqtrd 
 |-  ( ph -> ( 3 x. ( ( U ^ 2 ) x. -u ( M / U ) ) ) = -u ( P x. U ) )
100 99 oveq2d 
 |-  ( ph -> ( ( U ^ 3 ) + ( 3 x. ( ( U ^ 2 ) x. -u ( M / U ) ) ) ) = ( ( U ^ 3 ) + -u ( P x. U ) ) )
101 sqneg 
 |-  ( ( M / U ) e. CC -> ( -u ( M / U ) ^ 2 ) = ( ( M / U ) ^ 2 ) )
102 43 101 syl 
 |-  ( ph -> ( -u ( M / U ) ^ 2 ) = ( ( M / U ) ^ 2 ) )
103 43 sqvald 
 |-  ( ph -> ( ( M / U ) ^ 2 ) = ( ( M / U ) x. ( M / U ) ) )
104 102 103 eqtrd 
 |-  ( ph -> ( -u ( M / U ) ^ 2 ) = ( ( M / U ) x. ( M / U ) ) )
105 104 oveq2d 
 |-  ( ph -> ( U x. ( -u ( M / U ) ^ 2 ) ) = ( U x. ( ( M / U ) x. ( M / U ) ) ) )
106 11 43 43 mulassd 
 |-  ( ph -> ( ( U x. ( M / U ) ) x. ( M / U ) ) = ( U x. ( ( M / U ) x. ( M / U ) ) ) )
107 29 11 12 divcan2d 
 |-  ( ph -> ( U x. ( M / U ) ) = M )
108 107 oveq1d 
 |-  ( ph -> ( ( U x. ( M / U ) ) x. ( M / U ) ) = ( M x. ( M / U ) ) )
109 105 106 108 3eqtr2d 
 |-  ( ph -> ( U x. ( -u ( M / U ) ^ 2 ) ) = ( M x. ( M / U ) ) )
110 109 oveq2d 
 |-  ( ph -> ( 3 x. ( U x. ( -u ( M / U ) ^ 2 ) ) ) = ( 3 x. ( M x. ( M / U ) ) ) )
111 25 29 43 mulassd 
 |-  ( ph -> ( ( 3 x. M ) x. ( M / U ) ) = ( 3 x. ( M x. ( M / U ) ) ) )
112 95 oveq1d 
 |-  ( ph -> ( ( 3 x. M ) x. ( M / U ) ) = ( P x. ( M / U ) ) )
113 110 111 112 3eqtr2d 
 |-  ( ph -> ( 3 x. ( U x. ( -u ( M / U ) ^ 2 ) ) ) = ( P x. ( M / U ) ) )
114 3nn 
 |-  3 e. NN
115 114 a1i 
 |-  ( ph -> 3 e. NN )
116 n2dvds3 
 |-  -. 2 || 3
117 116 a1i 
 |-  ( ph -> -. 2 || 3 )
118 oexpneg 
 |-  ( ( ( M / U ) e. CC /\ 3 e. NN /\ -. 2 || 3 ) -> ( -u ( M / U ) ^ 3 ) = -u ( ( M / U ) ^ 3 ) )
119 43 115 117 118 syl3anc 
 |-  ( ph -> ( -u ( M / U ) ^ 3 ) = -u ( ( M / U ) ^ 3 ) )
120 14 a1i 
 |-  ( ph -> 3 e. NN0 )
121 29 11 12 120 expdivd 
 |-  ( ph -> ( ( M / U ) ^ 3 ) = ( ( M ^ 3 ) / ( U ^ 3 ) ) )
122 121 negeqd 
 |-  ( ph -> -u ( ( M / U ) ^ 3 ) = -u ( ( M ^ 3 ) / ( U ^ 3 ) ) )
123 119 122 eqtrd 
 |-  ( ph -> ( -u ( M / U ) ^ 3 ) = -u ( ( M ^ 3 ) / ( U ^ 3 ) ) )
124 113 123 oveq12d 
 |-  ( ph -> ( ( 3 x. ( U x. ( -u ( M / U ) ^ 2 ) ) ) + ( -u ( M / U ) ^ 3 ) ) = ( ( P x. ( M / U ) ) + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) )
125 100 124 oveq12d 
 |-  ( ph -> ( ( ( U ^ 3 ) + ( 3 x. ( ( U ^ 2 ) x. -u ( M / U ) ) ) ) + ( ( 3 x. ( U x. ( -u ( M / U ) ^ 2 ) ) ) + ( -u ( M / U ) ^ 3 ) ) ) = ( ( ( U ^ 3 ) + -u ( P x. U ) ) + ( ( P x. ( M / U ) ) + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) ) )
126 74 77 125 3eqtrd 
 |-  ( ph -> ( X ^ 3 ) = ( ( ( U ^ 3 ) + -u ( P x. U ) ) + ( ( P x. ( M / U ) ) + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) ) )
127 56 39 addcld 
 |-  ( ph -> ( ( P x. ( M / U ) ) + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) e. CC )
128 16 55 127 addassd 
 |-  ( ph -> ( ( ( U ^ 3 ) + -u ( P x. U ) ) + ( ( P x. ( M / U ) ) + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) ) = ( ( U ^ 3 ) + ( -u ( P x. U ) + ( ( P x. ( M / U ) ) + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) ) ) )
129 126 128 eqtrd 
 |-  ( ph -> ( X ^ 3 ) = ( ( U ^ 3 ) + ( -u ( P x. U ) + ( ( P x. ( M / U ) ) + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) ) ) )
130 129 oveq1d 
 |-  ( ph -> ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = ( ( ( U ^ 3 ) + ( -u ( P x. U ) + ( ( P x. ( M / U ) ) + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) ) ) + ( ( P x. X ) + Q ) ) )
131 55 127 addcld 
 |-  ( ph -> ( -u ( P x. U ) + ( ( P x. ( M / U ) ) + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) ) e. CC )
132 37 2 addcld 
 |-  ( ph -> ( ( P x. X ) + Q ) e. CC )
133 16 131 132 addassd 
 |-  ( ph -> ( ( ( U ^ 3 ) + ( -u ( P x. U ) + ( ( P x. ( M / U ) ) + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) ) ) + ( ( P x. X ) + Q ) ) = ( ( U ^ 3 ) + ( ( -u ( P x. U ) + ( ( P x. ( M / U ) ) + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) ) + ( ( P x. X ) + Q ) ) ) )
134 130 133 eqtrd 
 |-  ( ph -> ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = ( ( U ^ 3 ) + ( ( -u ( P x. U ) + ( ( P x. ( M / U ) ) + -u ( ( M ^ 3 ) / ( U ^ 3 ) ) ) ) + ( ( P x. X ) + Q ) ) ) )
135 16 sqcld 
 |-  ( ph -> ( ( U ^ 3 ) ^ 2 ) e. CC )
136 68 31 subcld 
 |-  ( ph -> ( ( Q x. ( U ^ 3 ) ) - ( M ^ 3 ) ) e. CC )
137 135 136 16 21 divdird 
 |-  ( ph -> ( ( ( ( U ^ 3 ) ^ 2 ) + ( ( Q x. ( U ^ 3 ) ) - ( M ^ 3 ) ) ) / ( U ^ 3 ) ) = ( ( ( ( U ^ 3 ) ^ 2 ) / ( U ^ 3 ) ) + ( ( ( Q x. ( U ^ 3 ) ) - ( M ^ 3 ) ) / ( U ^ 3 ) ) ) )
138 71 134 137 3eqtr4d 
 |-  ( ph -> ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = ( ( ( ( U ^ 3 ) ^ 2 ) + ( ( Q x. ( U ^ 3 ) ) - ( M ^ 3 ) ) ) / ( U ^ 3 ) ) )
139 138 eqeq1d 
 |-  ( ph -> ( ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 <-> ( ( ( ( U ^ 3 ) ^ 2 ) + ( ( Q x. ( U ^ 3 ) ) - ( M ^ 3 ) ) ) / ( U ^ 3 ) ) = 0 ) )
140 135 136 addcld 
 |-  ( ph -> ( ( ( U ^ 3 ) ^ 2 ) + ( ( Q x. ( U ^ 3 ) ) - ( M ^ 3 ) ) ) e. CC )
141 140 16 21 diveq0ad 
 |-  ( ph -> ( ( ( ( ( U ^ 3 ) ^ 2 ) + ( ( Q x. ( U ^ 3 ) ) - ( M ^ 3 ) ) ) / ( U ^ 3 ) ) = 0 <-> ( ( ( U ^ 3 ) ^ 2 ) + ( ( Q x. ( U ^ 3 ) ) - ( M ^ 3 ) ) ) = 0 ) )
142 139 141 bitrd 
 |-  ( ph -> ( ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 <-> ( ( ( U ^ 3 ) ^ 2 ) + ( ( Q x. ( U ^ 3 ) ) - ( M ^ 3 ) ) ) = 0 ) )