2sqmod - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > 2sqmod		Structured version Unicode version

Theorem 2sqmod 28353

Description: Given two decompositions of a prime as a sum of two squares, show that they are equal. (Contributed by Thierry Arnoux, 2-Feb-2020.)

**Hypotheses**
Ref	Expression
2sqmod.1
2sqmod.2
2sqmod.3
2sqmod.4
2sqmod.5
2sqmod.6
2sqmod.7
2sqmod.8
2sqmod.9

**Assertion**
Ref	Expression
2sqmod	$/\$

**Proof of Theorem 2sqmod**
Step	Hyp	Ref	Expression
1		2sqmod.6	. . . . . 6
2	1	adantr 466	. . . . 5 $/\$
3		2sqmod.4	. . . . . . . 8
4	3	nn0red 10870	. . . . . . 7
5	4	adantr 466	. . . . . 6 $/\$
6		2sqmod.3	. . . . . . . 8
7	6	nn0red 10870	. . . . . . 7
8	7	adantr 466	. . . . . 6 $/\$
9	3	nn0ge0d 10872	. . . . . . 7
10	9	adantr 466	. . . . . 6 $/\$
11	6	nn0ge0d 10872	. . . . . . 7
12	11	adantr 466	. . . . . 6 $/\$
13	3	nn0cnd 10871	. . . . . . . . 9
14	13	sqcld 12357	. . . . . . . 8
15	14	adantr 466	. . . . . . 7 $/\$
16	6	nn0cnd 10871	. . . . . . . . 9
17	16	sqcld 12357	. . . . . . . 8
18	17	adantr 466	. . . . . . 7 $/\$
19		2sqmod.2	. . . . . . . . . . . . 13
20	19	nn0cnd 10871	. . . . . . . . . . . 12
21	20	sqcld 12357	. . . . . . . . . . 11
22		2sqmod.5	. . . . . . . . . . . . 13
23	22	nn0cnd 10871	. . . . . . . . . . . 12
24	23	sqcld 12357	. . . . . . . . . . 11
25		2sqmod.8	. . . . . . . . . . . 12
26		2sqmod.9	. . . . . . . . . . . 12
27	25, 26	eqtr4d 2459	. . . . . . . . . . 11
28	21, 17, 14, 24, 27	addeqxfrd 28265	. . . . . . . . . 10
29	28	adantr 466	. . . . . . . . 9 $/\$
30	19	nn0zd 10982	. . . . . . . . . . . . . . . 16
31	3	nn0zd 10982	. . . . . . . . . . . . . . . 16
32		dvdsmul1 14260	. . . . . . . . . . . . . . . 16 $/\$
33	30, 31, 32	syl2anc 665	. . . . . . . . . . . . . . 15
34	33	adantr 466	. . . . . . . . . . . . . 14 $/\$
35	20, 13	mulcld 9607	. . . . . . . . . . . . . . . 16
36	35	adantr 466	. . . . . . . . . . . . . . 15 $/\$
37	16, 23	mulcld 9607	. . . . . . . . . . . . . . . 16
38	37	adantr 466	. . . . . . . . . . . . . . 15 $/\$
39	19	nn0red 10870	. . . . . . . . . . . . . . . . . . . 20
40	39, 4	remulcld 9615	. . . . . . . . . . . . . . . . . . 19
41	22	nn0red 10870	. . . . . . . . . . . . . . . . . . . 20
42	7, 41	remulcld 9615	. . . . . . . . . . . . . . . . . . 19
43	40, 42	resubcld 9991	. . . . . . . . . . . . . . . . . 18
44	43	recnd 9613	. . . . . . . . . . . . . . . . 17
45	44	adantr 466	. . . . . . . . . . . . . . . 16 $/\$
46	43	sqge0d 12386	. . . . . . . . . . . . . . . . . . . . . . 23
47		2sqmod.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
48	6	nn0zd 10982	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
49	47, 30, 48, 25	2sqn0 28351	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
50		elnnne0 10827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
51	19, 49, 50	sylanbrc 668	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
52	22	nn0zd 10982	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
53	24, 14	addcomd 9779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
54	53, 26	eqtrd 2456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
55	47, 52, 31, 54	2sqn0 28351	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
56		elnnne0 10827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
57	22, 55, 56	sylanbrc 668	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
58	51, 57	nnmulcld 10601	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
59	47, 31, 52, 26	2sqn0 28351	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
60		elnnne0 10827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
61	3, 59, 60	sylanbrc 668	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
62	17, 21	addcomd 9779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
63	62, 25	eqtrd 2456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
64	47, 48, 30, 63	2sqn0 28351	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
65		elnnne0 10827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
66	6, 64, 65	sylanbrc 668	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
67	61, 66	nnmulcld 10601	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
68	58, 67	nnaddcld 10600	. . . . . . . . . . . . . . . . . . . . . . . . . 26
69	68	nnsqcld 12379	. . . . . . . . . . . . . . . . . . . . . . . . 25
70	69	nnred 10568	. . . . . . . . . . . . . . . . . . . . . . . 24
71	43	resqcld 12385	. . . . . . . . . . . . . . . . . . . . . . . 24
72	70, 71	addge02d 10146	. . . . . . . . . . . . . . . . . . . . . . 23
73	46, 72	mpbid 213	. . . . . . . . . . . . . . . . . . . . . 22
74	25, 26	oveq12d 6260	. . . . . . . . . . . . . . . . . . . . . . . 24
75		bhmafibid1 28349	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
76	39, 7, 4, 41, 75	syl22anc 1265	. . . . . . . . . . . . . . . . . . . . . . . 24
77	74, 76	eqtr3d 2458	. . . . . . . . . . . . . . . . . . . . . . 23
78		prmz 14562	. . . . . . . . . . . . . . . . . . . . . . . . . 26
79	47, 78	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25
80	79	zcnd 10985	. . . . . . . . . . . . . . . . . . . . . . . 24
81	80	sqvald 12356	. . . . . . . . . . . . . . . . . . . . . . 23
82	13, 16	mulcomd 9608	. . . . . . . . . . . . . . . . . . . . . . . . . 26
83	82	oveq2d 6258	. . . . . . . . . . . . . . . . . . . . . . . . 25
84	83	oveq1d 6257	. . . . . . . . . . . . . . . . . . . . . . . 24
85	84	oveq2d 6258	. . . . . . . . . . . . . . . . . . . . . . 23
86	77, 81, 85	3eqtr4d 2466	. . . . . . . . . . . . . . . . . . . . . 22
87	73, 86	breqtrrd 4386	. . . . . . . . . . . . . . . . . . . . 21
88	87	adantr 466	. . . . . . . . . . . . . . . . . . . 20 $/\$
89	30, 52	zmulcld 10990	. . . . . . . . . . . . . . . . . . . . . . . 24
90	31, 48	zmulcld 10990	. . . . . . . . . . . . . . . . . . . . . . . 24
91	89, 90	zaddcld 10988	. . . . . . . . . . . . . . . . . . . . . . 23
92		dvdssqim 14457	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
93	79, 91, 92	syl2anc 665	. . . . . . . . . . . . . . . . . . . . . 22
94		zsqcl 12288	. . . . . . . . . . . . . . . . . . . . . . . 24
95	79, 94	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23
96		dvdsle 14286	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
97	95, 69, 96	syl2anc 665	. . . . . . . . . . . . . . . . . . . . . 22
98	93, 97	syld 45	. . . . . . . . . . . . . . . . . . . . 21
99	98	imp 430	. . . . . . . . . . . . . . . . . . . 20 $/\$
100	95	zred 10984	. . . . . . . . . . . . . . . . . . . . . 22
101	70, 100	letri3d 9721	. . . . . . . . . . . . . . . . . . . . 21 $/\$
102	101	adantr 466	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
103	88, 99, 102	mpbir2and 930	. . . . . . . . . . . . . . . . . . 19 $/\$
104	86	adantr 466	. . . . . . . . . . . . . . . . . . 19 $/\$
105	103, 104	eqtr2d 2457	. . . . . . . . . . . . . . . . . 18 $/\$
106	70	recnd 9613	. . . . . . . . . . . . . . . . . . . 20
107	71	recnd 9613	. . . . . . . . . . . . . . . . . . . 20
108	106, 106, 107	subadd2d 9949	. . . . . . . . . . . . . . . . . . 19
109	108	adantr 466	. . . . . . . . . . . . . . . . . 18 $/\$
110	105, 109	mpbird 235	. . . . . . . . . . . . . . . . 17 $/\$
111	106	subidd 9918	. . . . . . . . . . . . . . . . . 18
112	111	adantr 466	. . . . . . . . . . . . . . . . 17 $/\$
113	110, 112	eqtr3d 2458	. . . . . . . . . . . . . . . 16 $/\$
114	45, 113	sqeq0d 12358	. . . . . . . . . . . . . . 15 $/\$
115	36, 38, 114	subeq0d 9938	. . . . . . . . . . . . . 14 $/\$
116	34, 115	breqtrd 4384	. . . . . . . . . . . . 13 $/\$
117	47, 30, 48, 25	2sqcoprm 28352	. . . . . . . . . . . . . 14
118	117	adantr 466	. . . . . . . . . . . . 13 $/\$
119		coprmdvds 14595	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
120	30, 48, 52, 119	syl3anc 1264	. . . . . . . . . . . . . 14 $/\$
121	120	adantr 466	. . . . . . . . . . . . 13 $/\$ $/\$
122	116, 118, 121	mp2and 683	. . . . . . . . . . . 12 $/\$
123		dvdsle 14286	. . . . . . . . . . . . . 14 $/\$
124	30, 57, 123	syl2anc 665	. . . . . . . . . . . . 13
125	124	adantr 466	. . . . . . . . . . . 12 $/\$
126	122, 125	mpd 15	. . . . . . . . . . 11 $/\$
127	51	nnrpd 11283	. . . . . . . . . . . . . 14
128	127	rprege0d 11292	. . . . . . . . . . . . 13 $/\$
129	22	nn0ge0d 10872	. . . . . . . . . . . . 13
130		le2sq 12292	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
131	128, 41, 129, 130	syl12anc 1262	. . . . . . . . . . . 12
132	131	adantr 466	. . . . . . . . . . 11 $/\$
133	126, 132	mpbid 213	. . . . . . . . . 10 $/\$
134	51	nnsqcld 12379	. . . . . . . . . . . . 13
135	134	nnred 10568	. . . . . . . . . . . 12
136		zsqcl 12288	. . . . . . . . . . . . . 14
137	52, 136	syl 17	. . . . . . . . . . . . 13
138	137	zred 10984	. . . . . . . . . . . 12
139	135, 138	suble0d 10148	. . . . . . . . . . 11
140	139	adantr 466	. . . . . . . . . 10 $/\$
141	133, 140	mpbird 235	. . . . . . . . 9 $/\$
142	29, 141	eqbrtrrd 4382	. . . . . . . 8 $/\$
143		dvdsmul1 14260	. . . . . . . . . . . . . . 15 $/\$
144	48, 52, 143	syl2anc 665	. . . . . . . . . . . . . 14
145	144	adantr 466	. . . . . . . . . . . . 13 $/\$
146	145, 115	breqtrrd 4386	. . . . . . . . . . . 12 $/\$
147		gcdcom 14420	. . . . . . . . . . . . . . 15 $/\$
148	30, 48, 147	syl2anc 665	. . . . . . . . . . . . . 14
149	148, 117	eqtr3d 2458	. . . . . . . . . . . . 13
150	149	adantr 466	. . . . . . . . . . . 12 $/\$
151		coprmdvds 14595	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
152	48, 30, 31, 151	syl3anc 1264	. . . . . . . . . . . . 13 $/\$
153	152	adantr 466	. . . . . . . . . . . 12 $/\$ $/\$
154	146, 150, 153	mp2and 683	. . . . . . . . . . 11 $/\$
155		dvdsle 14286	. . . . . . . . . . . . 13 $/\$
156	48, 61, 155	syl2anc 665	. . . . . . . . . . . 12
157	156	adantr 466	. . . . . . . . . . 11 $/\$
158	154, 157	mpd 15	. . . . . . . . . 10 $/\$
159	7, 4, 11, 9	le2sqd 12394	. . . . . . . . . . 11
160	159	adantr 466	. . . . . . . . . 10 $/\$
161	158, 160	mpbid 213	. . . . . . . . 9 $/\$
162	4	resqcld 12385	. . . . . . . . . . 11
163		zsqcl 12288	. . . . . . . . . . . . 13
164	48, 163	syl 17	. . . . . . . . . . . 12
165	164	zred 10984	. . . . . . . . . . 11
166	162, 165	subge0d 10147	. . . . . . . . . 10
167	166	adantr 466	. . . . . . . . 9 $/\$
168	161, 167	mpbird 235	. . . . . . . 8 $/\$
169	135, 138	resubcld 9991	. . . . . . . . . . 11
170	28, 169	eqeltrrd 2501	. . . . . . . . . 10
171		0red 9588	. . . . . . . . . 10
172	170, 171	letri3d 9721	. . . . . . . . 9 $/\$
173	172	adantr 466	. . . . . . . 8 $/\$ $/\$
174	142, 168, 173	mpbir2and 930	. . . . . . 7 $/\$
175	15, 18, 174	subeq0d 9938	. . . . . 6 $/\$
176	5, 8, 10, 12, 175	sq11d 12395	. . . . 5 $/\$
177	2, 176	breqtrrd 4386	. . . 4 $/\$
178		2sqmod.7	. . . . . 6
179	178	adantr 466	. . . . 5 $/\$
180	39	adantr 466	. . . . . 6 $/\$
181	41	adantr 466	. . . . . 6 $/\$
182	19	nn0ge0d 10872	. . . . . . 7
183	182	adantr 466	. . . . . 6 $/\$
184	129	adantr 466	. . . . . 6 $/\$
185	21	adantr 466	. . . . . . 7 $/\$
186	24	adantr 466	. . . . . . 7 $/\$
187	168, 29	breqtrrd 4386	. . . . . . . 8 $/\$
188	169, 171	letri3d 9721	. . . . . . . . 9 $/\$
189	188	adantr 466	. . . . . . . 8 $/\$ $/\$
190	141, 187, 189	mpbir2and 930	. . . . . . 7 $/\$
191	185, 186, 190	subeq0d 9938	. . . . . 6 $/\$
192	180, 181, 183, 184, 191	sq11d 12395	. . . . 5 $/\$
193	179, 192	breqtrrd 4386	. . . 4 $/\$
194	39, 4	letri3d 9721	. . . . 5 $/\$
195	194	adantr 466	. . . 4 $/\$ $/\$
196	177, 193, 195	mpbir2and 930	. . 3 $/\$
197	20	adantr 466	. . . 4 $/\$
198	13	adantr 466	. . . 4 $/\$
199	16	adantr 466	. . . 4 $/\$
200	64	adantr 466	. . . 4 $/\$
201	41	adantr 466	. . . . . . 7 $/\$
202	7	adantr 466	. . . . . . 7 $/\$
203	129	adantr 466	. . . . . . 7 $/\$
204	11	adantr 466	. . . . . . 7 $/\$
205	24	adantr 466	. . . . . . . 8 $/\$
206	17	adantr 466	. . . . . . . 8 $/\$
207		prmnn 14561	. . . . . . . . . . . . 13
208	47, 207	syl 17	. . . . . . . . . . . 12
209	208	nnne0d 10598	. . . . . . . . . . 11
210	209	neneqd 2600	. . . . . . . . . 10
211	210	adantr 466	. . . . . . . . 9 $/\$
212	80, 24, 17	subdid 10018	. . . . . . . . . . . . . . 15
213	80, 24	mulcld 9607	. . . . . . . . . . . . . . . 16
214	21, 24	mulcld 9607	. . . . . . . . . . . . . . . 16
215	80, 17	mulcld 9607	. . . . . . . . . . . . . . . 16
216	14, 17	mulcld 9607	. . . . . . . . . . . . . . . 16
217	17, 24	mulcomd 9608	. . . . . . . . . . . . . . . . . 18
218	25	oveq1d 6257	. . . . . . . . . . . . . . . . . . . 20
219	21, 17	pncan2d 9932	. . . . . . . . . . . . . . . . . . . 20
220	218, 219	eqtr3d 2458	. . . . . . . . . . . . . . . . . . 19
221	220	oveq1d 6257	. . . . . . . . . . . . . . . . . 18
222	26	oveq1d 6257	. . . . . . . . . . . . . . . . . . . 20
223	14, 24	pncan2d 9932	. . . . . . . . . . . . . . . . . . . 20
224	222, 223	eqtr3d 2458	. . . . . . . . . . . . . . . . . . 19
225	224	oveq1d 6257	. . . . . . . . . . . . . . . . . 18
226	217, 221, 225	3eqtr4d 2466	. . . . . . . . . . . . . . . . 17
227	80, 21, 24	subdird 10019	. . . . . . . . . . . . . . . . 17
228	80, 14, 17	subdird 10019	. . . . . . . . . . . . . . . . 17
229	226, 227, 228	3eqtr3d 2464	. . . . . . . . . . . . . . . 16
230	213, 214, 215, 216, 229	subeqxfrd 28264	. . . . . . . . . . . . . . 15
231	212, 230	eqtrd 2456	. . . . . . . . . . . . . 14
232	20, 23	sqmuld 12371	. . . . . . . . . . . . . . 15
233	13, 16	sqmuld 12371	. . . . . . . . . . . . . . 15
234	232, 233	oveq12d 6260	. . . . . . . . . . . . . 14
235	20, 23	mulcld 9607	. . . . . . . . . . . . . . 15
236	13, 16	mulcld 9607	. . . . . . . . . . . . . . 15
237		subsq 12325	. . . . . . . . . . . . . . 15 $/\$
238	235, 236, 237	syl2anc 665	. . . . . . . . . . . . . 14
239	231, 234, 238	3eqtr2d 2462	. . . . . . . . . . . . 13
240	239	adantr 466	. . . . . . . . . . . 12 $/\$
241	235	adantr 466	. . . . . . . . . . . . . 14 $/\$
242		simpll 758	. . . . . . . . . . . . . . . 16 $/\$ $/\$
243		simpr 462	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
244	243	neqned 2602	. . . . . . . . . . . . . . . 16 $/\$ $/\$
245	89, 90	zsubcld 10989	. . . . . . . . . . . . . . . . . . 19
246		dvdssqim 14457	. . . . . . . . . . . . . . . . . . 19 $/\$
247	79, 245, 246	syl2anc 665	. . . . . . . . . . . . . . . . . 18
248	247	imp 430	. . . . . . . . . . . . . . . . 17 $/\$
249	248	adantr 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$
250	95	adantr 466	. . . . . . . . . . . . . . . . . 18 $/\$
251	245	adantr 466	. . . . . . . . . . . . . . . . . . 19 $/\$
252	235	adantr 466	. . . . . . . . . . . . . . . . . . . 20 $/\$
253	236	adantr 466	. . . . . . . . . . . . . . . . . . . 20 $/\$
254		simpr 462	. . . . . . . . . . . . . . . . . . . 20 $/\$
255	252, 253, 254	subne0d 9939	. . . . . . . . . . . . . . . . . . 19 $/\$
256	251, 255	znsqcld 28266	. . . . . . . . . . . . . . . . . 18 $/\$
257		dvdsle 14286	. . . . . . . . . . . . . . . . . 18 $/\$
258	250, 256, 257	syl2anc 665	. . . . . . . . . . . . . . . . 17 $/\$
259	258	imp 430	. . . . . . . . . . . . . . . 16 $/\$ $/\$
260	242, 244, 249, 259	syl21anc 1263	. . . . . . . . . . . . . . 15 $/\$ $/\$
261	39, 41	remulcld 9615	. . . . . . . . . . . . . . . . . . . . . 22
262	4, 7	remulcld 9615	. . . . . . . . . . . . . . . . . . . . . 22
263	261, 262	resubcld 9991	. . . . . . . . . . . . . . . . . . . . 21
264	263	resqcld 12385	. . . . . . . . . . . . . . . . . . . 20
265	61	nnrpd 11283	. . . . . . . . . . . . . . . . . . . . . . 23
266	127, 265	rpmulcld 11301	. . . . . . . . . . . . . . . . . . . . . 22
267	66	nnrpd 11283	. . . . . . . . . . . . . . . . . . . . . . 23
268	57	nnrpd 11283	. . . . . . . . . . . . . . . . . . . . . . 23
269	267, 268	rpmulcld 11301	. . . . . . . . . . . . . . . . . . . . . 22
270	266, 269	rpaddcld 11300	. . . . . . . . . . . . . . . . . . . . 21
271		2z 10913	. . . . . . . . . . . . . . . . . . . . . 22
272	271	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
273	270, 272	rpexpcld 12382	. . . . . . . . . . . . . . . . . . . 20
274	264, 273	ltaddrp2d 11316	. . . . . . . . . . . . . . . . . . 19
275		bhmafibid2 28350	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
276	39, 7, 4, 41, 275	syl22anc 1265	. . . . . . . . . . . . . . . . . . . . 21
277	74, 276	eqtr3d 2458	. . . . . . . . . . . . . . . . . . . 20
278	82	oveq2d 6258	. . . . . . . . . . . . . . . . . . . . . 22
279	278	oveq1d 6257	. . . . . . . . . . . . . . . . . . . . 21
280	279	oveq2d 6258	. . . . . . . . . . . . . . . . . . . 20
281	277, 280	eqtr4d 2459	. . . . . . . . . . . . . . . . . . 19
282	274, 281	breqtrrd 4386	. . . . . . . . . . . . . . . . . 18
283	282, 81	breqtrrd 4386	. . . . . . . . . . . . . . . . 17
284	242, 283	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$
285	264, 100	ltnled 9726	. . . . . . . . . . . . . . . . 17
286	242, 285	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$
287	284, 286	mpbid 213	. . . . . . . . . . . . . . 15 $/\$ $/\$
288	260, 287	condan 801	. . . . . . . . . . . . . 14 $/\$
289	241, 288	subeq0bd 9989	. . . . . . . . . . . . 13 $/\$
290	289	oveq2d 6258	. . . . . . . . . . . 12 $/\$
291	235, 236	addcld 9606	. . . . . . . . . . . . . 14
292	291	mul01d 9776	. . . . . . . . . . . . 13
293	292	adantr 466	. . . . . . . . . . . 12 $/\$
294	240, 290, 293	3eqtrd 2460	. . . . . . . . . . 11 $/\$
295	24, 17	subcld 9930	. . . . . . . . . . . . 13
296	80, 295	mul0ord 10206	. . . . . . . . . . . 12 $\/$
297	296	adantr 466	. . . . . . . . . . 11 $/\$ $\/$
298	294, 297	mpbid 213	. . . . . . . . . 10 $/\$ $\/$
299	298	ord 378	. . . . . . . . 9 $/\$
300	211, 299	mpd 15	. . . . . . . 8 $/\$
301	205, 206, 300	subeq0d 9938	. . . . . . 7 $/\$
302	201, 202, 203, 204, 301	sq11d 12395	. . . . . 6 $/\$
303	302	oveq2d 6258	. . . . 5 $/\$
304	303, 288	eqtr3d 2458	. . . 4 $/\$
305	197, 198, 199, 200, 304	mulcan2ad 10192	. . 3 $/\$
306	137, 164	zsubcld 10989	. . . . . 6
307		dvdsmul1 14260	. . . . . 6 $/\$
308	79, 306, 307	syl2anc 665	. . . . 5
309	308, 239	breqtrd 4384	. . . 4
310		euclemma 14601	. . . . 5 $/\$ $/\$ $\/$
311	47, 91, 245, 310	syl3anc 1264	. . . 4 $\/$
312	309, 311	mpbid 213	. . 3 $\/$
313	196, 305, 312	mpjaodan 793	. 2
314	313	oveq1d 6257	. . . . 5
315	314	oveq2d 6258	. . . 4
316	315, 220, 224	3eqtr3d 2464	. . 3
317	7, 41, 11, 129, 316	sq11d 12395	. 2
318	313, 317	jca 534	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $\/$ wo 369 $/\$ wa 370

wceq 1437

wcel 1872

wne 2593 class class class wbr 4359 (class class class)co 6242

cc 9481

cr 9482

cc0 9483

c1 9484

caddc 9486

cmul 9488

clt 9619

cle 9620

cmin 9804

cn 10553

c2 10603

cn0 10813

cz 10881

cexp 12215

cdvds 14241

cgcd 14404

cprime 14558

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1663 ax-4 1676 ax-5 1752 ax-6 1798 ax-7 1843 ax-8 1874 ax-9 1876 ax-10 1891 ax-11 1896 ax-12 1909 ax-13 2058 ax-ext 2402 ax-sep 4482 ax-nul 4491 ax-pow 4538 ax-pr 4596 ax-un 6534 ax-cnex 9539 ax-resscn 9540 ax-1cn 9541 ax-icn 9542 ax-addcl 9543 ax-addrcl 9544 ax-mulcl 9545 ax-mulrcl 9546 ax-mulcom 9547 ax-addass 9548 ax-mulass 9549 ax-distr 9550 ax-i2m1 9551 ax-1ne0 9552 ax-1rid 9553 ax-rnegex 9554 ax-rrecex 9555 ax-cnre 9556 ax-pre-lttri 9557 ax-pre-lttrn 9558 ax-pre-ltadd 9559 ax-pre-mulgt0 9560 ax-pre-sup 9561

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 1658 df-nf 1662 df-sb 1791 df-eu 2274 df-mo 2275 df-clab 2409 df-cleq 2415 df-clel 2418 df-nfc 2552 df-ne 2595 df-nel 2596 df-ral 2713 df-rex 2714 df-reu 2715 df-rmo 2716 df-rab 2717 df-v 3018 df-sbc 3236 df-csb 3332 df-dif 3375 df-un 3377 df-in 3379 df-ss 3386 df-pss 3388 df-nul 3698 df-if 3848 df-pw 3919 df-sn 3935 df-pr 3937 df-tp 3939 df-op 3941 df-uni 4156 df-int 4192 df-iun 4237 df-br 4360 df-opab 4419 df-mpt 4420 df-tr 4455 df-eprel 4700 df-id 4704 df-po 4710 df-so 4711 df-fr 4748 df-we 4750 df-xp 4795 df-rel 4796 df-cnv 4797 df-co 4798 df-dm 4799 df-rn 4800 df-res 4801 df-ima 4802 df-pred 5335 df-ord 5381 df-on 5382 df-lim 5383 df-suc 5384 df-iota 5501 df-fun 5539 df-fn 5540 df-f 5541 df-f1 5542 df-fo 5543 df-f1o 5544 df-fv 5545 df-riota 6204 df-ov 6245 df-oprab 6246 df-mpt2 6247 df-om 6644 df-2nd 6745 df-wrecs 6976 df-recs 7038 df-rdg 7076 df-1o 7130 df-2o 7131 df-oadd 7134 df-er 7311 df-en 7518 df-dom 7519 df-sdom 7520 df-fin 7521 df-sup 7902 df-inf 7903 df-pnf 9621 df-mnf 9622 df-xr 9623 df-ltxr 9624 df-le 9625 df-sub 9806 df-neg 9807 df-div 10214 df-nn 10554 df-2 10612 df-3 10613 df-n0 10814 df-z 10882 df-uz 11104 df-rp 11247 df-fl 11971 df-mod 12040 df-seq 12157 df-exp 12216 df-cj 13099 df-re 13100 df-im 13101 df-sqrt 13235 df-abs 13236 df-dvds 14242 df-gcd 14405 df-prm 14559

This theorem is referenced by: 2sqmo 28354

W3C validator