Metamath Proof Explorer

Theorem quart1cl

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

Ref Expression
Hypotheses quart1.a 
|- ( ph -> A e. CC )
quart1.b 
|- ( ph -> B e. CC )
quart1.c 
|- ( ph -> C e. CC )
quart1.d 
|- ( ph -> D e. CC )
quart1.p 
|- ( ph -> P = ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) )
quart1.q 
|- ( ph -> Q = ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) )
quart1.r 
|- ( ph -> R = ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) )
Assertion quart1cl 
|- ( ph -> ( P e. CC /\ Q e. CC /\ R e. CC ) )

Proof

Step Hyp Ref Expression
1 quart1.a 
 |-  ( ph -> A e. CC )
2 quart1.b 
 |-  ( ph -> B e. CC )
3 quart1.c 
 |-  ( ph -> C e. CC )
4 quart1.d 
 |-  ( ph -> D e. CC )
5 quart1.p 
 |-  ( ph -> P = ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) )
6 quart1.q 
 |-  ( ph -> Q = ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) )
7 quart1.r 
 |-  ( ph -> R = ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) )
8 3cn 
 |-  3 e. CC
9 8cn 
 |-  8 e. CC
10 8nn 
 |-  8 e. NN
11 10 nnne0i 
 |-  8 =/= 0
12 8 9 11 divcli 
 |-  ( 3 / 8 ) e. CC
13 1 sqcld 
 |-  ( ph -> ( A ^ 2 ) e. CC )
14 mulcl 
 |-  ( ( ( 3 / 8 ) e. CC /\ ( A ^ 2 ) e. CC ) -> ( ( 3 / 8 ) x. ( A ^ 2 ) ) e. CC )
15 12 13 14 sylancr 
 |-  ( ph -> ( ( 3 / 8 ) x. ( A ^ 2 ) ) e. CC )
16 2 15 subcld 
 |-  ( ph -> ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) e. CC )
17 5 16 eqeltrd 
 |-  ( ph -> P e. CC )
18 1 2 mulcld 
 |-  ( ph -> ( A x. B ) e. CC )
19 18 halfcld 
 |-  ( ph -> ( ( A x. B ) / 2 ) e. CC )
20 3 19 subcld 
 |-  ( ph -> ( C - ( ( A x. B ) / 2 ) ) e. CC )
21 3nn0 
 |-  3 e. NN0
22 expcl 
 |-  ( ( A e. CC /\ 3 e. NN0 ) -> ( A ^ 3 ) e. CC )
23 1 21 22 sylancl 
 |-  ( ph -> ( A ^ 3 ) e. CC )
24 9 a1i 
 |-  ( ph -> 8 e. CC )
25 11 a1i 
 |-  ( ph -> 8 =/= 0 )
26 23 24 25 divcld 
 |-  ( ph -> ( ( A ^ 3 ) / 8 ) e. CC )
27 20 26 addcld 
 |-  ( ph -> ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) e. CC )
28 6 27 eqeltrd 
 |-  ( ph -> Q e. CC )
29 3 1 mulcld 
 |-  ( ph -> ( C x. A ) e. CC )
30 4cn 
 |-  4 e. CC
31 30 a1i 
 |-  ( ph -> 4 e. CC )
32 4ne0 
 |-  4 =/= 0
33 32 a1i 
 |-  ( ph -> 4 =/= 0 )
34 29 31 33 divcld 
 |-  ( ph -> ( ( C x. A ) / 4 ) e. CC )
35 4 34 subcld 
 |-  ( ph -> ( D - ( ( C x. A ) / 4 ) ) e. CC )
36 13 2 mulcld 
 |-  ( ph -> ( ( A ^ 2 ) x. B ) e. CC )
37 1nn0 
 |-  1 e. NN0
38 6nn 
 |-  6 e. NN
39 37 38 decnncl 
 |-  ; 1 6 e. NN
40 39 nncni 
 |-  ; 1 6 e. CC
41 40 a1i 
 |-  ( ph -> ; 1 6 e. CC )
42 39 nnne0i 
 |-  ; 1 6 =/= 0
43 42 a1i 
 |-  ( ph -> ; 1 6 =/= 0 )
44 36 41 43 divcld 
 |-  ( ph -> ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) e. CC )
45 2nn0 
 |-  2 e. NN0
46 5nn0 
 |-  5 e. NN0
47 45 46 deccl 
 |-  ; 2 5 e. NN0
48 47 38 decnncl 
 |-  ; ; 2 5 6 e. NN
49 48 nncni 
 |-  ; ; 2 5 6 e. CC
50 48 nnne0i 
 |-  ; ; 2 5 6 =/= 0
51 8 49 50 divcli 
 |-  ( 3 / ; ; 2 5 6 ) e. CC
52 4nn0 
 |-  4 e. NN0
53 expcl 
 |-  ( ( A e. CC /\ 4 e. NN0 ) -> ( A ^ 4 ) e. CC )
54 1 52 53 sylancl 
 |-  ( ph -> ( A ^ 4 ) e. CC )
55 mulcl 
 |-  ( ( ( 3 / ; ; 2 5 6 ) e. CC /\ ( A ^ 4 ) e. CC ) -> ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) e. CC )
56 51 54 55 sylancr 
 |-  ( ph -> ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) e. CC )
57 44 56 subcld 
 |-  ( ph -> ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) e. CC )
58 35 57 addcld 
 |-  ( ph -> ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) e. CC )
59 7 58 eqeltrd 
 |-  ( ph -> R e. CC )
60 17 28 59 3jca 
 |-  ( ph -> ( P e. CC /\ Q e. CC /\ R e. CC ) )