Metamath Proof Explorer

Theorem quartlem2

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 ) ) ) ) )
Assertion quartlem2 
|- ( ph -> ( U e. CC /\ V e. CC /\ W 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 1 2 3 4 7 8 9 quart1cl 
 |-  ( ph -> ( P e. CC /\ Q e. CC /\ R e. CC ) )
14 13 simp1d 
 |-  ( ph -> P e. CC )
15 14 sqcld 
 |-  ( ph -> ( P ^ 2 ) e. CC )
16 1nn0 
 |-  1 e. NN0
17 2nn 
 |-  2 e. NN
18 16 17 decnncl 
 |-  ; 1 2 e. NN
19 18 nncni 
 |-  ; 1 2 e. CC
20 13 simp3d 
 |-  ( ph -> R e. CC )
21 mulcl 
 |-  ( ( ; 1 2 e. CC /\ R e. CC ) -> ( ; 1 2 x. R ) e. CC )
22 19 20 21 sylancr 
 |-  ( ph -> ( ; 1 2 x. R ) e. CC )
23 15 22 addcld 
 |-  ( ph -> ( ( P ^ 2 ) + ( ; 1 2 x. R ) ) e. CC )
24 10 23 eqeltrd 
 |-  ( ph -> U e. CC )
25 2cn 
 |-  2 e. CC
26 3nn0 
 |-  3 e. NN0
27 expcl 
 |-  ( ( P e. CC /\ 3 e. NN0 ) -> ( P ^ 3 ) e. CC )
28 14 26 27 sylancl 
 |-  ( ph -> ( P ^ 3 ) e. CC )
29 mulcl 
 |-  ( ( 2 e. CC /\ ( P ^ 3 ) e. CC ) -> ( 2 x. ( P ^ 3 ) ) e. CC )
30 25 28 29 sylancr 
 |-  ( ph -> ( 2 x. ( P ^ 3 ) ) e. CC )
31 30 negcld 
 |-  ( ph -> -u ( 2 x. ( P ^ 3 ) ) e. CC )
32 2nn0 
 |-  2 e. NN0
33 7nn 
 |-  7 e. NN
34 32 33 decnncl 
 |-  ; 2 7 e. NN
35 34 nncni 
 |-  ; 2 7 e. CC
36 13 simp2d 
 |-  ( ph -> Q e. CC )
37 36 sqcld 
 |-  ( ph -> ( Q ^ 2 ) e. CC )
38 mulcl 
 |-  ( ( ; 2 7 e. CC /\ ( Q ^ 2 ) e. CC ) -> ( ; 2 7 x. ( Q ^ 2 ) ) e. CC )
39 35 37 38 sylancr 
 |-  ( ph -> ( ; 2 7 x. ( Q ^ 2 ) ) e. CC )
40 31 39 subcld 
 |-  ( ph -> ( -u ( 2 x. ( P ^ 3 ) ) - ( ; 2 7 x. ( Q ^ 2 ) ) ) e. CC )
41 7nn0 
 |-  7 e. NN0
42 41 17 decnncl 
 |-  ; 7 2 e. NN
43 42 nncni 
 |-  ; 7 2 e. CC
44 14 20 mulcld 
 |-  ( ph -> ( P x. R ) e. CC )
45 mulcl 
 |-  ( ( ; 7 2 e. CC /\ ( P x. R ) e. CC ) -> ( ; 7 2 x. ( P x. R ) ) e. CC )
46 43 44 45 sylancr 
 |-  ( ph -> ( ; 7 2 x. ( P x. R ) ) e. CC )
47 40 46 addcld 
 |-  ( ph -> ( ( -u ( 2 x. ( P ^ 3 ) ) - ( ; 2 7 x. ( Q ^ 2 ) ) ) + ( ; 7 2 x. ( P x. R ) ) ) e. CC )
48 11 47 eqeltrd 
 |-  ( ph -> V e. CC )
49 48 sqcld 
 |-  ( ph -> ( V ^ 2 ) e. CC )
50 4cn 
 |-  4 e. CC
51 expcl 
 |-  ( ( U e. CC /\ 3 e. NN0 ) -> ( U ^ 3 ) e. CC )
52 24 26 51 sylancl 
 |-  ( ph -> ( U ^ 3 ) e. CC )
53 mulcl 
 |-  ( ( 4 e. CC /\ ( U ^ 3 ) e. CC ) -> ( 4 x. ( U ^ 3 ) ) e. CC )
54 50 52 53 sylancr 
 |-  ( ph -> ( 4 x. ( U ^ 3 ) ) e. CC )
55 49 54 subcld 
 |-  ( ph -> ( ( V ^ 2 ) - ( 4 x. ( U ^ 3 ) ) ) e. CC )
56 55 sqrtcld 
 |-  ( ph -> ( sqrt ` ( ( V ^ 2 ) - ( 4 x. ( U ^ 3 ) ) ) ) e. CC )
57 12 56 eqeltrd 
 |-  ( ph -> W e. CC )
58 24 48 57 3jca 
 |-  ( ph -> ( U e. CC /\ V e. CC /\ W e. CC ) )