Metamath Proof Explorer

Theorem dcubic

Description: Solutions to the depressed cubic, a special case of cubic . (The definitions of M , N , G , T here differ from mcubic by scale factors of -u 9 , 5 4 , 5 4 and -u 2 7 respectively, to simplify the algebra and presentation.) (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 )
Assertion dcubic 
|- ( ph -> ( ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 <-> 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 10 adantr 
 |-  ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) -> T =/= 0 )
12 4 adantr 
 |-  ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) -> T e. CC )
13 3z 
 |-  3 e. ZZ
14 expne0i 
 |-  ( ( T e. CC /\ T =/= 0 /\ 3 e. ZZ ) -> ( T ^ 3 ) =/= 0 )
15 13 14 mp3an3 
 |-  ( ( T e. CC /\ T =/= 0 ) -> ( T ^ 3 ) =/= 0 )
16 15 ex 
 |-  ( T e. CC -> ( T =/= 0 -> ( T ^ 3 ) =/= 0 ) )
17 12 16 syl 
 |-  ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) -> ( T =/= 0 -> ( T ^ 3 ) =/= 0 ) )
18 5 ad2antrr 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( T ^ 3 ) = ( G - N ) )
19 6 ad2antrr 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> G e. CC )
20 7 ad2antrr 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( G ^ 2 ) = ( ( N ^ 2 ) + ( M ^ 3 ) ) )
21 9 ad2antrr 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> N = ( Q / 2 ) )
22 simprl 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> X = 0 )
23 22 oveq2d 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( P x. X ) = ( P x. 0 ) )
24 1 ad2antrr 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> P e. CC )
25 24 mul01d 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( P x. 0 ) = 0 )
26 23 25 eqtrd 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( P x. X ) = 0 )
27 26 oveq1d 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( ( P x. X ) + Q ) = ( 0 + Q ) )
28 22 oveq1d 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( X ^ 3 ) = ( 0 ^ 3 ) )
29 3nn 
 |-  3 e. NN
30 0exp 
 |-  ( 3 e. NN -> ( 0 ^ 3 ) = 0 )
31 29 30 ax-mp 
 |-  ( 0 ^ 3 ) = 0
32 28 31 eqtrdi 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( X ^ 3 ) = 0 )
33 32 oveq1d 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = ( 0 + ( ( P x. X ) + Q ) ) )
34 simplr 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 )
35 0cnd 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> 0 e. CC )
36 26 35 eqeltrd 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( P x. X ) e. CC )
37 2 ad2antrr 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> Q e. CC )
38 36 37 addcld 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( ( P x. X ) + Q ) e. CC )
39 38 addlidd 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( 0 + ( ( P x. X ) + Q ) ) = ( ( P x. X ) + Q ) )
40 33 34 39 3eqtr3rd 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( ( P x. X ) + Q ) = 0 )
41 37 addlidd 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( 0 + Q ) = Q )
42 27 40 41 3eqtr3rd 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> Q = 0 )
43 42 oveq1d 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( Q / 2 ) = ( 0 / 2 ) )
44 2cn 
 |-  2 e. CC
45 2ne0 
 |-  2 =/= 0
46 44 45 div0i 
 |-  ( 0 / 2 ) = 0
47 43 46 eqtrdi 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( Q / 2 ) = 0 )
48 21 47 eqtrd 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> N = 0 )
49 48 sq0id 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( N ^ 2 ) = 0 )
50 3cn 
 |-  3 e. CC
51 50 a1i 
 |-  ( ph -> 3 e. CC )
52 3ne0 
 |-  3 =/= 0
53 52 a1i 
 |-  ( ph -> 3 =/= 0 )
54 1 51 53 divcld 
 |-  ( ph -> ( P / 3 ) e. CC )
55 8 54 eqeltrd 
 |-  ( ph -> M e. CC )
56 55 ad2antrr 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> M e. CC )
57 4cn 
 |-  4 e. CC
58 57 a1i 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> 4 e. CC )
59 4ne0 
 |-  4 =/= 0
60 59 a1i 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> 4 =/= 0 )
61 22 sq0id 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( X ^ 2 ) = 0 )
62 61 oveq1d 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( ( X ^ 2 ) + ( 4 x. M ) ) = ( 0 + ( 4 x. M ) ) )
63 3 sqcld 
 |-  ( ph -> ( X ^ 2 ) e. CC )
64 mulcl 
 |-  ( ( 4 e. CC /\ M e. CC ) -> ( 4 x. M ) e. CC )
65 57 55 64 sylancr 
 |-  ( ph -> ( 4 x. M ) e. CC )
66 63 65 addcld 
 |-  ( ph -> ( ( X ^ 2 ) + ( 4 x. M ) ) e. CC )
67 66 ad2antrr 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( ( X ^ 2 ) + ( 4 x. M ) ) e. CC )
68 simprr 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 )
69 67 68 sqr00d 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( ( X ^ 2 ) + ( 4 x. M ) ) = 0 )
70 65 ad2antrr 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( 4 x. M ) e. CC )
71 70 addlidd 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( 0 + ( 4 x. M ) ) = ( 4 x. M ) )
72 62 69 71 3eqtr3rd 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( 4 x. M ) = 0 )
73 57 mul01i 
 |-  ( 4 x. 0 ) = 0
74 72 73 eqtr4di 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( 4 x. M ) = ( 4 x. 0 ) )
75 56 35 58 60 74 mulcanad 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> M = 0 )
76 75 oveq1d 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( M ^ 3 ) = ( 0 ^ 3 ) )
77 76 31 eqtrdi 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( M ^ 3 ) = 0 )
78 49 77 oveq12d 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( ( N ^ 2 ) + ( M ^ 3 ) ) = ( 0 + 0 ) )
79 00id 
 |-  ( 0 + 0 ) = 0
80 78 79 eqtrdi 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( ( N ^ 2 ) + ( M ^ 3 ) ) = 0 )
81 20 80 eqtrd 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( G ^ 2 ) = 0 )
82 19 81 sqeq0d 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> G = 0 )
83 82 48 oveq12d 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( G - N ) = ( 0 - 0 ) )
84 0m0e0 
 |-  ( 0 - 0 ) = 0
85 83 84 eqtrdi 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( G - N ) = 0 )
86 18 85 eqtrd 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> ( T ^ 3 ) = 0 )
87 86 ex 
 |-  ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) -> ( ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) -> ( T ^ 3 ) = 0 ) )
88 87 necon3ad 
 |-  ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) -> ( ( T ^ 3 ) =/= 0 -> -. ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) )
89 17 88 syld 
 |-  ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) -> ( T =/= 0 -> -. ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) )
90 11 89 mpd 
 |-  ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) -> -. ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) )
91 oveq12 
 |-  ( ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) = 0 /\ ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) = 0 ) -> ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) + ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) ) = ( 0 + 0 ) )
92 91 79 eqtrdi 
 |-  ( ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) = 0 /\ ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) = 0 ) -> ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) + ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) ) = 0 )
93 oveq12 
 |-  ( ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) = 0 /\ ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) = 0 ) -> ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) - ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) ) = ( 0 - 0 ) )
94 93 84 eqtrdi 
 |-  ( ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) = 0 /\ ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) = 0 ) -> ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) - ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) ) = 0 )
95 92 94 jca 
 |-  ( ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) = 0 /\ ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) = 0 ) -> ( ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) + ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) ) = 0 /\ ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) - ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) ) = 0 ) )
96 66 sqrtcld 
 |-  ( ph -> ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) e. CC )
97 halfaddsub 
 |-  ( ( X e. CC /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) e. CC ) -> ( ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) + ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) ) = X /\ ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) - ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) ) = ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) )
98 3 96 97 syl2anc 
 |-  ( ph -> ( ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) + ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) ) = X /\ ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) - ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) ) = ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) )
99 98 simpld 
 |-  ( ph -> ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) + ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) ) = X )
100 99 eqeq1d 
 |-  ( ph -> ( ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) + ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) ) = 0 <-> X = 0 ) )
101 98 simprd 
 |-  ( ph -> ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) - ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) ) = ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) )
102 101 eqeq1d 
 |-  ( ph -> ( ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) - ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) ) = 0 <-> ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) )
103 100 102 anbi12d 
 |-  ( ph -> ( ( ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) + ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) ) = 0 /\ ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) - ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) ) = 0 ) <-> ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) )
104 95 103 imbitrid 
 |-  ( ph -> ( ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) = 0 /\ ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) = 0 ) -> ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) )
105 104 con3d 
 |-  ( ph -> ( -. ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) -> -. ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) = 0 /\ ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) = 0 ) ) )
106 eldifi 
 |-  ( u e. ( CC \ { 0 } ) -> u e. CC )
107 106 adantl 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> u e. CC )
108 55 adantr 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> M e. CC )
109 eldifsni 
 |-  ( u e. ( CC \ { 0 } ) -> u =/= 0 )
110 109 adantl 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> u =/= 0 )
111 108 107 110 divcld 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( M / u ) e. CC )
112 3 adantr 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> X e. CC )
113 107 111 112 subaddd 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( ( u - ( M / u ) ) = X <-> ( ( M / u ) + X ) = u ) )
114 eqcom 
 |-  ( X = ( u - ( M / u ) ) <-> ( u - ( M / u ) ) = X )
115 eqcom 
 |-  ( u = ( ( M / u ) + X ) <-> ( ( M / u ) + X ) = u )
116 113 114 115 3bitr4g 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( X = ( u - ( M / u ) ) <-> u = ( ( M / u ) + X ) ) )
117 107 sqcld 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( u ^ 2 ) e. CC )
118 112 107 mulcld 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( X x. u ) e. CC )
119 118 108 addcld 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( ( X x. u ) + M ) e. CC )
120 117 119 subeq0ad 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( ( ( u ^ 2 ) - ( ( X x. u ) + M ) ) = 0 <-> ( u ^ 2 ) = ( ( X x. u ) + M ) ) )
121 107 sqvald 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( u ^ 2 ) = ( u x. u ) )
122 111 112 107 adddird 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( ( ( M / u ) + X ) x. u ) = ( ( ( M / u ) x. u ) + ( X x. u ) ) )
123 108 107 110 divcan1d 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( ( M / u ) x. u ) = M )
124 123 oveq1d 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( ( ( M / u ) x. u ) + ( X x. u ) ) = ( M + ( X x. u ) ) )
125 108 118 addcomd 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( M + ( X x. u ) ) = ( ( X x. u ) + M ) )
126 122 124 125 3eqtrrd 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( ( X x. u ) + M ) = ( ( ( M / u ) + X ) x. u ) )
127 121 126 eqeq12d 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( ( u ^ 2 ) = ( ( X x. u ) + M ) <-> ( u x. u ) = ( ( ( M / u ) + X ) x. u ) ) )
128 111 112 addcld 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( ( M / u ) + X ) e. CC )
129 107 128 107 110 mulcan2d 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( ( u x. u ) = ( ( ( M / u ) + X ) x. u ) <-> u = ( ( M / u ) + X ) ) )
130 120 127 129 3bitrd 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( ( ( u ^ 2 ) - ( ( X x. u ) + M ) ) = 0 <-> u = ( ( M / u ) + X ) ) )
131 1cnd 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> 1 e. CC )
132 ax-1ne0 
 |-  1 =/= 0
133 132 a1i 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> 1 =/= 0 )
134 3 negcld 
 |-  ( ph -> -u X e. CC )
135 134 adantr 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> -u X e. CC )
136 55 negcld 
 |-  ( ph -> -u M e. CC )
137 136 adantr 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> -u M e. CC )
138 sqneg 
 |-  ( X e. CC -> ( -u X ^ 2 ) = ( X ^ 2 ) )
139 112 138 syl 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( -u X ^ 2 ) = ( X ^ 2 ) )
140 137 mullidd 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( 1 x. -u M ) = -u M )
141 140 oveq2d 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( 4 x. ( 1 x. -u M ) ) = ( 4 x. -u M ) )
142 mulneg2 
 |-  ( ( 4 e. CC /\ M e. CC ) -> ( 4 x. -u M ) = -u ( 4 x. M ) )
143 57 108 142 sylancr 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( 4 x. -u M ) = -u ( 4 x. M ) )
144 141 143 eqtrd 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( 4 x. ( 1 x. -u M ) ) = -u ( 4 x. M ) )
145 139 144 oveq12d 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( ( -u X ^ 2 ) - ( 4 x. ( 1 x. -u M ) ) ) = ( ( X ^ 2 ) - -u ( 4 x. M ) ) )
146 63 adantr 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( X ^ 2 ) e. CC )
147 65 adantr 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( 4 x. M ) e. CC )
148 146 147 subnegd 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( ( X ^ 2 ) - -u ( 4 x. M ) ) = ( ( X ^ 2 ) + ( 4 x. M ) ) )
149 145 148 eqtr2d 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( ( X ^ 2 ) + ( 4 x. M ) ) = ( ( -u X ^ 2 ) - ( 4 x. ( 1 x. -u M ) ) ) )
150 131 133 135 137 107 149 quad 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( ( ( 1 x. ( u ^ 2 ) ) + ( ( -u X x. u ) + -u M ) ) = 0 <-> ( u = ( ( -u -u X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / ( 2 x. 1 ) ) \/ u = ( ( -u -u X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / ( 2 x. 1 ) ) ) ) )
151 117 mullidd 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( 1 x. ( u ^ 2 ) ) = ( u ^ 2 ) )
152 112 107 mulneg1d 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( -u X x. u ) = -u ( X x. u ) )
153 152 oveq1d 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( ( -u X x. u ) + -u M ) = ( -u ( X x. u ) + -u M ) )
154 118 108 negdid 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> -u ( ( X x. u ) + M ) = ( -u ( X x. u ) + -u M ) )
155 153 154 eqtr4d 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( ( -u X x. u ) + -u M ) = -u ( ( X x. u ) + M ) )
156 151 155 oveq12d 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( ( 1 x. ( u ^ 2 ) ) + ( ( -u X x. u ) + -u M ) ) = ( ( u ^ 2 ) + -u ( ( X x. u ) + M ) ) )
157 117 119 negsubd 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( ( u ^ 2 ) + -u ( ( X x. u ) + M ) ) = ( ( u ^ 2 ) - ( ( X x. u ) + M ) ) )
158 156 157 eqtrd 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( ( 1 x. ( u ^ 2 ) ) + ( ( -u X x. u ) + -u M ) ) = ( ( u ^ 2 ) - ( ( X x. u ) + M ) ) )
159 158 eqeq1d 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( ( ( 1 x. ( u ^ 2 ) ) + ( ( -u X x. u ) + -u M ) ) = 0 <-> ( ( u ^ 2 ) - ( ( X x. u ) + M ) ) = 0 ) )
160 112 negnegd 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> -u -u X = X )
161 160 oveq1d 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( -u -u X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) = ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) )
162 2t1e2 
 |-  ( 2 x. 1 ) = 2
163 162 a1i 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( 2 x. 1 ) = 2 )
164 161 163 oveq12d 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( ( -u -u X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / ( 2 x. 1 ) ) = ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) )
165 164 eqeq2d 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( u = ( ( -u -u X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / ( 2 x. 1 ) ) <-> u = ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) ) )
166 160 oveq1d 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( -u -u X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) = ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) )
167 166 163 oveq12d 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( ( -u -u X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / ( 2 x. 1 ) ) = ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) )
168 167 eqeq2d 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( u = ( ( -u -u X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / ( 2 x. 1 ) ) <-> u = ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) ) )
169 165 168 orbi12d 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( ( u = ( ( -u -u X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / ( 2 x. 1 ) ) \/ u = ( ( -u -u X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / ( 2 x. 1 ) ) ) <-> ( u = ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) \/ u = ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) ) ) )
170 150 159 169 3bitr3d 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( ( ( u ^ 2 ) - ( ( X x. u ) + M ) ) = 0 <-> ( u = ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) \/ u = ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) ) ) )
171 116 130 170 3bitr2d 
 |-  ( ( ph /\ u e. ( CC \ { 0 } ) ) -> ( X = ( u - ( M / u ) ) <-> ( u = ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) \/ u = ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) ) ) )
172 171 rexbidva 
 |-  ( ph -> ( E. u e. ( CC \ { 0 } ) X = ( u - ( M / u ) ) <-> E. u e. ( CC \ { 0 } ) ( u = ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) \/ u = ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) ) ) )
173 r19.43 
 |-  ( E. u e. ( CC \ { 0 } ) ( u = ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) \/ u = ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) ) <-> ( E. u e. ( CC \ { 0 } ) u = ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) \/ E. u e. ( CC \ { 0 } ) u = ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) ) )
174 172 173 bitrdi 
 |-  ( ph -> ( E. u e. ( CC \ { 0 } ) X = ( u - ( M / u ) ) <-> ( E. u e. ( CC \ { 0 } ) u = ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) \/ E. u e. ( CC \ { 0 } ) u = ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) ) ) )
175 risset 
 |-  ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) e. ( CC \ { 0 } ) <-> E. u e. ( CC \ { 0 } ) u = ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) )
176 3 96 addcld 
 |-  ( ph -> ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) e. CC )
177 176 halfcld 
 |-  ( ph -> ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) e. CC )
178 eldifsn 
 |-  ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) e. ( CC \ { 0 } ) <-> ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) e. CC /\ ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) =/= 0 ) )
179 178 baib 
 |-  ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) e. CC -> ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) e. ( CC \ { 0 } ) <-> ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) =/= 0 ) )
180 177 179 syl 
 |-  ( ph -> ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) e. ( CC \ { 0 } ) <-> ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) =/= 0 ) )
181 175 180 bitr3id 
 |-  ( ph -> ( E. u e. ( CC \ { 0 } ) u = ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) <-> ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) =/= 0 ) )
182 risset 
 |-  ( ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) e. ( CC \ { 0 } ) <-> E. u e. ( CC \ { 0 } ) u = ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) )
183 3 96 subcld 
 |-  ( ph -> ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) e. CC )
184 183 halfcld 
 |-  ( ph -> ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) e. CC )
185 eldifsn 
 |-  ( ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) e. ( CC \ { 0 } ) <-> ( ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) e. CC /\ ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) =/= 0 ) )
186 185 baib 
 |-  ( ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) e. CC -> ( ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) e. ( CC \ { 0 } ) <-> ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) =/= 0 ) )
187 184 186 syl 
 |-  ( ph -> ( ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) e. ( CC \ { 0 } ) <-> ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) =/= 0 ) )
188 182 187 bitr3id 
 |-  ( ph -> ( E. u e. ( CC \ { 0 } ) u = ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) <-> ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) =/= 0 ) )
189 181 188 orbi12d 
 |-  ( ph -> ( ( E. u e. ( CC \ { 0 } ) u = ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) \/ E. u e. ( CC \ { 0 } ) u = ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) ) <-> ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) =/= 0 \/ ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) =/= 0 ) ) )
190 neorian 
 |-  ( ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) =/= 0 \/ ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) =/= 0 ) <-> -. ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) = 0 /\ ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) = 0 ) )
191 189 190 bitrdi 
 |-  ( ph -> ( ( E. u e. ( CC \ { 0 } ) u = ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) \/ E. u e. ( CC \ { 0 } ) u = ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) ) <-> -. ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) = 0 /\ ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) = 0 ) ) )
192 174 191 bitrd 
 |-  ( ph -> ( E. u e. ( CC \ { 0 } ) X = ( u - ( M / u ) ) <-> -. ( ( ( X + ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) = 0 /\ ( ( X - ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) ) / 2 ) = 0 ) ) )
193 105 192 sylibrd 
 |-  ( ph -> ( -. ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) -> E. u e. ( CC \ { 0 } ) X = ( u - ( M / u ) ) ) )
194 193 imp 
 |-  ( ( ph /\ -. ( X = 0 /\ ( sqrt ` ( ( X ^ 2 ) + ( 4 x. M ) ) ) = 0 ) ) -> E. u e. ( CC \ { 0 } ) X = ( u - ( M / u ) ) )
195 90 194 syldan 
 |-  ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) -> E. u e. ( CC \ { 0 } ) X = ( u - ( M / u ) ) )
196 1 ad2antrr 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( u e. ( CC \ { 0 } ) /\ X = ( u - ( M / u ) ) ) ) -> P e. CC )
197 2 ad2antrr 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( u e. ( CC \ { 0 } ) /\ X = ( u - ( M / u ) ) ) ) -> Q e. CC )
198 3 ad2antrr 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( u e. ( CC \ { 0 } ) /\ X = ( u - ( M / u ) ) ) ) -> X e. CC )
199 4 ad2antrr 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( u e. ( CC \ { 0 } ) /\ X = ( u - ( M / u ) ) ) ) -> T e. CC )
200 5 ad2antrr 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( u e. ( CC \ { 0 } ) /\ X = ( u - ( M / u ) ) ) ) -> ( T ^ 3 ) = ( G - N ) )
201 6 ad2antrr 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( u e. ( CC \ { 0 } ) /\ X = ( u - ( M / u ) ) ) ) -> G e. CC )
202 7 ad2antrr 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( u e. ( CC \ { 0 } ) /\ X = ( u - ( M / u ) ) ) ) -> ( G ^ 2 ) = ( ( N ^ 2 ) + ( M ^ 3 ) ) )
203 8 ad2antrr 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( u e. ( CC \ { 0 } ) /\ X = ( u - ( M / u ) ) ) ) -> M = ( P / 3 ) )
204 9 ad2antrr 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( u e. ( CC \ { 0 } ) /\ X = ( u - ( M / u ) ) ) ) -> N = ( Q / 2 ) )
205 10 ad2antrr 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( u e. ( CC \ { 0 } ) /\ X = ( u - ( M / u ) ) ) ) -> T =/= 0 )
206 106 ad2antrl 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( u e. ( CC \ { 0 } ) /\ X = ( u - ( M / u ) ) ) ) -> u e. CC )
207 109 ad2antrl 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( u e. ( CC \ { 0 } ) /\ X = ( u - ( M / u ) ) ) ) -> u =/= 0 )
208 simprr 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( u e. ( CC \ { 0 } ) /\ X = ( u - ( M / u ) ) ) ) -> X = ( u - ( M / u ) ) )
209 simplr 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( u e. ( CC \ { 0 } ) /\ X = ( u - ( M / u ) ) ) ) -> ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 )
210 196 197 198 199 200 201 202 203 204 205 206 207 208 209 dcubic2 
 |-  ( ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) /\ ( u e. ( CC \ { 0 } ) /\ X = ( u - ( M / u ) ) ) ) -> E. r e. CC ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) )
211 195 210 rexlimddv 
 |-  ( ( ph /\ ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) -> E. r e. CC ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) )
212 211 ex 
 |-  ( ph -> ( ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 -> E. r e. CC ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) ) )
213 1 ad2antrr 
 |-  ( ( ( ph /\ r e. CC ) /\ ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) ) -> P e. CC )
214 2 ad2antrr 
 |-  ( ( ( ph /\ r e. CC ) /\ ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) ) -> Q e. CC )
215 3 ad2antrr 
 |-  ( ( ( ph /\ r e. CC ) /\ ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) ) -> X e. CC )
216 simplr 
 |-  ( ( ( ph /\ r e. CC ) /\ ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) ) -> r e. CC )
217 4 ad2antrr 
 |-  ( ( ( ph /\ r e. CC ) /\ ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) ) -> T e. CC )
218 216 217 mulcld 
 |-  ( ( ( ph /\ r e. CC ) /\ ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) ) -> ( r x. T ) e. CC )
219 3nn0 
 |-  3 e. NN0
220 219 a1i 
 |-  ( ( ( ph /\ r e. CC ) /\ ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) ) -> 3 e. NN0 )
221 216 217 220 mulexpd 
 |-  ( ( ( ph /\ r e. CC ) /\ ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) ) -> ( ( r x. T ) ^ 3 ) = ( ( r ^ 3 ) x. ( T ^ 3 ) ) )
222 simprl 
 |-  ( ( ( ph /\ r e. CC ) /\ ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) ) -> ( r ^ 3 ) = 1 )
223 222 oveq1d 
 |-  ( ( ( ph /\ r e. CC ) /\ ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) ) -> ( ( r ^ 3 ) x. ( T ^ 3 ) ) = ( 1 x. ( T ^ 3 ) ) )
224 expcl 
 |-  ( ( T e. CC /\ 3 e. NN0 ) -> ( T ^ 3 ) e. CC )
225 4 219 224 sylancl 
 |-  ( ph -> ( T ^ 3 ) e. CC )
226 225 mullidd 
 |-  ( ph -> ( 1 x. ( T ^ 3 ) ) = ( T ^ 3 ) )
227 226 5 eqtrd 
 |-  ( ph -> ( 1 x. ( T ^ 3 ) ) = ( G - N ) )
228 227 ad2antrr 
 |-  ( ( ( ph /\ r e. CC ) /\ ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) ) -> ( 1 x. ( T ^ 3 ) ) = ( G - N ) )
229 221 223 228 3eqtrd 
 |-  ( ( ( ph /\ r e. CC ) /\ ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) ) -> ( ( r x. T ) ^ 3 ) = ( G - N ) )
230 6 ad2antrr 
 |-  ( ( ( ph /\ r e. CC ) /\ ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) ) -> G e. CC )
231 7 ad2antrr 
 |-  ( ( ( ph /\ r e. CC ) /\ ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) ) -> ( G ^ 2 ) = ( ( N ^ 2 ) + ( M ^ 3 ) ) )
232 8 ad2antrr 
 |-  ( ( ( ph /\ r e. CC ) /\ ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) ) -> M = ( P / 3 ) )
233 9 ad2antrr 
 |-  ( ( ( ph /\ r e. CC ) /\ ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) ) -> N = ( Q / 2 ) )
234 132 a1i 
 |-  ( ( ( ph /\ r e. CC ) /\ ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) ) -> 1 =/= 0 )
235 222 234 eqnetrd 
 |-  ( ( ( ph /\ r e. CC ) /\ ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) ) -> ( r ^ 3 ) =/= 0 )
236 oveq1 
 |-  ( r = 0 -> ( r ^ 3 ) = ( 0 ^ 3 ) )
237 236 31 eqtrdi 
 |-  ( r = 0 -> ( r ^ 3 ) = 0 )
238 237 necon3i 
 |-  ( ( r ^ 3 ) =/= 0 -> r =/= 0 )
239 235 238 syl 
 |-  ( ( ( ph /\ r e. CC ) /\ ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) ) -> r =/= 0 )
240 10 ad2antrr 
 |-  ( ( ( ph /\ r e. CC ) /\ ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) ) -> T =/= 0 )
241 216 217 239 240 mulne0d 
 |-  ( ( ( ph /\ r e. CC ) /\ ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) ) -> ( r x. T ) =/= 0 )
242 simprr 
 |-  ( ( ( ph /\ r e. CC ) /\ ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) ) -> X = ( ( r x. T ) - ( M / ( r x. T ) ) ) )
243 213 214 215 218 229 230 231 232 233 241 242 dcubic1 
 |-  ( ( ( ph /\ r e. CC ) /\ ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) ) -> ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 )
244 243 rexlimdva2 
 |-  ( ph -> ( E. r e. CC ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) -> ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 ) )
245 212 244 impbid 
 |-  ( ph -> ( ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 <-> E. r e. CC ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) ) )