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 27968

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 463	. . . . 5 $/\$
3		2sqmod.4	. . . . . . . 8
4	3	nn0red 10814	. . . . . . 7
5	4	adantr 463	. . . . . 6 $/\$
6		2sqmod.3	. . . . . . . 8
7	6	nn0red 10814	. . . . . . 7
8	7	adantr 463	. . . . . 6 $/\$
9	3	nn0ge0d 10816	. . . . . . 7
10	9	adantr 463	. . . . . 6 $/\$
11	6	nn0ge0d 10816	. . . . . . 7
12	11	adantr 463	. . . . . 6 $/\$
13	3	nn0cnd 10815	. . . . . . . . 9
14	13	sqcld 12262	. . . . . . . 8
15	14	adantr 463	. . . . . . 7 $/\$
16	6	nn0cnd 10815	. . . . . . . . 9
17	16	sqcld 12262	. . . . . . . 8
18	17	adantr 463	. . . . . . 7 $/\$
19		2sqmod.2	. . . . . . . . . . . . 13
20	19	nn0cnd 10815	. . . . . . . . . . . 12
21	20	sqcld 12262	. . . . . . . . . . 11
22		2sqmod.5	. . . . . . . . . . . . 13
23	22	nn0cnd 10815	. . . . . . . . . . . 12
24	23	sqcld 12262	. . . . . . . . . . 11
25		2sqmod.8	. . . . . . . . . . . 12
26		2sqmod.9	. . . . . . . . . . . 12
27	25, 26	eqtr4d 2446	. . . . . . . . . . 11
28	21, 17, 14, 24, 27	addeqxfrd 27887	. . . . . . . . . 10
29	28	adantr 463	. . . . . . . . 9 $/\$
30	19	nn0zd 10926	. . . . . . . . . . . . . . . 16
31	3	nn0zd 10926	. . . . . . . . . . . . . . . 16
32		dvdsmul1 14106	. . . . . . . . . . . . . . . 16 $/\$
33	30, 31, 32	syl2anc 659	. . . . . . . . . . . . . . 15
34	33	adantr 463	. . . . . . . . . . . . . 14 $/\$
35	20, 13	mulcld 9566	. . . . . . . . . . . . . . . 16
36	35	adantr 463	. . . . . . . . . . . . . . 15 $/\$
37	16, 23	mulcld 9566	. . . . . . . . . . . . . . . 16
38	37	adantr 463	. . . . . . . . . . . . . . 15 $/\$
39	19	nn0red 10814	. . . . . . . . . . . . . . . . . . . 20
40	39, 4	remulcld 9574	. . . . . . . . . . . . . . . . . . 19
41	22	nn0red 10814	. . . . . . . . . . . . . . . . . . . 20
42	7, 41	remulcld 9574	. . . . . . . . . . . . . . . . . . 19
43	40, 42	resubcld 9948	. . . . . . . . . . . . . . . . . 18
44	43	recnd 9572	. . . . . . . . . . . . . . . . 17
45	44	adantr 463	. . . . . . . . . . . . . . . 16 $/\$
46	43	sqge0d 12291	. . . . . . . . . . . . . . . . . . . . . . 23
47		2sqmod.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
48	6	nn0zd 10926	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
49	47, 30, 48, 25	2sqn0 27966	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
50		elnnne0 10770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
51	19, 49, 50	sylanbrc 662	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
52	22	nn0zd 10926	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
53	24, 14	addcomd 9736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
54	53, 26	eqtrd 2443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
55	47, 52, 31, 54	2sqn0 27966	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
56		elnnne0 10770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
57	22, 55, 56	sylanbrc 662	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
58	51, 57	nnmulcld 10544	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
59	47, 31, 52, 26	2sqn0 27966	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
60		elnnne0 10770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
61	3, 59, 60	sylanbrc 662	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
62	17, 21	addcomd 9736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
63	62, 25	eqtrd 2443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
64	47, 48, 30, 63	2sqn0 27966	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
65		elnnne0 10770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
66	6, 64, 65	sylanbrc 662	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
67	61, 66	nnmulcld 10544	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
68	58, 67	nnaddcld 10543	. . . . . . . . . . . . . . . . . . . . . . . . . 26
69	68	nnsqcld 12284	. . . . . . . . . . . . . . . . . . . . . . . . 25
70	69	nnred 10511	. . . . . . . . . . . . . . . . . . . . . . . 24
71	43	resqcld 12290	. . . . . . . . . . . . . . . . . . . . . . . 24
72	70, 71	addge02d 10101	. . . . . . . . . . . . . . . . . . . . . . 23
73	46, 72	mpbid 210	. . . . . . . . . . . . . . . . . . . . . 22
74	25, 26	oveq12d 6252	. . . . . . . . . . . . . . . . . . . . . . . 24
75		bhmafibid1 27964	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
76	39, 7, 4, 41, 75	syl22anc 1231	. . . . . . . . . . . . . . . . . . . . . . . 24
77	74, 76	eqtr3d 2445	. . . . . . . . . . . . . . . . . . . . . . 23
78		prmz 14322	. . . . . . . . . . . . . . . . . . . . . . . . . 26
79	47, 78	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25
80	79	zcnd 10929	. . . . . . . . . . . . . . . . . . . . . . . 24
81	80	sqvald 12261	. . . . . . . . . . . . . . . . . . . . . . 23
82	13, 16	mulcomd 9567	. . . . . . . . . . . . . . . . . . . . . . . . . 26
83	82	oveq2d 6250	. . . . . . . . . . . . . . . . . . . . . . . . 25
84	83	oveq1d 6249	. . . . . . . . . . . . . . . . . . . . . . . 24
85	84	oveq2d 6250	. . . . . . . . . . . . . . . . . . . . . . 23
86	77, 81, 85	3eqtr4d 2453	. . . . . . . . . . . . . . . . . . . . . 22
87	73, 86	breqtrrd 4420	. . . . . . . . . . . . . . . . . . . . 21
88	87	adantr 463	. . . . . . . . . . . . . . . . . . . 20 $/\$
89	30, 52	zmulcld 10934	. . . . . . . . . . . . . . . . . . . . . . . 24
90	31, 48	zmulcld 10934	. . . . . . . . . . . . . . . . . . . . . . . 24
91	89, 90	zaddcld 10932	. . . . . . . . . . . . . . . . . . . . . . 23
92		dvdssqim 14292	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
93	79, 91, 92	syl2anc 659	. . . . . . . . . . . . . . . . . . . . . 22
94		zsqcl 12193	. . . . . . . . . . . . . . . . . . . . . . . 24
95	79, 94	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23
96		dvdsle 14132	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
97	95, 69, 96	syl2anc 659	. . . . . . . . . . . . . . . . . . . . . 22
98	93, 97	syld 42	. . . . . . . . . . . . . . . . . . . . 21
99	98	imp 427	. . . . . . . . . . . . . . . . . . . 20 $/\$
100	95	zred 10928	. . . . . . . . . . . . . . . . . . . . . 22
101	70, 100	letri3d 9679	. . . . . . . . . . . . . . . . . . . . 21 $/\$
102	101	adantr 463	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
103	88, 99, 102	mpbir2and 923	. . . . . . . . . . . . . . . . . . 19 $/\$
104	86	adantr 463	. . . . . . . . . . . . . . . . . . 19 $/\$
105	103, 104	eqtr2d 2444	. . . . . . . . . . . . . . . . . 18 $/\$
106	70	recnd 9572	. . . . . . . . . . . . . . . . . . . 20
107	71	recnd 9572	. . . . . . . . . . . . . . . . . . . 20
108	106, 106, 107	subadd2d 9906	. . . . . . . . . . . . . . . . . . 19
109	108	adantr 463	. . . . . . . . . . . . . . . . . 18 $/\$
110	105, 109	mpbird 232	. . . . . . . . . . . . . . . . 17 $/\$
111	106	subidd 9875	. . . . . . . . . . . . . . . . . 18
112	111	adantr 463	. . . . . . . . . . . . . . . . 17 $/\$
113	110, 112	eqtr3d 2445	. . . . . . . . . . . . . . . 16 $/\$
114	45, 113	sqeq0d 12263	. . . . . . . . . . . . . . 15 $/\$
115	36, 38, 114	subeq0d 9895	. . . . . . . . . . . . . 14 $/\$
116	34, 115	breqtrd 4418	. . . . . . . . . . . . 13 $/\$
117	47, 30, 48, 25	2sqcoprm 27967	. . . . . . . . . . . . . 14
118	117	adantr 463	. . . . . . . . . . . . 13 $/\$
119		coprmdvds 14344	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
120	30, 48, 52, 119	syl3anc 1230	. . . . . . . . . . . . . 14 $/\$
121	120	adantr 463	. . . . . . . . . . . . 13 $/\$ $/\$
122	116, 118, 121	mp2and 677	. . . . . . . . . . . 12 $/\$
123		dvdsle 14132	. . . . . . . . . . . . . 14 $/\$
124	30, 57, 123	syl2anc 659	. . . . . . . . . . . . 13
125	124	adantr 463	. . . . . . . . . . . 12 $/\$
126	122, 125	mpd 15	. . . . . . . . . . 11 $/\$
127	51	nnrpd 11220	. . . . . . . . . . . . . 14
128	127	rprege0d 11229	. . . . . . . . . . . . 13 $/\$
129	22	nn0ge0d 10816	. . . . . . . . . . . . 13
130		le2sq 12197	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
131	128, 41, 129, 130	syl12anc 1228	. . . . . . . . . . . 12
132	131	adantr 463	. . . . . . . . . . 11 $/\$
133	126, 132	mpbid 210	. . . . . . . . . 10 $/\$
134	51	nnsqcld 12284	. . . . . . . . . . . . 13
135	134	nnred 10511	. . . . . . . . . . . 12
136		zsqcl 12193	. . . . . . . . . . . . . 14
137	52, 136	syl 17	. . . . . . . . . . . . 13
138	137	zred 10928	. . . . . . . . . . . 12
139	135, 138	suble0d 10103	. . . . . . . . . . 11
140	139	adantr 463	. . . . . . . . . 10 $/\$
141	133, 140	mpbird 232	. . . . . . . . 9 $/\$
142	29, 141	eqbrtrrd 4416	. . . . . . . 8 $/\$
143		dvdsmul1 14106	. . . . . . . . . . . . . . 15 $/\$
144	48, 52, 143	syl2anc 659	. . . . . . . . . . . . . 14
145	144	adantr 463	. . . . . . . . . . . . 13 $/\$
146	145, 115	breqtrrd 4420	. . . . . . . . . . . 12 $/\$
147		gcdcom 14259	. . . . . . . . . . . . . . 15 $/\$
148	30, 48, 147	syl2anc 659	. . . . . . . . . . . . . 14
149	148, 117	eqtr3d 2445	. . . . . . . . . . . . 13
150	149	adantr 463	. . . . . . . . . . . 12 $/\$
151		coprmdvds 14344	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
152	48, 30, 31, 151	syl3anc 1230	. . . . . . . . . . . . 13 $/\$
153	152	adantr 463	. . . . . . . . . . . 12 $/\$ $/\$
154	146, 150, 153	mp2and 677	. . . . . . . . . . 11 $/\$
155		dvdsle 14132	. . . . . . . . . . . . 13 $/\$
156	48, 61, 155	syl2anc 659	. . . . . . . . . . . 12
157	156	adantr 463	. . . . . . . . . . 11 $/\$
158	154, 157	mpd 15	. . . . . . . . . 10 $/\$
159	7, 4, 11, 9	le2sqd 12299	. . . . . . . . . . 11
160	159	adantr 463	. . . . . . . . . 10 $/\$
161	158, 160	mpbid 210	. . . . . . . . 9 $/\$
162	4	resqcld 12290	. . . . . . . . . . 11
163		zsqcl 12193	. . . . . . . . . . . . 13
164	48, 163	syl 17	. . . . . . . . . . . 12
165	164	zred 10928	. . . . . . . . . . 11
166	162, 165	subge0d 10102	. . . . . . . . . 10
167	166	adantr 463	. . . . . . . . 9 $/\$
168	161, 167	mpbird 232	. . . . . . . 8 $/\$
169	135, 138	resubcld 9948	. . . . . . . . . . 11
170	28, 169	eqeltrrd 2491	. . . . . . . . . 10
171		0red 9547	. . . . . . . . . 10
172	170, 171	letri3d 9679	. . . . . . . . 9 $/\$
173	172	adantr 463	. . . . . . . 8 $/\$ $/\$
174	142, 168, 173	mpbir2and 923	. . . . . . 7 $/\$
175	15, 18, 174	subeq0d 9895	. . . . . 6 $/\$
176	5, 8, 10, 12, 175	sq11d 12300	. . . . 5 $/\$
177	2, 176	breqtrrd 4420	. . . 4 $/\$
178		2sqmod.7	. . . . . 6
179	178	adantr 463	. . . . 5 $/\$
180	39	adantr 463	. . . . . 6 $/\$
181	41	adantr 463	. . . . . 6 $/\$
182	19	nn0ge0d 10816	. . . . . . 7
183	182	adantr 463	. . . . . 6 $/\$
184	129	adantr 463	. . . . . 6 $/\$
185	21	adantr 463	. . . . . . 7 $/\$
186	24	adantr 463	. . . . . . 7 $/\$
187	168, 29	breqtrrd 4420	. . . . . . . 8 $/\$
188	169, 171	letri3d 9679	. . . . . . . . 9 $/\$
189	188	adantr 463	. . . . . . . 8 $/\$ $/\$
190	141, 187, 189	mpbir2and 923	. . . . . . 7 $/\$
191	185, 186, 190	subeq0d 9895	. . . . . 6 $/\$
192	180, 181, 183, 184, 191	sq11d 12300	. . . . 5 $/\$
193	179, 192	breqtrrd 4420	. . . 4 $/\$
194	39, 4	letri3d 9679	. . . . 5 $/\$
195	194	adantr 463	. . . 4 $/\$ $/\$
196	177, 193, 195	mpbir2and 923	. . 3 $/\$
197	20	adantr 463	. . . 4 $/\$
198	13	adantr 463	. . . 4 $/\$
199	16	adantr 463	. . . 4 $/\$
200	64	adantr 463	. . . 4 $/\$
201	41	adantr 463	. . . . . . 7 $/\$
202	7	adantr 463	. . . . . . 7 $/\$
203	129	adantr 463	. . . . . . 7 $/\$
204	11	adantr 463	. . . . . . 7 $/\$
205	24	adantr 463	. . . . . . . 8 $/\$
206	17	adantr 463	. . . . . . . 8 $/\$
207		prmnn 14321	. . . . . . . . . . . . 13
208	47, 207	syl 17	. . . . . . . . . . . 12
209	208	nnne0d 10541	. . . . . . . . . . 11
210	209	neneqd 2605	. . . . . . . . . 10
211	210	adantr 463	. . . . . . . . 9 $/\$
212	80, 24, 17	subdid 9973	. . . . . . . . . . . . . . 15
213	80, 24	mulcld 9566	. . . . . . . . . . . . . . . 16
214	21, 24	mulcld 9566	. . . . . . . . . . . . . . . 16
215	80, 17	mulcld 9566	. . . . . . . . . . . . . . . 16
216	14, 17	mulcld 9566	. . . . . . . . . . . . . . . 16
217	17, 24	mulcomd 9567	. . . . . . . . . . . . . . . . . 18
218	25	oveq1d 6249	. . . . . . . . . . . . . . . . . . . 20
219	21, 17	pncan2d 9889	. . . . . . . . . . . . . . . . . . . 20
220	218, 219	eqtr3d 2445	. . . . . . . . . . . . . . . . . . 19
221	220	oveq1d 6249	. . . . . . . . . . . . . . . . . 18
222	26	oveq1d 6249	. . . . . . . . . . . . . . . . . . . 20
223	14, 24	pncan2d 9889	. . . . . . . . . . . . . . . . . . . 20
224	222, 223	eqtr3d 2445	. . . . . . . . . . . . . . . . . . 19
225	224	oveq1d 6249	. . . . . . . . . . . . . . . . . 18
226	217, 221, 225	3eqtr4d 2453	. . . . . . . . . . . . . . . . 17
227	80, 21, 24	subdird 9974	. . . . . . . . . . . . . . . . 17
228	80, 14, 17	subdird 9974	. . . . . . . . . . . . . . . . 17
229	226, 227, 228	3eqtr3d 2451	. . . . . . . . . . . . . . . 16
230	213, 214, 215, 216, 229	subeqxfrd 27886	. . . . . . . . . . . . . . 15
231	212, 230	eqtrd 2443	. . . . . . . . . . . . . 14
232	20, 23	sqmuld 12276	. . . . . . . . . . . . . . 15
233	13, 16	sqmuld 12276	. . . . . . . . . . . . . . 15
234	232, 233	oveq12d 6252	. . . . . . . . . . . . . 14
235	20, 23	mulcld 9566	. . . . . . . . . . . . . . 15
236	13, 16	mulcld 9566	. . . . . . . . . . . . . . 15
237		subsq 12230	. . . . . . . . . . . . . . 15 $/\$
238	235, 236, 237	syl2anc 659	. . . . . . . . . . . . . 14
239	231, 234, 238	3eqtr2d 2449	. . . . . . . . . . . . 13
240	239	adantr 463	. . . . . . . . . . . 12 $/\$
241	235	adantr 463	. . . . . . . . . . . . . 14 $/\$
242		simpll 752	. . . . . . . . . . . . . . . 16 $/\$ $/\$
243		simpr 459	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
244	243	neqned 2606	. . . . . . . . . . . . . . . 16 $/\$ $/\$
245	89, 90	zsubcld 10933	. . . . . . . . . . . . . . . . . . 19
246		dvdssqim 14292	. . . . . . . . . . . . . . . . . . 19 $/\$
247	79, 245, 246	syl2anc 659	. . . . . . . . . . . . . . . . . 18
248	247	imp 427	. . . . . . . . . . . . . . . . 17 $/\$
249	248	adantr 463	. . . . . . . . . . . . . . . 16 $/\$ $/\$
250	95	adantr 463	. . . . . . . . . . . . . . . . . 18 $/\$
251	245	adantr 463	. . . . . . . . . . . . . . . . . . 19 $/\$
252	235	adantr 463	. . . . . . . . . . . . . . . . . . . 20 $/\$
253	236	adantr 463	. . . . . . . . . . . . . . . . . . . 20 $/\$
254		simpr 459	. . . . . . . . . . . . . . . . . . . 20 $/\$
255	252, 253, 254	subne0d 9896	. . . . . . . . . . . . . . . . . . 19 $/\$
256	251, 255	znsqcld 27888	. . . . . . . . . . . . . . . . . 18 $/\$
257		dvdsle 14132	. . . . . . . . . . . . . . . . . 18 $/\$
258	250, 256, 257	syl2anc 659	. . . . . . . . . . . . . . . . 17 $/\$
259	258	imp 427	. . . . . . . . . . . . . . . 16 $/\$ $/\$
260	242, 244, 249, 259	syl21anc 1229	. . . . . . . . . . . . . . 15 $/\$ $/\$
261	39, 41	remulcld 9574	. . . . . . . . . . . . . . . . . . . . . 22
262	4, 7	remulcld 9574	. . . . . . . . . . . . . . . . . . . . . 22
263	261, 262	resubcld 9948	. . . . . . . . . . . . . . . . . . . . 21
264	263	resqcld 12290	. . . . . . . . . . . . . . . . . . . 20
265	61	nnrpd 11220	. . . . . . . . . . . . . . . . . . . . . . 23
266	127, 265	rpmulcld 11238	. . . . . . . . . . . . . . . . . . . . . 22
267	66	nnrpd 11220	. . . . . . . . . . . . . . . . . . . . . . 23
268	57	nnrpd 11220	. . . . . . . . . . . . . . . . . . . . . . 23
269	267, 268	rpmulcld 11238	. . . . . . . . . . . . . . . . . . . . . 22
270	266, 269	rpaddcld 11237	. . . . . . . . . . . . . . . . . . . . 21
271		2z 10857	. . . . . . . . . . . . . . . . . . . . . 22
272	271	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
273	270, 272	rpexpcld 12287	. . . . . . . . . . . . . . . . . . . 20
274	264, 273	ltaddrp2d 11252	. . . . . . . . . . . . . . . . . . 19
275		bhmafibid2 27965	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
276	39, 7, 4, 41, 275	syl22anc 1231	. . . . . . . . . . . . . . . . . . . . 21
277	74, 276	eqtr3d 2445	. . . . . . . . . . . . . . . . . . . 20
278	82	oveq2d 6250	. . . . . . . . . . . . . . . . . . . . . 22
279	278	oveq1d 6249	. . . . . . . . . . . . . . . . . . . . 21
280	279	oveq2d 6250	. . . . . . . . . . . . . . . . . . . 20
281	277, 280	eqtr4d 2446	. . . . . . . . . . . . . . . . . . 19
282	274, 281	breqtrrd 4420	. . . . . . . . . . . . . . . . . 18
283	282, 81	breqtrrd 4420	. . . . . . . . . . . . . . . . 17
284	242, 283	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$
285	264, 100	ltnled 9684	. . . . . . . . . . . . . . . . 17
286	242, 285	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$
287	284, 286	mpbid 210	. . . . . . . . . . . . . . 15 $/\$ $/\$
288	260, 287	condan 795	. . . . . . . . . . . . . 14 $/\$
289	241, 288	subeq0bd 9946	. . . . . . . . . . . . 13 $/\$
290	289	oveq2d 6250	. . . . . . . . . . . 12 $/\$
291	235, 236	addcld 9565	. . . . . . . . . . . . . 14
292	291	mul01d 9733	. . . . . . . . . . . . 13
293	292	adantr 463	. . . . . . . . . . . 12 $/\$
294	240, 290, 293	3eqtrd 2447	. . . . . . . . . . 11 $/\$
295	24, 17	subcld 9887	. . . . . . . . . . . . 13
296	80, 295	mul0ord 10160	. . . . . . . . . . . 12 $\/$
297	296	adantr 463	. . . . . . . . . . 11 $/\$ $\/$
298	294, 297	mpbid 210	. . . . . . . . . 10 $/\$ $\/$
299	298	ord 375	. . . . . . . . 9 $/\$
300	211, 299	mpd 15	. . . . . . . 8 $/\$
301	205, 206, 300	subeq0d 9895	. . . . . . 7 $/\$
302	201, 202, 203, 204, 301	sq11d 12300	. . . . . 6 $/\$
303	302	oveq2d 6250	. . . . 5 $/\$
304	303, 288	eqtr3d 2445	. . . 4 $/\$
305	197, 198, 199, 200, 304	mulcan2ad 10146	. . 3 $/\$
306	137, 164	zsubcld 10933	. . . . . 6
307		dvdsmul1 14106	. . . . . 6 $/\$
308	79, 306, 307	syl2anc 659	. . . . 5
309	308, 239	breqtrd 4418	. . . 4
310		euclemma 14350	. . . . 5 $/\$ $/\$ $\/$
311	47, 91, 245, 310	syl3anc 1230	. . . 4 $\/$
312	309, 311	mpbid 210	. . 3 $\/$
313	196, 305, 312	mpjaodan 787	. 2
314	313	oveq1d 6249	. . . . 5
315	314	oveq2d 6250	. . . 4
316	315, 220, 224	3eqtr3d 2451	. . 3
317	7, 41, 11, 129, 316	sq11d 12300	. 2
318	313, 317	jca 530	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 366 $/\$ wa 367

wceq 1405

wcel 1842

wne 2598 class class class wbr 4394 (class class class)co 6234

cc 9440

cr 9441

cc0 9442

c1 9443

caddc 9445

cmul 9447

clt 9578

cle 9579

cmin 9761

cn 10496

c2 10546

cn0 10756

cz 10825

cexp 12120

cdvds 14087

cgcd 14245

cprime 14318

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1639 ax-4 1652 ax-5 1725 ax-6 1771 ax-7 1814 ax-8 1844 ax-9 1846 ax-10 1861 ax-11 1866 ax-12 1878 ax-13 2026 ax-ext 2380 ax-sep 4516 ax-nul 4524 ax-pow 4571 ax-pr 4629 ax-un 6530 ax-cnex 9498 ax-resscn 9499 ax-1cn 9500 ax-icn 9501 ax-addcl 9502 ax-addrcl 9503 ax-mulcl 9504 ax-mulrcl 9505 ax-mulcom 9506 ax-addass 9507 ax-mulass 9508 ax-distr 9509 ax-i2m1 9510 ax-1ne0 9511 ax-1rid 9512 ax-rnegex 9513 ax-rrecex 9514 ax-cnre 9515 ax-pre-lttri 9516 ax-pre-lttrn 9517 ax-pre-ltadd 9518 ax-pre-mulgt0 9519 ax-pre-sup 9520

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 975 df-3an 976 df-tru 1408 df-ex 1634 df-nf 1638 df-sb 1764 df-eu 2242 df-mo 2243 df-clab 2388 df-cleq 2394 df-clel 2397 df-nfc 2552 df-ne 2600 df-nel 2601 df-ral 2758 df-rex 2759 df-reu 2760 df-rmo 2761 df-rab 2762 df-v 3060 df-sbc 3277 df-csb 3373 df-dif 3416 df-un 3418 df-in 3420 df-ss 3427 df-pss 3429 df-nul 3738 df-if 3885 df-pw 3956 df-sn 3972 df-pr 3974 df-tp 3976 df-op 3978 df-uni 4191 df-int 4227 df-iun 4272 df-br 4395 df-opab 4453 df-mpt 4454 df-tr 4489 df-eprel 4733 df-id 4737 df-po 4743 df-so 4744 df-fr 4781 df-we 4783 df-ord 4824 df-on 4825 df-lim 4826 df-suc 4827 df-xp 4948 df-rel 4949 df-cnv 4950 df-co 4951 df-dm 4952 df-rn 4953 df-res 4954 df-ima 4955 df-iota 5489 df-fun 5527 df-fn 5528 df-f 5529 df-f1 5530 df-fo 5531 df-f1o 5532 df-fv 5533 df-riota 6196 df-ov 6237 df-oprab 6238 df-mpt2 6239 df-om 6639 df-2nd 6739 df-recs 6999 df-rdg 7033 df-1o 7087 df-2o 7088 df-oadd 7091 df-er 7268 df-en 7475 df-dom 7476 df-sdom 7477 df-fin 7478 df-sup 7855 df-pnf 9580 df-mnf 9581 df-xr 9582 df-ltxr 9583 df-le 9584 df-sub 9763 df-neg 9764 df-div 10168 df-nn 10497 df-2 10555 df-3 10556 df-n0 10757 df-z 10826 df-uz 11046 df-rp 11184 df-fl 11879 df-mod 11948 df-seq 12062 df-exp 12121 df-cj 12988 df-re 12989 df-im 12990 df-sqrt 13124 df-abs 13125 df-dvds 14088 df-gcd 14246 df-prm 14319

This theorem is referenced by: 2sqmo 27969

W3C validator