Metamath Proof Explorer

Theorem dcubic1

Description: Forward direction of dcubic : the claimed formula produces solutions to the cubic equation. (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 )
dcubic1.x 
|- ( ph -> X = ( T - ( M / T ) ) )
Assertion dcubic1 
|- ( ph -> ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 )

Proof

Step Hyp Ref Expression
1 dcubic.c 
 |-  ( ph -> P e. CC )
2 dcubic.d 
 |-  ( ph -> Q e. CC )
3 dcubic.x 
 |-  ( ph -> X e. CC )
4 dcubic.t 
 |-  ( ph -> T e. CC )
5 dcubic.3 
 |-  ( ph -> ( T ^ 3 ) = ( G - N ) )
6 dcubic.g 
 |-  ( ph -> G e. CC )
7 dcubic.2 
 |-  ( ph -> ( G ^ 2 ) = ( ( N ^ 2 ) + ( M ^ 3 ) ) )
8 dcubic.m 
 |-  ( ph -> M = ( P / 3 ) )
9 dcubic.n 
 |-  ( ph -> N = ( Q / 2 ) )
10 dcubic.0 
 |-  ( ph -> T =/= 0 )
11 dcubic1.x 
 |-  ( ph -> X = ( T - ( M / T ) ) )
12 5 oveq1d 
 |-  ( ph -> ( ( T ^ 3 ) ^ 2 ) = ( ( G - N ) ^ 2 ) )
13 2 halfcld 
 |-  ( ph -> ( Q / 2 ) e. CC )
14 9 13 eqeltrd 
 |-  ( ph -> N e. CC )
15 binom2sub 
 |-  ( ( G e. CC /\ N e. CC ) -> ( ( G - N ) ^ 2 ) = ( ( ( G ^ 2 ) - ( 2 x. ( G x. N ) ) ) + ( N ^ 2 ) ) )
16 6 14 15 syl2anc 
 |-  ( ph -> ( ( G - N ) ^ 2 ) = ( ( ( G ^ 2 ) - ( 2 x. ( G x. N ) ) ) + ( N ^ 2 ) ) )
17 2cnd 
 |-  ( ph -> 2 e. CC )
18 17 6 14 mul12d 
 |-  ( ph -> ( 2 x. ( G x. N ) ) = ( G x. ( 2 x. N ) ) )
19 9 oveq2d 
 |-  ( ph -> ( 2 x. N ) = ( 2 x. ( Q / 2 ) ) )
20 2ne0 
 |-  2 =/= 0
21 20 a1i 
 |-  ( ph -> 2 =/= 0 )
22 2 17 21 divcan2d 
 |-  ( ph -> ( 2 x. ( Q / 2 ) ) = Q )
23 19 22 eqtrd 
 |-  ( ph -> ( 2 x. N ) = Q )
24 23 oveq2d 
 |-  ( ph -> ( G x. ( 2 x. N ) ) = ( G x. Q ) )
25 6 2 mulcomd 
 |-  ( ph -> ( G x. Q ) = ( Q x. G ) )
26 18 24 25 3eqtrd 
 |-  ( ph -> ( 2 x. ( G x. N ) ) = ( Q x. G ) )
27 7 26 oveq12d 
 |-  ( ph -> ( ( G ^ 2 ) - ( 2 x. ( G x. N ) ) ) = ( ( ( N ^ 2 ) + ( M ^ 3 ) ) - ( Q x. G ) ) )
28 27 oveq1d 
 |-  ( ph -> ( ( ( G ^ 2 ) - ( 2 x. ( G x. N ) ) ) + ( N ^ 2 ) ) = ( ( ( ( N ^ 2 ) + ( M ^ 3 ) ) - ( Q x. G ) ) + ( N ^ 2 ) ) )
29 12 16 28 3eqtrd 
 |-  ( ph -> ( ( T ^ 3 ) ^ 2 ) = ( ( ( ( N ^ 2 ) + ( M ^ 3 ) ) - ( Q x. G ) ) + ( N ^ 2 ) ) )
30 14 sqcld 
 |-  ( ph -> ( N ^ 2 ) e. CC )
31 3cn 
 |-  3 e. CC
32 31 a1i 
 |-  ( ph -> 3 e. CC )
33 3ne0 
 |-  3 =/= 0
34 33 a1i 
 |-  ( ph -> 3 =/= 0 )
35 1 32 34 divcld 
 |-  ( ph -> ( P / 3 ) e. CC )
36 8 35 eqeltrd 
 |-  ( ph -> M e. CC )
37 3nn0 
 |-  3 e. NN0
38 expcl 
 |-  ( ( M e. CC /\ 3 e. NN0 ) -> ( M ^ 3 ) e. CC )
39 36 37 38 sylancl 
 |-  ( ph -> ( M ^ 3 ) e. CC )
40 30 39 addcld 
 |-  ( ph -> ( ( N ^ 2 ) + ( M ^ 3 ) ) e. CC )
41 2 6 mulcld 
 |-  ( ph -> ( Q x. G ) e. CC )
42 40 30 41 addsubd 
 |-  ( ph -> ( ( ( ( N ^ 2 ) + ( M ^ 3 ) ) + ( N ^ 2 ) ) - ( Q x. G ) ) = ( ( ( ( N ^ 2 ) + ( M ^ 3 ) ) - ( Q x. G ) ) + ( N ^ 2 ) ) )
43 30 39 30 add32d 
 |-  ( ph -> ( ( ( N ^ 2 ) + ( M ^ 3 ) ) + ( N ^ 2 ) ) = ( ( ( N ^ 2 ) + ( N ^ 2 ) ) + ( M ^ 3 ) ) )
44 30 2timesd 
 |-  ( ph -> ( 2 x. ( N ^ 2 ) ) = ( ( N ^ 2 ) + ( N ^ 2 ) ) )
45 44 oveq1d 
 |-  ( ph -> ( ( 2 x. ( N ^ 2 ) ) + ( M ^ 3 ) ) = ( ( ( N ^ 2 ) + ( N ^ 2 ) ) + ( M ^ 3 ) ) )
46 43 45 eqtr4d 
 |-  ( ph -> ( ( ( N ^ 2 ) + ( M ^ 3 ) ) + ( N ^ 2 ) ) = ( ( 2 x. ( N ^ 2 ) ) + ( M ^ 3 ) ) )
47 46 oveq1d 
 |-  ( ph -> ( ( ( ( N ^ 2 ) + ( M ^ 3 ) ) + ( N ^ 2 ) ) - ( Q x. G ) ) = ( ( ( 2 x. ( N ^ 2 ) ) + ( M ^ 3 ) ) - ( Q x. G ) ) )
48 29 42 47 3eqtr2d 
 |-  ( ph -> ( ( T ^ 3 ) ^ 2 ) = ( ( ( 2 x. ( N ^ 2 ) ) + ( M ^ 3 ) ) - ( Q x. G ) ) )
49 2 6 14 subdid 
 |-  ( ph -> ( Q x. ( G - N ) ) = ( ( Q x. G ) - ( Q x. N ) ) )
50 5 oveq2d 
 |-  ( ph -> ( Q x. ( T ^ 3 ) ) = ( Q x. ( G - N ) ) )
51 14 sqvald 
 |-  ( ph -> ( N ^ 2 ) = ( N x. N ) )
52 51 oveq2d 
 |-  ( ph -> ( 2 x. ( N ^ 2 ) ) = ( 2 x. ( N x. N ) ) )
53 17 14 14 mulassd 
 |-  ( ph -> ( ( 2 x. N ) x. N ) = ( 2 x. ( N x. N ) ) )
54 23 oveq1d 
 |-  ( ph -> ( ( 2 x. N ) x. N ) = ( Q x. N ) )
55 52 53 54 3eqtr2d 
 |-  ( ph -> ( 2 x. ( N ^ 2 ) ) = ( Q x. N ) )
56 55 oveq2d 
 |-  ( ph -> ( ( Q x. G ) - ( 2 x. ( N ^ 2 ) ) ) = ( ( Q x. G ) - ( Q x. N ) ) )
57 49 50 56 3eqtr4d 
 |-  ( ph -> ( Q x. ( T ^ 3 ) ) = ( ( Q x. G ) - ( 2 x. ( N ^ 2 ) ) ) )
58 57 oveq1d 
 |-  ( ph -> ( ( Q x. ( T ^ 3 ) ) - ( M ^ 3 ) ) = ( ( ( Q x. G ) - ( 2 x. ( N ^ 2 ) ) ) - ( M ^ 3 ) ) )
59 2cn 
 |-  2 e. CC
60 mulcl 
 |-  ( ( 2 e. CC /\ ( N ^ 2 ) e. CC ) -> ( 2 x. ( N ^ 2 ) ) e. CC )
61 59 30 60 sylancr 
 |-  ( ph -> ( 2 x. ( N ^ 2 ) ) e. CC )
62 41 61 39 subsub4d 
 |-  ( ph -> ( ( ( Q x. G ) - ( 2 x. ( N ^ 2 ) ) ) - ( M ^ 3 ) ) = ( ( Q x. G ) - ( ( 2 x. ( N ^ 2 ) ) + ( M ^ 3 ) ) ) )
63 58 62 eqtrd 
 |-  ( ph -> ( ( Q x. ( T ^ 3 ) ) - ( M ^ 3 ) ) = ( ( Q x. G ) - ( ( 2 x. ( N ^ 2 ) ) + ( M ^ 3 ) ) ) )
64 48 63 oveq12d 
 |-  ( ph -> ( ( ( T ^ 3 ) ^ 2 ) + ( ( Q x. ( T ^ 3 ) ) - ( M ^ 3 ) ) ) = ( ( ( ( 2 x. ( N ^ 2 ) ) + ( M ^ 3 ) ) - ( Q x. G ) ) + ( ( Q x. G ) - ( ( 2 x. ( N ^ 2 ) ) + ( M ^ 3 ) ) ) ) )
65 61 39 addcld 
 |-  ( ph -> ( ( 2 x. ( N ^ 2 ) ) + ( M ^ 3 ) ) e. CC )
66 npncan2 
 |-  ( ( ( ( 2 x. ( N ^ 2 ) ) + ( M ^ 3 ) ) e. CC /\ ( Q x. G ) e. CC ) -> ( ( ( ( 2 x. ( N ^ 2 ) ) + ( M ^ 3 ) ) - ( Q x. G ) ) + ( ( Q x. G ) - ( ( 2 x. ( N ^ 2 ) ) + ( M ^ 3 ) ) ) ) = 0 )
67 65 41 66 syl2anc 
 |-  ( ph -> ( ( ( ( 2 x. ( N ^ 2 ) ) + ( M ^ 3 ) ) - ( Q x. G ) ) + ( ( Q x. G ) - ( ( 2 x. ( N ^ 2 ) ) + ( M ^ 3 ) ) ) ) = 0 )
68 64 67 eqtrd 
 |-  ( ph -> ( ( ( T ^ 3 ) ^ 2 ) + ( ( Q x. ( T ^ 3 ) ) - ( M ^ 3 ) ) ) = 0 )
69 1 2 3 4 5 6 7 8 9 10 4 10 11 dcubic1lem 
 |-  ( ph -> ( ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 <-> ( ( ( T ^ 3 ) ^ 2 ) + ( ( Q x. ( T ^ 3 ) ) - ( M ^ 3 ) ) ) = 0 ) )
70 68 69 mpbird 
 |-  ( ph -> ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 )