Metamath Proof Explorer


Theorem quartlem4

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
quart.m0 φ M 0
quart.i φ I = S 2 - P 2 + Q 4 S
quart.j φ J = S 2 - P 2 - Q 4 S
Assertion quartlem4 φ S 0 I J

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