Metamath Proof Explorer


Theorem quart1lem

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

Ref Expression
Hypotheses quart1.a φ A
quart1.b φ B
quart1.c φ C
quart1.d φ D
quart1.p φ P = B 3 8 A 2
quart1.q φ Q = C - A B 2 + A 3 8
quart1.r φ R = D C A 4 + A 2 B 16 - 3 256 A 4
quart1.x φ X
quart1.y φ Y = X + A 4
Assertion quart1lem φ D = A 4 256 + P A 4 2 + Q A 4 + R

Proof

Step Hyp Ref Expression
1 quart1.a φ A
2 quart1.b φ B
3 quart1.c φ C
4 quart1.d φ D
5 quart1.p φ P = B 3 8 A 2
6 quart1.q φ Q = C - A B 2 + A 3 8
7 quart1.r φ R = D C A 4 + A 2 B 16 - 3 256 A 4
8 quart1.x φ X
9 quart1.y φ Y = X + A 4
10 1 2 mulcld φ A B
11 10 halfcld φ A B 2
12 3 11 subcld φ C A B 2
13 3nn0 3 0
14 expcl A 3 0 A 3
15 1 13 14 sylancl φ A 3
16 8cn 8
17 16 a1i φ 8
18 8nn 8
19 18 nnne0i 8 0
20 19 a1i φ 8 0
21 15 17 20 divcld φ A 3 8
22 4cn 4
23 22 a1i φ 4
24 4ne0 4 0
25 24 a1i φ 4 0
26 1 23 25 divcld φ A 4
27 12 21 26 adddird φ C - A B 2 + A 3 8 A 4 = C A B 2 A 4 + A 3 8 A 4
28 6 oveq1d φ Q A 4 = C - A B 2 + A 3 8 A 4
29 3 1 23 25 divassd φ C A 4 = C A 4
30 1 sqvald φ A 2 = A A
31 30 oveq1d φ A 2 B = A A B
32 1 1 2 mul32d φ A A B = A B A
33 31 32 eqtrd φ A 2 B = A B A
34 33 oveq1d φ A 2 B 8 = A B A 8
35 2cn 2
36 4t2e8 4 2 = 8
37 22 35 36 mulcomli 2 4 = 8
38 37 oveq2i A B A 2 4 = A B A 8
39 34 38 eqtr4di φ A 2 B 8 = A B A 2 4
40 35 a1i φ 2
41 2ne0 2 0
42 41 a1i φ 2 0
43 10 40 1 23 42 25 divmuldivd φ A B 2 A 4 = A B A 2 4
44 39 43 eqtr4d φ A 2 B 8 = A B 2 A 4
45 29 44 oveq12d φ C A 4 A 2 B 8 = C A 4 A B 2 A 4
46 3 11 26 subdird φ C A B 2 A 4 = C A 4 A B 2 A 4
47 45 46 eqtr4d φ C A 4 A 2 B 8 = C A B 2 A 4
48 df-4 4 = 3 + 1
49 48 oveq2i A 4 = A 3 + 1
50 expp1 A 3 0 A 3 + 1 = A 3 A
51 1 13 50 sylancl φ A 3 + 1 = A 3 A
52 49 51 syl5eq φ A 4 = A 3 A
53 52 oveq1d φ A 4 8 = A 3 A 8
54 15 1 17 20 div23d φ A 3 A 8 = A 3 8 A
55 53 54 eqtrd φ A 4 8 = A 3 8 A
56 55 oveq1d φ A 4 8 4 = A 3 8 A 4
57 21 1 23 25 divassd φ A 3 8 A 4 = A 3 8 A 4
58 56 57 eqtrd φ A 4 8 4 = A 3 8 A 4
59 47 58 oveq12d φ C A 4 - A 2 B 8 + A 4 8 4 = C A B 2 A 4 + A 3 8 A 4
60 27 28 59 3eqtr4d φ Q A 4 = C A 4 - A 2 B 8 + A 4 8 4
61 3 1 mulcld φ C A
62 61 23 25 divcld φ C A 4
63 1 sqcld φ A 2
64 63 2 mulcld φ A 2 B
65 64 17 20 divcld φ A 2 B 8
66 4nn0 4 0
67 expcl A 4 0 A 4
68 1 66 67 sylancl φ A 4
69 68 17 20 divcld φ A 4 8
70 69 23 25 divcld φ A 4 8 4
71 62 65 70 subadd23d φ C A 4 - A 2 B 8 + A 4 8 4 = C A 4 + A 4 8 4 - A 2 B 8
72 70 65 subcld φ A 4 8 4 A 2 B 8
73 62 72 addcomd φ C A 4 + A 4 8 4 - A 2 B 8 = A 4 8 4 - A 2 B 8 + C A 4
74 60 71 73 3eqtrd φ Q A 4 = A 4 8 4 - A 2 B 8 + C A 4
75 1nn0 1 0
76 6nn 6
77 75 76 decnncl 16
78 77 nncni 16
79 78 a1i φ 16
80 77 nnne0i 16 0
81 80 a1i φ 16 0
82 64 79 81 divcld φ A 2 B 16
83 3cn 3
84 2nn0 2 0
85 5nn0 5 0
86 84 85 deccl 25 0
87 86 76 decnncl 256
88 87 nncni 256
89 87 nnne0i 256 0
90 83 88 89 divcli 3 256
91 mulcl 3 256 A 4 3 256 A 4
92 90 68 91 sylancr φ 3 256 A 4
93 82 92 subcld φ A 2 B 16 3 256 A 4
94 4 93 62 addsubd φ D + A 2 B 16 3 256 A 4 - C A 4 = D C A 4 + A 2 B 16 - 3 256 A 4
95 7 94 eqtr4d φ R = D + A 2 B 16 3 256 A 4 - C A 4
96 74 95 oveq12d φ Q A 4 + R = A 4 8 4 A 2 B 8 + C A 4 + D + A 2 B 16 3 256 A 4 - C A 4
97 4 93 addcld φ D + A 2 B 16 - 3 256 A 4
98 72 62 97 ppncand φ A 4 8 4 A 2 B 8 + C A 4 + D + A 2 B 16 3 256 A 4 - C A 4 = A 4 8 4 A 2 B 8 + D + A 2 B 16 3 256 A 4
99 72 4 93 add12d φ A 4 8 4 A 2 B 8 + D + A 2 B 16 3 256 A 4 = D + A 4 8 4 A 2 B 8 + A 2 B 16 3 256 A 4
100 65 92 addcld φ A 2 B 8 + 3 256 A 4
101 70 82 addcld φ A 4 8 4 + A 2 B 16
102 100 101 negsubdi2d φ A 2 B 8 + 3 256 A 4 - A 4 8 4 + A 2 B 16 = A 4 8 4 + A 2 B 16 - A 2 B 8 + 3 256 A 4
103 70 82 addcomd φ A 4 8 4 + A 2 B 16 = A 2 B 16 + A 4 8 4
104 103 oveq2d φ A 2 B 8 + 3 256 A 4 - A 4 8 4 + A 2 B 16 = A 2 B 8 + 3 256 A 4 - A 2 B 16 + A 4 8 4
105 65 92 82 70 addsub4d φ A 2 B 8 + 3 256 A 4 - A 2 B 16 + A 4 8 4 = A 2 B 8 A 2 B 16 + 3 256 A 4 - A 4 8 4
106 83 a1i φ 3
107 88 a1i φ 256
108 89 a1i φ 256 0
109 106 68 107 108 divassd φ 3 A 4 256 = 3 A 4 256
110 106 68 107 108 div23d φ 3 A 4 256 = 3 256 A 4
111 1p2e3 1 + 2 = 3
112 111 oveq1i 1 + 2 A 4 256 = 3 A 4 256
113 1cnd φ 1
114 68 107 108 divcld φ A 4 256
115 113 40 114 adddird φ 1 + 2 A 4 256 = 1 A 4 256 + 2 A 4 256
116 112 115 eqtr3id φ 3 A 4 256 = 1 A 4 256 + 2 A 4 256
117 114 mulid2d φ 1 A 4 256 = A 4 256
118 117 oveq1d φ 1 A 4 256 + 2 A 4 256 = A 4 256 + 2 A 4 256
119 116 118 eqtrd φ 3 A 4 256 = A 4 256 + 2 A 4 256
120 109 110 119 3eqtr3d φ 3 256 A 4 = A 4 256 + 2 A 4 256
121 48 oveq1i 4 A 4 8 4 4 = 3 + 1 A 4 8 4 4
122 70 23 25 divcld φ A 4 8 4 4
123 106 113 122 adddird φ 3 + 1 A 4 8 4 4 = 3 A 4 8 4 4 + 1 A 4 8 4 4
124 121 123 syl5eq φ 4 A 4 8 4 4 = 3 A 4 8 4 4 + 1 A 4 8 4 4
125 70 23 25 divcan2d φ 4 A 4 8 4 4 = A 4 8 4
126 122 mulid2d φ 1 A 4 8 4 4 = A 4 8 4 4
127 69 23 23 25 25 divdiv1d φ A 4 8 4 4 = A 4 8 4 4
128 4t4e16 4 4 = 16
129 128 oveq2i A 4 8 4 4 = A 4 8 16
130 127 129 eqtrdi φ A 4 8 4 4 = A 4 8 16
131 68 17 79 20 81 divdiv1d φ A 4 8 16 = A 4 8 16
132 16 78 mulcli 8 16
133 132 a1i φ 8 16
134 16 78 19 80 mulne0i 8 16 0
135 134 a1i φ 8 16 0
136 68 133 135 divcld φ A 4 8 16
137 136 40 42 divcan2d φ 2 A 4 8 16 2 = A 4 8 16
138 68 133 40 135 42 divdiv1d φ A 4 8 16 2 = A 4 8 16 2
139 16 78 35 mul32i 8 16 2 = 8 2 16
140 2exp4 2 4 = 16
141 8t2e16 8 2 = 16
142 140 141 eqtr4i 2 4 = 8 2
143 142 140 oveq12i 2 4 2 4 = 8 2 16
144 4p4e8 4 + 4 = 8
145 144 oveq2i 2 4 + 4 = 2 8
146 expadd 2 4 0 4 0 2 4 + 4 = 2 4 2 4
147 35 66 66 146 mp3an 2 4 + 4 = 2 4 2 4
148 2exp8 2 8 = 256
149 145 147 148 3eqtr3i 2 4 2 4 = 256
150 139 143 149 3eqtr2i 8 16 2 = 256
151 150 oveq2i A 4 8 16 2 = A 4 256
152 138 151 eqtrdi φ A 4 8 16 2 = A 4 256
153 152 oveq2d φ 2 A 4 8 16 2 = 2 A 4 256
154 131 137 153 3eqtr2d φ A 4 8 16 = 2 A 4 256
155 126 130 154 3eqtrd φ 1 A 4 8 4 4 = 2 A 4 256
156 155 oveq2d φ 3 A 4 8 4 4 + 1 A 4 8 4 4 = 3 A 4 8 4 4 + 2 A 4 256
157 124 125 156 3eqtr3d φ A 4 8 4 = 3 A 4 8 4 4 + 2 A 4 256
158 120 157 oveq12d φ 3 256 A 4 A 4 8 4 = A 4 256 + 2 A 4 256 - 3 A 4 8 4 4 + 2 A 4 256
159 mulcl 3 A 4 8 4 4 3 A 4 8 4 4
160 83 122 159 sylancr φ 3 A 4 8 4 4
161 mulcl 2 A 4 256 2 A 4 256
162 35 114 161 sylancr φ 2 A 4 256
163 114 160 162 pnpcan2d φ A 4 256 + 2 A 4 256 - 3 A 4 8 4 4 + 2 A 4 256 = A 4 256 3 A 4 8 4 4
164 158 163 eqtrd φ 3 256 A 4 A 4 8 4 = A 4 256 3 A 4 8 4 4
165 164 oveq2d φ A 2 B 16 + 3 256 A 4 - A 4 8 4 = A 2 B 16 + A 4 256 - 3 A 4 8 4 4
166 82 114 160 addsub12d φ A 2 B 16 + A 4 256 - 3 A 4 8 4 4 = A 4 256 + A 2 B 16 - 3 A 4 8 4 4
167 165 166 eqtrd φ A 2 B 16 + 3 256 A 4 - A 4 8 4 = A 4 256 + A 2 B 16 - 3 A 4 8 4 4
168 64 17 40 20 42 divdiv1d φ A 2 B 8 2 = A 2 B 8 2
169 141 oveq2i A 2 B 8 2 = A 2 B 16
170 168 169 eqtrdi φ A 2 B 8 2 = A 2 B 16
171 170 oveq2d φ 2 A 2 B 8 2 = 2 A 2 B 16
172 65 40 42 divcan2d φ 2 A 2 B 8 2 = A 2 B 8
173 82 2timesd φ 2 A 2 B 16 = A 2 B 16 + A 2 B 16
174 171 172 173 3eqtr3d φ A 2 B 8 = A 2 B 16 + A 2 B 16
175 82 82 174 mvrladdd φ A 2 B 8 A 2 B 16 = A 2 B 16
176 175 oveq1d φ A 2 B 8 A 2 B 16 + 3 256 A 4 - A 4 8 4 = A 2 B 16 + 3 256 A 4 - A 4 8 4
177 5 oveq1d φ P A 4 2 = B 3 8 A 2 A 4 2
178 83 16 19 divcli 3 8
179 mulcl 3 8 A 2 3 8 A 2
180 178 63 179 sylancr φ 3 8 A 2
181 26 sqcld φ A 4 2
182 2 180 181 subdird φ B 3 8 A 2 A 4 2 = B A 4 2 3 8 A 2 A 4 2
183 1 23 25 sqdivd φ A 4 2 = A 2 4 2
184 22 sqvali 4 2 = 4 4
185 184 128 eqtri 4 2 = 16
186 185 oveq2i A 2 4 2 = A 2 16
187 183 186 eqtrdi φ A 4 2 = A 2 16
188 187 oveq2d φ B A 4 2 = B A 2 16
189 2 63 79 81 divassd φ B A 2 16 = B A 2 16
190 2 63 mulcomd φ B A 2 = A 2 B
191 190 oveq1d φ B A 2 16 = A 2 B 16
192 188 189 191 3eqtr2d φ B A 4 2 = A 2 B 16
193 178 a1i φ 3 8
194 193 63 63 mulassd φ 3 8 A 2 A 2 = 3 8 A 2 A 2
195 106 68 17 20 div23d φ 3 A 4 8 = 3 8 A 4
196 2p2e4 2 + 2 = 4
197 196 oveq2i A 2 + 2 = A 4
198 84 a1i φ 2 0
199 1 198 198 expaddd φ A 2 + 2 = A 2 A 2
200 197 199 eqtr3id φ A 4 = A 2 A 2
201 200 oveq2d φ 3 8 A 4 = 3 8 A 2 A 2
202 195 201 eqtrd φ 3 A 4 8 = 3 8 A 2 A 2
203 106 68 17 20 divassd φ 3 A 4 8 = 3 A 4 8
204 194 202 203 3eqtr2d φ 3 8 A 2 A 2 = 3 A 4 8
205 204 oveq1d φ 3 8 A 2 A 2 4 2 = 3 A 4 8 4 2
206 185 79 eqeltrid φ 4 2
207 185 80 eqnetri 4 2 0
208 207 a1i φ 4 2 0
209 180 63 206 208 divassd φ 3 8 A 2 A 2 4 2 = 3 8 A 2 A 2 4 2
210 106 69 206 208 divassd φ 3 A 4 8 4 2 = 3 A 4 8 4 2
211 205 209 210 3eqtr3d φ 3 8 A 2 A 2 4 2 = 3 A 4 8 4 2
212 183 oveq2d φ 3 8 A 2 A 4 2 = 3 8 A 2 A 2 4 2
213 185 oveq2i A 4 8 4 2 = A 4 8 16
214 130 213 eqtr4di φ A 4 8 4 4 = A 4 8 4 2
215 214 oveq2d φ 3 A 4 8 4 4 = 3 A 4 8 4 2
216 211 212 215 3eqtr4d φ 3 8 A 2 A 4 2 = 3 A 4 8 4 4
217 192 216 oveq12d φ B A 4 2 3 8 A 2 A 4 2 = A 2 B 16 3 A 4 8 4 4
218 177 182 217 3eqtrd φ P A 4 2 = A 2 B 16 3 A 4 8 4 4
219 218 oveq2d φ A 4 256 + P A 4 2 = A 4 256 + A 2 B 16 - 3 A 4 8 4 4
220 167 176 219 3eqtr4d φ A 2 B 8 A 2 B 16 + 3 256 A 4 - A 4 8 4 = A 4 256 + P A 4 2
221 104 105 220 3eqtrd φ A 2 B 8 + 3 256 A 4 - A 4 8 4 + A 2 B 16 = A 4 256 + P A 4 2
222 221 negeqd φ A 2 B 8 + 3 256 A 4 - A 4 8 4 + A 2 B 16 = A 4 256 + P A 4 2
223 70 82 65 92 addsub4d φ A 4 8 4 + A 2 B 16 - A 2 B 8 + 3 256 A 4 = A 4 8 4 A 2 B 8 + A 2 B 16 - 3 256 A 4
224 102 222 223 3eqtr3rd φ A 4 8 4 A 2 B 8 + A 2 B 16 - 3 256 A 4 = A 4 256 + P A 4 2
225 224 oveq2d φ D + A 4 8 4 A 2 B 8 + A 2 B 16 3 256 A 4 = D + A 4 256 + P A 4 2
226 2 180 subcld φ B 3 8 A 2
227 5 226 eqeltrd φ P
228 227 181 mulcld φ P A 4 2
229 114 228 addcld φ A 4 256 + P A 4 2
230 4 229 negsubd φ D + A 4 256 + P A 4 2 = D A 4 256 + P A 4 2
231 99 225 230 3eqtrd φ A 4 8 4 A 2 B 8 + D + A 2 B 16 3 256 A 4 = D A 4 256 + P A 4 2
232 96 98 231 3eqtrd φ Q A 4 + R = D A 4 256 + P A 4 2
233 232 oveq2d φ A 4 256 + P A 4 2 + Q A 4 + R = A 4 256 + P A 4 2 + D A 4 256 + P A 4 2
234 229 4 pncan3d φ A 4 256 + P A 4 2 + D A 4 256 + P A 4 2 = D
235 233 234 eqtr2d φ D = A 4 256 + P A 4 2 + Q A 4 + R