MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dcubic Structured version   Unicode version

Theorem dcubic 23714
Description: Solutions to the depressed cubic, a special case of cubic 23717. (The definitions of  M ,  N ,  G ,  T here differ from mcubic 23715 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.)
Hypotheses
Ref Expression
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
Ref Expression
dcubic  |-  ( ph  ->  ( ( ( X ^ 3 )  +  ( ( P  x.  X )  +  Q
) )  =  0  <->  E. r  e.  CC  ( ( r ^
3 )  =  1  /\  X  =  ( ( r  x.  T
)  -  ( M  /  ( r  x.  T ) ) ) ) ) )
Distinct variable groups:    M, r    P, r    ph, r    Q, r    T, r    X, r
Allowed substitution hints:    G( r)    N( r)

Proof of Theorem dcubic
Dummy variable  u is distinct from all other variables.
StepHypRef Expression
1 dcubic.0 . . . . . . 7  |-  ( ph  ->  T  =/=  0 )
21adantr 466 . . . . . 6  |-  ( (
ph  /\  ( ( X ^ 3 )  +  ( ( P  x.  X )  +  Q
) )  =  0 )  ->  T  =/=  0 )
3 dcubic.t . . . . . . . . 9  |-  ( ph  ->  T  e.  CC )
43adantr 466 . . . . . . . 8  |-  ( (
ph  /\  ( ( X ^ 3 )  +  ( ( P  x.  X )  +  Q
) )  =  0 )  ->  T  e.  CC )
5 3z 10921 . . . . . . . . . 10  |-  3  e.  ZZ
6 expne0i 12254 . . . . . . . . . 10  |-  ( ( T  e.  CC  /\  T  =/=  0  /\  3  e.  ZZ )  ->  ( T ^ 3 )  =/=  0 )
75, 6mp3an3 1349 . . . . . . . . 9  |-  ( ( T  e.  CC  /\  T  =/=  0 )  -> 
( T ^ 3 )  =/=  0 )
87ex 435 . . . . . . . 8  |-  ( T  e.  CC  ->  ( T  =/=  0  ->  ( T ^ 3 )  =/=  0 ) )
94, 8syl 17 . . . . . . 7  |-  ( (
ph  /\  ( ( X ^ 3 )  +  ( ( P  x.  X )  +  Q
) )  =  0 )  ->  ( T  =/=  0  ->  ( T ^ 3 )  =/=  0 ) )
10 dcubic.3 . . . . . . . . . . 11  |-  ( ph  ->  ( T ^ 3 )  =  ( G  -  N ) )
1110ad2antrr 730 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( T ^ 3 )  =  ( G  -  N
) )
12 dcubic.g . . . . . . . . . . . . . 14  |-  ( ph  ->  G  e.  CC )
1312ad2antrr 730 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  G  e.  CC )
14 dcubic.2 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( G ^ 2 )  =  ( ( N ^ 2 )  +  ( M ^
3 ) ) )
1514ad2antrr 730 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( G ^ 2 )  =  ( ( N ^
2 )  +  ( M ^ 3 ) ) )
16 dcubic.n . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  N  =  ( Q  /  2 ) )
1716ad2antrr 730 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  N  =  ( Q  /  2
) )
18 simprl 762 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  X  = 
0 )
1918oveq2d 6265 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( P  x.  X )  =  ( P  x.  0 ) )
20 dcubic.c . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  P  e.  CC )
2120ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  P  e.  CC )
2221mul01d 9783 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( P  x.  0 )  =  0 )
2319, 22eqtrd 2462 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( P  x.  X )  =  0 )
2423oveq1d 6264 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( ( P  x.  X )  +  Q )  =  ( 0  +  Q ) )
2518oveq1d 6264 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( X ^ 3 )  =  ( 0 ^ 3 ) )
26 3nn 10719 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  3  e.  NN
27 0exp 12257 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 3  e.  NN  ->  (
0 ^ 3 )  =  0 )
2826, 27ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 0 ^ 3 )  =  0
2925, 28syl6eq 2478 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( X ^ 3 )  =  0 )
3029oveq1d 6264 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( ( X ^ 3 )  +  ( ( P  x.  X )  +  Q
) )  =  ( 0  +  ( ( P  x.  X )  +  Q ) ) )
31 simplr 760 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( ( X ^ 3 )  +  ( ( P  x.  X )  +  Q
) )  =  0 )
32 0cnd 9587 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  0  e.  CC )
3323, 32eqeltrd 2506 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( P  x.  X )  e.  CC )
34 dcubic.d . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  Q  e.  CC )
3534ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  Q  e.  CC )
3633, 35addcld 9613 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( ( P  x.  X )  +  Q )  e.  CC )
3736addid2d 9785 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( 0  +  ( ( P  x.  X )  +  Q ) )  =  ( ( P  x.  X )  +  Q
) )
3830, 31, 373eqtr3rd 2471 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( ( P  x.  X )  +  Q )  =  0 )
3935addid2d 9785 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( 0  +  Q )  =  Q )
4024, 38, 393eqtr3rd 2471 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  Q  = 
0 )
4140oveq1d 6264 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( Q  /  2 )  =  ( 0  /  2
) )
42 2cn 10631 . . . . . . . . . . . . . . . . . . . 20  |-  2  e.  CC
43 2ne0 10653 . . . . . . . . . . . . . . . . . . . 20  |-  2  =/=  0
4442, 43div0i 10292 . . . . . . . . . . . . . . . . . . 19  |-  ( 0  /  2 )  =  0
4541, 44syl6eq 2478 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( Q  /  2 )  =  0 )
4617, 45eqtrd 2462 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  N  = 
0 )
4746sq0id 12318 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( N ^ 2 )  =  0 )
48 dcubic.m . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  M  =  ( P  /  3 ) )
49 3cn 10635 . . . . . . . . . . . . . . . . . . . . . . 23  |-  3  e.  CC
5049a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  3  e.  CC )
51 3ne0 10655 . . . . . . . . . . . . . . . . . . . . . . 23  |-  3  =/=  0
5251a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  3  =/=  0 )
5320, 50, 52divcld 10334 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( P  /  3
)  e.  CC )
5448, 53eqeltrd 2506 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  M  e.  CC )
5554ad2antrr 730 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  M  e.  CC )
56 4cn 10638 . . . . . . . . . . . . . . . . . . . 20  |-  4  e.  CC
5756a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  4  e.  CC )
58 4ne0 10657 . . . . . . . . . . . . . . . . . . . 20  |-  4  =/=  0
5958a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  4  =/=  0 )
6018sq0id 12318 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( X ^ 2 )  =  0 )
6160oveq1d 6264 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( ( X ^ 2 )  +  ( 4  x.  M
) )  =  ( 0  +  ( 4  x.  M ) ) )
62 dcubic.x . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  X  e.  CC )
6362sqcld 12364 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( X ^ 2 )  e.  CC )
64 mulcl 9574 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 4  e.  CC  /\  M  e.  CC )  ->  ( 4  x.  M
)  e.  CC )
6556, 54, 64sylancr 667 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( 4  x.  M
)  e.  CC )
6663, 65addcld 9613 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( X ^
2 )  +  ( 4  x.  M ) )  e.  CC )
6766ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( ( X ^ 2 )  +  ( 4  x.  M
) )  e.  CC )
68 simprr 764 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( sqr `  ( ( X ^
2 )  +  ( 4  x.  M ) ) )  =  0 )
6967, 68sqr00d 13446 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( ( X ^ 2 )  +  ( 4  x.  M
) )  =  0 )
7065ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( 4  x.  M )  e.  CC )
7170addid2d 9785 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( 0  +  ( 4  x.  M ) )  =  ( 4  x.  M
) )
7261, 69, 713eqtr3rd 2471 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( 4  x.  M )  =  0 )
7356mul01i 9774 . . . . . . . . . . . . . . . . . . . 20  |-  ( 4  x.  0 )  =  0
7472, 73syl6eqr 2480 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( 4  x.  M )  =  ( 4  x.  0 ) )
7555, 32, 57, 59, 74mulcanad 10198 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  M  = 
0 )
7675oveq1d 6264 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( M ^ 3 )  =  ( 0 ^ 3 ) )
7776, 28syl6eq 2478 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( M ^ 3 )  =  0 )
7847, 77oveq12d 6267 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( ( N ^ 2 )  +  ( M ^ 3 ) )  =  ( 0  +  0 ) )
79 00id 9759 . . . . . . . . . . . . . . 15  |-  ( 0  +  0 )  =  0
8078, 79syl6eq 2478 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( ( N ^ 2 )  +  ( M ^ 3 ) )  =  0 )
8115, 80eqtrd 2462 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( G ^ 2 )  =  0 )
8213, 81sqeq0d 12365 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  G  = 
0 )
8382, 46oveq12d 6267 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( G  -  N )  =  ( 0  -  0 ) )
84 0m0e0 10670 . . . . . . . . . . 11  |-  ( 0  -  0 )  =  0
8583, 84syl6eq 2478 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( G  -  N )  =  0 )
8611, 85eqtrd 2462 . . . . . . . . 9  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( X  =  0  /\  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  ( T ^ 3 )  =  0 )
8786ex 435 . . . . . . . 8  |-  ( (
ph  /\  ( ( X ^ 3 )  +  ( ( P  x.  X )  +  Q
) )  =  0 )  ->  ( ( X  =  0  /\  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 )  -> 
( T ^ 3 )  =  0 ) )
8887necon3ad 2614 . . . . . . 7  |-  ( (
ph  /\  ( ( X ^ 3 )  +  ( ( P  x.  X )  +  Q
) )  =  0 )  ->  ( ( T ^ 3 )  =/=  0  ->  -.  ( X  =  0  /\  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) ) )
899, 88syld 45 . . . . . 6  |-  ( (
ph  /\  ( ( X ^ 3 )  +  ( ( P  x.  X )  +  Q
) )  =  0 )  ->  ( T  =/=  0  ->  -.  ( X  =  0  /\  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) ) )
902, 89mpd 15 . . . . 5  |-  ( (
ph  /\  ( ( X ^ 3 )  +  ( ( P  x.  X )  +  Q
) )  =  0 )  ->  -.  ( X  =  0  /\  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )
91 oveq12 6258 . . . . . . . . . . 11  |-  ( ( ( ( X  +  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 )  =  0  /\  (
( X  -  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M
) ) ) )  /  2 )  =  0 )  ->  (
( ( X  +  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 )  +  ( ( X  -  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2
) )  =  ( 0  +  0 ) )
9291, 79syl6eq 2478 . . . . . . . . . 10  |-  ( ( ( ( X  +  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 )  =  0  /\  (
( X  -  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M
) ) ) )  /  2 )  =  0 )  ->  (
( ( X  +  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 )  +  ( ( X  -  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2
) )  =  0 )
93 oveq12 6258 . . . . . . . . . . 11  |-  ( ( ( ( X  +  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 )  =  0  /\  (
( X  -  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M
) ) ) )  /  2 )  =  0 )  ->  (
( ( X  +  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 )  -  ( ( X  -  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2
) )  =  ( 0  -  0 ) )
9493, 84syl6eq 2478 . . . . . . . . . 10  |-  ( ( ( ( X  +  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 )  =  0  /\  (
( X  -  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M
) ) ) )  /  2 )  =  0 )  ->  (
( ( X  +  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 )  -  ( ( X  -  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2
) )  =  0 )
9592, 94jca 534 . . . . . . . . 9  |-  ( ( ( ( X  +  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 )  =  0  /\  (
( X  -  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M
) ) ) )  /  2 )  =  0 )  ->  (
( ( ( X  +  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2
)  +  ( ( X  -  ( sqr `  ( ( X ^
2 )  +  ( 4  x.  M ) ) ) )  / 
2 ) )  =  0  /\  ( ( ( X  +  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 )  -  ( ( X  -  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2
) )  =  0 ) )
9666sqrtcld 13442 . . . . . . . . . . . . 13  |-  ( ph  ->  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) )  e.  CC )
97 halfaddsub 10797 . . . . . . . . . . . . 13  |-  ( ( X  e.  CC  /\  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) )  e.  CC )  -> 
( ( ( ( X  +  ( sqr `  ( ( X ^
2 )  +  ( 4  x.  M ) ) ) )  / 
2 )  +  ( ( X  -  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M
) ) ) )  /  2 ) )  =  X  /\  (
( ( X  +  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 )  -  ( ( X  -  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2
) )  =  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) ) )
9862, 96, 97syl2anc 665 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( ( X  +  ( sqr `  ( ( X ^
2 )  +  ( 4  x.  M ) ) ) )  / 
2 )  +  ( ( X  -  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M
) ) ) )  /  2 ) )  =  X  /\  (
( ( X  +  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 )  -  ( ( X  -  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2
) )  =  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) ) )
9998simpld 460 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( X  +  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2
)  +  ( ( X  -  ( sqr `  ( ( X ^
2 )  +  ( 4  x.  M ) ) ) )  / 
2 ) )  =  X )
10099eqeq1d 2430 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( X  +  ( sqr `  ( ( X ^
2 )  +  ( 4  x.  M ) ) ) )  / 
2 )  +  ( ( X  -  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M
) ) ) )  /  2 ) )  =  0  <->  X  = 
0 ) )
10198simprd 464 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( X  +  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2
)  -  ( ( X  -  ( sqr `  ( ( X ^
2 )  +  ( 4  x.  M ) ) ) )  / 
2 ) )  =  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )
102101eqeq1d 2430 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( X  +  ( sqr `  ( ( X ^
2 )  +  ( 4  x.  M ) ) ) )  / 
2 )  -  (
( X  -  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M
) ) ) )  /  2 ) )  =  0  <->  ( sqr `  ( ( X ^
2 )  +  ( 4  x.  M ) ) )  =  0 ) )
103100, 102anbi12d 715 . . . . . . . . 9  |-  ( ph  ->  ( ( ( ( ( X  +  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 )  +  ( ( X  -  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2
) )  =  0  /\  ( ( ( X  +  ( sqr `  ( ( X ^
2 )  +  ( 4  x.  M ) ) ) )  / 
2 )  -  (
( X  -  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M
) ) ) )  /  2 ) )  =  0 )  <->  ( X  =  0  /\  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M
) ) )  =  0 ) ) )
10495, 103syl5ib 222 . . . . . . . 8  |-  ( ph  ->  ( ( ( ( X  +  ( sqr `  ( ( X ^
2 )  +  ( 4  x.  M ) ) ) )  / 
2 )  =  0  /\  ( ( X  -  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2
)  =  0 )  ->  ( X  =  0  /\  ( sqr `  ( ( X ^
2 )  +  ( 4  x.  M ) ) )  =  0 ) ) )
105104con3d 138 . . . . . . 7  |-  ( ph  ->  ( -.  ( X  =  0  /\  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M
) ) )  =  0 )  ->  -.  ( ( ( X  +  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2
)  =  0  /\  ( ( X  -  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 )  =  0 ) ) )
106 eldifi 3530 . . . . . . . . . . . . . 14  |-  ( u  e.  ( CC  \  { 0 } )  ->  u  e.  CC )
107106adantl 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  ->  u  e.  CC )
10854adantr 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  ->  M  e.  CC )
109 eldifsni 4069 . . . . . . . . . . . . . . 15  |-  ( u  e.  ( CC  \  { 0 } )  ->  u  =/=  0
)
110109adantl 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  ->  u  =/=  0 )
111108, 107, 110divcld 10334 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( M  /  u
)  e.  CC )
11262adantr 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  ->  X  e.  CC )
113107, 111, 112subaddd 9955 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( ( u  -  ( M  /  u
) )  =  X  <-> 
( ( M  /  u )  +  X
)  =  u ) )
114 eqcom 2435 . . . . . . . . . . . 12  |-  ( X  =  ( u  -  ( M  /  u
) )  <->  ( u  -  ( M  /  u ) )  =  X )
115 eqcom 2435 . . . . . . . . . . . 12  |-  ( u  =  ( ( M  /  u )  +  X )  <->  ( ( M  /  u )  +  X )  =  u )
116113, 114, 1153bitr4g 291 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( X  =  ( u  -  ( M  /  u ) )  <-> 
u  =  ( ( M  /  u )  +  X ) ) )
117107sqcld 12364 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( u ^ 2 )  e.  CC )
118112, 107mulcld 9614 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( X  x.  u
)  e.  CC )
119118, 108addcld 9613 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( ( X  x.  u )  +  M
)  e.  CC )
120117, 119subeq0ad 9947 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( ( ( u ^ 2 )  -  ( ( X  x.  u )  +  M
) )  =  0  <-> 
( u ^ 2 )  =  ( ( X  x.  u )  +  M ) ) )
121107sqvald 12363 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( u ^ 2 )  =  ( u  x.  u ) )
122111, 112, 107adddird 9619 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( ( ( M  /  u )  +  X )  x.  u
)  =  ( ( ( M  /  u
)  x.  u )  +  ( X  x.  u ) ) )
123108, 107, 110divcan1d 10335 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( ( M  /  u )  x.  u
)  =  M )
124123oveq1d 6264 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( ( ( M  /  u )  x.  u )  +  ( X  x.  u ) )  =  ( M  +  ( X  x.  u ) ) )
125108, 118addcomd 9786 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( M  +  ( X  x.  u ) )  =  ( ( X  x.  u )  +  M ) )
126122, 124, 1253eqtrrd 2467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( ( X  x.  u )  +  M
)  =  ( ( ( M  /  u
)  +  X )  x.  u ) )
127121, 126eqeq12d 2443 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( ( u ^
2 )  =  ( ( X  x.  u
)  +  M )  <-> 
( u  x.  u
)  =  ( ( ( M  /  u
)  +  X )  x.  u ) ) )
128111, 112addcld 9613 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( ( M  /  u )  +  X
)  e.  CC )
129107, 128, 107, 110mulcan2d 10197 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( ( u  x.  u )  =  ( ( ( M  /  u )  +  X
)  x.  u )  <-> 
u  =  ( ( M  /  u )  +  X ) ) )
130120, 127, 1293bitrd 282 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( ( ( u ^ 2 )  -  ( ( X  x.  u )  +  M
) )  =  0  <-> 
u  =  ( ( M  /  u )  +  X ) ) )
131 1cnd 9610 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
1  e.  CC )
132 ax-1ne0 9559 . . . . . . . . . . . . . 14  |-  1  =/=  0
133132a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
1  =/=  0 )
13462negcld 9924 . . . . . . . . . . . . . 14  |-  ( ph  -> 
-u X  e.  CC )
135134adantr 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  ->  -u X  e.  CC )
13654negcld 9924 . . . . . . . . . . . . . 14  |-  ( ph  -> 
-u M  e.  CC )
137136adantr 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  ->  -u M  e.  CC )
138 sqneg 12285 . . . . . . . . . . . . . . . 16  |-  ( X  e.  CC  ->  ( -u X ^ 2 )  =  ( X ^
2 ) )
139112, 138syl 17 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( -u X ^ 2 )  =  ( X ^ 2 ) )
140137mulid2d 9612 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( 1  x.  -u M
)  =  -u M
)
141140oveq2d 6265 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( 4  x.  (
1  x.  -u M
) )  =  ( 4  x.  -u M
) )
142 mulneg2 10007 . . . . . . . . . . . . . . . . 17  |-  ( ( 4  e.  CC  /\  M  e.  CC )  ->  ( 4  x.  -u M
)  =  -u (
4  x.  M ) )
14356, 108, 142sylancr 667 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( 4  x.  -u M
)  =  -u (
4  x.  M ) )
144141, 143eqtrd 2462 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( 4  x.  (
1  x.  -u M
) )  =  -u ( 4  x.  M
) )
145139, 144oveq12d 6267 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( ( -u X ^ 2 )  -  ( 4  x.  (
1  x.  -u M
) ) )  =  ( ( X ^
2 )  -  -u (
4  x.  M ) ) )
14663adantr 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( X ^ 2 )  e.  CC )
14765adantr 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( 4  x.  M
)  e.  CC )
148146, 147subnegd 9944 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( ( X ^
2 )  -  -u (
4  x.  M ) )  =  ( ( X ^ 2 )  +  ( 4  x.  M ) ) )
149145, 148eqtr2d 2463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( ( X ^
2 )  +  ( 4  x.  M ) )  =  ( (
-u X ^ 2 )  -  ( 4  x.  ( 1  x.  -u M ) ) ) )
150131, 133, 135, 137, 107, 149quad 23708 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( ( ( 1  x.  ( u ^
2 ) )  +  ( ( -u X  x.  u )  +  -u M ) )  =  0  <->  ( u  =  ( ( -u -u X  +  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  (
2  x.  1 ) )  \/  u  =  ( ( -u -u X  -  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  (
2  x.  1 ) ) ) ) )
151117mulid2d 9612 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( 1  x.  (
u ^ 2 ) )  =  ( u ^ 2 ) )
152112, 107mulneg1d 10022 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( -u X  x.  u
)  =  -u ( X  x.  u )
)
153152oveq1d 6264 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( ( -u X  x.  u )  +  -u M )  =  (
-u ( X  x.  u )  +  -u M ) )
154118, 108negdid 9950 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  ->  -u ( ( X  x.  u )  +  M
)  =  ( -u ( X  x.  u
)  +  -u M
) )
155153, 154eqtr4d 2465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( ( -u X  x.  u )  +  -u M )  =  -u ( ( X  x.  u )  +  M
) )
156151, 155oveq12d 6267 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( ( 1  x.  ( u ^ 2 ) )  +  ( ( -u X  x.  u )  +  -u M ) )  =  ( ( u ^
2 )  +  -u ( ( X  x.  u )  +  M
) ) )
157117, 119negsubd 9943 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( ( u ^
2 )  +  -u ( ( X  x.  u )  +  M
) )  =  ( ( u ^ 2 )  -  ( ( X  x.  u )  +  M ) ) )
158156, 157eqtrd 2462 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( ( 1  x.  ( u ^ 2 ) )  +  ( ( -u X  x.  u )  +  -u M ) )  =  ( ( u ^
2 )  -  (
( X  x.  u
)  +  M ) ) )
159158eqeq1d 2430 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( ( ( 1  x.  ( u ^
2 ) )  +  ( ( -u X  x.  u )  +  -u M ) )  =  0  <->  ( ( u ^ 2 )  -  ( ( X  x.  u )  +  M
) )  =  0 ) )
160112negnegd 9928 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  ->  -u -u X  =  X
)
161160oveq1d 6264 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( -u -u X  +  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  =  ( X  +  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) ) )
162 2t1e2 10709 . . . . . . . . . . . . . . . 16  |-  ( 2  x.  1 )  =  2
163162a1i 11 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( 2  x.  1 )  =  2 )
164161, 163oveq12d 6267 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( ( -u -u X  +  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  (
2  x.  1 ) )  =  ( ( X  +  ( sqr `  ( ( X ^
2 )  +  ( 4  x.  M ) ) ) )  / 
2 ) )
165164eqeq2d 2438 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( u  =  ( ( -u -u X  +  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  (
2  x.  1 ) )  <->  u  =  (
( X  +  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 ) ) )
166160oveq1d 6264 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( -u -u X  -  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M
) ) ) )  =  ( X  -  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) ) )
167166, 163oveq12d 6267 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( ( -u -u X  -  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  (
2  x.  1 ) )  =  ( ( X  -  ( sqr `  ( ( X ^
2 )  +  ( 4  x.  M ) ) ) )  / 
2 ) )
168167eqeq2d 2438 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( u  =  ( ( -u -u X  -  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  (
2  x.  1 ) )  <->  u  =  (
( X  -  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M
) ) ) )  /  2 ) ) )
169165, 168orbi12d 714 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( ( u  =  ( ( -u -u X  +  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  (
2  x.  1 ) )  \/  u  =  ( ( -u -u X  -  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  (
2  x.  1 ) ) )  <->  ( u  =  ( ( X  +  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2
)  \/  u  =  ( ( X  -  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 ) ) ) )
170150, 159, 1693bitr3d 286 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( ( ( u ^ 2 )  -  ( ( X  x.  u )  +  M
) )  =  0  <-> 
( u  =  ( ( X  +  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 )  \/  u  =  ( ( X  -  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M
) ) ) )  /  2 ) ) ) )
171116, 130, 1703bitr2d 284 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( CC  \  { 0 } ) )  -> 
( X  =  ( u  -  ( M  /  u ) )  <-> 
( u  =  ( ( X  +  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 )  \/  u  =  ( ( X  -  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M
) ) ) )  /  2 ) ) ) )
172171rexbidva 2875 . . . . . . . . 9  |-  ( ph  ->  ( E. u  e.  ( CC  \  {
0 } ) X  =  ( u  -  ( M  /  u
) )  <->  E. u  e.  ( CC  \  {
0 } ) ( u  =  ( ( X  +  ( sqr `  ( ( X ^
2 )  +  ( 4  x.  M ) ) ) )  / 
2 )  \/  u  =  ( ( X  -  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2
) ) ) )
173 r19.43 2923 . . . . . . . . 9  |-  ( E. u  e.  ( CC 
\  { 0 } ) ( u  =  ( ( X  +  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 )  \/  u  =  ( ( X  -  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M
) ) ) )  /  2 ) )  <-> 
( E. u  e.  ( CC  \  {
0 } ) u  =  ( ( X  +  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2
)  \/  E. u  e.  ( CC  \  {
0 } ) u  =  ( ( X  -  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2
) ) )
174172, 173syl6bb 264 . . . . . . . 8  |-  ( ph  ->  ( E. u  e.  ( CC  \  {
0 } ) X  =  ( u  -  ( M  /  u
) )  <->  ( E. u  e.  ( CC  \  { 0 } ) u  =  ( ( X  +  ( sqr `  ( ( X ^
2 )  +  ( 4  x.  M ) ) ) )  / 
2 )  \/  E. u  e.  ( CC  \  { 0 } ) u  =  ( ( X  -  ( sqr `  ( ( X ^
2 )  +  ( 4  x.  M ) ) ) )  / 
2 ) ) ) )
175 risset 2892 . . . . . . . . . . 11  |-  ( ( ( X  +  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 )  e.  ( CC  \  { 0 } )  <->  E. u  e.  ( CC  \  { 0 } ) u  =  ( ( X  +  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 ) )
17662, 96addcld 9613 . . . . . . . . . . . . 13  |-  ( ph  ->  ( X  +  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  e.  CC )
177176halfcld 10808 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( X  +  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 )  e.  CC )
178 eldifsn 4068 . . . . . . . . . . . . 13  |-  ( ( ( X  +  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 )  e.  ( CC  \  { 0 } )  <-> 
( ( ( X  +  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2
)  e.  CC  /\  ( ( X  +  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 )  =/=  0 ) )
179178baib 911 . . . . . . . . . . . 12  |-  ( ( ( X  +  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 )  e.  CC  ->  (
( ( X  +  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 )  e.  ( CC  \  { 0 } )  <-> 
( ( X  +  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 )  =/=  0 ) )
180177, 179syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( X  +  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2
)  e.  ( CC 
\  { 0 } )  <->  ( ( X  +  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2
)  =/=  0 ) )
181175, 180syl5bbr 262 . . . . . . . . . 10  |-  ( ph  ->  ( E. u  e.  ( CC  \  {
0 } ) u  =  ( ( X  +  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2
)  <->  ( ( X  +  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2
)  =/=  0 ) )
182 risset 2892 . . . . . . . . . . 11  |-  ( ( ( X  -  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M
) ) ) )  /  2 )  e.  ( CC  \  {
0 } )  <->  E. u  e.  ( CC  \  {
0 } ) u  =  ( ( X  -  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2
) )
18362, 96subcld 9937 . . . . . . . . . . . . 13  |-  ( ph  ->  ( X  -  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M
) ) ) )  e.  CC )
184183halfcld 10808 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( X  -  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 )  e.  CC )
185 eldifsn 4068 . . . . . . . . . . . . 13  |-  ( ( ( X  -  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M
) ) ) )  /  2 )  e.  ( CC  \  {
0 } )  <->  ( (
( X  -  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M
) ) ) )  /  2 )  e.  CC  /\  ( ( X  -  ( sqr `  ( ( X ^
2 )  +  ( 4  x.  M ) ) ) )  / 
2 )  =/=  0
) )
186185baib 911 . . . . . . . . . . . 12  |-  ( ( ( X  -  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M
) ) ) )  /  2 )  e.  CC  ->  ( (
( X  -  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M
) ) ) )  /  2 )  e.  ( CC  \  {
0 } )  <->  ( ( X  -  ( sqr `  ( ( X ^
2 )  +  ( 4  x.  M ) ) ) )  / 
2 )  =/=  0
) )
187184, 186syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( X  -  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2
)  e.  ( CC 
\  { 0 } )  <->  ( ( X  -  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2
)  =/=  0 ) )
188182, 187syl5bbr 262 . . . . . . . . . 10  |-  ( ph  ->  ( E. u  e.  ( CC  \  {
0 } ) u  =  ( ( X  -  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2
)  <->  ( ( X  -  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2
)  =/=  0 ) )
189181, 188orbi12d 714 . . . . . . . . 9  |-  ( ph  ->  ( ( E. u  e.  ( CC  \  {
0 } ) u  =  ( ( X  +  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2
)  \/  E. u  e.  ( CC  \  {
0 } ) u  =  ( ( X  -  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2
) )  <->  ( (
( X  +  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 )  =/=  0  \/  (
( X  -  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M
) ) ) )  /  2 )  =/=  0 ) ) )
190 neorian 2695 . . . . . . . . 9  |-  ( ( ( ( X  +  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 )  =/=  0  \/  (
( X  -  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M
) ) ) )  /  2 )  =/=  0 )  <->  -.  (
( ( X  +  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 )  =  0  /\  (
( X  -  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M
) ) ) )  /  2 )  =  0 ) )
191189, 190syl6bb 264 . . . . . . . 8  |-  ( ph  ->  ( ( E. u  e.  ( CC  \  {
0 } ) u  =  ( ( X  +  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2
)  \/  E. u  e.  ( CC  \  {
0 } ) u  =  ( ( X  -  ( sqr `  (
( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2
) )  <->  -.  (
( ( X  +  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 )  =  0  /\  (
( X  -  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M
) ) ) )  /  2 )  =  0 ) ) )
192174, 191bitrd 256 . . . . . . 7  |-  ( ph  ->  ( E. u  e.  ( CC  \  {
0 } ) X  =  ( u  -  ( M  /  u
) )  <->  -.  (
( ( X  +  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) ) )  /  2 )  =  0  /\  (
( X  -  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M
) ) ) )  /  2 )  =  0 ) ) )
193105, 192sylibrd 237 . . . . . 6  |-  ( ph  ->  ( -.  ( X  =  0  /\  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M
) ) )  =  0 )  ->  E. u  e.  ( CC  \  {
0 } ) X  =  ( u  -  ( M  /  u
) ) ) )
194193imp 430 . . . . 5  |-  ( (
ph  /\  -.  ( X  =  0  /\  ( sqr `  ( ( X ^ 2 )  +  ( 4  x.  M ) ) )  =  0 ) )  ->  E. u  e.  ( CC  \  { 0 } ) X  =  ( u  -  ( M  /  u ) ) )
19590, 194syldan 472 . . . 4  |-  ( (
ph  /\  ( ( X ^ 3 )  +  ( ( P  x.  X )  +  Q
) )  =  0 )  ->  E. u  e.  ( CC  \  {
0 } ) X  =  ( u  -  ( M  /  u
) ) )
19620ad2antrr 730 . . . . 5  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( u  e.  ( CC  \  { 0 } )  /\  X  =  ( u  -  ( M  /  u ) ) ) )  ->  P  e.  CC )
19734ad2antrr 730 . . . . 5  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( u  e.  ( CC  \  { 0 } )  /\  X  =  ( u  -  ( M  /  u ) ) ) )  ->  Q  e.  CC )
19862ad2antrr 730 . . . . 5  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( u  e.  ( CC  \  { 0 } )  /\  X  =  ( u  -  ( M  /  u ) ) ) )  ->  X  e.  CC )
1993ad2antrr 730 . . . . 5  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( u  e.  ( CC  \  { 0 } )  /\  X  =  ( u  -  ( M  /  u ) ) ) )  ->  T  e.  CC )
20010ad2antrr 730 . . . . 5  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( u  e.  ( CC  \  { 0 } )  /\  X  =  ( u  -  ( M  /  u ) ) ) )  ->  ( T ^ 3 )  =  ( G  -  N
) )
20112ad2antrr 730 . . . . 5  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( u  e.  ( CC  \  { 0 } )  /\  X  =  ( u  -  ( M  /  u ) ) ) )  ->  G  e.  CC )
20214ad2antrr 730 . . . . 5  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( u  e.  ( CC  \  { 0 } )  /\  X  =  ( u  -  ( M  /  u ) ) ) )  ->  ( G ^ 2 )  =  ( ( N ^
2 )  +  ( M ^ 3 ) ) )
20348ad2antrr 730 . . . . 5  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( u  e.  ( CC  \  { 0 } )  /\  X  =  ( u  -  ( M  /  u ) ) ) )  ->  M  =  ( P  / 
3 ) )
20416ad2antrr 730 . . . . 5  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( u  e.  ( CC  \  { 0 } )  /\  X  =  ( u  -  ( M  /  u ) ) ) )  ->  N  =  ( Q  / 
2 ) )
2051ad2antrr 730 . . . . 5  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( u  e.  ( CC  \  { 0 } )  /\  X  =  ( u  -  ( M  /  u ) ) ) )  ->  T  =/=  0 )
206106ad2antrl 732 . . . . 5  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( u  e.  ( CC  \  { 0 } )  /\  X  =  ( u  -  ( M  /  u ) ) ) )  ->  u  e.  CC )
207109ad2antrl 732 . . . . 5  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( u  e.  ( CC  \  { 0 } )  /\  X  =  ( u  -  ( M  /  u ) ) ) )  ->  u  =/=  0 )
208 simprr 764 . . . . 5  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( u  e.  ( CC  \  { 0 } )  /\  X  =  ( u  -  ( M  /  u ) ) ) )  ->  X  =  ( u  -  ( M  /  u
) ) )
209 simplr 760 . . . . 5  |-  ( ( ( ph  /\  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )  /\  ( u  e.  ( CC  \  { 0 } )  /\  X  =  ( u  -  ( M  /  u ) ) ) )  ->  (
( X ^ 3 )  +  ( ( P  x.  X )  +  Q ) )  =  0 )
210196, 197, 198, 199, 200, 201, 202, 203, 204, 205, 206, 207, 208, 209dcubic2 23712 . . . 4  |-  ( ( ( 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 ) ) ) ) )
211195, 210rexlimddv 2860 . . 3  |-  ( (
ph  /\  ( ( X ^ 3 )  +  ( ( P  x.  X )  +  Q
) )  =  0 )  ->  E. r  e.  CC  ( ( r ^ 3 )  =  1  /\  X  =  ( ( r  x.  T )  -  ( M  /  ( r  x.  T ) ) ) ) )
212211ex 435 . 2  |-  ( ph  ->  ( ( ( X ^ 3 )  +  ( ( P  x.  X )  +  Q
) )  =  0  ->  E. r  e.  CC  ( ( r ^
3 )  =  1  /\  X  =  ( ( r  x.  T
)  -  ( M  /  ( r  x.  T ) ) ) ) ) )
21320ad2antrr 730 . . . . 5  |-  ( ( ( ph  /\  r  e.  CC )  /\  (
( r ^ 3 )  =  1  /\  X  =  ( ( r  x.  T )  -  ( M  / 
( r  x.  T
) ) ) ) )  ->  P  e.  CC )
21434ad2antrr 730 . . . . 5  |-  ( ( ( ph  /\  r  e.  CC )  /\  (
( r ^ 3 )  =  1  /\  X  =  ( ( r  x.  T )  -  ( M  / 
( r  x.  T
) ) ) ) )  ->  Q  e.  CC )
21562ad2antrr 730 . . . . 5  |-  ( ( ( ph  /\  r  e.  CC )  /\  (
( r ^ 3 )  =  1  /\  X  =  ( ( r  x.  T )  -  ( M  / 
( r  x.  T
) ) ) ) )  ->  X  e.  CC )
216 simplr 760 . . . . . 6  |-  ( ( ( ph  /\  r  e.  CC )  /\  (
( r ^ 3 )  =  1  /\  X  =  ( ( r  x.  T )  -  ( M  / 
( r  x.  T
) ) ) ) )  ->  r  e.  CC )
2173ad2antrr 730 . . . . . 6  |-  ( ( ( ph  /\  r  e.  CC )  /\  (
( r ^ 3 )  =  1  /\  X  =  ( ( r  x.  T )  -  ( M  / 
( r  x.  T
) ) ) ) )  ->  T  e.  CC )
218216, 217mulcld 9614 . . . . 5  |-  ( ( ( ph  /\  r  e.  CC )  /\  (
( r ^ 3 )  =  1  /\  X  =  ( ( r  x.  T )  -  ( M  / 
( r  x.  T
) ) ) ) )  ->  ( r  x.  T )  e.  CC )
219 3nn0 10838 . . . . . . . 8  |-  3  e.  NN0
220219a1i 11 . . . . . . 7  |-  ( ( ( ph  /\  r  e.  CC )  /\  (
( r ^ 3 )  =  1  /\  X  =  ( ( r  x.  T )  -  ( M  / 
( r  x.  T
) ) ) ) )  ->  3  e.  NN0 )
221216, 217, 220mulexpd 12381 . . . . . 6  |-  ( ( ( 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 762 . . . . . . 7  |-  ( ( ( ph  /\  r  e.  CC )  /\  (
( r ^ 3 )  =  1  /\  X  =  ( ( r  x.  T )  -  ( M  / 
( r  x.  T
) ) ) ) )  ->  ( r ^ 3 )  =  1 )
223222oveq1d 6264 . . . . . 6  |-  ( ( ( 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 12240 . . . . . . . . . 10  |-  ( ( T  e.  CC  /\  3  e.  NN0 )  -> 
( T ^ 3 )  e.  CC )
2253, 219, 224sylancl 666 . . . . . . . . 9  |-  ( ph  ->  ( T ^ 3 )  e.  CC )
226225mulid2d 9612 . . . . . . . 8  |-  ( ph  ->  ( 1  x.  ( T ^ 3 ) )  =  ( T ^
3 ) )
227226, 10eqtrd 2462 . . . . . . 7  |-  ( ph  ->  ( 1  x.  ( T ^ 3 ) )  =  ( G  -  N ) )
228227ad2antrr 730 . . . . . 6  |-  ( ( ( ph  /\  r  e.  CC )  /\  (
( r ^ 3 )  =  1  /\  X  =  ( ( r  x.  T )  -  ( M  / 
( r  x.  T
) ) ) ) )  ->  ( 1  x.  ( T ^
3 ) )  =  ( G  -  N
) )
229221, 223, 2283eqtrd 2466 . . . . 5  |-  ( ( ( ph  /\  r  e.  CC )  /\  (
( r ^ 3 )  =  1  /\  X  =  ( ( r  x.  T )  -  ( M  / 
( r  x.  T
) ) ) ) )  ->  ( (
r  x.  T ) ^ 3 )  =  ( G  -  N
) )
23012ad2antrr 730 . . . . 5  |-  ( ( ( ph  /\  r  e.  CC )  /\  (
( r ^ 3 )  =  1  /\  X  =  ( ( r  x.  T )  -  ( M  / 
( r  x.  T
) ) ) ) )  ->  G  e.  CC )
23114ad2antrr 730 . . . . 5  |-  ( ( ( ph  /\  r  e.  CC )  /\  (
( r ^ 3 )  =  1  /\  X  =  ( ( r  x.  T )  -  ( M  / 
( r  x.  T
) ) ) ) )  ->  ( G ^ 2 )  =  ( ( N ^
2 )  +  ( M ^ 3 ) ) )
23248ad2antrr 730 . . . . 5  |-  ( ( ( ph  /\  r  e.  CC )  /\  (
( r ^ 3 )  =  1  /\  X  =  ( ( r  x.  T )  -  ( M  / 
( r  x.  T
) ) ) ) )  ->  M  =  ( P  /  3
) )
23316ad2antrr 730 . . . . 5  |-  ( ( ( ph  /\  r  e.  CC )  /\  (
( r ^ 3 )  =  1  /\  X  =  ( ( r  x.  T )  -  ( M  / 
( r  x.  T
) ) ) ) )  ->  N  =  ( Q  /  2
) )
234132a1i 11 . . . . . . . 8  |-  ( ( ( ph  /\  r  e.  CC )  /\  (
( r ^ 3 )  =  1  /\  X  =  ( ( r  x.  T )  -  ( M  / 
( r  x.  T
) ) ) ) )  ->  1  =/=  0 )
235222, 234eqnetrd 2668 . . . . . . 7  |-  ( ( ( ph  /\  r  e.  CC )  /\  (
( r ^ 3 )  =  1  /\  X  =  ( ( r  x.  T )  -  ( M  / 
( r  x.  T
) ) ) ) )  ->  ( r ^ 3 )  =/=  0 )
236 oveq1 6256 . . . . . . . . 9  |-  ( r  =  0  ->  (
r ^ 3 )  =  ( 0 ^ 3 ) )
237236, 28syl6eq 2478 . . . . . . . 8  |-  ( r  =  0  ->  (
r ^ 3 )  =  0 )
238237necon3i 2633 . . . . . . 7  |-  ( ( r ^ 3 )  =/=  0  ->  r  =/=  0 )
239235, 238syl 17 . . . . . 6  |-  ( ( ( ph  /\  r  e.  CC )  /\  (
( r ^ 3 )  =  1  /\  X  =  ( ( r  x.  T )  -  ( M  / 
( r  x.  T
) ) ) ) )  ->  r  =/=  0 )
2401ad2antrr 730 . . . . . 6  |-  ( ( ( ph  /\  r  e.  CC )  /\  (
( r ^ 3 )  =  1  /\  X  =  ( ( r  x.  T )  -  ( M  / 
( r  x.  T
) ) ) ) )  ->  T  =/=  0 )
241216, 217, 239, 240mulne0d 10215 . . . . 5  |-  ( ( ( ph  /\  r  e.  CC )  /\  (
( r ^ 3 )  =  1  /\  X  =  ( ( r  x.  T )  -  ( M  / 
( r  x.  T
) ) ) ) )  ->  ( r  x.  T )  =/=  0
)
242 simprr 764 . . . . 5  |-  ( ( ( ph  /\  r  e.  CC )  /\  (
( r ^ 3 )  =  1  /\  X  =  ( ( r  x.  T )  -  ( M  / 
( r  x.  T
) ) ) ) )  ->  X  =  ( ( r  x.  T )  -  ( M  /  ( r  x.  T ) ) ) )
243213, 214, 215, 218, 229, 230, 231, 232, 233, 241, 242dcubic1 23713 . . . 4  |-  ( ( ( ph  /\  r  e.  CC )  /\  (
( r ^ 3 )  =  1  /\  X  =  ( ( r  x.  T )  -  ( M  / 
( r  x.  T
) ) ) ) )  ->  ( ( X ^ 3 )  +  ( ( P  x.  X )  +  Q
) )  =  0 )
244243ex 435 . . 3  |-  ( (
ph  /\  r  e.  CC )  ->  ( ( ( r ^ 3 )  =  1  /\  X  =  ( ( r  x.  T )  -  ( M  / 
( r  x.  T
) ) ) )  ->  ( ( X ^ 3 )  +  ( ( P  x.  X )  +  Q
) )  =  0 ) )
245244rexlimdva 2856 . 2  |-  ( ph  ->  ( E. r  e.  CC  ( ( r ^ 3 )  =  1  /\  X  =  ( ( r  x.  T )  -  ( M  /  ( r  x.  T ) ) ) )  ->  ( ( X ^ 3 )  +  ( ( P  x.  X )  +  Q
) )  =  0 ) )
246212, 245impbid 193 1  |-  ( ph  ->  ( ( ( X ^ 3 )  +  ( ( P  x.  X )  +  Q
) )  =  0  <->  E. r  e.  CC  ( ( r ^
3 )  =  1  /\  X  =  ( ( r  x.  T
)  -  ( M  /  ( r  x.  T ) ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    \/ wo 369    /\ wa 370    = wceq 1437    e. wcel 1872    =/= wne 2599   E.wrex 2715    \ cdif 3376   {csn 3941   ` cfv 5544  (class class class)co 6249   CCcc 9488   0cc0 9490   1c1 9491    + caddc 9493    x. cmul 9495    - cmin 9811   -ucneg 9812    / cdiv 10220   NNcn 10560   2c2 10610   3c3 10611   4c4 10612   NN0cn0 10820   ZZcz 10888   ^cexp 12222   sqrcsqrt 13240
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603  ax-un 6541  ax-cnex 9546  ax-resscn 9547  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-mulcom 9554  ax-addass 9555  ax-mulass 9556  ax-distr 9557  ax-i2m1 9558  ax-1ne0 9559  ax-1rid 9560  ax-rnegex 9561  ax-rrecex 9562  ax-cnre 9563  ax-pre-lttri 9564  ax-pre-lttrn 9565  ax-pre-ltadd 9566  ax-pre-mulgt0 9567  ax-pre-sup 9568
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-nel 2602  df-ral 2719  df-rex 2720  df-reu 2721  df-rmo 2722  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-pss 3395  df-nul 3705  df-if 3855  df-pw 3926  df-sn 3942  df-pr 3944  df-tp 3946  df-op 3948  df-uni 4163  df-iun 4244  df-br 4367  df-opab 4426  df-mpt 4427  df-tr 4462  df-eprel 4707  df-id 4711  df-po 4717  df-so 4718  df-fr 4755  df-we 4757  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-pred 5342  df-ord 5388  df-on 5389  df-lim 5390  df-suc 5391  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-f1 5549  df-fo 5550  df-f1o 5551  df-fv 5552  df-riota 6211  df-ov 6252  df-oprab 6253  df-mpt2 6254  df-om 6651  df-1st 6751  df-2nd 6752  df-wrecs 6983  df-recs 7045  df-rdg 7083  df-er 7318  df-en 7525  df-dom 7526  df-sdom 7527  df-sup 7909  df-inf 7910  df-pnf 9628  df-mnf 9629  df-xr 9630  df-ltxr 9631  df-le 9632  df-sub 9813  df-neg 9814  df-div 10221  df-nn 10561  df-2 10619  df-3 10620  df-4 10621  df-n0 10821  df-z 10889  df-uz 11111  df-rp 11254  df-fz 11736  df-seq 12164  df-exp 12223  df-cj 13106  df-re 13107  df-im 13108  df-sqrt 13242  df-abs 13243  df-dvds 14249
This theorem is referenced by:  mcubic  23715
  Copyright terms: Public domain W3C validator