Metamath Proof Explorer


Theorem quartlem2

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

Ref Expression
Hypotheses quart.a φ A
quart.b φ B
quart.c φ C
quart.d φ D
quart.x φ X
quart.e φ E = A 4
quart.p φ P = B 3 8 A 2
quart.q φ Q = C - A B 2 + A 3 8
quart.r φ R = D C A 4 + A 2 B 16 - 3 256 A 4
quart.u φ U = P 2 + 12 R
quart.v φ V = 2 P 3 - 27 Q 2 + 72 P R
quart.w φ W = V 2 4 U 3
Assertion quartlem2 φ U V W

Proof

Step Hyp Ref Expression
1 quart.a φ A
2 quart.b φ B
3 quart.c φ C
4 quart.d φ D
5 quart.x φ X
6 quart.e φ E = A 4
7 quart.p φ P = B 3 8 A 2
8 quart.q φ Q = C - A B 2 + A 3 8
9 quart.r φ R = D C A 4 + A 2 B 16 - 3 256 A 4
10 quart.u φ U = P 2 + 12 R
11 quart.v φ V = 2 P 3 - 27 Q 2 + 72 P R
12 quart.w φ W = V 2 4 U 3
13 1 2 3 4 7 8 9 quart1cl φ P Q R
14 13 simp1d φ P
15 14 sqcld φ P 2
16 1nn0 1 0
17 2nn 2
18 16 17 decnncl 12
19 18 nncni 12
20 13 simp3d φ R
21 mulcl 12 R 12 R
22 19 20 21 sylancr φ 12 R
23 15 22 addcld φ P 2 + 12 R
24 10 23 eqeltrd φ U
25 2cn 2
26 3nn0 3 0
27 expcl P 3 0 P 3
28 14 26 27 sylancl φ P 3
29 mulcl 2 P 3 2 P 3
30 25 28 29 sylancr φ 2 P 3
31 30 negcld φ 2 P 3
32 2nn0 2 0
33 7nn 7
34 32 33 decnncl 27
35 34 nncni 27
36 13 simp2d φ Q
37 36 sqcld φ Q 2
38 mulcl 27 Q 2 27 Q 2
39 35 37 38 sylancr φ 27 Q 2
40 31 39 subcld φ - 2 P 3 - 27 Q 2
41 7nn0 7 0
42 41 17 decnncl 72
43 42 nncni 72
44 14 20 mulcld φ P R
45 mulcl 72 P R 72 P R
46 43 44 45 sylancr φ 72 P R
47 40 46 addcld φ 2 P 3 - 27 Q 2 + 72 P R
48 11 47 eqeltrd φ V
49 48 sqcld φ V 2
50 4cn 4
51 expcl U 3 0 U 3
52 24 26 51 sylancl φ U 3
53 mulcl 4 U 3 4 U 3
54 50 52 53 sylancr φ 4 U 3
55 49 54 subcld φ V 2 4 U 3
56 55 sqrtcld φ V 2 4 U 3
57 12 56 eqeltrd φ W
58 24 48 57 3jca φ U V W