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 27788

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 465	. . . . 5 $/\$
3		2sqmod.4	. . . . . . . 8
4	3	nn0red 10874	. . . . . . 7
5	4	adantr 465	. . . . . 6 $/\$
6		2sqmod.3	. . . . . . . 8
7	6	nn0red 10874	. . . . . . 7
8	7	adantr 465	. . . . . 6 $/\$
9	3	nn0ge0d 10876	. . . . . . 7
10	9	adantr 465	. . . . . 6 $/\$
11	6	nn0ge0d 10876	. . . . . . 7
12	11	adantr 465	. . . . . 6 $/\$
13	3	nn0cnd 10875	. . . . . . . . 9
14	13	sqcld 12310	. . . . . . . 8
15	14	adantr 465	. . . . . . 7 $/\$
16	6	nn0cnd 10875	. . . . . . . . 9
17	16	sqcld 12310	. . . . . . . 8
18	17	adantr 465	. . . . . . 7 $/\$
19		2sqmod.2	. . . . . . . . . . . . 13
20	19	nn0cnd 10875	. . . . . . . . . . . 12
21	20	sqcld 12310	. . . . . . . . . . 11
22		2sqmod.5	. . . . . . . . . . . . 13
23	22	nn0cnd 10875	. . . . . . . . . . . 12
24	23	sqcld 12310	. . . . . . . . . . 11
25		2sqmod.8	. . . . . . . . . . . 12
26		2sqmod.9	. . . . . . . . . . . 12
27	25, 26	eqtr4d 2501	. . . . . . . . . . 11
28	21, 17, 14, 24, 27	addeqxfrd 27710	. . . . . . . . . 10
29	28	adantr 465	. . . . . . . . 9 $/\$
30	19	nn0zd 10988	. . . . . . . . . . . . . . . 16
31	3	nn0zd 10988	. . . . . . . . . . . . . . . 16
32		dvdsmul1 14016	. . . . . . . . . . . . . . . 16 $/\$
33	30, 31, 32	syl2anc 661	. . . . . . . . . . . . . . 15
34	33	adantr 465	. . . . . . . . . . . . . 14 $/\$
35	20, 13	mulcld 9633	. . . . . . . . . . . . . . . 16
36	35	adantr 465	. . . . . . . . . . . . . . 15 $/\$
37	16, 23	mulcld 9633	. . . . . . . . . . . . . . . 16
38	37	adantr 465	. . . . . . . . . . . . . . 15 $/\$
39	19	nn0red 10874	. . . . . . . . . . . . . . . . . . . 20
40	39, 4	remulcld 9641	. . . . . . . . . . . . . . . . . . 19
41	22	nn0red 10874	. . . . . . . . . . . . . . . . . . . 20
42	7, 41	remulcld 9641	. . . . . . . . . . . . . . . . . . 19
43	40, 42	resubcld 10008	. . . . . . . . . . . . . . . . . 18
44	43	recnd 9639	. . . . . . . . . . . . . . . . 17
45	44	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
46	43	sqge0d 12339	. . . . . . . . . . . . . . . . . . . . . . 23
47		2sqmod.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
48	6	nn0zd 10988	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
49	47, 30, 48, 25	2sqn0 27786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
50		elnnne0 10830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
51	19, 49, 50	sylanbrc 664	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
52	22	nn0zd 10988	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
53	24, 14	addcomd 9799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
54	53, 26	eqtrd 2498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
55	47, 52, 31, 54	2sqn0 27786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
56		elnnne0 10830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
57	22, 55, 56	sylanbrc 664	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
58	51, 57	nnmulcld 10604	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
59	47, 31, 52, 26	2sqn0 27786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
60		elnnne0 10830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
61	3, 59, 60	sylanbrc 664	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
62	17, 21	addcomd 9799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
63	62, 25	eqtrd 2498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
64	47, 48, 30, 63	2sqn0 27786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
65		elnnne0 10830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
66	6, 64, 65	sylanbrc 664	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
67	61, 66	nnmulcld 10604	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
68	58, 67	nnaddcld 10603	. . . . . . . . . . . . . . . . . . . . . . . . . 26
69	68	nnsqcld 12332	. . . . . . . . . . . . . . . . . . . . . . . . 25
70	69	nnred 10571	. . . . . . . . . . . . . . . . . . . . . . . 24
71	43	resqcld 12338	. . . . . . . . . . . . . . . . . . . . . . . 24
72	70, 71	addge02d 10162	. . . . . . . . . . . . . . . . . . . . . . 23
73	46, 72	mpbid 210	. . . . . . . . . . . . . . . . . . . . . 22
74	25, 26	oveq12d 6314	. . . . . . . . . . . . . . . . . . . . . . . 24
75		bhmafibid1 27784	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
76	39, 7, 4, 41, 75	syl22anc 1229	. . . . . . . . . . . . . . . . . . . . . . . 24
77	74, 76	eqtr3d 2500	. . . . . . . . . . . . . . . . . . . . . . 23
78		prmz 14232	. . . . . . . . . . . . . . . . . . . . . . . . . 26
79	47, 78	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25
80	79	zcnd 10991	. . . . . . . . . . . . . . . . . . . . . . . 24
81	80	sqvald 12309	. . . . . . . . . . . . . . . . . . . . . . 23
82	13, 16	mulcomd 9634	. . . . . . . . . . . . . . . . . . . . . . . . . 26
83	82	oveq2d 6312	. . . . . . . . . . . . . . . . . . . . . . . . 25
84	83	oveq1d 6311	. . . . . . . . . . . . . . . . . . . . . . . 24
85	84	oveq2d 6312	. . . . . . . . . . . . . . . . . . . . . . 23
86	77, 81, 85	3eqtr4d 2508	. . . . . . . . . . . . . . . . . . . . . 22
87	73, 86	breqtrrd 4482	. . . . . . . . . . . . . . . . . . . . 21
88	87	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$
89	30, 52	zmulcld 10996	. . . . . . . . . . . . . . . . . . . . . . . 24
90	31, 48	zmulcld 10996	. . . . . . . . . . . . . . . . . . . . . . . 24
91	89, 90	zaddcld 10994	. . . . . . . . . . . . . . . . . . . . . . 23
92		dvdssqim 14202	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
93	79, 91, 92	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . 22
94		zsqcl 12240	. . . . . . . . . . . . . . . . . . . . . . . 24
95	79, 94	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23
96		dvdsle 14042	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
97	95, 69, 96	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . 22
98	93, 97	syld 44	. . . . . . . . . . . . . . . . . . . . 21
99	98	imp 429	. . . . . . . . . . . . . . . . . . . 20 $/\$
100	95	zred 10990	. . . . . . . . . . . . . . . . . . . . . 22
101	70, 100	letri3d 9744	. . . . . . . . . . . . . . . . . . . . 21 $/\$
102	101	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
103	88, 99, 102	mpbir2and 922	. . . . . . . . . . . . . . . . . . 19 $/\$
104	86	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$
105	103, 104	eqtr2d 2499	. . . . . . . . . . . . . . . . . 18 $/\$
106	70	recnd 9639	. . . . . . . . . . . . . . . . . . . 20
107	71	recnd 9639	. . . . . . . . . . . . . . . . . . . 20
108	106, 106, 107	subadd2d 9969	. . . . . . . . . . . . . . . . . . 19
109	108	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
110	105, 109	mpbird 232	. . . . . . . . . . . . . . . . 17 $/\$
111	106	subidd 9938	. . . . . . . . . . . . . . . . . 18
112	111	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$
113	110, 112	eqtr3d 2500	. . . . . . . . . . . . . . . 16 $/\$
114	45, 113	sqeq0d 12311	. . . . . . . . . . . . . . 15 $/\$
115	36, 38, 114	subeq0d 9958	. . . . . . . . . . . . . 14 $/\$
116	34, 115	breqtrd 4480	. . . . . . . . . . . . 13 $/\$
117	47, 30, 48, 25	2sqcoprm 27787	. . . . . . . . . . . . . 14
118	117	adantr 465	. . . . . . . . . . . . 13 $/\$
119		coprmdvds 14254	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
120	30, 48, 52, 119	syl3anc 1228	. . . . . . . . . . . . . 14 $/\$
121	120	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$
122	116, 118, 121	mp2and 679	. . . . . . . . . . . 12 $/\$
123		dvdsle 14042	. . . . . . . . . . . . . 14 $/\$
124	30, 57, 123	syl2anc 661	. . . . . . . . . . . . 13
125	124	adantr 465	. . . . . . . . . . . 12 $/\$
126	122, 125	mpd 15	. . . . . . . . . . 11 $/\$
127	51	nnrpd 11280	. . . . . . . . . . . . . 14
128	127	rprege0d 11288	. . . . . . . . . . . . 13 $/\$
129	22	nn0ge0d 10876	. . . . . . . . . . . . 13
130		le2sq 12244	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
131	128, 41, 129, 130	syl12anc 1226	. . . . . . . . . . . 12
132	131	adantr 465	. . . . . . . . . . 11 $/\$
133	126, 132	mpbid 210	. . . . . . . . . 10 $/\$
134	51	nnsqcld 12332	. . . . . . . . . . . . 13
135	134	nnred 10571	. . . . . . . . . . . 12
136		zsqcl 12240	. . . . . . . . . . . . . 14
137	52, 136	syl 16	. . . . . . . . . . . . 13
138	137	zred 10990	. . . . . . . . . . . 12
139	135, 138	suble0d 10164	. . . . . . . . . . 11
140	139	adantr 465	. . . . . . . . . 10 $/\$
141	133, 140	mpbird 232	. . . . . . . . 9 $/\$
142	29, 141	eqbrtrrd 4478	. . . . . . . 8 $/\$
143		dvdsmul1 14016	. . . . . . . . . . . . . . 15 $/\$
144	48, 52, 143	syl2anc 661	. . . . . . . . . . . . . 14
145	144	adantr 465	. . . . . . . . . . . . 13 $/\$
146	145, 115	breqtrrd 4482	. . . . . . . . . . . 12 $/\$
147		gcdcom 14169	. . . . . . . . . . . . . . 15 $/\$
148	30, 48, 147	syl2anc 661	. . . . . . . . . . . . . 14
149	148, 117	eqtr3d 2500	. . . . . . . . . . . . 13
150	149	adantr 465	. . . . . . . . . . . 12 $/\$
151		coprmdvds 14254	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
152	48, 30, 31, 151	syl3anc 1228	. . . . . . . . . . . . 13 $/\$
153	152	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$
154	146, 150, 153	mp2and 679	. . . . . . . . . . 11 $/\$
155		dvdsle 14042	. . . . . . . . . . . . 13 $/\$
156	48, 61, 155	syl2anc 661	. . . . . . . . . . . 12
157	156	adantr 465	. . . . . . . . . . 11 $/\$
158	154, 157	mpd 15	. . . . . . . . . 10 $/\$
159	7, 4, 11, 9	le2sqd 12347	. . . . . . . . . . 11
160	159	adantr 465	. . . . . . . . . 10 $/\$
161	158, 160	mpbid 210	. . . . . . . . 9 $/\$
162	4	resqcld 12338	. . . . . . . . . . 11
163		zsqcl 12240	. . . . . . . . . . . . 13
164	48, 163	syl 16	. . . . . . . . . . . 12
165	164	zred 10990	. . . . . . . . . . 11
166	162, 165	subge0d 10163	. . . . . . . . . 10
167	166	adantr 465	. . . . . . . . 9 $/\$
168	161, 167	mpbird 232	. . . . . . . 8 $/\$
169	135, 138	resubcld 10008	. . . . . . . . . . 11
170	28, 169	eqeltrrd 2546	. . . . . . . . . 10
171		0red 9614	. . . . . . . . . 10
172	170, 171	letri3d 9744	. . . . . . . . 9 $/\$
173	172	adantr 465	. . . . . . . 8 $/\$ $/\$
174	142, 168, 173	mpbir2and 922	. . . . . . 7 $/\$
175	15, 18, 174	subeq0d 9958	. . . . . 6 $/\$
176	5, 8, 10, 12, 175	sq11d 12348	. . . . 5 $/\$
177	2, 176	breqtrrd 4482	. . . 4 $/\$
178		2sqmod.7	. . . . . 6
179	178	adantr 465	. . . . 5 $/\$
180	39	adantr 465	. . . . . 6 $/\$
181	41	adantr 465	. . . . . 6 $/\$
182	19	nn0ge0d 10876	. . . . . . 7
183	182	adantr 465	. . . . . 6 $/\$
184	129	adantr 465	. . . . . 6 $/\$
185	21	adantr 465	. . . . . . 7 $/\$
186	24	adantr 465	. . . . . . 7 $/\$
187	168, 29	breqtrrd 4482	. . . . . . . 8 $/\$
188	169, 171	letri3d 9744	. . . . . . . . 9 $/\$
189	188	adantr 465	. . . . . . . 8 $/\$ $/\$
190	141, 187, 189	mpbir2and 922	. . . . . . 7 $/\$
191	185, 186, 190	subeq0d 9958	. . . . . 6 $/\$
192	180, 181, 183, 184, 191	sq11d 12348	. . . . 5 $/\$
193	179, 192	breqtrrd 4482	. . . 4 $/\$
194	39, 4	letri3d 9744	. . . . 5 $/\$
195	194	adantr 465	. . . 4 $/\$ $/\$
196	177, 193, 195	mpbir2and 922	. . 3 $/\$
197	20	adantr 465	. . . 4 $/\$
198	13	adantr 465	. . . 4 $/\$
199	16	adantr 465	. . . 4 $/\$
200	64	adantr 465	. . . 4 $/\$
201	41	adantr 465	. . . . . . 7 $/\$
202	7	adantr 465	. . . . . . 7 $/\$
203	129	adantr 465	. . . . . . 7 $/\$
204	11	adantr 465	. . . . . . 7 $/\$
205	24	adantr 465	. . . . . . . 8 $/\$
206	17	adantr 465	. . . . . . . 8 $/\$
207		prmnn 14231	. . . . . . . . . . . . 13
208	47, 207	syl 16	. . . . . . . . . . . 12
209	208	nnne0d 10601	. . . . . . . . . . 11
210	209	neneqd 2659	. . . . . . . . . 10
211	210	adantr 465	. . . . . . . . 9 $/\$
212	80, 24, 17	subdid 10033	. . . . . . . . . . . . . . 15
213	80, 24	mulcld 9633	. . . . . . . . . . . . . . . 16
214	21, 24	mulcld 9633	. . . . . . . . . . . . . . . 16
215	80, 17	mulcld 9633	. . . . . . . . . . . . . . . 16
216	14, 17	mulcld 9633	. . . . . . . . . . . . . . . 16
217	17, 24	mulcomd 9634	. . . . . . . . . . . . . . . . . 18
218	25	oveq1d 6311	. . . . . . . . . . . . . . . . . . . 20
219	21, 17	pncan2d 9952	. . . . . . . . . . . . . . . . . . . 20
220	218, 219	eqtr3d 2500	. . . . . . . . . . . . . . . . . . 19
221	220	oveq1d 6311	. . . . . . . . . . . . . . . . . 18
222	26	oveq1d 6311	. . . . . . . . . . . . . . . . . . . 20
223	14, 24	pncan2d 9952	. . . . . . . . . . . . . . . . . . . 20
224	222, 223	eqtr3d 2500	. . . . . . . . . . . . . . . . . . 19
225	224	oveq1d 6311	. . . . . . . . . . . . . . . . . 18
226	217, 221, 225	3eqtr4d 2508	. . . . . . . . . . . . . . . . 17
227	80, 21, 24	subdird 10034	. . . . . . . . . . . . . . . . 17
228	80, 14, 17	subdird 10034	. . . . . . . . . . . . . . . . 17
229	226, 227, 228	3eqtr3d 2506	. . . . . . . . . . . . . . . 16
230	213, 214, 215, 216, 229	subeqxfrd 27709	. . . . . . . . . . . . . . 15
231	212, 230	eqtrd 2498	. . . . . . . . . . . . . 14
232	20, 23	sqmuld 12324	. . . . . . . . . . . . . . 15
233	13, 16	sqmuld 12324	. . . . . . . . . . . . . . 15
234	232, 233	oveq12d 6314	. . . . . . . . . . . . . 14
235	20, 23	mulcld 9633	. . . . . . . . . . . . . . 15
236	13, 16	mulcld 9633	. . . . . . . . . . . . . . 15
237		subsq 12277	. . . . . . . . . . . . . . 15 $/\$
238	235, 236, 237	syl2anc 661	. . . . . . . . . . . . . 14
239	231, 234, 238	3eqtr2d 2504	. . . . . . . . . . . . 13
240	239	adantr 465	. . . . . . . . . . . 12 $/\$
241	235	adantr 465	. . . . . . . . . . . . . 14 $/\$
242		simpll 753	. . . . . . . . . . . . . . . 16 $/\$ $/\$
243		simpr 461	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
244	243	neqned 2660	. . . . . . . . . . . . . . . 16 $/\$ $/\$
245	89, 90	zsubcld 10995	. . . . . . . . . . . . . . . . . . 19
246		dvdssqim 14202	. . . . . . . . . . . . . . . . . . 19 $/\$
247	79, 245, 246	syl2anc 661	. . . . . . . . . . . . . . . . . 18
248	247	imp 429	. . . . . . . . . . . . . . . . 17 $/\$
249	248	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$
250	95	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
251	245	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$
252	235	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$
253	236	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$
254		simpr 461	. . . . . . . . . . . . . . . . . . . 20 $/\$
255	252, 253, 254	subne0d 9959	. . . . . . . . . . . . . . . . . . 19 $/\$
256	251, 255	znsqcld 27711	. . . . . . . . . . . . . . . . . 18 $/\$
257		dvdsle 14042	. . . . . . . . . . . . . . . . . 18 $/\$
258	250, 256, 257	syl2anc 661	. . . . . . . . . . . . . . . . 17 $/\$
259	258	imp 429	. . . . . . . . . . . . . . . 16 $/\$ $/\$
260	242, 244, 249, 259	syl21anc 1227	. . . . . . . . . . . . . . 15 $/\$ $/\$
261	39, 41	remulcld 9641	. . . . . . . . . . . . . . . . . . . . . 22
262	4, 7	remulcld 9641	. . . . . . . . . . . . . . . . . . . . . 22
263	261, 262	resubcld 10008	. . . . . . . . . . . . . . . . . . . . 21
264	263	resqcld 12338	. . . . . . . . . . . . . . . . . . . 20
265	61	nnrpd 11280	. . . . . . . . . . . . . . . . . . . . . . 23
266	127, 265	rpmulcld 11297	. . . . . . . . . . . . . . . . . . . . . 22
267	66	nnrpd 11280	. . . . . . . . . . . . . . . . . . . . . . 23
268	57	nnrpd 11280	. . . . . . . . . . . . . . . . . . . . . . 23
269	267, 268	rpmulcld 11297	. . . . . . . . . . . . . . . . . . . . . 22
270	266, 269	rpaddcld 11296	. . . . . . . . . . . . . . . . . . . . 21
271		2z 10917	. . . . . . . . . . . . . . . . . . . . . 22
272	271	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
273	270, 272	rpexpcld 12335	. . . . . . . . . . . . . . . . . . . 20
274	264, 273	ltaddrp2d 11311	. . . . . . . . . . . . . . . . . . 19
275		bhmafibid2 27785	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
276	39, 7, 4, 41, 275	syl22anc 1229	. . . . . . . . . . . . . . . . . . . . 21
277	74, 276	eqtr3d 2500	. . . . . . . . . . . . . . . . . . . 20
278	82	oveq2d 6312	. . . . . . . . . . . . . . . . . . . . . 22
279	278	oveq1d 6311	. . . . . . . . . . . . . . . . . . . . 21
280	279	oveq2d 6312	. . . . . . . . . . . . . . . . . . . 20
281	277, 280	eqtr4d 2501	. . . . . . . . . . . . . . . . . . 19
282	274, 281	breqtrrd 4482	. . . . . . . . . . . . . . . . . 18
283	282, 81	breqtrrd 4482	. . . . . . . . . . . . . . . . 17
284	242, 283	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
285	264, 100	ltnled 9749	. . . . . . . . . . . . . . . . 17
286	242, 285	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
287	284, 286	mpbid 210	. . . . . . . . . . . . . . 15 $/\$ $/\$
288	260, 287	condan 794	. . . . . . . . . . . . . 14 $/\$
289	241, 288	subeq0bd 10006	. . . . . . . . . . . . 13 $/\$
290	289	oveq2d 6312	. . . . . . . . . . . 12 $/\$
291	235, 236	addcld 9632	. . . . . . . . . . . . . 14
292	291	mul01d 9796	. . . . . . . . . . . . 13
293	292	adantr 465	. . . . . . . . . . . 12 $/\$
294	240, 290, 293	3eqtrd 2502	. . . . . . . . . . 11 $/\$
295	24, 17	subcld 9950	. . . . . . . . . . . . 13
296	80, 295	mul0ord 10220	. . . . . . . . . . . 12 $\/$
297	296	adantr 465	. . . . . . . . . . 11 $/\$ $\/$
298	294, 297	mpbid 210	. . . . . . . . . 10 $/\$ $\/$
299	298	ord 377	. . . . . . . . 9 $/\$
300	211, 299	mpd 15	. . . . . . . 8 $/\$
301	205, 206, 300	subeq0d 9958	. . . . . . 7 $/\$
302	201, 202, 203, 204, 301	sq11d 12348	. . . . . 6 $/\$
303	302	oveq2d 6312	. . . . 5 $/\$
304	303, 288	eqtr3d 2500	. . . 4 $/\$
305	197, 198, 199, 200, 304	mulcan2ad 10206	. . 3 $/\$
306	137, 164	zsubcld 10995	. . . . . 6
307		dvdsmul1 14016	. . . . . 6 $/\$
308	79, 306, 307	syl2anc 661	. . . . 5
309	308, 239	breqtrd 4480	. . . 4
310		euclemma 14260	. . . . 5 $/\$ $/\$ $\/$
311	47, 91, 245, 310	syl3anc 1228	. . . 4 $\/$
312	309, 311	mpbid 210	. . 3 $\/$
313	196, 305, 312	mpjaodan 786	. 2
314	313	oveq1d 6311	. . . . 5
315	314	oveq2d 6312	. . . 4
316	315, 220, 224	3eqtr3d 2506	. . 3
317	7, 41, 11, 129, 316	sq11d 12348	. 2
318	313, 317	jca 532	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369

wceq 1395

wcel 1819

wne 2652 class class class wbr 4456 (class class class)co 6296

cc 9507

cr 9508

cc0 9509

c1 9510

caddc 9512

cmul 9514

clt 9645

cle 9646

cmin 9824

cn 10556

c2 10606

cn0 10816

cz 10885

cexp 12168

cdvds 13997

cgcd 14155

cprime 14228

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586 ax-pre-sup 9587

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-int 4289 df-iun 4334 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6700 df-2nd 6800 df-recs 7060 df-rdg 7094 df-1o 7148 df-2o 7149 df-oadd 7152 df-er 7329 df-en 7536 df-dom 7537 df-sdom 7538 df-fin 7539 df-sup 7919 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-div 10228 df-nn 10557 df-2 10615 df-3 10616 df-n0 10817 df-z 10886 df-uz 11107 df-rp 11246 df-fl 11931 df-mod 11999 df-seq 12110 df-exp 12169 df-cj 12943 df-re 12944 df-im 12945 df-sqrt 13079 df-abs 13080 df-dvds 13998 df-gcd 14156 df-prm 14229

This theorem is referenced by: 2sqmo 27789

W3C validator