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

Theorem mul4sqlem 14100
Description: Lemma for mul4sq 14101: algebraic manipulations. The extra assumptions involving are for a part of 4sqlem17 14108 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:   , , , ,   ,   ,   ,   ,   ,M   ,   S,

Proof of Theorem mul4sqlem
StepHypRef Expression
1 mul4sq.1 . . . . . . . . . . 11
2 gzcn 14079 . . . . . . . . . . 11
31, 2syl 16 . . . . . . . . . 10
4 mul4sq.3 . . . . . . . . . . 11
5 gzcn 14079 . . . . . . . . . . 11
64, 5syl 16 . . . . . . . . . 10
73, 6mulcld 9491 . . . . . . . . 9
87absvalsqd 13014 . . . . . . . 8
97cjcld 12771 . . . . . . . . 9
107, 9mulcld 9491 . . . . . . . 8
118, 10eqeltrd 2536 . . . . . . 7
12 mul4sq.2 . . . . . . . . . . 11
13 gzcn 14079 . . . . . . . . . . 11
1412, 13syl 16 . . . . . . . . . 10
15 mul4sq.4 . . . . . . . . . . 11
16 gzcn 14079 . . . . . . . . . . 11
1715, 16syl 16 . . . . . . . . . 10
1814, 17mulcld 9491 . . . . . . . . 9
1918absvalsqd 13014 . . . . . . . 8
2018cjcld 12771 . . . . . . . . 9
2118, 20mulcld 9491 . . . . . . . 8
2219, 21eqeltrd 2536 . . . . . . 7
2311, 22addcld 9490 . . . . . 6
243cjcld 12771 . . . . . . . . 9
2524, 6mulcld 9491 . . . . . . . 8
2614cjcld 12771 . . . . . . . . 9
2726, 17mulcld 9491 . . . . . . . 8
2825, 27mulcld 9491 . . . . . . 7
296cjcld 12771 . . . . . . . . 9
3014, 29mulcld 9491 . . . . . . . 8
3117cjcld 12771 . . . . . . . . 9
323, 31mulcld 9491 . . . . . . . 8
3330, 32mulcld 9491 . . . . . . 7
3428, 33addcld 9490 . . . . . 6
353, 17mulcld 9491 . . . . . . . . 9
3635absvalsqd 13014 . . . . . . . 8
3735cjcld 12771 . . . . . . . . 9
3835, 37mulcld 9491 . . . . . . . 8
3936, 38eqeltrd 2536 . . . . . . 7
4014, 6mulcld 9491 . . . . . . . . 9
4140absvalsqd 13014 . . . . . . . 8
4240cjcld 12771 . . . . . . . . 9
4340, 42mulcld 9491 . . . . . . . 8
4441, 43eqeltrd 2536 . . . . . . 7
4539, 44addcld 9490 . . . . . 6
4623, 34, 45ppncand 9844 . . . . 5
4714, 31mulcld 9491 . . . . . . . . 9
4825, 47addcld 9490 . . . . . . . 8
4948absvalsqd 13014 . . . . . . 7
5025, 47cjaddd 12795 . . . . . . . . 9
5124, 6cjmuld 12796 . . . . . . . . . . 11
523cjcjd 12774 . . . . . . . . . . . 12
5352oveq1d 6189 . . . . . . . . . . 11
5451, 53eqtrd 2490 . . . . . . . . . 10
5514, 31cjmuld 12796 . . . . . . . . . . 11
5617cjcjd 12774 . . . . . . . . . . . 12
5756oveq2d 6190 . . . . . . . . . . 11
5855, 57eqtrd 2490 . . . . . . . . . 10
5954, 58oveq12d 6192 . . . . . . . . 9
6050, 59eqtrd 2490 . . . . . . . 8
6160oveq2d 6190 . . . . . . 7
623, 29mulcld 9491 . . . . . . . . . . 11
6325, 62, 27adddid 9495 . . . . . . . . . 10
646, 24, 3, 29mul4d 9666 . . . . . . . . . . . . 13
6524, 6mulcomd 9492 . . . . . . . . . . . . . 14
6665oveq1d 6189 . . . . . . . . . . . . 13
673, 6mulcomd 9492 . . . . . . . . . . . . . 14
683, 6cjmuld 12796 . . . . . . . . . . . . . 14
6967, 68oveq12d 6192 . . . . . . . . . . . . 13
7064, 66, 693eqtr4d 2500 . . . . . . . . . . . 12
7170, 8eqtr4d 2493 . . . . . . . . . . 11
7271oveq1d 6189 . . . . . . . . . 10
7363, 72eqtrd 2490 . . . . . . . . 9
7447, 62, 27adddid 9495 . . . . . . . . . 10
753, 29mulcomd 9492 . . . . . . . . . . . . 13
7675oveq2d 6190 . . . . . . . . . . . 12
7714, 31, 29, 3mul4d 9666 . . . . . . . . . . . 12
7831, 3mulcomd 9492 . . . . . . . . . . . . 13
7978oveq2d 6190 . . . . . . . . . . . 12
8076, 77, 793eqtrd 2494 . . . . . . . . . . 11
8114, 31, 17, 26mul4d 9666 . . . . . . . . . . . . 13
8226, 17mulcomd 9492 . . . . . . . . . . . . . 14
8382oveq2d 6190 . . . . . . . . . . . . 13
8414, 17cjmuld 12796 . . . . . . . . . . . . . . 15
8526, 31mulcomd 9492 . . . . . . . . . . . . . . 15
8684, 85eqtrd 2490 . . . . . . . . . . . . . 14
8786oveq2d 6190 . . . . . . . . . . . . 13
8881, 83, 873eqtr4d 2500 . . . . . . . . . . . 12
8988, 19eqtr4d 2493 . . . . . . . . . . 11
9080, 89oveq12d 6192 . . . . . . . . . 10
9174, 90eqtrd 2490 . . . . . . . . 9
9273, 91oveq12d 6192 . . . . . . . 8
9362, 27addcld 9490 . . . . . . . . 9
9425, 47, 93adddird 9496 . . . . . . . 8
9511, 22, 28, 33add42d 9679 . . . . . . . 8
9692, 94, 953eqtr4d 2500 . . . . . . 7
9749, 61, 963eqtrd 2494 . . . . . 6
9824, 17mulcld 9491 . . . . . . . . 9
9998, 30subcld 9804 . . . . . . . 8
10099absvalsqd 13014 . . . . . . 7
101 cjsub 12724 . . . . . . . . . 10
10298, 30, 101syl2anc 661 . . . . . . . . 9
10324, 17cjmuld 12796 . . . . . . . . . . 11
10452oveq1d 6189 . . . . . . . . . . 11
105103, 104eqtrd 2490 . . . . . . . . . 10
10614, 29cjmuld 12796 . . . . . . . . . . 11
1076cjcjd 12774 . . . . . . . . . . . 12
108107oveq2d 6190 . . . . . . . . . . 11
109106, 108eqtrd 2490 . . . . . . . . . 10
110105, 109oveq12d 6192 . . . . . . . . 9
111102, 110eqtrd 2490 . . . . . . . 8
112111oveq2d 6190 . . . . . . 7
11326, 6mulcld 9491 . . . . . . . . . 10
11432, 113subcld 9804 . . . . . . . . 9
11598, 30, 114subdird 9886 . . . . . . . 8
11698, 32, 113subdid 9885 . . . . . . . . . 10
11717, 24, 3, 31mul4d 9666 . . . . . . . . . . . . 13
11824, 17mulcomd 9492 . . . . . . . . . . . . . 14
119118oveq1d 6189 . . . . . . . . . . . . 13
1203, 17mulcomd 9492 . . . . . . . . . . . . . 14
1213, 17cjmuld 12796 . . . . . . . . . . . . . 14
122120, 121oveq12d 6192 . . . . . . . . . . . . 13
123117, 119, 1223eqtr4d 2500 . . . . . . . . . . . 12
124123, 36eqtr4d 2493 . . . . . . . . . . 11
12526, 6mulcomd 9492 . . . . . . . . . . . . 13
126125oveq2d 6190 . . . . . . . . . . . 12
12724, 17, 6, 26mul4d 9666 . . . . . . . . . . . 12
12817, 26mulcomd 9492 . . . . . . . . . . . . 13
129128oveq2d 6190 . . . . . . . . . . . 12
130126, 127, 1293eqtrd 2494 . . . . . . . . . . 11
131124, 130oveq12d 6192 . . . . . . . . . 10
132116, 131eqtrd 2490 . . . . . . . . 9
13330, 32, 113subdid 9885 . . . . . . . . . 10
134125oveq2d 6190 . . . . . . . . . . . . 13
13514, 29, 6, 26mul4d 9666 . . . . . . . . . . . . 13
13629, 26mulcomd 9492 . . . . . . . . . . . . . . 15
13714, 6cjmuld 12796 . . . . . . . . . . . . . . 15
138136, 137eqtr4d 2493 . . . . . . . . . . . . . 14
139138oveq2d 6190 . . . . . . . . . . . . 13
140134, 135, 1393eqtrd 2494 . . . . . . . . . . . 12
141140, 41eqtr4d 2493 . . . . . . . . . . 11
142141oveq2d 6190 . . . . . . . . . 10
143133, 142eqtrd 2490 . . . . . . . . 9
144132, 143oveq12d 6192 . . . . . . . 8
14539, 28, 33, 44subadd4d 9852 . . . . . . . 8
146115, 144, 1453eqtrd 2494 . . . . . . 7
147100, 112, 1463eqtrd 2494 . . . . . 6
14897, 147oveq12d 6192 . . . . 5
1493, 24mulcld 9491 . . . . . . . 8
15014, 26mulcld 9491 . . . . . . . 8
1516, 29mulcld 9491 . . . . . . . . 9
15217, 31mulcld 9491 . . . . . . . . 9
153151, 152addcld 9490 . . . . . . . 8
154149, 150, 153adddird 9496 . . . . . . 7
15568oveq2d 6190 . . . . . . . . . . 11
1563, 6, 24, 29mul4d 9666 . . . . . . . . . . 11
1578, 155, 1563eqtrd 2494 . . . . . . . . . 10
158121oveq2d 6190 . . . . . . . . . . 11
1593, 17, 24, 31mul4d 9666 . . . . . . . . . . 11
16036, 158, 1593eqtrd 2494 . . . . . . . . . 10
161157, 160oveq12d 6192 . . . . . . . . 9
162149, 151, 152adddid 9495 . . . . . . . . 9
163161, 162eqtr4d 2493 . . . . . . . 8
164137oveq2d 6190 . . . . . . . . . . 11
16514, 6, 26, 29mul4d 9666 . . . . . . . . . . 11
16641, 164, 1653eqtrd 2494 . . . . . . . . . 10
16784oveq2d 6190 . . . . . . . . . . 11
16814, 17, 26, 31mul4d 9666 . . . . . . . . . . 11
16919, 167, 1683eqtrd 2494 . . . . . . . . . 10
170166, 169oveq12d 6192 . . . . . . . . 9
171150, 151, 152adddid 9495 . . . . . . . . 9
172170, 171eqtr4d 2493 . . . . . . . 8
173163, 172oveq12d 6192 . . . . . . 7
174154, 173eqtr4d 2493 . . . . . 6
175 mul4sq.5 . . . . . . . 8
1763absvalsqd 13014 . . . . . . . . 9
17714absvalsqd 13014 . . . . . . . . 9
178176, 177oveq12d 6192 . . . . . . . 8
179175, 178syl5eq 2502 . . . . . . 7
180 mul4sq.6 . . . . . . . 8
1816absvalsqd 13014 . . . . . . . . 9
18217absvalsqd 13014 . . . . . . . . 9
183181, 182oveq12d 6192 . . . . . . . 8
184180, 183syl5eq 2502 . . . . . . 7
185179, 184oveq12d 6192 . . . . . 6
18611, 22, 39, 44add42d 9679 . . . . . 6
187174, 185, 1863eqtr4d 2500 . . . . 5
18846, 148, 1873eqtr4d 2500 . . . 4
189188oveq1d 6189 . . 3
190 mul4sq.7 . . . . . . . . . 10
191190nncnd 10423 . . . . . . . . 9
192190nnne0d 10451 . . . . . . . . 9
19348, 191, 192absdivd 13027 . . . . . . . 8
194190nnred 10422 . . . . . . . . . 10
195190nnnn0d 10721 . . . . . . . . . . 11
196195nn0ge0d 10724 . . . . . . . . . 10
197194, 196absidd 12995 . . . . . . . . 9
198197oveq2d 6190 . . . . . . . 8
199193, 198eqtrd 2490 . . . . . . 7
200199oveq1d 6189 . . . . . 6
20148abscld 13008 . . . . . . . 8
202201recnd 9497 . . . . . . 7
203202, 191, 192sqdivd 12106 . . . . . 6
204200, 203eqtrd 2490 . . . . 5
20599, 191, 192absdivd 13027 . . . . . . . 8
206197oveq2d 6190 . . . . . . . 8
207205, 206eqtrd 2490 . . . . . . 7
208207oveq1d 6189 . . . . . 6
20999abscld 13008 . . . . . . . 8
210209recnd 9497 . . . . . . 7
211210, 191, 192sqdivd 12106 . . . . . 6
212208, 211eqtrd 2490 . . . . 5
213204, 212oveq12d 6192 . . . 4
21423, 34addcld 9490 . . . . . 6
21597, 214eqeltrd 2536 . . . . 5
21645, 34subcld 9804 . . . . . 6
217147, 216eqeltrd 2536 . . . . 5
218190nnsqcld 12113 . . . . . 6
219218nncnd 10423 . . . . 5
220218nnne0d 10451 . . . . 5
221215, 217, 219, 220divdird 10230 . . . 4
222213, 221eqtr4d 2493 . . 3
223176, 149eqeltrd 2536 . . . . . . 7
224177, 150eqeltrd 2536 . . . . . . 7
225223, 224addcld 9490 . . . . . 6
226175, 225syl5eqel 2540 . . . . 5
227184, 153eqeltrd 2536 . . . . 5
228226, 191, 227, 191, 192, 192divmuldivd 10233 . . . 4
229191sqvald 12090 . . . . 5
230229oveq2d 6190 . . . 4
231228, 230eqtr4d 2493 . . 3
232189, 222, 2313eqtr4d 2500 . 2
233226, 48nncand 9809 . . . . . . 7
234149, 150, 25, 47addsub4d 9851 . . . . . . . . 9
235179oveq1d 6189 . . . . . . . . 9
23624, 3, 6subdid 9885 . . . . . . . . . . 11
23724, 3mulcomd 9492 . . . . . . . . . . . 12
238237oveq1d 6189 . . . . . . . . . . 11
239236, 238eqtrd 2490 . . . . . . . . . 10
240 cjsub 12724 . . . . . . . . . . . . 13
24114, 17, 240syl2anc 661 . . . . . . . . . . . 12
242241oveq2d 6190 . . . . . . . . . . 11
24314, 26, 31subdid 9885 . . . . . . . . . . 11
244242, 243eqtrd 2490 . . . . . . . . . 10
245239, 244oveq12d 6192 . . . . . . . . 9
246234, 235, 2453eqtr4d 2500 . . . . . . . 8
247246oveq2d 6190 . . . . . . 7
248233, 247eqtr3d 2492 . . . . . 6
249248oveq1d 6189 . . . . 5
2503, 6subcld 9804 . . . . . . . 8
25124, 250mulcld 9491 . . . . . . 7
25214, 17subcld 9804 . . . . . . . . 9
253252cjcld 12771 . . . . . . . 8
25414, 253mulcld 9491 . . . . . . 7
255251, 254addcld 9490 . . . . . 6
256226, 255, 191, 192divsubdird 10231 . . . . 5
257251, 254, 191, 192divdird 10230 . . . . . . 7
25824, 250, 191, 192divassd 10227 . . . . . . . 8
25914, 253, 191, 192divassd 10227 . . . . . . . . 9
260252, 191, 192cjdivd 12798 . . . . . . . . . . 11
261194cjred 12801 . . . . . . . . . . . 12
262261oveq2d 6190 . . . . . . . . . . 11
263260, 262eqtrd 2490 . . . . . . . . . 10
264263oveq2d 6190 . . . . . . . . 9
265259, 264eqtr4d 2493 . . . . . . . 8
266258, 265oveq12d 6192 . . . . . . 7
267257, 266eqtrd 2490 . . . . . 6
268267oveq2d 6190 . . . . 5
269249, 256, 2683eqtrd 2494 . . . 4
270 mul4sq.10 . . . . . . 7
271270nn0zd 10830 . . . . . 6
272 zgz 14080 . . . . . 6