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

Theorem mul4sqlem 14326
 Description: Lemma for mul4sq 14327: algebraic manipulations. The extra assumptions involving are for a part of 4sqlem17 14334 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 14305 . . . . . . . . . . 11
31, 2syl 16 . . . . . . . . . 10
4 mul4sq.3 . . . . . . . . . . 11
5 gzcn 14305 . . . . . . . . . . 11
64, 5syl 16 . . . . . . . . . 10
73, 6mulcld 9612 . . . . . . . . 9
87absvalsqd 13232 . . . . . . . 8
97cjcld 12988 . . . . . . . . 9
107, 9mulcld 9612 . . . . . . . 8
118, 10eqeltrd 2555 . . . . . . 7
12 mul4sq.2 . . . . . . . . . . 11
13 gzcn 14305 . . . . . . . . . . 11
1412, 13syl 16 . . . . . . . . . 10
15 mul4sq.4 . . . . . . . . . . 11
16 gzcn 14305 . . . . . . . . . . 11
1715, 16syl 16 . . . . . . . . . 10
1814, 17mulcld 9612 . . . . . . . . 9
1918absvalsqd 13232 . . . . . . . 8
2018cjcld 12988 . . . . . . . . 9
2118, 20mulcld 9612 . . . . . . . 8
2219, 21eqeltrd 2555 . . . . . . 7
2311, 22addcld 9611 . . . . . 6
243cjcld 12988 . . . . . . . . 9
2524, 6mulcld 9612 . . . . . . . 8
2614cjcld 12988 . . . . . . . . 9
2726, 17mulcld 9612 . . . . . . . 8
2825, 27mulcld 9612 . . . . . . 7
296cjcld 12988 . . . . . . . . 9
3014, 29mulcld 9612 . . . . . . . 8
3117cjcld 12988 . . . . . . . . 9
323, 31mulcld 9612 . . . . . . . 8
3330, 32mulcld 9612 . . . . . . 7
3428, 33addcld 9611 . . . . . 6
353, 17mulcld 9612 . . . . . . . . 9
3635absvalsqd 13232 . . . . . . . 8
3735cjcld 12988 . . . . . . . . 9
3835, 37mulcld 9612 . . . . . . . 8
3936, 38eqeltrd 2555 . . . . . . 7
4014, 6mulcld 9612 . . . . . . . . 9
4140absvalsqd 13232 . . . . . . . 8
4240cjcld 12988 . . . . . . . . 9
4340, 42mulcld 9612 . . . . . . . 8
4441, 43eqeltrd 2555 . . . . . . 7
4539, 44addcld 9611 . . . . . 6
4623, 34, 45ppncand 9966 . . . . 5
4714, 31mulcld 9612 . . . . . . . . 9
4825, 47addcld 9611 . . . . . . . 8
4948absvalsqd 13232 . . . . . . 7
5025, 47cjaddd 13012 . . . . . . . . 9
5124, 6cjmuld 13013 . . . . . . . . . . 11
523cjcjd 12991 . . . . . . . . . . . 12
5352oveq1d 6297 . . . . . . . . . . 11
5451, 53eqtrd 2508 . . . . . . . . . 10
5514, 31cjmuld 13013 . . . . . . . . . . 11
5617cjcjd 12991 . . . . . . . . . . . 12
5756oveq2d 6298 . . . . . . . . . . 11
5855, 57eqtrd 2508 . . . . . . . . . 10
5954, 58oveq12d 6300 . . . . . . . . 9
6050, 59eqtrd 2508 . . . . . . . 8
6160oveq2d 6298 . . . . . . 7
623, 29mulcld 9612 . . . . . . . . . . 11
6325, 62, 27adddid 9616 . . . . . . . . . 10
646, 24, 3, 29mul4d 9787 . . . . . . . . . . . . 13
6524, 6mulcomd 9613 . . . . . . . . . . . . . 14
6665oveq1d 6297 . . . . . . . . . . . . 13
673, 6mulcomd 9613 . . . . . . . . . . . . . 14
683, 6cjmuld 13013 . . . . . . . . . . . . . 14
6967, 68oveq12d 6300 . . . . . . . . . . . . 13
7064, 66, 693eqtr4d 2518 . . . . . . . . . . . 12
7170, 8eqtr4d 2511 . . . . . . . . . . 11
7271oveq1d 6297 . . . . . . . . . 10
7363, 72eqtrd 2508 . . . . . . . . 9
7447, 62, 27adddid 9616 . . . . . . . . . 10
753, 29mulcomd 9613 . . . . . . . . . . . . 13
7675oveq2d 6298 . . . . . . . . . . . 12
7714, 31, 29, 3mul4d 9787 . . . . . . . . . . . 12
7831, 3mulcomd 9613 . . . . . . . . . . . . 13
7978oveq2d 6298 . . . . . . . . . . . 12
8076, 77, 793eqtrd 2512 . . . . . . . . . . 11
8114, 31, 17, 26mul4d 9787 . . . . . . . . . . . . 13
8226, 17mulcomd 9613 . . . . . . . . . . . . . 14
8382oveq2d 6298 . . . . . . . . . . . . 13
8414, 17cjmuld 13013 . . . . . . . . . . . . . . 15
8526, 31mulcomd 9613 . . . . . . . . . . . . . . 15
8684, 85eqtrd 2508 . . . . . . . . . . . . . 14
8786oveq2d 6298 . . . . . . . . . . . . 13
8881, 83, 873eqtr4d 2518 . . . . . . . . . . . 12
8988, 19eqtr4d 2511 . . . . . . . . . . 11
9080, 89oveq12d 6300 . . . . . . . . . 10
9174, 90eqtrd 2508 . . . . . . . . 9
9273, 91oveq12d 6300 . . . . . . . 8
9362, 27addcld 9611 . . . . . . . . 9
9425, 47, 93adddird 9617 . . . . . . . 8
9511, 22, 28, 33add42d 9800 . . . . . . . 8
9692, 94, 953eqtr4d 2518 . . . . . . 7
9749, 61, 963eqtrd 2512 . . . . . 6
9824, 17mulcld 9612 . . . . . . . . 9
9998, 30subcld 9926 . . . . . . . 8
10099absvalsqd 13232 . . . . . . 7
101 cjsub 12941 . . . . . . . . . 10
10298, 30, 101syl2anc 661 . . . . . . . . 9
10324, 17cjmuld 13013 . . . . . . . . . . 11
10452oveq1d 6297 . . . . . . . . . . 11
105103, 104eqtrd 2508 . . . . . . . . . 10
10614, 29cjmuld 13013 . . . . . . . . . . 11
1076cjcjd 12991 . . . . . . . . . . . 12
108107oveq2d 6298 . . . . . . . . . . 11
109106, 108eqtrd 2508 . . . . . . . . . 10
110105, 109oveq12d 6300 . . . . . . . . 9
111102, 110eqtrd 2508 . . . . . . . 8
112111oveq2d 6298 . . . . . . 7
11326, 6mulcld 9612 . . . . . . . . . 10
11432, 113subcld 9926 . . . . . . . . 9
11598, 30, 114subdird 10009 . . . . . . . 8
11698, 32, 113subdid 10008 . . . . . . . . . 10
11717, 24, 3, 31mul4d 9787 . . . . . . . . . . . . 13
11824, 17mulcomd 9613 . . . . . . . . . . . . . 14
119118oveq1d 6297 . . . . . . . . . . . . 13
1203, 17mulcomd 9613 . . . . . . . . . . . . . 14
1213, 17cjmuld 13013 . . . . . . . . . . . . . 14
122120, 121oveq12d 6300 . . . . . . . . . . . . 13
123117, 119, 1223eqtr4d 2518 . . . . . . . . . . . 12
124123, 36eqtr4d 2511 . . . . . . . . . . 11
12526, 6mulcomd 9613 . . . . . . . . . . . . 13
126125oveq2d 6298 . . . . . . . . . . . 12
12724, 17, 6, 26mul4d 9787 . . . . . . . . . . . 12
12817, 26mulcomd 9613 . . . . . . . . . . . . 13
129128oveq2d 6298 . . . . . . . . . . . 12
130126, 127, 1293eqtrd 2512 . . . . . . . . . . 11
131124, 130oveq12d 6300 . . . . . . . . . 10
132116, 131eqtrd 2508 . . . . . . . . 9
13330, 32, 113subdid 10008 . . . . . . . . . 10
134125oveq2d 6298 . . . . . . . . . . . . 13
13514, 29, 6, 26mul4d 9787 . . . . . . . . . . . . 13
13629, 26mulcomd 9613 . . . . . . . . . . . . . . 15
13714, 6cjmuld 13013 . . . . . . . . . . . . . . 15
138136, 137eqtr4d 2511 . . . . . . . . . . . . . 14
139138oveq2d 6298 . . . . . . . . . . . . 13
140134, 135, 1393eqtrd 2512 . . . . . . . . . . . 12
141140, 41eqtr4d 2511 . . . . . . . . . . 11
142141oveq2d 6298 . . . . . . . . . 10
143133, 142eqtrd 2508 . . . . . . . . 9
144132, 143oveq12d 6300 . . . . . . . 8
14539, 28, 33, 44subadd4d 9974 . . . . . . . 8
146115, 144, 1453eqtrd 2512 . . . . . . 7
147100, 112, 1463eqtrd 2512 . . . . . 6
14897, 147oveq12d 6300 . . . . 5
1493, 24mulcld 9612 . . . . . . . 8
15014, 26mulcld 9612 . . . . . . . 8
1516, 29mulcld 9612 . . . . . . . . 9
15217, 31mulcld 9612 . . . . . . . . 9
153151, 152addcld 9611 . . . . . . . 8
154149, 150, 153adddird 9617 . . . . . . 7
15568oveq2d 6298 . . . . . . . . . . 11
1563, 6, 24, 29mul4d 9787 . . . . . . . . . . 11
1578, 155, 1563eqtrd 2512 . . . . . . . . . 10
158121oveq2d 6298 . . . . . . . . . . 11
1593, 17, 24, 31mul4d 9787 . . . . . . . . . . 11
16036, 158, 1593eqtrd 2512 . . . . . . . . . 10
161157, 160oveq12d 6300 . . . . . . . . 9
162149, 151, 152adddid 9616 . . . . . . . . 9
163161, 162eqtr4d 2511 . . . . . . . 8
164137oveq2d 6298 . . . . . . . . . . 11
16514, 6, 26, 29mul4d 9787 . . . . . . . . . . 11
16641, 164, 1653eqtrd 2512 . . . . . . . . . 10
16784oveq2d 6298 . . . . . . . . . . 11
16814, 17, 26, 31mul4d 9787 . . . . . . . . . . 11
16919, 167, 1683eqtrd 2512 . . . . . . . . . 10
170166, 169oveq12d 6300 . . . . . . . . 9
171150, 151, 152adddid 9616 . . . . . . . . 9
172170, 171eqtr4d 2511 . . . . . . . 8
173163, 172oveq12d 6300 . . . . . . 7
174154, 173eqtr4d 2511 . . . . . 6
175 mul4sq.5 . . . . . . . 8
1763absvalsqd 13232 . . . . . . . . 9
17714absvalsqd 13232 . . . . . . . . 9
178176, 177oveq12d 6300 . . . . . . . 8
179175, 178syl5eq 2520 . . . . . . 7
180 mul4sq.6 . . . . . . . 8
1816absvalsqd 13232 . . . . . . . . 9
18217absvalsqd 13232 . . . . . . . . 9
183181, 182oveq12d 6300 . . . . . . . 8
184180, 183syl5eq 2520 . . . . . . 7
185179, 184oveq12d 6300 . . . . . 6
18611, 22, 39, 44add42d 9800 . . . . . 6
187174, 185, 1863eqtr4d 2518 . . . . 5
18846, 148, 1873eqtr4d 2518 . . . 4
189188oveq1d 6297 . . 3
190 mul4sq.7 . . . . . . . . . 10
191190nncnd 10548 . . . . . . . . 9
192190nnne0d 10576 . . . . . . . . 9
19348, 191, 192absdivd 13245 . . . . . . . 8
194190nnred 10547 . . . . . . . . . 10
195190nnnn0d 10848 . . . . . . . . . . 11
196195nn0ge0d 10851 . . . . . . . . . 10
197194, 196absidd 13213 . . . . . . . . 9
198197oveq2d 6298 . . . . . . . 8
199193, 198eqtrd 2508 . . . . . . 7
200199oveq1d 6297 . . . . . 6
20148abscld 13226 . . . . . . . 8
202201recnd 9618 . . . . . . 7
203202, 191, 192sqdivd 12287 . . . . . 6
204200, 203eqtrd 2508 . . . . 5
20599, 191, 192absdivd 13245 . . . . . . . 8
206197oveq2d 6298 . . . . . . . 8
207205, 206eqtrd 2508 . . . . . . 7
208207oveq1d 6297 . . . . . 6
20999abscld 13226 . . . . . . . 8
210209recnd 9618 . . . . . . 7
211210, 191, 192sqdivd 12287 . . . . . 6
212208, 211eqtrd 2508 . . . . 5
213204, 212oveq12d 6300 . . . 4
21423, 34addcld 9611 . . . . . 6
21597, 214eqeltrd 2555 . . . . 5
21645, 34subcld 9926 . . . . . 6
217147, 216eqeltrd 2555 . . . . 5
218190nnsqcld 12294 . . . . . 6
219218nncnd 10548 . . . . 5
220218nnne0d 10576 . . . . 5
221215, 217, 219, 220divdird 10354 . . . 4
222213, 221eqtr4d 2511 . . 3
223176, 149eqeltrd 2555 . . . . . . 7
224177, 150eqeltrd 2555 . . . . . . 7
225223, 224addcld 9611 . . . . . 6
226175, 225syl5eqel 2559 . . . . 5
227184, 153eqeltrd 2555 . . . . 5
228226, 191, 227, 191, 192, 192divmuldivd 10357 . . . 4
229191sqvald 12271 . . . . 5
230229oveq2d 6298 . . . 4
231228, 230eqtr4d 2511 . . 3
232189, 222, 2313eqtr4d 2518 . 2
233226, 48nncand 9931 . . . . . . 7
234149, 150, 25, 47addsub4d 9973 . . . . . . . . 9
235179oveq1d 6297 . . . . . . . . 9
23624, 3, 6subdid 10008 . . . . . . . . . . 11
23724, 3mulcomd 9613 . . . . . . . . . . . 12
238237oveq1d 6297 . . . . . . . . . . 11
239236, 238eqtrd 2508 . . . . . . . . . 10
240 cjsub 12941 . . . . . . . . . . . . 13
24114, 17, 240syl2anc 661 . . . . . . . . . . . 12
242241oveq2d 6298 . . . . . . . . . . 11
24314, 26, 31subdid 10008 . . . . . . . . . . 11
244242, 243eqtrd 2508 . . . . . . . . . 10
245239, 244oveq12d 6300 . . . . . . . . 9
246234, 235, 2453eqtr4d 2518 . . . . . . . 8
247246oveq2d 6298 . . . . . . 7
248233, 247eqtr3d 2510 . . . . . 6
249248oveq1d 6297 . . . . 5
2503, 6subcld 9926 . . . . . . . 8
25124, 250mulcld 9612 . . . . . . 7
25214, 17subcld 9926 . . . . . . . . 9
253252cjcld 12988 . . . . . . . 8
25414, 253mulcld 9612 . . . . . . 7
255251, 254addcld 9611 . . . . . 6
256226, 255, 191, 192divsubdird 10355 . . . . 5
257251, 254, 191, 192divdird 10354 . . . . . . 7
25824, 250, 191, 192divassd 10351 . . . . . . . 8
25914, 253, 191, 192divassd 10351 . . . . . . . . 9
260252, 191, 192cjdivd 13015 . . . . . . . . . . 11
261194cjred 13018 . . . . . . . . . . . 12
262261oveq2d 6298 . . . . . . . . . . 11
263260, 262eqtrd 2508 . . . . . . . . . 10
264263oveq2d 6298 . . . . . . . . 9
265259, 264eqtr4d 2511 . . . . . . . 8
266258, 265oveq12d 6300 . . . . . . 7
267257, 266eqtrd 2508 . . . . . 6
268267oveq2d 6298 . . . . 5
269249, 256, 2683eqtrd 2512 . . . 4
270 mul4sq.10 . . . . . . 7
271270nn0zd 10960 . . . . . 6
272 zgz 14306 . . . . . 6
273271, 272syl 16 . . . . 5
274 gzcjcl 14309 . . . . . . . 8
2751, 274syl 16 . . . . . . 7
276 mul4sq.8 . . . . . . 7
277 gzmulcl 14311 . . . . . . 7
278275, 276, 277syl2anc 661 . . . . . 6
279 mul4sq.9 . . . . . . . 8
280 gzcjcl 14309 . . . . . . . 8
281279, 280syl 16 . . . . . . 7
282 gzmulcl 14311 . . . . . . 7
28312, 281, 282syl2anc 661 . . . . . 6
284 gzaddcl 14310 . . . . . 6
285278, 283, 284syl2anc 661 . . . . 5
286 gzsubcl 14313 . . . . 5
287273, 285, 286syl2anc 661 . . . 4
288269, 287eqeltrd 2555 . . 3
289250cjcld 12988 . . . . . . . 8
29014, 289mulcld 9612 . . . . . . 7
29124, 252mulcld 9612 . . . . . . 7
292290, 291, 191, 192divsubdird 10355 . . . . . 6
293 cjsub 12941 . . . . . . . . . . . 12
2943, 6, 293syl2anc 661 . . . . . . . . . . 11
295294oveq2d 6298 . . . . . . . . . 10
29614, 24, 29subdid 10008 . . . . . . . . . 10
297295, 296eqtrd 2508 . . . . . . . . 9
29824, 14, 17subdid 10008 . . . . . . . . . 10
29924, 14mulcomd 9613 . . . . . . . . . . 11
300299oveq1d 6297 . . . . . . . . . 10
301298, 300eqtrd 2508 . . . . . . . . 9
302297, 301oveq12d 6300 . . . . . . . 8
30314, 24mulcld 9612 . . . . . . . . 9
304303, 30, 98nnncan1d 9960 . . . . . . . 8
305302, 304eqtrd 2508 . . . . . . 7
306305oveq1d 6297 . . . . . 6
307292, 306eqtr3d 2510 . . . . 5
30814, 289, 191, 192divassd 10351 . . . . . . 7
309250, 191, 192cjdivd 13015 . . . . . . . . 9
310261oveq2d 6298 . . . . . . . . 9
311309, 310eqtrd 2508 . . . . . . . 8
312311oveq2d 6298 . . . . . . 7
313308, 312eqtr4d 2511 . . . . . 6
31424, 252, 191, 192divassd 10351 . . . . . 6
315313, 314oveq12d 6300 . . . . 5
316307, 315eqtr3d 2510 . . . 4
317 gzcjcl 14309 . . . . . . 7
318276, 317syl 16 . . . . . 6
319 gzmulcl 14311 . . . . . 6
32012, 318, 319syl2anc 661 . . . . 5
321 gzmulcl 14311 . . . . . 6
322275, 279, 321syl2anc 661 . . . . 5
323 gzsubcl 14313 . . . . 5
324320, 322, 323syl2anc 661 . . . 4
325316, 324eqeltrd 2555 . . 3
326 4sq.1 . . . 4
3273264sqlem4a 14324 . . 3
328288, 325, 327syl2anc 661 . 2
329232, 328eqeltrrd 2556 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wceq 1379   wcel 1767  cab 2452  wrex 2815  cfv 5586  (class class class)co 6282  cc 9486   caddc 9491   cmul 9493   cmin 9801   cdiv 10202  cn 10532  c2 10581  cn0 10791  cz 10860  cexp 12130  ccj 12888  cabs 13026  cgz 14302 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574  ax-cnex 9544  ax-resscn 9545  ax-1cn 9546  ax-icn 9547  ax-addcl 9548  ax-addrcl 9549  ax-mulcl 9550  ax-mulrcl 9551  ax-mulcom 9552  ax-addass 9553  ax-mulass 9554  ax-distr 9555  ax-i2m1 9556  ax-1ne0 9557  ax-1rid 9558  ax-rnegex 9559  ax-rrecex 9560  ax-cnre 9561  ax-pre-lttri 9562  ax-pre-lttrn 9563  ax-pre-ltadd 9564  ax-pre-mulgt0 9565  ax-pre-sup 9566 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-riota 6243  df-ov 6285  df-oprab 6286  df-mpt2 6287  df-om 6679  df-2nd 6782  df-recs 7039  df-rdg 7073  df-er 7308  df-en 7514  df-dom 7515  df-sdom 7516  df-sup 7897  df-pnf 9626  df-mnf 9627  df-xr 9628  df-ltxr 9629  df-le 9630  df-sub 9803  df-neg 9804  df-div 10203  df-nn 10533  df-2 10590  df-3 10591  df-n0 10792  df-z 10861  df-uz 11079  df-rp 11217  df-seq 12072  df-exp 12131  df-cj 12891  df-re 12892  df-im 12893  df-sqrt 13027  df-abs 13028  df-gz 14303 This theorem is referenced by:  mul4sq  14327  4sqlem17  14334
 Copyright terms: Public domain W3C validator