Metamath Proof Explorer

Theorem quartlem3

Description: Closure lemmas for quart . (Contributed by Mario Carneiro, 7-May-2015)

Ref Expression
Hypotheses quart.a 
|- ( ph -> A e. CC )
quart.b 
|- ( ph -> B e. CC )
quart.c 
|- ( ph -> C e. CC )
quart.d 
|- ( ph -> D e. CC )
quart.x 
|- ( ph -> X e. CC )
quart.e 
|- ( ph -> E = -u ( A / 4 ) )
quart.p 
|- ( ph -> P = ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) )
quart.q 
|- ( ph -> Q = ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) )
quart.r 
|- ( ph -> R = ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) )
quart.u 
|- ( ph -> U = ( ( P ^ 2 ) + ( ; 1 2 x. R ) ) )
quart.v 
|- ( ph -> V = ( ( -u ( 2 x. ( P ^ 3 ) ) - ( ; 2 7 x. ( Q ^ 2 ) ) ) + ( ; 7 2 x. ( P x. R ) ) ) )
quart.w 
|- ( ph -> W = ( sqrt ` ( ( V ^ 2 ) - ( 4 x. ( U ^ 3 ) ) ) ) )
quart.s 
|- ( ph -> S = ( ( sqrt ` M ) / 2 ) )
quart.m 
|- ( ph -> M = -u ( ( ( ( 2 x. P ) + T ) + ( U / T ) ) / 3 ) )
quart.t 
|- ( ph -> T = ( ( ( V + W ) / 2 ) ^c ( 1 / 3 ) ) )
quart.t0 
|- ( ph -> T =/= 0 )
Assertion quartlem3 
|- ( ph -> ( S e. CC /\ M e. CC /\ T e. CC ) )

Proof

Step Hyp Ref Expression
1 quart.a 
 |-  ( ph -> A e. CC )
2 quart.b 
 |-  ( ph -> B e. CC )
3 quart.c 
 |-  ( ph -> C e. CC )
4 quart.d 
 |-  ( ph -> D e. CC )
5 quart.x 
 |-  ( ph -> X e. CC )
6 quart.e 
 |-  ( ph -> E = -u ( A / 4 ) )
7 quart.p 
 |-  ( ph -> P = ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) )
8 quart.q 
 |-  ( ph -> Q = ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) )
9 quart.r 
 |-  ( ph -> R = ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) )
10 quart.u 
 |-  ( ph -> U = ( ( P ^ 2 ) + ( ; 1 2 x. R ) ) )
11 quart.v 
 |-  ( ph -> V = ( ( -u ( 2 x. ( P ^ 3 ) ) - ( ; 2 7 x. ( Q ^ 2 ) ) ) + ( ; 7 2 x. ( P x. R ) ) ) )
12 quart.w 
 |-  ( ph -> W = ( sqrt ` ( ( V ^ 2 ) - ( 4 x. ( U ^ 3 ) ) ) ) )
13 quart.s 
 |-  ( ph -> S = ( ( sqrt ` M ) / 2 ) )
14 quart.m 
 |-  ( ph -> M = -u ( ( ( ( 2 x. P ) + T ) + ( U / T ) ) / 3 ) )
15 quart.t 
 |-  ( ph -> T = ( ( ( V + W ) / 2 ) ^c ( 1 / 3 ) ) )
16 quart.t0 
 |-  ( ph -> T =/= 0 )
17 2cn 
 |-  2 e. CC
18 1 2 3 4 7 8 9 quart1cl 
 |-  ( ph -> ( P e. CC /\ Q e. CC /\ R e. CC ) )
19 18 simp1d 
 |-  ( ph -> P e. CC )
20 mulcl 
 |-  ( ( 2 e. CC /\ P e. CC ) -> ( 2 x. P ) e. CC )
21 17 19 20 sylancr 
 |-  ( ph -> ( 2 x. P ) e. CC )
22 1 2 3 4 1 6 7 8 9 10 11 12 quartlem2 
 |-  ( ph -> ( U e. CC /\ V e. CC /\ W e. CC ) )
23 22 simp2d 
 |-  ( ph -> V e. CC )
24 22 simp3d 
 |-  ( ph -> W e. CC )
25 23 24 addcld 
 |-  ( ph -> ( V + W ) e. CC )
26 25 halfcld 
 |-  ( ph -> ( ( V + W ) / 2 ) e. CC )
27 3nn 
 |-  3 e. NN
28 nnrecre 
 |-  ( 3 e. NN -> ( 1 / 3 ) e. RR )
29 27 28 ax-mp 
 |-  ( 1 / 3 ) e. RR
30 29 recni 
 |-  ( 1 / 3 ) e. CC
31 cxpcl 
 |-  ( ( ( ( V + W ) / 2 ) e. CC /\ ( 1 / 3 ) e. CC ) -> ( ( ( V + W ) / 2 ) ^c ( 1 / 3 ) ) e. CC )
32 26 30 31 sylancl 
 |-  ( ph -> ( ( ( V + W ) / 2 ) ^c ( 1 / 3 ) ) e. CC )
33 15 32 eqeltrd 
 |-  ( ph -> T e. CC )
34 21 33 addcld 
 |-  ( ph -> ( ( 2 x. P ) + T ) e. CC )
35 22 simp1d 
 |-  ( ph -> U e. CC )
36 35 33 16 divcld 
 |-  ( ph -> ( U / T ) e. CC )
37 34 36 addcld 
 |-  ( ph -> ( ( ( 2 x. P ) + T ) + ( U / T ) ) e. CC )
38 3cn 
 |-  3 e. CC
39 38 a1i 
 |-  ( ph -> 3 e. CC )
40 3ne0 
 |-  3 =/= 0
41 40 a1i 
 |-  ( ph -> 3 =/= 0 )
42 37 39 41 divcld 
 |-  ( ph -> ( ( ( ( 2 x. P ) + T ) + ( U / T ) ) / 3 ) e. CC )
43 42 negcld 
 |-  ( ph -> -u ( ( ( ( 2 x. P ) + T ) + ( U / T ) ) / 3 ) e. CC )
44 14 43 eqeltrd 
 |-  ( ph -> M e. CC )
45 44 sqrtcld 
 |-  ( ph -> ( sqrt ` M ) e. CC )
46 45 halfcld 
 |-  ( ph -> ( ( sqrt ` M ) / 2 ) e. CC )
47 13 46 eqeltrd 
 |-  ( ph -> S e. CC )
48 47 44 33 3jca 
 |-  ( ph -> ( S e. CC /\ M e. CC /\ T e. CC ) )