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

Theorem mul4sqlem 13323
 Description: Lemma for mul4sq 13324: algebraic manipulations. The extra assumptions involving are for a part of 4sqlem17 13331 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 13302 . . . . . . . . . . 11
31, 2syl 16 . . . . . . . . . 10
4 mul4sq.3 . . . . . . . . . . 11
5 gzcn 13302 . . . . . . . . . . 11
64, 5syl 16 . . . . . . . . . 10
73, 6mulcld 9110 . . . . . . . . 9
87absvalsqd 12246 . . . . . . . 8
97cjcld 12003 . . . . . . . . 9
107, 9mulcld 9110 . . . . . . . 8
118, 10eqeltrd 2512 . . . . . . 7
12 mul4sq.2 . . . . . . . . . . 11
13 gzcn 13302 . . . . . . . . . . 11
1412, 13syl 16 . . . . . . . . . 10
15 mul4sq.4 . . . . . . . . . . 11
16 gzcn 13302 . . . . . . . . . . 11
1715, 16syl 16 . . . . . . . . . 10
1814, 17mulcld 9110 . . . . . . . . 9
1918absvalsqd 12246 . . . . . . . 8
2018cjcld 12003 . . . . . . . . 9
2118, 20mulcld 9110 . . . . . . . 8
2219, 21eqeltrd 2512 . . . . . . 7
2311, 22addcld 9109 . . . . . 6
243cjcld 12003 . . . . . . . . 9
2524, 6mulcld 9110 . . . . . . . 8
2614cjcld 12003 . . . . . . . . 9
2726, 17mulcld 9110 . . . . . . . 8
2825, 27mulcld 9110 . . . . . . 7
296cjcld 12003 . . . . . . . . 9
3014, 29mulcld 9110 . . . . . . . 8
3117cjcld 12003 . . . . . . . . 9
323, 31mulcld 9110 . . . . . . . 8
3330, 32mulcld 9110 . . . . . . 7
3428, 33addcld 9109 . . . . . 6
353, 17mulcld 9110 . . . . . . . . 9
3635absvalsqd 12246 . . . . . . . 8
3735cjcld 12003 . . . . . . . . 9
3835, 37mulcld 9110 . . . . . . . 8
3936, 38eqeltrd 2512 . . . . . . 7
4014, 6mulcld 9110 . . . . . . . . 9
4140absvalsqd 12246 . . . . . . . 8
4240cjcld 12003 . . . . . . . . 9
4340, 42mulcld 9110 . . . . . . . 8
4441, 43eqeltrd 2512 . . . . . . 7
4539, 44addcld 9109 . . . . . 6
4623, 34, 45ppncand 9453 . . . . 5
4714, 31mulcld 9110 . . . . . . . . 9
4825, 47addcld 9109 . . . . . . . 8
4948absvalsqd 12246 . . . . . . 7
5025, 47cjaddd 12027 . . . . . . . . 9
5124, 6cjmuld 12028 . . . . . . . . . . 11
523cjcjd 12006 . . . . . . . . . . . 12
5352oveq1d 6098 . . . . . . . . . . 11
5451, 53eqtrd 2470 . . . . . . . . . 10
5514, 31cjmuld 12028 . . . . . . . . . . 11
5617cjcjd 12006 . . . . . . . . . . . 12
5756oveq2d 6099 . . . . . . . . . . 11
5855, 57eqtrd 2470 . . . . . . . . . 10
5954, 58oveq12d 6101 . . . . . . . . 9
6050, 59eqtrd 2470 . . . . . . . 8
6160oveq2d 6099 . . . . . . 7
623, 29mulcld 9110 . . . . . . . . . . 11
6325, 62, 27adddid 9114 . . . . . . . . . 10
646, 24, 3, 29mul4d 9280 . . . . . . . . . . . . 13
6524, 6mulcomd 9111 . . . . . . . . . . . . . 14
6665oveq1d 6098 . . . . . . . . . . . . 13
673, 6mulcomd 9111 . . . . . . . . . . . . . 14
683, 6cjmuld 12028 . . . . . . . . . . . . . 14
6967, 68oveq12d 6101 . . . . . . . . . . . . 13
7064, 66, 693eqtr4d 2480 . . . . . . . . . . . 12
7170, 8eqtr4d 2473 . . . . . . . . . . 11
7271oveq1d 6098 . . . . . . . . . 10
7363, 72eqtrd 2470 . . . . . . . . 9
7447, 62, 27adddid 9114 . . . . . . . . . 10
753, 29mulcomd 9111 . . . . . . . . . . . . 13
7675oveq2d 6099 . . . . . . . . . . . 12
7714, 31, 29, 3mul4d 9280 . . . . . . . . . . . 12
7831, 3mulcomd 9111 . . . . . . . . . . . . 13
7978oveq2d 6099 . . . . . . . . . . . 12
8076, 77, 793eqtrd 2474 . . . . . . . . . . 11
8114, 31, 17, 26mul4d 9280 . . . . . . . . . . . . 13
8226, 17mulcomd 9111 . . . . . . . . . . . . . 14
8382oveq2d 6099 . . . . . . . . . . . . 13
8414, 17cjmuld 12028 . . . . . . . . . . . . . . 15
8526, 31mulcomd 9111 . . . . . . . . . . . . . . 15
8684, 85eqtrd 2470 . . . . . . . . . . . . . 14
8786oveq2d 6099 . . . . . . . . . . . . 13
8881, 83, 873eqtr4d 2480 . . . . . . . . . . . 12
8988, 19eqtr4d 2473 . . . . . . . . . . 11
9080, 89oveq12d 6101 . . . . . . . . . 10
9174, 90eqtrd 2470 . . . . . . . . 9
9273, 91oveq12d 6101 . . . . . . . 8
9362, 27addcld 9109 . . . . . . . . 9
9425, 47, 93adddird 9115 . . . . . . . 8
9511, 22, 28, 33add42d 9292 . . . . . . . 8
9692, 94, 953eqtr4d 2480 . . . . . . 7
9749, 61, 963eqtrd 2474 . . . . . 6
9824, 17mulcld 9110 . . . . . . . . 9
9998, 30subcld 9413 . . . . . . . 8
10099absvalsqd 12246 . . . . . . 7
101 cjsub 11956 . . . . . . . . . 10
10298, 30, 101syl2anc 644 . . . . . . . . 9
10324, 17cjmuld 12028 . . . . . . . . . . 11
10452oveq1d 6098 . . . . . . . . . . 11
105103, 104eqtrd 2470 . . . . . . . . . 10
10614, 29cjmuld 12028 . . . . . . . . . . 11
1076cjcjd 12006 . . . . . . . . . . . 12
108107oveq2d 6099 . . . . . . . . . . 11
109106, 108eqtrd 2470 . . . . . . . . . 10
110105, 109oveq12d 6101 . . . . . . . . 9
111102, 110eqtrd 2470 . . . . . . . 8
112111oveq2d 6099 . . . . . . 7
11326, 6mulcld 9110 . . . . . . . . . 10
11432, 113subcld 9413 . . . . . . . . 9
11598, 30, 114subdird 9492 . . . . . . . 8
11698, 32, 113subdid 9491 . . . . . . . . . 10
11717, 24, 3, 31mul4d 9280 . . . . . . . . . . . . 13
11824, 17mulcomd 9111 . . . . . . . . . . . . . 14
119118oveq1d 6098 . . . . . . . . . . . . 13
1203, 17mulcomd 9111 . . . . . . . . . . . . . 14
1213, 17cjmuld 12028 . . . . . . . . . . . . . 14
122120, 121oveq12d 6101 . . . . . . . . . . . . 13
123117, 119, 1223eqtr4d 2480 . . . . . . . . . . . 12
124123, 36eqtr4d 2473 . . . . . . . . . . 11
12526, 6mulcomd 9111 . . . . . . . . . . . . 13
126125oveq2d 6099 . . . . . . . . . . . 12
12724, 17, 6, 26mul4d 9280 . . . . . . . . . . . 12
12817, 26mulcomd 9111 . . . . . . . . . . . . 13
129128oveq2d 6099 . . . . . . . . . . . 12
130126, 127, 1293eqtrd 2474 . . . . . . . . . . 11
131124, 130oveq12d 6101 . . . . . . . . . 10
132116, 131eqtrd 2470 . . . . . . . . 9
13330, 32, 113subdid 9491 . . . . . . . . . 10
134125oveq2d 6099 . . . . . . . . . . . . 13
13514, 29, 6, 26mul4d 9280 . . . . . . . . . . . . 13
13629, 26mulcomd 9111 . . . . . . . . . . . . . . 15
13714, 6cjmuld 12028 . . . . . . . . . . . . . . 15
138136, 137eqtr4d 2473 . . . . . . . . . . . . . 14
139138oveq2d 6099 . . . . . . . . . . . . 13
140134, 135, 1393eqtrd 2474 . . . . . . . . . . . 12
141140, 41eqtr4d 2473 . . . . . . . . . . 11
142141oveq2d 6099 . . . . . . . . . 10
143133, 142eqtrd 2470 . . . . . . . . 9
144132, 143oveq12d 6101 . . . . . . . 8
14539, 28, 33, 44subadd4d 9461 . . . . . . . 8
146115, 144, 1453eqtrd 2474 . . . . . . 7
147100, 112, 1463eqtrd 2474 . . . . . 6
14897, 147oveq12d 6101 . . . . 5
1493, 24mulcld 9110 . . . . . . . 8
15014, 26mulcld 9110 . . . . . . . 8
1516, 29mulcld 9110 . . . . . . . . 9
15217, 31mulcld 9110 . . . . . . . . 9
153151, 152addcld 9109 . . . . . . . 8
154149, 150, 153adddird 9115 . . . . . . 7
15568oveq2d 6099 . . . . . . . . . . 11
1563, 6, 24, 29mul4d 9280 . . . . . . . . . . 11
1578, 155, 1563eqtrd 2474 . . . . . . . . . 10
158121oveq2d 6099 . . . . . . . . . . 11
1593, 17, 24, 31mul4d 9280 . . . . . . . . . . 11
16036, 158, 1593eqtrd 2474 . . . . . . . . . 10
161157, 160oveq12d 6101 . . . . . . . . 9
162149, 151, 152adddid 9114 . . . . . . . . 9
163161, 162eqtr4d 2473 . . . . . . . 8
164137oveq2d 6099 . . . . . . . . . . 11
16514, 6, 26, 29mul4d 9280 . . . . . . . . . . 11
16641, 164, 1653eqtrd 2474 . . . . . . . . . 10
16784oveq2d 6099 . . . . . . . . . . 11
16814, 17, 26, 31mul4d 9280 . . . . . . . . . . 11
16919, 167, 1683eqtrd 2474 . . . . . . . . . 10
170166, 169oveq12d 6101 . . . . . . . . 9
171150, 151, 152adddid 9114 . . . . . . . . 9
172170, 171eqtr4d 2473 . . . . . . . 8
173163, 172oveq12d 6101 . . . . . . 7
174154, 173eqtr4d 2473 . . . . . 6
175 mul4sq.5 . . . . . . . 8
1763absvalsqd 12246 . . . . . . . . 9
17714absvalsqd 12246 . . . . . . . . 9
178176, 177oveq12d 6101 . . . . . . . 8
179175, 178syl5eq 2482 . . . . . . 7
180 mul4sq.6 . . . . . . . 8
1816absvalsqd 12246 . . . . . . . . 9
18217absvalsqd 12246 . . . . . . . . 9
183181, 182oveq12d 6101 . . . . . . . 8
184180, 183syl5eq 2482 . . . . . . 7
185179, 184oveq12d 6101 . . . . . 6
18611, 22, 39, 44add42d 9292 . . . . . 6
187174, 185, 1863eqtr4d 2480 . . . . 5
18846, 148, 1873eqtr4d 2480 . . . 4
189188oveq1d 6098 . . 3
190 mul4sq.7 . . . . . . . . . 10
191190nncnd 10018 . . . . . . . . 9
192190nnne0d 10046 . . . . . . . . 9
19348, 191, 192absdivd 12259 . . . . . . . 8
194190nnred 10017 . . . . . . . . . 10
195190nnnn0d 10276 . . . . . . . . . . 11
196195nn0ge0d 10279 . . . . . . . . . 10
197194, 196absidd 12227 . . . . . . . . 9
198197oveq2d 6099 . . . . . . . 8
199193, 198eqtrd 2470 . . . . . . 7
200199oveq1d 6098 . . . . . 6
20148abscld 12240 . . . . . . . 8
202201recnd 9116 . . . . . . 7
203202, 191, 192sqdivd 11538 . . . . . 6
204200, 203eqtrd 2470 . . . . 5
20599, 191, 192absdivd 12259 . . . . . . . 8
206197oveq2d 6099 . . . . . . . 8
207205, 206eqtrd 2470 . . . . . . 7
208207oveq1d 6098 . . . . . 6
20999abscld 12240 . . . . . . . 8
210209recnd 9116 . . . . . . 7
211210, 191, 192sqdivd 11538 . . . . . 6
212208, 211eqtrd 2470 . . . . 5
213204, 212oveq12d 6101 . . . 4
21423, 34addcld 9109 . . . . . 6
21597, 214eqeltrd 2512 . . . . 5
21645, 34subcld 9413 . . . . . 6
217147, 216eqeltrd 2512 . . . . 5
218190nnsqcld 11545 . . . . . 6
219218nncnd 10018 . . . . 5
220218nnne0d 10046 . . . . 5
221215, 217, 219, 220divdird 9830 . . . 4
222213, 221eqtr4d 2473 . . 3
223176, 149eqeltrd 2512 . . . . . . 7
224177, 150eqeltrd 2512 . . . . . . 7
225223, 224addcld 9109 . . . . . 6
226175, 225syl5eqel 2522 . . . . 5
227184, 153eqeltrd 2512 . . . . 5
228226, 191, 227, 191, 192, 192divmuldivd 9833 . . . 4
229191sqvald 11522 . . . . 5
230229oveq2d 6099 . . . 4
231228, 230eqtr4d 2473 . . 3
232189, 222, 2313eqtr4d 2480 . 2
233226, 48nncand 9418 . . . . . . 7
234149, 150, 25, 47addsub4d 9460 . . . . . . . . 9
235179oveq1d 6098 . . . . . . . . 9
23624, 3, 6subdid 9491 . . . . . . . . . . 11
23724, 3mulcomd 9111 . . . . . . . . . . . 12
238237oveq1d 6098 . . . . . . . . . . 11
239236, 238eqtrd 2470 . . . . . . . . . 10
240 cjsub 11956 . . . . . . . . . . . . 13
24114, 17, 240syl2anc 644 . . . . . . . . . . . 12
242241oveq2d 6099 . . . . . . . . . . 11
24314, 26, 31subdid 9491 . . . . . . . . . . 11
244242, 243eqtrd 2470 . . . . . . . . . 10
245239, 244oveq12d 6101 . . . . . . . . 9
246234, 235, 2453eqtr4d 2480 . . . . . . . 8
247246oveq2d 6099 . . . . . . 7
248233, 247eqtr3d 2472 . . . . . 6
249248oveq1d 6098 . . . . 5
2503, 6subcld 9413 . . . . . . . 8
25124, 250mulcld 9110 . . . . . . 7
25214, 17subcld 9413 . . . . . . . . 9
253252cjcld 12003 . . . . . . . 8
25414, 253mulcld 9110 . . . . . . 7
255251, 254addcld 9109 . . . . . 6
256226, 255, 191, 192divsubdird 9831 . . . . 5
257251, 254, 191, 192divdird 9830 . . . . . . 7
25824, 250, 191, 192divassd 9827 . . . . . . . 8
25914, 253, 191, 192divassd 9827 . . . . . . . . 9
260252, 191, 192cjdivd 12030 . . . . . . . . . . 11
261194cjred 12033 . . . . . . . . . . . 12
262261oveq2d 6099 . . . . . . . . . . 11
263260, 262eqtrd 2470 . . . . . . . . . 10
264263oveq2d 6099 . . . . . . . . 9
265259, 264eqtr4d 2473 . . . . . . . 8
266258, 265oveq12d 6101 . . . . . . 7
267257, 266eqtrd 2470 . . . . . 6
268267oveq2d 6099 . . . . 5
269249, 256, 2683eqtrd 2474 . . . 4
270 mul4sq.10 . . . . . . 7
271270nn0zd 10375 . . . . . 6
272 zgz 13303 . . . . . 6
273271, 272syl 16 . . . . 5
274 gzcjcl 13306 . . . . . . . 8
2751, 274syl 16 . . . . . . 7
276 mul4sq.8 . . . . . . 7
277 gzmulcl 13308 . . . . . . 7
278275, 276, 277syl2anc 644 . . . . . 6
279 mul4sq.9 . . . . . . . 8
280 gzcjcl 13306 . . . . . . . 8
281279, 280syl 16 . . . . . . 7
282 gzmulcl 13308 . . . . . . 7
28312, 281, 282syl2anc 644 . . . . . 6
284 gzaddcl 13307 . . . . . 6
285278, 283, 284syl2anc 644 . . . . 5
286 gzsubcl 13310 . . . . 5
287273, 285, 286syl2anc 644 . . . 4
288269, 287eqeltrd 2512 . . 3
289250cjcld 12003 . . . . . . . 8
29014, 289mulcld 9110 . . . . . . 7
29124, 252mulcld 9110 . . . . . . 7
292290, 291, 191, 192divsubdird 9831 . . . . . 6
293 cjsub 11956 . . . . . . . . . . . 12
2943, 6, 293syl2anc 644 . . . . . . . . . . 11
295294oveq2d 6099 . . . . . . . . . 10
29614, 24, 29subdid 9491 . . . . . . . . . 10
297295, 296eqtrd 2470 . . . . . . . . 9
29824, 14, 17subdid 9491 . . . . . . . . . 10
29924, 14mulcomd 9111 . . . . . . . . . . 11
300299oveq1d 6098 . . . . . . . . . 10
301298, 300eqtrd 2470 . . . . . . . . 9
302297, 301oveq12d 6101 . . . . . . . 8
30314, 24mulcld 9110 . . . . . . . . 9
304303, 30, 98nnncan1d 9447 . . . . . . . 8
305302, 304eqtrd 2470 . . . . . . 7
306305oveq1d 6098 . . . . . 6
307292, 306eqtr3d 2472 . . . . 5
30814, 289, 191, 192divassd 9827 . . . . . . 7
309250, 191, 192cjdivd 12030 . . . . . . . . 9
310261oveq2d 6099 . . . . . . . . 9
311309, 310eqtrd 2470 . . . . . . . 8
312311oveq2d 6099 . . . . . . 7
313308, 312eqtr4d 2473 . . . . . 6
31424, 252, 191, 192divassd 9827 . . . . . 6
315313, 314oveq12d 6101 . . . . 5
316307, 315eqtr3d 2472 . . . 4
317 gzcjcl 13306 . . . . . . 7
318276, 317syl 16 . . . . . 6
319 gzmulcl 13308 . . . . . 6
32012, 318, 319syl2anc 644 . . . . 5
321 gzmulcl 13308 . . . . . 6
322275, 279, 321syl2anc 644 . . . . 5
323 gzsubcl 13310 . . . . 5
324320, 322, 323syl2anc 644 . . . 4
325316, 324eqeltrd 2512 . . 3
326 4sq.1 . . . 4
3273264sqlem4a 13321 . . 3
328288, 325, 327syl2anc 644 . 2
329232, 328eqeltrrd 2513 1
 Colors of variables: wff set class Syntax hints:   wi 4   wceq 1653   wcel 1726  cab 2424  wrex 2708  cfv 5456  (class class class)co 6083  cc 8990   caddc 8995   cmul 8997   cmin 9293   cdiv 9679  cn 10002  c2 10051  cn0 10223  cz 10284  cexp 11384  ccj 11903  cabs 12041  cgz 13299 This theorem is referenced by:  mul4sq  13324  4sqlem17  13331 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4332  ax-nul 4340  ax-pow 4379  ax-pr 4405  ax-un 4703  ax-cnex 9048  ax-resscn 9049  ax-1cn 9050  ax-icn 9051  ax-addcl 9052  ax-addrcl 9053  ax-mulcl 9054  ax-mulrcl 9055  ax-mulcom 9056  ax-addass 9057  ax-mulass 9058  ax-distr 9059  ax-i2m1 9060  ax-1ne0 9061  ax-1rid 9062  ax-rnegex 9063  ax-rrecex 9064  ax-cnre 9065  ax-pre-lttri 9066  ax-pre-lttrn 9067  ax-pre-ltadd 9068  ax-pre-mulgt0 9069  ax-pre-sup 9070 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-iun 4097  df-br 4215  df-opab 4269  df-mpt 4270  df-tr 4305  df-eprel 4496  df-id 4500  df-po 4505  df-so 4506  df-fr 4543  df-we 4545  df-ord 4586  df-on 4587  df-lim 4588  df-suc 4589  df-om 4848  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-iota 5420  df-fun 5458  df-fn 5459  df-f 5460  df-f1 5461  df-fo 5462  df-f1o 5463  df-fv 5464  df-ov 6086  df-oprab 6087  df-mpt2 6088  df-2nd 6352  df-riota 6551  df-recs 6635  df-rdg 6670  df-er 6907  df-en 7112  df-dom 7113  df-sdom 7114  df-sup 7448  df-pnf 9124  df-mnf 9125  df-xr 9126  df-ltxr 9127  df-le 9128  df-sub 9295  df-neg 9296  df-div 9680  df-nn 10003  df-2 10060  df-3 10061  df-n0 10224  df-z 10285  df-uz 10491  df-rp 10615  df-seq 11326  df-exp 11385  df-cj 11906  df-re 11907  df-im 11908  df-sqr 12042  df-abs 12043  df-gz 13300
 Copyright terms: Public domain W3C validator