Metamath Proof Explorer


Theorem quartlem3

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
quart.s φ S = M 2
quart.m φ M = 2 P + T + U T 3
quart.t φ T = V + W 2 1 3
quart.t0 φ T 0
Assertion quartlem3 φ S M T

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 quart.s φ S = M 2
14 quart.m φ M = 2 P + T + U T 3
15 quart.t φ T = V + W 2 1 3
16 quart.t0 φ T 0
17 2cn 2
18 1 2 3 4 7 8 9 quart1cl φ P Q R
19 18 simp1d φ P
20 mulcl 2 P 2 P
21 17 19 20 sylancr φ 2 P
22 1 2 3 4 1 6 7 8 9 10 11 12 quartlem2 φ U V W
23 22 simp2d φ V
24 22 simp3d φ W
25 23 24 addcld φ V + W
26 25 halfcld φ V + W 2
27 3nn 3
28 nnrecre 3 1 3
29 27 28 ax-mp 1 3
30 29 recni 1 3
31 cxpcl V + W 2 1 3 V + W 2 1 3
32 26 30 31 sylancl φ V + W 2 1 3
33 15 32 eqeltrd φ T
34 21 33 addcld φ 2 P + T
35 22 simp1d φ U
36 35 33 16 divcld φ U T
37 34 36 addcld φ 2 P + T + U T
38 3cn 3
39 38 a1i φ 3
40 3ne0 3 0
41 40 a1i φ 3 0
42 37 39 41 divcld φ 2 P + T + U T 3
43 42 negcld φ 2 P + T + U T 3
44 14 43 eqeltrd φ M
45 44 sqrtcld φ M
46 45 halfcld φ M 2
47 13 46 eqeltrd φ S
48 47 44 33 3jca φ S M T