Metamath Proof Explorer


Theorem quartlem1

Description: Lemma for quart . (Contributed by Mario Carneiro, 6-May-2015)

Ref Expression
Hypotheses quartlem1.p φ P
quartlem1.q φ Q
quartlem1.r φ R
quartlem1.u φ U = P 2 + 12 R
quartlem1.v φ V = 2 P 3 - 27 Q 2 + 72 P R
Assertion quartlem1 φ U = 2 P 2 3 P 2 4 R V = 2 2 P 3 - 9 2 P P 2 4 R + 27 Q 2

Proof

Step Hyp Ref Expression
1 quartlem1.p φ P
2 quartlem1.q φ Q
3 quartlem1.r φ R
4 quartlem1.u φ U = P 2 + 12 R
5 quartlem1.v φ V = 2 P 3 - 27 Q 2 + 72 P R
6 2cn 2
7 sqmul 2 P 2 P 2 = 2 2 P 2
8 6 1 7 sylancr φ 2 P 2 = 2 2 P 2
9 sq2 2 2 = 4
10 9 oveq1i 2 2 P 2 = 4 P 2
11 8 10 eqtrdi φ 2 P 2 = 4 P 2
12 11 oveq1d φ 2 P 2 3 P 2 = 4 P 2 3 P 2
13 4cn 4
14 13 a1i φ 4
15 3cn 3
16 15 a1i φ 3
17 1 sqcld φ P 2
18 14 16 17 subdird φ 4 3 P 2 = 4 P 2 3 P 2
19 12 18 eqtr4d φ 2 P 2 3 P 2 = 4 3 P 2
20 ax-1cn 1
21 3p1e4 3 + 1 = 4
22 13 15 20 21 subaddrii 4 3 = 1
23 22 oveq1i 4 3 P 2 = 1 P 2
24 mulid2 P 2 1 P 2 = P 2
25 23 24 syl5eq P 2 4 3 P 2 = P 2
26 17 25 syl φ 4 3 P 2 = P 2
27 19 26 eqtr2d φ P 2 = 2 P 2 3 P 2
28 27 oveq1d φ P 2 + 12 R = 2 P 2 - 3 P 2 + 12 R
29 mulcl 2 P 2 P
30 6 1 29 sylancr φ 2 P
31 30 sqcld φ 2 P 2
32 mulcl 3 P 2 3 P 2
33 15 17 32 sylancr φ 3 P 2
34 1nn0 1 0
35 2nn 2
36 34 35 decnncl 12
37 36 nncni 12
38 mulcl 12 R 12 R
39 37 3 38 sylancr φ 12 R
40 31 33 39 subsubd φ 2 P 2 3 P 2 12 R = 2 P 2 - 3 P 2 + 12 R
41 28 40 eqtr4d φ P 2 + 12 R = 2 P 2 3 P 2 12 R
42 mulcl 4 R 4 R
43 13 3 42 sylancr φ 4 R
44 16 17 43 subdid φ 3 P 2 4 R = 3 P 2 3 4 R
45 4t3e12 4 3 = 12
46 13 15 45 mulcomli 3 4 = 12
47 46 oveq1i 3 4 R = 12 R
48 16 14 3 mulassd φ 3 4 R = 3 4 R
49 47 48 eqtr3id φ 12 R = 3 4 R
50 49 oveq2d φ 3 P 2 12 R = 3 P 2 3 4 R
51 44 50 eqtr4d φ 3 P 2 4 R = 3 P 2 12 R
52 51 oveq2d φ 2 P 2 3 P 2 4 R = 2 P 2 3 P 2 12 R
53 41 4 52 3eqtr4d φ U = 2 P 2 3 P 2 4 R
54 6 a1i φ 2
55 3nn0 3 0
56 55 a1i φ 3 0
57 54 1 56 mulexpd φ 2 P 3 = 2 3 P 3
58 cu2 2 3 = 8
59 58 oveq1i 2 3 P 3 = 8 P 3
60 57 59 eqtrdi φ 2 P 3 = 8 P 3
61 60 oveq2d φ 2 2 P 3 = 2 8 P 3
62 8cn 8
63 62 a1i φ 8
64 expcl P 3 0 P 3
65 1 55 64 sylancl φ P 3
66 54 63 65 mul12d φ 2 8 P 3 = 8 2 P 3
67 61 66 eqtrd φ 2 2 P 3 = 8 2 P 3
68 9cn 9
69 68 a1i φ 9
70 mulcl 2 P 3 2 P 3
71 6 65 70 sylancr φ 2 P 3
72 1 3 mulcld φ P R
73 mulcl 8 P R 8 P R
74 62 72 73 sylancr φ 8 P R
75 69 71 74 subdid φ 9 2 P 3 8 P R = 9 2 P 3 9 8 P R
76 30 17 43 subdid φ 2 P P 2 4 R = 2 P P 2 2 P 4 R
77 54 1 17 mulassd φ 2 P P 2 = 2 P P 2
78 1 17 mulcomd φ P P 2 = P 2 P
79 df-3 3 = 2 + 1
80 79 oveq2i P 3 = P 2 + 1
81 2nn0 2 0
82 expp1 P 2 0 P 2 + 1 = P 2 P
83 1 81 82 sylancl φ P 2 + 1 = P 2 P
84 80 83 syl5eq φ P 3 = P 2 P
85 78 84 eqtr4d φ P P 2 = P 3
86 85 oveq2d φ 2 P P 2 = 2 P 3
87 77 86 eqtrd φ 2 P P 2 = 2 P 3
88 54 1 14 3 mul4d φ 2 P 4 R = 2 4 P R
89 4t2e8 4 2 = 8
90 13 6 89 mulcomli 2 4 = 8
91 90 oveq1i 2 4 P R = 8 P R
92 88 91 eqtrdi φ 2 P 4 R = 8 P R
93 87 92 oveq12d φ 2 P P 2 2 P 4 R = 2 P 3 8 P R
94 76 93 eqtrd φ 2 P P 2 4 R = 2 P 3 8 P R
95 94 oveq2d φ 9 2 P P 2 4 R = 9 2 P 3 8 P R
96 9t8e72 9 8 = 72
97 96 oveq1i 9 8 P R = 72 P R
98 69 63 72 mulassd φ 9 8 P R = 9 8 P R
99 97 98 eqtr3id φ 72 P R = 9 8 P R
100 99 oveq2d φ 9 2 P 3 72 P R = 9 2 P 3 9 8 P R
101 75 95 100 3eqtr4d φ 9 2 P P 2 4 R = 9 2 P 3 72 P R
102 67 101 oveq12d φ 2 2 P 3 9 2 P P 2 4 R = 8 2 P 3 9 2 P 3 72 P R
103 mulcl 8 2 P 3 8 2 P 3
104 62 71 103 sylancr φ 8 2 P 3
105 mulcl 9 2 P 3 9 2 P 3
106 68 71 105 sylancr φ 9 2 P 3
107 7nn0 7 0
108 107 35 decnncl 72
109 108 nncni 72
110 mulcl 72 P R 72 P R
111 109 72 110 sylancr φ 72 P R
112 104 106 111 subsubd φ 8 2 P 3 9 2 P 3 72 P R = 8 2 P 3 - 9 2 P 3 + 72 P R
113 106 104 negsubdi2d φ 9 2 P 3 8 2 P 3 = 8 2 P 3 9 2 P 3
114 69 63 71 subdird φ 9 8 2 P 3 = 9 2 P 3 8 2 P 3
115 8p1e9 8 + 1 = 9
116 68 62 20 115 subaddrii 9 8 = 1
117 116 oveq1i 9 8 2 P 3 = 1 2 P 3
118 71 mulid2d φ 1 2 P 3 = 2 P 3
119 117 118 syl5eq φ 9 8 2 P 3 = 2 P 3
120 114 119 eqtr3d φ 9 2 P 3 8 2 P 3 = 2 P 3
121 120 negeqd φ 9 2 P 3 8 2 P 3 = 2 P 3
122 113 121 eqtr3d φ 8 2 P 3 9 2 P 3 = 2 P 3
123 122 oveq1d φ 8 2 P 3 - 9 2 P 3 + 72 P R = - 2 P 3 + 72 P R
124 102 112 123 3eqtrd φ 2 2 P 3 9 2 P P 2 4 R = - 2 P 3 + 72 P R
125 7nn 7
126 81 125 decnncl 27
127 126 nncni 27
128 2 sqcld φ Q 2
129 mulneg2 27 Q 2 27 Q 2 = 27 Q 2
130 127 128 129 sylancr φ 27 Q 2 = 27 Q 2
131 124 130 oveq12d φ 2 2 P 3 - 9 2 P P 2 4 R + 27 Q 2 = 2 P 3 + 72 P R + 27 Q 2
132 71 negcld φ 2 P 3
133 mulcl 27 Q 2 27 Q 2
134 127 128 133 sylancr φ 27 Q 2
135 132 111 134 addsubd φ 2 P 3 + 72 P R - 27 Q 2 = 2 P 3 - 27 Q 2 + 72 P R
136 132 111 addcld φ - 2 P 3 + 72 P R
137 136 134 negsubd φ 2 P 3 + 72 P R + 27 Q 2 = 2 P 3 + 72 P R - 27 Q 2
138 135 137 5 3eqtr4d φ 2 P 3 + 72 P R + 27 Q 2 = V
139 131 138 eqtr2d φ V = 2 2 P 3 - 9 2 P P 2 4 R + 27 Q 2
140 53 139 jca φ U = 2 P 2 3 P 2 4 R V = 2 2 P 3 - 9 2 P P 2 4 R + 27 Q 2