Metamath Proof Explorer

Theorem quartlem4

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 )
quart.m0 
|- ( ph -> M =/= 0 )
quart.i 
|- ( ph -> I = ( sqrt ` ( ( -u ( S ^ 2 ) - ( P / 2 ) ) + ( ( Q / 4 ) / S ) ) ) )
quart.j 
|- ( ph -> J = ( sqrt ` ( ( -u ( S ^ 2 ) - ( P / 2 ) ) - ( ( Q / 4 ) / S ) ) ) )
Assertion quartlem4 
|- ( ph -> ( S =/= 0 /\ I e. CC /\ J 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 quart.m0 
 |-  ( ph -> M =/= 0 )
18 quart.i 
 |-  ( ph -> I = ( sqrt ` ( ( -u ( S ^ 2 ) - ( P / 2 ) ) + ( ( Q / 4 ) / S ) ) ) )
19 quart.j 
 |-  ( ph -> J = ( sqrt ` ( ( -u ( S ^ 2 ) - ( P / 2 ) ) - ( ( Q / 4 ) / S ) ) ) )
20 1 2 3 4 1 6 7 8 9 10 11 12 13 14 15 16 quartlem3 
 |-  ( ph -> ( S e. CC /\ M e. CC /\ T e. CC ) )
21 20 simp2d 
 |-  ( ph -> M e. CC )
22 21 sqrtcld 
 |-  ( ph -> ( sqrt ` M ) e. CC )
23 2cnd 
 |-  ( ph -> 2 e. CC )
24 21 sqsqrtd 
 |-  ( ph -> ( ( sqrt ` M ) ^ 2 ) = M )
25 24 17 eqnetrd 
 |-  ( ph -> ( ( sqrt ` M ) ^ 2 ) =/= 0 )
26 sqne0 
 |-  ( ( sqrt ` M ) e. CC -> ( ( ( sqrt ` M ) ^ 2 ) =/= 0 <-> ( sqrt ` M ) =/= 0 ) )
27 22 26 syl 
 |-  ( ph -> ( ( ( sqrt ` M ) ^ 2 ) =/= 0 <-> ( sqrt ` M ) =/= 0 ) )
28 25 27 mpbid 
 |-  ( ph -> ( sqrt ` M ) =/= 0 )
29 2ne0 
 |-  2 =/= 0
30 29 a1i 
 |-  ( ph -> 2 =/= 0 )
31 22 23 28 30 divne0d 
 |-  ( ph -> ( ( sqrt ` M ) / 2 ) =/= 0 )
32 13 31 eqnetrd 
 |-  ( ph -> S =/= 0 )
33 20 simp1d 
 |-  ( ph -> S e. CC )
34 33 sqcld 
 |-  ( ph -> ( S ^ 2 ) e. CC )
35 34 negcld 
 |-  ( ph -> -u ( S ^ 2 ) e. CC )
36 1 2 3 4 7 8 9 quart1cl 
 |-  ( ph -> ( P e. CC /\ Q e. CC /\ R e. CC ) )
37 36 simp1d 
 |-  ( ph -> P e. CC )
38 37 halfcld 
 |-  ( ph -> ( P / 2 ) e. CC )
39 35 38 subcld 
 |-  ( ph -> ( -u ( S ^ 2 ) - ( P / 2 ) ) e. CC )
40 36 simp2d 
 |-  ( ph -> Q e. CC )
41 4cn 
 |-  4 e. CC
42 41 a1i 
 |-  ( ph -> 4 e. CC )
43 4ne0 
 |-  4 =/= 0
44 43 a1i 
 |-  ( ph -> 4 =/= 0 )
45 40 42 44 divcld 
 |-  ( ph -> ( Q / 4 ) e. CC )
46 45 33 32 divcld 
 |-  ( ph -> ( ( Q / 4 ) / S ) e. CC )
47 39 46 addcld 
 |-  ( ph -> ( ( -u ( S ^ 2 ) - ( P / 2 ) ) + ( ( Q / 4 ) / S ) ) e. CC )
48 47 sqrtcld 
 |-  ( ph -> ( sqrt ` ( ( -u ( S ^ 2 ) - ( P / 2 ) ) + ( ( Q / 4 ) / S ) ) ) e. CC )
49 18 48 eqeltrd 
 |-  ( ph -> I e. CC )
50 39 46 subcld 
 |-  ( ph -> ( ( -u ( S ^ 2 ) - ( P / 2 ) ) - ( ( Q / 4 ) / S ) ) e. CC )
51 50 sqrtcld 
 |-  ( ph -> ( sqrt ` ( ( -u ( S ^ 2 ) - ( P / 2 ) ) - ( ( Q / 4 ) / S ) ) ) e. CC )
52 19 51 eqeltrd 
 |-  ( ph -> J e. CC )
53 32 49 52 3jca 
 |-  ( ph -> ( S =/= 0 /\ I e. CC /\ J e. CC ) )