Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mul4sqlem Structured version   Unicode version

Theorem mul4sqlem 14849
 Description: Lemma for mul4sq 14850: algebraic manipulations. The extra assumptions involving are for a part of 4sqlem17 14863 which needs to know not just that the product is a sum of squares, but also that it preserves divisibility by . (Contributed by Mario Carneiro, 14-Jul-2014.)
Hypotheses
Ref Expression
4sq.1
mul4sq.1
mul4sq.2
mul4sq.3
mul4sq.4
mul4sq.5
mul4sq.6
mul4sq.7
mul4sq.8
mul4sq.9
mul4sq.10
Assertion
Ref Expression
mul4sqlem
Distinct variable groups:   ,,,,   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   (,,,)   (,,,)   (,,,)   (,,,)   (,,,)   (,,,)   (,,,)   (,,,,)   (,,,,)

Proof of Theorem mul4sqlem
StepHypRef Expression
1 mul4sq.1 . . . . . . . . . . 11
2 gzcn 14828 . . . . . . . . . . 11
31, 2syl 17 . . . . . . . . . 10
4 mul4sq.3 . . . . . . . . . . 11
5 gzcn 14828 . . . . . . . . . . 11
64, 5syl 17 . . . . . . . . . 10
73, 6mulcld 9652 . . . . . . . . 9
87absvalsqd 13471 . . . . . . . 8
97cjcld 13227 . . . . . . . . 9
107, 9mulcld 9652 . . . . . . . 8
118, 10eqeltrd 2508 . . . . . . 7
12 mul4sq.2 . . . . . . . . . . 11
13 gzcn 14828 . . . . . . . . . . 11
1412, 13syl 17 . . . . . . . . . 10
15 mul4sq.4 . . . . . . . . . . 11
16 gzcn 14828 . . . . . . . . . . 11
1715, 16syl 17 . . . . . . . . . 10
1814, 17mulcld 9652 . . . . . . . . 9
1918absvalsqd 13471 . . . . . . . 8
2018cjcld 13227 . . . . . . . . 9
2118, 20mulcld 9652 . . . . . . . 8
2219, 21eqeltrd 2508 . . . . . . 7
2311, 22addcld 9651 . . . . . 6
243cjcld 13227 . . . . . . . . 9
2524, 6mulcld 9652 . . . . . . . 8
2614cjcld 13227 . . . . . . . . 9
2726, 17mulcld 9652 . . . . . . . 8
2825, 27mulcld 9652 . . . . . . 7
296cjcld 13227 . . . . . . . . 9
3014, 29mulcld 9652 . . . . . . . 8
3117cjcld 13227 . . . . . . . . 9
323, 31mulcld 9652 . . . . . . . 8
3330, 32mulcld 9652 . . . . . . 7
3428, 33addcld 9651 . . . . . 6
353, 17mulcld 9652 . . . . . . . . 9
3635absvalsqd 13471 . . . . . . . 8
3735cjcld 13227 . . . . . . . . 9
3835, 37mulcld 9652 . . . . . . . 8
3936, 38eqeltrd 2508 . . . . . . 7
4014, 6mulcld 9652 . . . . . . . . 9
4140absvalsqd 13471 . . . . . . . 8
4240cjcld 13227 . . . . . . . . 9
4340, 42mulcld 9652 . . . . . . . 8
4441, 43eqeltrd 2508 . . . . . . 7
4539, 44addcld 9651 . . . . . 6
4623, 34, 45ppncand 10015 . . . . 5
4714, 31mulcld 9652 . . . . . . . . 9
4825, 47addcld 9651 . . . . . . . 8
4948absvalsqd 13471 . . . . . . 7
5025, 47cjaddd 13251 . . . . . . . . 9
5124, 6cjmuld 13252 . . . . . . . . . . 11
523cjcjd 13230 . . . . . . . . . . . 12
5352oveq1d 6311 . . . . . . . . . . 11
5451, 53eqtrd 2461 . . . . . . . . . 10
5514, 31cjmuld 13252 . . . . . . . . . . 11
5617cjcjd 13230 . . . . . . . . . . . 12
5756oveq2d 6312 . . . . . . . . . . 11
5855, 57eqtrd 2461 . . . . . . . . . 10
5954, 58oveq12d 6314 . . . . . . . . 9
6050, 59eqtrd 2461 . . . . . . . 8
6160oveq2d 6312 . . . . . . 7
623, 29mulcld 9652 . . . . . . . . . . 11
6325, 62, 27adddid 9656 . . . . . . . . . 10
646, 24, 3, 29mul4d 9834 . . . . . . . . . . . . 13
6524, 6mulcomd 9653 . . . . . . . . . . . . . 14
6665oveq1d 6311 . . . . . . . . . . . . 13
673, 6mulcomd 9653 . . . . . . . . . . . . . 14
683, 6cjmuld 13252 . . . . . . . . . . . . . 14
6967, 68oveq12d 6314 . . . . . . . . . . . . 13
7064, 66, 693eqtr4d 2471 . . . . . . . . . . . 12
7170, 8eqtr4d 2464 . . . . . . . . . . 11
7271oveq1d 6311 . . . . . . . . . 10
7363, 72eqtrd 2461 . . . . . . . . 9
7447, 62, 27adddid 9656 . . . . . . . . . 10
753, 29mulcomd 9653 . . . . . . . . . . . . 13
7675oveq2d 6312 . . . . . . . . . . . 12
7714, 31, 29, 3mul4d 9834 . . . . . . . . . . . 12
7831, 3mulcomd 9653 . . . . . . . . . . . . 13
7978oveq2d 6312 . . . . . . . . . . . 12
8076, 77, 793eqtrd 2465 . . . . . . . . . . 11
8114, 31, 17, 26mul4d 9834 . . . . . . . . . . . . 13
8226, 17mulcomd 9653 . . . . . . . . . . . . . 14
8382oveq2d 6312 . . . . . . . . . . . . 13
8414, 17cjmuld 13252 . . . . . . . . . . . . . . 15
8526, 31mulcomd 9653 . . . . . . . . . . . . . . 15
8684, 85eqtrd 2461 . . . . . . . . . . . . . 14
8786oveq2d 6312 . . . . . . . . . . . . 13
8881, 83, 873eqtr4d 2471 . . . . . . . . . . . 12
8988, 19eqtr4d 2464 . . . . . . . . . . 11
9080, 89oveq12d 6314 . . . . . . . . . 10
9174, 90eqtrd 2461 . . . . . . . . 9
9273, 91oveq12d 6314 . . . . . . . 8
9362, 27addcld 9651 . . . . . . . . 9
9425, 47, 93adddird 9657 . . . . . . . 8
9511, 22, 28, 33add42d 9848 . . . . . . . 8
9692, 94, 953eqtr4d 2471 . . . . . . 7
9749, 61, 963eqtrd 2465 . . . . . 6
9824, 17mulcld 9652 . . . . . . . . 9
9998, 30subcld 9975 . . . . . . . 8
10099absvalsqd 13471 . . . . . . 7
101 cjsub 13180 . . . . . . . . . 10
10298, 30, 101syl2anc 665 . . . . . . . . 9
10324, 17cjmuld 13252 . . . . . . . . . . 11
10452oveq1d 6311 . . . . . . . . . . 11
105103, 104eqtrd 2461 . . . . . . . . . 10
10614, 29cjmuld 13252 . . . . . . . . . . 11
1076cjcjd 13230 . . . . . . . . . . . 12
108107oveq2d 6312 . . . . . . . . . . 11
109106, 108eqtrd 2461 . . . . . . . . . 10
110105, 109oveq12d 6314 . . . . . . . . 9
111102, 110eqtrd 2461 . . . . . . . 8
112111oveq2d 6312 . . . . . . 7
11326, 6mulcld 9652 . . . . . . . . . 10
11432, 113subcld 9975 . . . . . . . . 9
11598, 30, 114subdird 10064 . . . . . . . 8
11698, 32, 113subdid 10063 . . . . . . . . . 10
11717, 24, 3, 31mul4d 9834 . . . . . . . . . . . . 13
11824, 17mulcomd 9653 . . . . . . . . . . . . . 14
119118oveq1d 6311 . . . . . . . . . . . . 13
1203, 17mulcomd 9653 . . . . . . . . . . . . . 14
1213, 17cjmuld 13252 . . . . . . . . . . . . . 14
122120, 121oveq12d 6314 . . . . . . . . . . . . 13
123117, 119, 1223eqtr4d 2471 . . . . . . . . . . . 12
124123, 36eqtr4d 2464 . . . . . . . . . . 11
12526, 6mulcomd 9653 . . . . . . . . . . . . 13
126125oveq2d 6312 . . . . . . . . . . . 12
12724, 17, 6, 26mul4d 9834 . . . . . . . . . . . 12
12817, 26mulcomd 9653 . . . . . . . . . . . . 13
129128oveq2d 6312 . . . . . . . . . . . 12
130126, 127, 1293eqtrd 2465 . . . . . . . . . . 11
131124, 130oveq12d 6314 . . . . . . . . . 10
132116, 131eqtrd 2461 . . . . . . . . 9
13330, 32, 113subdid 10063 . . . . . . . . . 10
134125oveq2d 6312 . . . . . . . . . . . . 13
13514, 29, 6, 26mul4d 9834 . . . . . . . . . . . . 13
13629, 26mulcomd 9653 . . . . . . . . . . . . . . 15
13714, 6cjmuld 13252 . . . . . . . . . . . . . . 15
138136, 137eqtr4d 2464 . . . . . . . . . . . . . 14
139138oveq2d 6312 . . . . . . . . . . . . 13
140134, 135, 1393eqtrd 2465 . . . . . . . . . . . 12
141140, 41eqtr4d 2464 . . . . . . . . . . 11
142141oveq2d 6312 . . . . . . . . . 10
143133, 142eqtrd 2461 . . . . . . . . 9
144132, 143oveq12d 6314 . . . . . . . 8
14539, 28, 33, 44subadd4d 10023 . . . . . . . 8
146115, 144, 1453eqtrd 2465 . . . . . . 7
147100, 112, 1463eqtrd 2465 . . . . . 6
14897, 147oveq12d 6314 . . . . 5
1493, 24mulcld 9652 . . . . . . . 8
15014, 26mulcld 9652 . . . . . . . 8
1516, 29mulcld 9652 . . . . . . . . 9
15217, 31mulcld 9652 . . . . . . . . 9
153151, 152addcld 9651 . . . . . . . 8
154149, 150, 153adddird 9657 . . . . . . 7
15568oveq2d 6312 . . . . . . . . . . 11
1563, 6, 24, 29mul4d 9834 . . . . . . . . . . 11
1578, 155, 1563eqtrd 2465 . . . . . . . . . 10
158121oveq2d 6312 . . . . . . . . . . 11
1593, 17, 24, 31mul4d 9834 . . . . . . . . . . 11
16036, 158, 1593eqtrd 2465 . . . . . . . . . 10
161157, 160oveq12d 6314 . . . . . . . . 9
162149, 151, 152adddid 9656 . . . . . . . . 9
163161, 162eqtr4d 2464 . . . . . . . 8
164137oveq2d 6312 . . . . . . . . . . 11
16514, 6, 26, 29mul4d 9834 . . . . . . . . . . 11
16641, 164, 1653eqtrd 2465 . . . . . . . . . 10
16784oveq2d 6312 . . . . . . . . . . 11
16814, 17, 26, 31mul4d 9834 . . . . . . . . . . 11
16919, 167, 1683eqtrd 2465 . . . . . . . . . 10
170166, 169oveq12d 6314 . . . . . . . . 9
171150, 151, 152adddid 9656 . . . . . . . . 9
172170, 171eqtr4d 2464 . . . . . . . 8
173163, 172oveq12d 6314 . . . . . . 7
174154, 173eqtr4d 2464 . . . . . 6
175 mul4sq.5 . . . . . . . 8
1763absvalsqd 13471 . . . . . . . . 9
17714absvalsqd 13471 . . . . . . . . 9
178176, 177oveq12d 6314 . . . . . . . 8
179175, 178syl5eq 2473 . . . . . . 7
180 mul4sq.6 . . . . . . . 8
1816absvalsqd 13471 . . . . . . . . 9
18217absvalsqd 13471 . . . . . . . . 9
183181, 182oveq12d 6314 . . . . . . . 8
184180, 183syl5eq 2473 . . . . . . 7
185179, 184oveq12d 6314 . . . . . 6
18611, 22, 39, 44add42d 9848 . . . . . 6
187174, 185, 1863eqtr4d 2471 . . . . 5
18846, 148, 1873eqtr4d 2471 . . . 4
189188oveq1d 6311 . . 3
190 mul4sq.7 . . . . . . . . . 10
191190nncnd 10614 . . . . . . . . 9
192190nnne0d 10643 . . . . . . . . 9
19348, 191, 192absdivd 13484 . . . . . . . 8
194190nnred 10613 . . . . . . . . . 10
195190nnnn0d 10914 . . . . . . . . . . 11
196195nn0ge0d 10917 . . . . . . . . . 10
197194, 196absidd 13452 . . . . . . . . 9
198197oveq2d 6312 . . . . . . . 8
199193, 198eqtrd 2461 . . . . . . 7
200199oveq1d 6311 . . . . . 6
20148abscld 13465 . . . . . . . 8
202201recnd 9658 . . . . . . 7
203202, 191, 192sqdivd 12415 . . . . . 6
204200, 203eqtrd 2461 . . . . 5
20599, 191, 192absdivd 13484 . . . . . . . 8
206197oveq2d 6312 . . . . . . . 8
207205, 206eqtrd 2461 . . . . . . 7
208207oveq1d 6311 . . . . . 6
20999abscld 13465 . . . . . . . 8
210209recnd 9658 . . . . . . 7
211210, 191, 192sqdivd 12415 . . . . . 6
212208, 211eqtrd 2461 . . . . 5
213204, 212oveq12d 6314 . . . 4
21423, 34addcld 9651 . . . . . 6
21597, 214eqeltrd 2508 . . . . 5
21645, 34subcld 9975 . . . . . 6
217147, 216eqeltrd 2508 . . . . 5
218190nnsqcld 12422 . . . . . 6
219218nncnd 10614 . . . . 5
220218nnne0d 10643 . . . . 5
221215, 217, 219, 220divdird 10410 . . . 4
222213, 221eqtr4d 2464 . . 3
223176, 149eqeltrd 2508 . . . . . . 7
224177, 150eqeltrd 2508 . . . . . . 7
225223, 224addcld 9651 . . . . . 6
226175, 225syl5eqel 2512 . . . . 5
227184, 153eqeltrd 2508 . . . . 5
228226, 191, 227, 191, 192, 192divmuldivd 10413 . . . 4
229191sqvald 12399 . . . . 5
230229oveq2d 6312 . . . 4
231228, 230eqtr4d 2464 . . 3
232189, 222, 2313eqtr4d 2471 . 2
233226, 48nncand 9980 . . . . . . 7
234149, 150, 25, 47addsub4d 10022 . . . . . . . . 9
235179oveq1d 6311 . . . . . . . . 9
23624, 3, 6subdid 10063 . . . . . . . . . . 11
23724, 3mulcomd 9653 . . . . . . . . . . . 12
238237oveq1d 6311 . . . . . . . . . . 11
239236, 238eqtrd 2461 . . . . . . . . . 10
240 cjsub 13180 . . . . . . . . . . . . 13
24114, 17, 240syl2anc 665 . . . . . . . . . . . 12
242241oveq2d 6312 . . . . . . . . . . 11
24314, 26, 31subdid 10063 . . . . . . . . . . 11
244242, 243eqtrd 2461 . . . . . . . . . 10
245239, 244oveq12d 6314 . . . . . . . . 9
246234, 235, 2453eqtr4d 2471 . . . . . . . 8
247246oveq2d 6312 . . . . . . 7
248233, 247eqtr3d 2463 . . . . . 6
249248oveq1d 6311 . . . . 5
2503, 6subcld 9975 . . . . . . . 8
25124, 250mulcld 9652 . . . . . . 7
25214, 17subcld 9975 . . . . . . . . 9
253252cjcld 13227 . . . . . . . 8
25414, 253mulcld 9652 . . . . . . 7
255251, 254addcld 9651 . . . . . 6
256226, 255, 191, 192divsubdird 10411 . . . . 5
257251, 254, 191, 192divdird 10410 . . . . . . 7
25824, 250, 191, 192divassd 10407 . . . . . . . 8
25914, 253, 191, 192divassd 10407 . . . . . . . . 9
260252, 191, 192cjdivd 13254 . . . . . . . . . . 11
261194cjred 13257 . . . . . . . . . . . 12
262261oveq2d 6312 . . . . . . . . . . 11
263260, 262eqtrd 2461 . . . . . . . . . 10
264263oveq2d 6312 . . . . . . . . 9
265259, 264eqtr4d 2464 . . . . . . . 8
266258, 265oveq12d 6314 . . . . . . 7
267257, 266eqtrd 2461 . . . . . 6
268267oveq2d 6312 . . . . 5
269249, 256, 2683eqtrd 2465 . . . 4
270 mul4sq.10 . . . . . . 7
271270nn0zd 11027 . . . . . 6
272 zgz 14829 . . . . . 6
273271, 272syl 17 . . . . 5
274 gzcjcl 14832 . . . . . . . 8
2751, 274syl 17 . . . . . . 7
276 mul4sq.8 . . . . . . 7
277 gzmulcl 14834 . . . . . . 7
278275, 276, 277syl2anc 665 . . . . . 6
279 mul4sq.9 . . . . . . . 8
280 gzcjcl 14832 . . . . . . . 8
281279, 280syl 17 . . . . . . 7
282 gzmulcl 14834 . . . . . . 7
28312, 281, 282syl2anc 665 . . . . . 6
284 gzaddcl 14833 . . . . . 6
285278, 283, 284syl2anc 665 . . . . 5
286 gzsubcl 14836 . . . . 5
287273, 285, 286syl2anc 665 . . . 4
288269, 287eqeltrd 2508 . . 3
289250cjcld 13227 . . . . . . . 8
29014, 289mulcld 9652 . . . . . . 7
29124, 252mulcld 9652 . . . . . . 7
292290, 291, 191, 192divsubdird 10411 . . . . . 6
293 cjsub 13180 . . . . . . . . . . . 12
2943, 6, 293syl2anc 665 . . . . . . . . . . 11
295294oveq2d 6312 . . . . . . . . . 10
29614, 24, 29subdid 10063 . . . . . . . . . 10
297295, 296eqtrd 2461 . . . . . . . . 9
29824, 14, 17subdid 10063 . . . . . . . . . 10
29924, 14mulcomd 9653 . . . . . . . . . . 11
300299oveq1d 6311 . . . . . . . . . 10
301298, 300eqtrd 2461 . . . . . . . . 9
302297, 301oveq12d 6314 . . . . . . . 8
30314, 24mulcld 9652 . . . . . . . . 9
304303, 30, 98nnncan1d 10009 . . . . . . . 8
305302, 304eqtrd 2461 . . . . . . 7
306305oveq1d 6311 . . . . . 6
307292, 306eqtr3d 2463 . . . . 5
30814, 289, 191, 192divassd 10407 . . . . . . 7
309250, 191, 192cjdivd 13254 . . . . . . . . 9
310261oveq2d 6312 . . . . . . . . 9
311309, 310eqtrd 2461 . . . . . . . 8
312311oveq2d 6312 . . . . . . 7
313308, 312eqtr4d 2464 . . . . . 6
31424, 252, 191, 192divassd 10407 . . . . . 6
315313, 314oveq12d 6314 . . . . 5
316307, 315eqtr3d 2463 . . . 4
317 gzcjcl 14832 . . . . . . 7
318276, 317syl 17 . . . . . 6
319 gzmulcl 14834 . . . . . 6
32012, 318, 319syl2anc 665 . . . . 5
321 gzmulcl 14834 . . . . . 6
322275, 279, 321syl2anc 665 . . . . 5
323 gzsubcl 14836 . . . . 5
324320, 322, 323syl2anc 665 . . . 4
325316, 324eqeltrd 2508 . . 3
326 4sq.1 . . . 4
3273264sqlem4a 14847 . . 3
328288, 325, 327syl2anc 665 . 2
329232, 328eqeltrrd 2509 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wceq 1437   wcel 1867  cab 2405  wrex 2774  cfv 5592  (class class class)co 6296  cc 9526   caddc 9531   cmul 9533   cmin 9849   cdiv 10258  cn 10598  c2 10648  cn0 10858  cz 10926  cexp 12258  ccj 13127  cabs 13265  cgz 14825 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6588  ax-cnex 9584  ax-resscn 9585  ax-1cn 9586  ax-icn 9587  ax-addcl 9588  ax-addrcl 9589  ax-mulcl 9590  ax-mulrcl 9591  ax-mulcom 9592  ax-addass 9593  ax-mulass 9594  ax-distr 9595  ax-i2m1 9596  ax-1ne0 9597  ax-1rid 9598  ax-rnegex 9599  ax-rrecex 9600  ax-cnre 9601  ax-pre-lttri 9602  ax-pre-lttrn 9603  ax-pre-ltadd 9604  ax-pre-mulgt0 9605  ax-pre-sup 9606 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-nel 2619  df-ral 2778  df-rex 2779  df-reu 2780  df-rmo 2781  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-pss 3449  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-tp 3998  df-op 4000  df-uni 4214  df-iun 4295  df-br 4418  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4756  df-id 4760  df-po 4766  df-so 4767  df-fr 4804  df-we 4806  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-pred 5390  df-ord 5436  df-on 5437  df-lim 5438  df-suc 5439  df-iota 5556  df-fun 5594  df-fn 5595  df-f 5596  df-f1 5597  df-fo 5598  df-f1o 5599  df-fv 5600  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6698  df-2nd 6799  df-wrecs 7027  df-recs 7089  df-rdg 7127  df-er 7362  df-en 7569  df-dom 7570  df-sdom 7571  df-sup 7953  df-pnf 9666  df-mnf 9667  df-xr 9668  df-ltxr 9669  df-le 9670  df-sub 9851  df-neg 9852  df-div 10259  df-nn 10599  df-2 10657  df-3 10658  df-n0 10859  df-z 10927  df-uz 11149  df-rp 11292  df-seq 12200  df-exp 12259  df-cj 13130  df-re 13131  df-im 13132  df-sqrt 13266  df-abs 13267  df-gz 14826 This theorem is referenced by:  mul4sq  14850  4sqlem17OLD  14857  4sqlem17  14863
 Copyright terms: Public domain W3C validator