Metamath Proof Explorer

Theorem dcubic2

Description: Reverse direction of dcubic . Given a solution U to the "substitution" quadratic equation X = U - M / U , show that X is in the desired form. (Contributed by Mario Carneiro, 25-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 ) ) )
dcubic2.x 
|- ( ph -> ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 )
Assertion dcubic2 
|- ( ph -> E. r e. CC ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) )

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 dcubic2.x 
 |-  ( ph -> ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 )
15 11 4 10 divcld 
 |-  ( ph -> ( U / T ) e. CC )
16 15 adantr 
 |-  ( ( ph /\ ( U ^ 3 ) = ( G - N ) ) -> ( U / T ) e. CC )
17 3nn0 
 |-  3 e. NN0
18 17 a1i 
 |-  ( ph -> 3 e. NN0 )
19 11 4 10 18 expdivd 
 |-  ( ph -> ( ( U / T ) ^ 3 ) = ( ( U ^ 3 ) / ( T ^ 3 ) ) )
20 19 adantr 
 |-  ( ( ph /\ ( U ^ 3 ) = ( G - N ) ) -> ( ( U / T ) ^ 3 ) = ( ( U ^ 3 ) / ( T ^ 3 ) ) )
21 oveq1 
 |-  ( ( U ^ 3 ) = ( G - N ) -> ( ( U ^ 3 ) / ( T ^ 3 ) ) = ( ( G - N ) / ( T ^ 3 ) ) )
22 5 oveq1d 
 |-  ( ph -> ( ( T ^ 3 ) / ( T ^ 3 ) ) = ( ( G - N ) / ( T ^ 3 ) ) )
23 expcl 
 |-  ( ( T e. CC /\ 3 e. NN0 ) -> ( T ^ 3 ) e. CC )
24 4 17 23 sylancl 
 |-  ( ph -> ( T ^ 3 ) e. CC )
25 3z 
 |-  3 e. ZZ
26 25 a1i 
 |-  ( ph -> 3 e. ZZ )
27 4 10 26 expne0d 
 |-  ( ph -> ( T ^ 3 ) =/= 0 )
28 24 27 dividd 
 |-  ( ph -> ( ( T ^ 3 ) / ( T ^ 3 ) ) = 1 )
29 22 28 eqtr3d 
 |-  ( ph -> ( ( G - N ) / ( T ^ 3 ) ) = 1 )
30 21 29 sylan9eqr 
 |-  ( ( ph /\ ( U ^ 3 ) = ( G - N ) ) -> ( ( U ^ 3 ) / ( T ^ 3 ) ) = 1 )
31 20 30 eqtrd 
 |-  ( ( ph /\ ( U ^ 3 ) = ( G - N ) ) -> ( ( U / T ) ^ 3 ) = 1 )
32 11 4 10 divcan1d 
 |-  ( ph -> ( ( U / T ) x. T ) = U )
33 32 oveq2d 
 |-  ( ph -> ( M / ( ( U / T ) x. T ) ) = ( M / U ) )
34 32 33 oveq12d 
 |-  ( ph -> ( ( ( U / T ) x. T ) - ( M / ( ( U / T ) x. T ) ) ) = ( U - ( M / U ) ) )
35 13 34 eqtr4d 
 |-  ( ph -> X = ( ( ( U / T ) x. T ) - ( M / ( ( U / T ) x. T ) ) ) )
36 35 adantr 
 |-  ( ( ph /\ ( U ^ 3 ) = ( G - N ) ) -> X = ( ( ( U / T ) x. T ) - ( M / ( ( U / T ) x. T ) ) ) )
37 oveq1 
 |-  ( r = ( U / T ) -> ( r ^ 3 ) = ( ( U / T ) ^ 3 ) )
38 37 eqeq1d 
 |-  ( r = ( U / T ) -> ( ( r ^ 3 ) = 1 <-> ( ( U / T ) ^ 3 ) = 1 ) )
39 oveq1 
 |-  ( r = ( U / T ) -> ( r x. T ) = ( ( U / T ) x. T ) )
40 39 oveq2d 
 |-  ( r = ( U / T ) -> ( M / ( r x. T ) ) = ( M / ( ( U / T ) x. T ) ) )
41 39 40 oveq12d 
 |-  ( r = ( U / T ) -> ( ( r x. T ) - ( M / ( r x. T ) ) ) = ( ( ( U / T ) x. T ) - ( M / ( ( U / T ) x. T ) ) ) )
42 41 eqeq2d 
 |-  ( r = ( U / T ) -> ( X = ( ( r x. T ) - ( M / ( r x. T ) ) ) <-> X = ( ( ( U / T ) x. T ) - ( M / ( ( U / T ) x. T ) ) ) ) )
43 38 42 anbi12d 
 |-  ( r = ( U / T ) -> ( ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) <-> ( ( ( U / T ) ^ 3 ) = 1 /\ X = ( ( ( U / T ) x. T ) - ( M / ( ( U / T ) x. T ) ) ) ) ) )
44 43 rspcev 
 |-  ( ( ( U / T ) e. CC /\ ( ( ( U / T ) ^ 3 ) = 1 /\ X = ( ( ( U / T ) x. T ) - ( M / ( ( U / T ) x. T ) ) ) ) ) -> E. r e. CC ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) )
45 16 31 36 44 syl12anc 
 |-  ( ( ph /\ ( U ^ 3 ) = ( G - N ) ) -> E. r e. CC ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) )
46 3cn 
 |-  3 e. CC
47 46 a1i 
 |-  ( ph -> 3 e. CC )
48 3ne0 
 |-  3 =/= 0
49 48 a1i 
 |-  ( ph -> 3 =/= 0 )
50 1 47 49 divcld 
 |-  ( ph -> ( P / 3 ) e. CC )
51 8 50 eqeltrd 
 |-  ( ph -> M e. CC )
52 51 11 12 divcld 
 |-  ( ph -> ( M / U ) e. CC )
53 52 negcld 
 |-  ( ph -> -u ( M / U ) e. CC )
54 53 4 10 divcld 
 |-  ( ph -> ( -u ( M / U ) / T ) e. CC )
55 54 adantr 
 |-  ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> ( -u ( M / U ) / T ) e. CC )
56 53 4 10 18 expdivd 
 |-  ( ph -> ( ( -u ( M / U ) / T ) ^ 3 ) = ( ( -u ( M / U ) ^ 3 ) / ( T ^ 3 ) ) )
57 51 11 12 divnegd 
 |-  ( ph -> -u ( M / U ) = ( -u M / U ) )
58 57 oveq1d 
 |-  ( ph -> ( -u ( M / U ) ^ 3 ) = ( ( -u M / U ) ^ 3 ) )
59 51 negcld 
 |-  ( ph -> -u M e. CC )
60 59 11 12 18 expdivd 
 |-  ( ph -> ( ( -u M / U ) ^ 3 ) = ( ( -u M ^ 3 ) / ( U ^ 3 ) ) )
61 5 oveq2d 
 |-  ( ph -> ( ( G + N ) x. ( T ^ 3 ) ) = ( ( G + N ) x. ( G - N ) ) )
62 2 halfcld 
 |-  ( ph -> ( Q / 2 ) e. CC )
63 9 62 eqeltrd 
 |-  ( ph -> N e. CC )
64 subsq 
 |-  ( ( G e. CC /\ N e. CC ) -> ( ( G ^ 2 ) - ( N ^ 2 ) ) = ( ( G + N ) x. ( G - N ) ) )
65 6 63 64 syl2anc 
 |-  ( ph -> ( ( G ^ 2 ) - ( N ^ 2 ) ) = ( ( G + N ) x. ( G - N ) ) )
66 61 65 eqtr4d 
 |-  ( ph -> ( ( G + N ) x. ( T ^ 3 ) ) = ( ( G ^ 2 ) - ( N ^ 2 ) ) )
67 7 oveq1d 
 |-  ( ph -> ( ( G ^ 2 ) - ( N ^ 2 ) ) = ( ( ( N ^ 2 ) + ( M ^ 3 ) ) - ( N ^ 2 ) ) )
68 63 sqcld 
 |-  ( ph -> ( N ^ 2 ) e. CC )
69 expcl 
 |-  ( ( M e. CC /\ 3 e. NN0 ) -> ( M ^ 3 ) e. CC )
70 51 17 69 sylancl 
 |-  ( ph -> ( M ^ 3 ) e. CC )
71 68 70 pncan2d 
 |-  ( ph -> ( ( ( N ^ 2 ) + ( M ^ 3 ) ) - ( N ^ 2 ) ) = ( M ^ 3 ) )
72 66 67 71 3eqtrd 
 |-  ( ph -> ( ( G + N ) x. ( T ^ 3 ) ) = ( M ^ 3 ) )
73 72 negeqd 
 |-  ( ph -> -u ( ( G + N ) x. ( T ^ 3 ) ) = -u ( M ^ 3 ) )
74 6 63 addcld 
 |-  ( ph -> ( G + N ) e. CC )
75 74 24 mulneg1d 
 |-  ( ph -> ( -u ( G + N ) x. ( T ^ 3 ) ) = -u ( ( G + N ) x. ( T ^ 3 ) ) )
76 3nn 
 |-  3 e. NN
77 76 a1i 
 |-  ( ph -> 3 e. NN )
78 n2dvds3 
 |-  -. 2 || 3
79 78 a1i 
 |-  ( ph -> -. 2 || 3 )
80 oexpneg 
 |-  ( ( M e. CC /\ 3 e. NN /\ -. 2 || 3 ) -> ( -u M ^ 3 ) = -u ( M ^ 3 ) )
81 51 77 79 80 syl3anc 
 |-  ( ph -> ( -u M ^ 3 ) = -u ( M ^ 3 ) )
82 73 75 81 3eqtr4d 
 |-  ( ph -> ( -u ( G + N ) x. ( T ^ 3 ) ) = ( -u M ^ 3 ) )
83 82 oveq1d 
 |-  ( ph -> ( ( -u ( G + N ) x. ( T ^ 3 ) ) / ( U ^ 3 ) ) = ( ( -u M ^ 3 ) / ( U ^ 3 ) ) )
84 74 negcld 
 |-  ( ph -> -u ( G + N ) e. CC )
85 expcl 
 |-  ( ( U e. CC /\ 3 e. NN0 ) -> ( U ^ 3 ) e. CC )
86 11 17 85 sylancl 
 |-  ( ph -> ( U ^ 3 ) e. CC )
87 11 12 26 expne0d 
 |-  ( ph -> ( U ^ 3 ) =/= 0 )
88 84 24 86 87 div23d 
 |-  ( ph -> ( ( -u ( G + N ) x. ( T ^ 3 ) ) / ( U ^ 3 ) ) = ( ( -u ( G + N ) / ( U ^ 3 ) ) x. ( T ^ 3 ) ) )
89 83 88 eqtr3d 
 |-  ( ph -> ( ( -u M ^ 3 ) / ( U ^ 3 ) ) = ( ( -u ( G + N ) / ( U ^ 3 ) ) x. ( T ^ 3 ) ) )
90 58 60 89 3eqtrd 
 |-  ( ph -> ( -u ( M / U ) ^ 3 ) = ( ( -u ( G + N ) / ( U ^ 3 ) ) x. ( T ^ 3 ) ) )
91 90 oveq1d 
 |-  ( ph -> ( ( -u ( M / U ) ^ 3 ) / ( T ^ 3 ) ) = ( ( ( -u ( G + N ) / ( U ^ 3 ) ) x. ( T ^ 3 ) ) / ( T ^ 3 ) ) )
92 84 86 87 divcld 
 |-  ( ph -> ( -u ( G + N ) / ( U ^ 3 ) ) e. CC )
93 92 24 27 divcan4d 
 |-  ( ph -> ( ( ( -u ( G + N ) / ( U ^ 3 ) ) x. ( T ^ 3 ) ) / ( T ^ 3 ) ) = ( -u ( G + N ) / ( U ^ 3 ) ) )
94 56 91 93 3eqtrd 
 |-  ( ph -> ( ( -u ( M / U ) / T ) ^ 3 ) = ( -u ( G + N ) / ( U ^ 3 ) ) )
95 94 adantr 
 |-  ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> ( ( -u ( M / U ) / T ) ^ 3 ) = ( -u ( G + N ) / ( U ^ 3 ) ) )
96 oveq1 
 |-  ( ( U ^ 3 ) = -u ( G + N ) -> ( ( U ^ 3 ) / ( U ^ 3 ) ) = ( -u ( G + N ) / ( U ^ 3 ) ) )
97 96 eqcomd 
 |-  ( ( U ^ 3 ) = -u ( G + N ) -> ( -u ( G + N ) / ( U ^ 3 ) ) = ( ( U ^ 3 ) / ( U ^ 3 ) ) )
98 86 87 dividd 
 |-  ( ph -> ( ( U ^ 3 ) / ( U ^ 3 ) ) = 1 )
99 97 98 sylan9eqr 
 |-  ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> ( -u ( G + N ) / ( U ^ 3 ) ) = 1 )
100 95 99 eqtrd 
 |-  ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> ( ( -u ( M / U ) / T ) ^ 3 ) = 1 )
101 52 11 neg2subd 
 |-  ( ph -> ( -u ( M / U ) - -u U ) = ( U - ( M / U ) ) )
102 13 101 eqtr4d 
 |-  ( ph -> X = ( -u ( M / U ) - -u U ) )
103 102 adantr 
 |-  ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> X = ( -u ( M / U ) - -u U ) )
104 53 4 10 divcan1d 
 |-  ( ph -> ( ( -u ( M / U ) / T ) x. T ) = -u ( M / U ) )
105 104 adantr 
 |-  ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> ( ( -u ( M / U ) / T ) x. T ) = -u ( M / U ) )
106 51 11 12 divneg2d 
 |-  ( ph -> -u ( M / U ) = ( M / -u U ) )
107 104 106 eqtrd 
 |-  ( ph -> ( ( -u ( M / U ) / T ) x. T ) = ( M / -u U ) )
108 107 adantr 
 |-  ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> ( ( -u ( M / U ) / T ) x. T ) = ( M / -u U ) )
109 108 oveq2d 
 |-  ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> ( M / ( ( -u ( M / U ) / T ) x. T ) ) = ( M / ( M / -u U ) ) )
110 51 adantr 
 |-  ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> M e. CC )
111 11 negcld 
 |-  ( ph -> -u U e. CC )
112 111 adantr 
 |-  ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> -u U e. CC )
113 75 73 eqtrd 
 |-  ( ph -> ( -u ( G + N ) x. ( T ^ 3 ) ) = -u ( M ^ 3 ) )
114 113 adantr 
 |-  ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> ( -u ( G + N ) x. ( T ^ 3 ) ) = -u ( M ^ 3 ) )
115 84 adantr 
 |-  ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> -u ( G + N ) e. CC )
116 24 adantr 
 |-  ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> ( T ^ 3 ) e. CC )
117 simpr 
 |-  ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> ( U ^ 3 ) = -u ( G + N ) )
118 87 adantr 
 |-  ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> ( U ^ 3 ) =/= 0 )
119 117 118 eqnetrrd 
 |-  ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> -u ( G + N ) =/= 0 )
120 27 adantr 
 |-  ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> ( T ^ 3 ) =/= 0 )
121 115 116 119 120 mulne0d 
 |-  ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> ( -u ( G + N ) x. ( T ^ 3 ) ) =/= 0 )
122 114 121 eqnetrrd 
 |-  ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> -u ( M ^ 3 ) =/= 0 )
123 oveq1 
 |-  ( M = 0 -> ( M ^ 3 ) = ( 0 ^ 3 ) )
124 0exp 
 |-  ( 3 e. NN -> ( 0 ^ 3 ) = 0 )
125 76 124 ax-mp 
 |-  ( 0 ^ 3 ) = 0
126 123 125 eqtrdi 
 |-  ( M = 0 -> ( M ^ 3 ) = 0 )
127 126 negeqd 
 |-  ( M = 0 -> -u ( M ^ 3 ) = -u 0 )
128 neg0 
 |-  -u 0 = 0
129 127 128 eqtrdi 
 |-  ( M = 0 -> -u ( M ^ 3 ) = 0 )
130 129 necon3i 
 |-  ( -u ( M ^ 3 ) =/= 0 -> M =/= 0 )
131 122 130 syl 
 |-  ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> M =/= 0 )
132 11 12 negne0d 
 |-  ( ph -> -u U =/= 0 )
133 132 adantr 
 |-  ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> -u U =/= 0 )
134 110 112 131 133 ddcand 
 |-  ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> ( M / ( M / -u U ) ) = -u U )
135 109 134 eqtrd 
 |-  ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> ( M / ( ( -u ( M / U ) / T ) x. T ) ) = -u U )
136 105 135 oveq12d 
 |-  ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> ( ( ( -u ( M / U ) / T ) x. T ) - ( M / ( ( -u ( M / U ) / T ) x. T ) ) ) = ( -u ( M / U ) - -u U ) )
137 103 136 eqtr4d 
 |-  ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> X = ( ( ( -u ( M / U ) / T ) x. T ) - ( M / ( ( -u ( M / U ) / T ) x. T ) ) ) )
138 oveq1 
 |-  ( r = ( -u ( M / U ) / T ) -> ( r ^ 3 ) = ( ( -u ( M / U ) / T ) ^ 3 ) )
139 138 eqeq1d 
 |-  ( r = ( -u ( M / U ) / T ) -> ( ( r ^ 3 ) = 1 <-> ( ( -u ( M / U ) / T ) ^ 3 ) = 1 ) )
140 oveq1 
 |-  ( r = ( -u ( M / U ) / T ) -> ( r x. T ) = ( ( -u ( M / U ) / T ) x. T ) )
141 140 oveq2d 
 |-  ( r = ( -u ( M / U ) / T ) -> ( M / ( r x. T ) ) = ( M / ( ( -u ( M / U ) / T ) x. T ) ) )
142 140 141 oveq12d 
 |-  ( r = ( -u ( M / U ) / T ) -> ( ( r x. T ) - ( M / ( r x. T ) ) ) = ( ( ( -u ( M / U ) / T ) x. T ) - ( M / ( ( -u ( M / U ) / T ) x. T ) ) ) )
143 142 eqeq2d 
 |-  ( r = ( -u ( M / U ) / T ) -> ( X = ( ( r x. T ) - ( M / ( r x. T ) ) ) <-> X = ( ( ( -u ( M / U ) / T ) x. T ) - ( M / ( ( -u ( M / U ) / T ) x. T ) ) ) ) )
144 139 143 anbi12d 
 |-  ( r = ( -u ( M / U ) / T ) -> ( ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) <-> ( ( ( -u ( M / U ) / T ) ^ 3 ) = 1 /\ X = ( ( ( -u ( M / U ) / T ) x. T ) - ( M / ( ( -u ( M / U ) / T ) x. T ) ) ) ) ) )
145 144 rspcev 
 |-  ( ( ( -u ( M / U ) / T ) e. CC /\ ( ( ( -u ( M / U ) / T ) ^ 3 ) = 1 /\ X = ( ( ( -u ( M / U ) / T ) x. T ) - ( M / ( ( -u ( M / U ) / T ) x. T ) ) ) ) ) -> E. r e. CC ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) )
146 55 100 137 145 syl12anc 
 |-  ( ( ph /\ ( U ^ 3 ) = -u ( G + N ) ) -> E. r e. CC ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) )
147 86 sqcld 
 |-  ( ph -> ( ( U ^ 3 ) ^ 2 ) e. CC )
148 147 mullidd 
 |-  ( ph -> ( 1 x. ( ( U ^ 3 ) ^ 2 ) ) = ( ( U ^ 3 ) ^ 2 ) )
149 2 86 mulcld 
 |-  ( ph -> ( Q x. ( U ^ 3 ) ) e. CC )
150 149 70 negsubd 
 |-  ( ph -> ( ( Q x. ( U ^ 3 ) ) + -u ( M ^ 3 ) ) = ( ( Q x. ( U ^ 3 ) ) - ( M ^ 3 ) ) )
151 148 150 oveq12d 
 |-  ( ph -> ( ( 1 x. ( ( U ^ 3 ) ^ 2 ) ) + ( ( Q x. ( U ^ 3 ) ) + -u ( M ^ 3 ) ) ) = ( ( ( U ^ 3 ) ^ 2 ) + ( ( Q x. ( U ^ 3 ) ) - ( M ^ 3 ) ) ) )
152 1 2 3 4 5 6 7 8 9 10 11 12 13 dcubic1lem 
 |-  ( ph -> ( ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 <-> ( ( ( U ^ 3 ) ^ 2 ) + ( ( Q x. ( U ^ 3 ) ) - ( M ^ 3 ) ) ) = 0 ) )
153 14 152 mpbid 
 |-  ( ph -> ( ( ( U ^ 3 ) ^ 2 ) + ( ( Q x. ( U ^ 3 ) ) - ( M ^ 3 ) ) ) = 0 )
154 151 153 eqtrd 
 |-  ( ph -> ( ( 1 x. ( ( U ^ 3 ) ^ 2 ) ) + ( ( Q x. ( U ^ 3 ) ) + -u ( M ^ 3 ) ) ) = 0 )
155 1cnd 
 |-  ( ph -> 1 e. CC )
156 ax-1ne0 
 |-  1 =/= 0
157 156 a1i 
 |-  ( ph -> 1 =/= 0 )
158 70 negcld 
 |-  ( ph -> -u ( M ^ 3 ) e. CC )
159 2cn 
 |-  2 e. CC
160 mulcl 
 |-  ( ( 2 e. CC /\ G e. CC ) -> ( 2 x. G ) e. CC )
161 159 6 160 sylancr 
 |-  ( ph -> ( 2 x. G ) e. CC )
162 sqmul 
 |-  ( ( 2 e. CC /\ G e. CC ) -> ( ( 2 x. G ) ^ 2 ) = ( ( 2 ^ 2 ) x. ( G ^ 2 ) ) )
163 159 6 162 sylancr 
 |-  ( ph -> ( ( 2 x. G ) ^ 2 ) = ( ( 2 ^ 2 ) x. ( G ^ 2 ) ) )
164 7 oveq2d 
 |-  ( ph -> ( ( 2 ^ 2 ) x. ( G ^ 2 ) ) = ( ( 2 ^ 2 ) x. ( ( N ^ 2 ) + ( M ^ 3 ) ) ) )
165 159 sqcli 
 |-  ( 2 ^ 2 ) e. CC
166 mulcl 
 |-  ( ( ( 2 ^ 2 ) e. CC /\ ( N ^ 2 ) e. CC ) -> ( ( 2 ^ 2 ) x. ( N ^ 2 ) ) e. CC )
167 165 68 166 sylancr 
 |-  ( ph -> ( ( 2 ^ 2 ) x. ( N ^ 2 ) ) e. CC )
168 mulcl 
 |-  ( ( ( 2 ^ 2 ) e. CC /\ ( M ^ 3 ) e. CC ) -> ( ( 2 ^ 2 ) x. ( M ^ 3 ) ) e. CC )
169 165 70 168 sylancr 
 |-  ( ph -> ( ( 2 ^ 2 ) x. ( M ^ 3 ) ) e. CC )
170 167 169 subnegd 
 |-  ( ph -> ( ( ( 2 ^ 2 ) x. ( N ^ 2 ) ) - -u ( ( 2 ^ 2 ) x. ( M ^ 3 ) ) ) = ( ( ( 2 ^ 2 ) x. ( N ^ 2 ) ) + ( ( 2 ^ 2 ) x. ( M ^ 3 ) ) ) )
171 9 oveq2d 
 |-  ( ph -> ( 2 x. N ) = ( 2 x. ( Q / 2 ) ) )
172 159 a1i 
 |-  ( ph -> 2 e. CC )
173 2ne0 
 |-  2 =/= 0
174 173 a1i 
 |-  ( ph -> 2 =/= 0 )
175 2 172 174 divcan2d 
 |-  ( ph -> ( 2 x. ( Q / 2 ) ) = Q )
176 171 175 eqtrd 
 |-  ( ph -> ( 2 x. N ) = Q )
177 176 oveq1d 
 |-  ( ph -> ( ( 2 x. N ) ^ 2 ) = ( Q ^ 2 ) )
178 sqmul 
 |-  ( ( 2 e. CC /\ N e. CC ) -> ( ( 2 x. N ) ^ 2 ) = ( ( 2 ^ 2 ) x. ( N ^ 2 ) ) )
179 159 63 178 sylancr 
 |-  ( ph -> ( ( 2 x. N ) ^ 2 ) = ( ( 2 ^ 2 ) x. ( N ^ 2 ) ) )
180 177 179 eqtr3d 
 |-  ( ph -> ( Q ^ 2 ) = ( ( 2 ^ 2 ) x. ( N ^ 2 ) ) )
181 158 mullidd 
 |-  ( ph -> ( 1 x. -u ( M ^ 3 ) ) = -u ( M ^ 3 ) )
182 181 oveq2d 
 |-  ( ph -> ( 4 x. ( 1 x. -u ( M ^ 3 ) ) ) = ( 4 x. -u ( M ^ 3 ) ) )
183 4cn 
 |-  4 e. CC
184 mulneg2 
 |-  ( ( 4 e. CC /\ ( M ^ 3 ) e. CC ) -> ( 4 x. -u ( M ^ 3 ) ) = -u ( 4 x. ( M ^ 3 ) ) )
185 183 70 184 sylancr 
 |-  ( ph -> ( 4 x. -u ( M ^ 3 ) ) = -u ( 4 x. ( M ^ 3 ) ) )
186 182 185 eqtrd 
 |-  ( ph -> ( 4 x. ( 1 x. -u ( M ^ 3 ) ) ) = -u ( 4 x. ( M ^ 3 ) ) )
187 sq2 
 |-  ( 2 ^ 2 ) = 4
188 187 oveq1i 
 |-  ( ( 2 ^ 2 ) x. ( M ^ 3 ) ) = ( 4 x. ( M ^ 3 ) )
189 188 negeqi 
 |-  -u ( ( 2 ^ 2 ) x. ( M ^ 3 ) ) = -u ( 4 x. ( M ^ 3 ) )
190 186 189 eqtr4di 
 |-  ( ph -> ( 4 x. ( 1 x. -u ( M ^ 3 ) ) ) = -u ( ( 2 ^ 2 ) x. ( M ^ 3 ) ) )
191 180 190 oveq12d 
 |-  ( ph -> ( ( Q ^ 2 ) - ( 4 x. ( 1 x. -u ( M ^ 3 ) ) ) ) = ( ( ( 2 ^ 2 ) x. ( N ^ 2 ) ) - -u ( ( 2 ^ 2 ) x. ( M ^ 3 ) ) ) )
192 165 a1i 
 |-  ( ph -> ( 2 ^ 2 ) e. CC )
193 192 68 70 adddid 
 |-  ( ph -> ( ( 2 ^ 2 ) x. ( ( N ^ 2 ) + ( M ^ 3 ) ) ) = ( ( ( 2 ^ 2 ) x. ( N ^ 2 ) ) + ( ( 2 ^ 2 ) x. ( M ^ 3 ) ) ) )
194 170 191 193 3eqtr4rd 
 |-  ( ph -> ( ( 2 ^ 2 ) x. ( ( N ^ 2 ) + ( M ^ 3 ) ) ) = ( ( Q ^ 2 ) - ( 4 x. ( 1 x. -u ( M ^ 3 ) ) ) ) )
195 163 164 194 3eqtrd 
 |-  ( ph -> ( ( 2 x. G ) ^ 2 ) = ( ( Q ^ 2 ) - ( 4 x. ( 1 x. -u ( M ^ 3 ) ) ) ) )
196 155 157 2 158 86 161 195 quad2 
 |-  ( ph -> ( ( ( 1 x. ( ( U ^ 3 ) ^ 2 ) ) + ( ( Q x. ( U ^ 3 ) ) + -u ( M ^ 3 ) ) ) = 0 <-> ( ( U ^ 3 ) = ( ( -u Q + ( 2 x. G ) ) / ( 2 x. 1 ) ) \/ ( U ^ 3 ) = ( ( -u Q - ( 2 x. G ) ) / ( 2 x. 1 ) ) ) ) )
197 154 196 mpbid 
 |-  ( ph -> ( ( U ^ 3 ) = ( ( -u Q + ( 2 x. G ) ) / ( 2 x. 1 ) ) \/ ( U ^ 3 ) = ( ( -u Q - ( 2 x. G ) ) / ( 2 x. 1 ) ) ) )
198 2t1e2 
 |-  ( 2 x. 1 ) = 2
199 198 oveq2i 
 |-  ( ( -u Q + ( 2 x. G ) ) / ( 2 x. 1 ) ) = ( ( -u Q + ( 2 x. G ) ) / 2 )
200 2 negcld 
 |-  ( ph -> -u Q e. CC )
201 200 161 172 174 divdird 
 |-  ( ph -> ( ( -u Q + ( 2 x. G ) ) / 2 ) = ( ( -u Q / 2 ) + ( ( 2 x. G ) / 2 ) ) )
202 9 negeqd 
 |-  ( ph -> -u N = -u ( Q / 2 ) )
203 2 172 174 divnegd 
 |-  ( ph -> -u ( Q / 2 ) = ( -u Q / 2 ) )
204 202 203 eqtr2d 
 |-  ( ph -> ( -u Q / 2 ) = -u N )
205 6 172 174 divcan3d 
 |-  ( ph -> ( ( 2 x. G ) / 2 ) = G )
206 204 205 oveq12d 
 |-  ( ph -> ( ( -u Q / 2 ) + ( ( 2 x. G ) / 2 ) ) = ( -u N + G ) )
207 63 negcld 
 |-  ( ph -> -u N e. CC )
208 207 6 addcomd 
 |-  ( ph -> ( -u N + G ) = ( G + -u N ) )
209 6 63 negsubd 
 |-  ( ph -> ( G + -u N ) = ( G - N ) )
210 208 209 eqtrd 
 |-  ( ph -> ( -u N + G ) = ( G - N ) )
211 201 206 210 3eqtrd 
 |-  ( ph -> ( ( -u Q + ( 2 x. G ) ) / 2 ) = ( G - N ) )
212 199 211 eqtrid 
 |-  ( ph -> ( ( -u Q + ( 2 x. G ) ) / ( 2 x. 1 ) ) = ( G - N ) )
213 212 eqeq2d 
 |-  ( ph -> ( ( U ^ 3 ) = ( ( -u Q + ( 2 x. G ) ) / ( 2 x. 1 ) ) <-> ( U ^ 3 ) = ( G - N ) ) )
214 198 oveq2i 
 |-  ( ( -u Q - ( 2 x. G ) ) / ( 2 x. 1 ) ) = ( ( -u Q - ( 2 x. G ) ) / 2 )
215 204 205 oveq12d 
 |-  ( ph -> ( ( -u Q / 2 ) - ( ( 2 x. G ) / 2 ) ) = ( -u N - G ) )
216 200 161 172 174 divsubdird 
 |-  ( ph -> ( ( -u Q - ( 2 x. G ) ) / 2 ) = ( ( -u Q / 2 ) - ( ( 2 x. G ) / 2 ) ) )
217 6 63 addcomd 
 |-  ( ph -> ( G + N ) = ( N + G ) )
218 217 negeqd 
 |-  ( ph -> -u ( G + N ) = -u ( N + G ) )
219 63 6 negdi2d 
 |-  ( ph -> -u ( N + G ) = ( -u N - G ) )
220 218 219 eqtrd 
 |-  ( ph -> -u ( G + N ) = ( -u N - G ) )
221 215 216 220 3eqtr4d 
 |-  ( ph -> ( ( -u Q - ( 2 x. G ) ) / 2 ) = -u ( G + N ) )
222 214 221 eqtrid 
 |-  ( ph -> ( ( -u Q - ( 2 x. G ) ) / ( 2 x. 1 ) ) = -u ( G + N ) )
223 222 eqeq2d 
 |-  ( ph -> ( ( U ^ 3 ) = ( ( -u Q - ( 2 x. G ) ) / ( 2 x. 1 ) ) <-> ( U ^ 3 ) = -u ( G + N ) ) )
224 213 223 orbi12d 
 |-  ( ph -> ( ( ( U ^ 3 ) = ( ( -u Q + ( 2 x. G ) ) / ( 2 x. 1 ) ) \/ ( U ^ 3 ) = ( ( -u Q - ( 2 x. G ) ) / ( 2 x. 1 ) ) ) <-> ( ( U ^ 3 ) = ( G - N ) \/ ( U ^ 3 ) = -u ( G + N ) ) ) )
225 197 224 mpbid 
 |-  ( ph -> ( ( U ^ 3 ) = ( G - N ) \/ ( U ^ 3 ) = -u ( G + N ) ) )
226 45 146 225 mpjaodan 
 |-  ( ph -> E. r e. CC ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) )