2sqmod - Mathbox for Thierry Arnoux

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

Theorem 2sqmod 28484

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 472	. . . . 5 $/\$
3		2sqmod.4	. . . . . . . 8
4	3	nn0red 10950	. . . . . . 7
5	4	adantr 472	. . . . . 6 $/\$
6		2sqmod.3	. . . . . . . 8
7	6	nn0red 10950	. . . . . . 7
8	7	adantr 472	. . . . . 6 $/\$
9	3	nn0ge0d 10952	. . . . . . 7
10	9	adantr 472	. . . . . 6 $/\$
11	6	nn0ge0d 10952	. . . . . . 7
12	11	adantr 472	. . . . . 6 $/\$
13	3	nn0cnd 10951	. . . . . . . . 9
14	13	sqcld 12452	. . . . . . . 8
15	14	adantr 472	. . . . . . 7 $/\$
16	6	nn0cnd 10951	. . . . . . . . 9
17	16	sqcld 12452	. . . . . . . 8
18	17	adantr 472	. . . . . . 7 $/\$
19		2sqmod.2	. . . . . . . . . . . . 13
20	19	nn0cnd 10951	. . . . . . . . . . . 12
21	20	sqcld 12452	. . . . . . . . . . 11
22		2sqmod.5	. . . . . . . . . . . . 13
23	22	nn0cnd 10951	. . . . . . . . . . . 12
24	23	sqcld 12452	. . . . . . . . . . 11
25		2sqmod.8	. . . . . . . . . . . 12
26		2sqmod.9	. . . . . . . . . . . 12
27	25, 26	eqtr4d 2508	. . . . . . . . . . 11
28	21, 17, 14, 24, 27	addeqxfrd 28397	. . . . . . . . . 10
29	28	adantr 472	. . . . . . . . 9 $/\$
30	19	nn0zd 11061	. . . . . . . . . . . . . . . 16
31	3	nn0zd 11061	. . . . . . . . . . . . . . . 16
32		dvdsmul1 14401	. . . . . . . . . . . . . . . 16 $/\$
33	30, 31, 32	syl2anc 673	. . . . . . . . . . . . . . 15
34	33	adantr 472	. . . . . . . . . . . . . 14 $/\$
35	20, 13	mulcld 9681	. . . . . . . . . . . . . . . 16
36	35	adantr 472	. . . . . . . . . . . . . . 15 $/\$
37	16, 23	mulcld 9681	. . . . . . . . . . . . . . . 16
38	37	adantr 472	. . . . . . . . . . . . . . 15 $/\$
39	19	nn0red 10950	. . . . . . . . . . . . . . . . . . . 20
40	39, 4	remulcld 9689	. . . . . . . . . . . . . . . . . . 19
41	22	nn0red 10950	. . . . . . . . . . . . . . . . . . . 20
42	7, 41	remulcld 9689	. . . . . . . . . . . . . . . . . . 19
43	40, 42	resubcld 10068	. . . . . . . . . . . . . . . . . 18
44	43	recnd 9687	. . . . . . . . . . . . . . . . 17
45	44	adantr 472	. . . . . . . . . . . . . . . 16 $/\$
46	43	sqge0d 12481	. . . . . . . . . . . . . . . . . . . . . . 23
47		2sqmod.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
48	6	nn0zd 11061	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
49	47, 30, 48, 25	2sqn0 28482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
50		elnnne0 10907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
51	19, 49, 50	sylanbrc 677	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
52	22	nn0zd 11061	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
53	24, 14	addcomd 9853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
54	53, 26	eqtrd 2505	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
55	47, 52, 31, 54	2sqn0 28482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
56		elnnne0 10907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
57	22, 55, 56	sylanbrc 677	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
58	51, 57	nnmulcld 10679	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
59	47, 31, 52, 26	2sqn0 28482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
60		elnnne0 10907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
61	3, 59, 60	sylanbrc 677	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
62	17, 21	addcomd 9853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
63	62, 25	eqtrd 2505	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
64	47, 48, 30, 63	2sqn0 28482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
65		elnnne0 10907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
66	6, 64, 65	sylanbrc 677	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
67	61, 66	nnmulcld 10679	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
68	58, 67	nnaddcld 10678	. . . . . . . . . . . . . . . . . . . . . . . . . 26
69	68	nnsqcld 12474	. . . . . . . . . . . . . . . . . . . . . . . . 25
70	69	nnred 10646	. . . . . . . . . . . . . . . . . . . . . . . 24
71	43	resqcld 12480	. . . . . . . . . . . . . . . . . . . . . . . 24
72	70, 71	addge02d 10223	. . . . . . . . . . . . . . . . . . . . . . 23
73	46, 72	mpbid 215	. . . . . . . . . . . . . . . . . . . . . 22
74	25, 26	oveq12d 6326	. . . . . . . . . . . . . . . . . . . . . . . 24
75		bhmafibid1 28480	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
76	39, 7, 4, 41, 75	syl22anc 1293	. . . . . . . . . . . . . . . . . . . . . . . 24
77	74, 76	eqtr3d 2507	. . . . . . . . . . . . . . . . . . . . . . 23
78		prmz 14705	. . . . . . . . . . . . . . . . . . . . . . . . . 26
79	47, 78	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25
80	79	zcnd 11064	. . . . . . . . . . . . . . . . . . . . . . . 24
81	80	sqvald 12451	. . . . . . . . . . . . . . . . . . . . . . 23
82	13, 16	mulcomd 9682	. . . . . . . . . . . . . . . . . . . . . . . . . 26
83	82	oveq2d 6324	. . . . . . . . . . . . . . . . . . . . . . . . 25
84	83	oveq1d 6323	. . . . . . . . . . . . . . . . . . . . . . . 24
85	84	oveq2d 6324	. . . . . . . . . . . . . . . . . . . . . . 23
86	77, 81, 85	3eqtr4d 2515	. . . . . . . . . . . . . . . . . . . . . 22
87	73, 86	breqtrrd 4422	. . . . . . . . . . . . . . . . . . . . 21
88	87	adantr 472	. . . . . . . . . . . . . . . . . . . 20 $/\$
89	30, 52	zmulcld 11069	. . . . . . . . . . . . . . . . . . . . . . . 24
90	31, 48	zmulcld 11069	. . . . . . . . . . . . . . . . . . . . . . . 24
91	89, 90	zaddcld 11067	. . . . . . . . . . . . . . . . . . . . . . 23
92		dvdssqim 14600	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
93	79, 91, 92	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . 22
94		zsqcl 12383	. . . . . . . . . . . . . . . . . . . . . . . 24
95	79, 94	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23
96		dvdsle 14427	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
97	95, 69, 96	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . 22
98	93, 97	syld 44	. . . . . . . . . . . . . . . . . . . . 21
99	98	imp 436	. . . . . . . . . . . . . . . . . . . 20 $/\$
100	95	zred 11063	. . . . . . . . . . . . . . . . . . . . . 22
101	70, 100	letri3d 9794	. . . . . . . . . . . . . . . . . . . . 21 $/\$
102	101	adantr 472	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
103	88, 99, 102	mpbir2and 936	. . . . . . . . . . . . . . . . . . 19 $/\$
104	86	adantr 472	. . . . . . . . . . . . . . . . . . 19 $/\$
105	103, 104	eqtr2d 2506	. . . . . . . . . . . . . . . . . 18 $/\$
106	70	recnd 9687	. . . . . . . . . . . . . . . . . . . 20
107	71	recnd 9687	. . . . . . . . . . . . . . . . . . . 20
108	106, 106, 107	subadd2d 10024	. . . . . . . . . . . . . . . . . . 19
109	108	adantr 472	. . . . . . . . . . . . . . . . . 18 $/\$
110	105, 109	mpbird 240	. . . . . . . . . . . . . . . . 17 $/\$
111	106	subidd 9993	. . . . . . . . . . . . . . . . . 18
112	111	adantr 472	. . . . . . . . . . . . . . . . 17 $/\$
113	110, 112	eqtr3d 2507	. . . . . . . . . . . . . . . 16 $/\$
114	45, 113	sqeq0d 12453	. . . . . . . . . . . . . . 15 $/\$
115	36, 38, 114	subeq0d 10013	. . . . . . . . . . . . . 14 $/\$
116	34, 115	breqtrd 4420	. . . . . . . . . . . . 13 $/\$
117	47, 30, 48, 25	2sqcoprm 28483	. . . . . . . . . . . . . 14
118	117	adantr 472	. . . . . . . . . . . . 13 $/\$
119		coprmdvds 14738	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
120	30, 48, 52, 119	syl3anc 1292	. . . . . . . . . . . . . 14 $/\$
121	120	adantr 472	. . . . . . . . . . . . 13 $/\$ $/\$
122	116, 118, 121	mp2and 693	. . . . . . . . . . . 12 $/\$
123		dvdsle 14427	. . . . . . . . . . . . . 14 $/\$
124	30, 57, 123	syl2anc 673	. . . . . . . . . . . . 13
125	124	adantr 472	. . . . . . . . . . . 12 $/\$
126	122, 125	mpd 15	. . . . . . . . . . 11 $/\$
127	51	nnrpd 11362	. . . . . . . . . . . . . 14
128	127	rprege0d 11371	. . . . . . . . . . . . 13 $/\$
129	22	nn0ge0d 10952	. . . . . . . . . . . . 13
130		le2sq 12387	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
131	128, 41, 129, 130	syl12anc 1290	. . . . . . . . . . . 12
132	131	adantr 472	. . . . . . . . . . 11 $/\$
133	126, 132	mpbid 215	. . . . . . . . . 10 $/\$
134	51	nnsqcld 12474	. . . . . . . . . . . . 13
135	134	nnred 10646	. . . . . . . . . . . 12
136		zsqcl 12383	. . . . . . . . . . . . . 14
137	52, 136	syl 17	. . . . . . . . . . . . 13
138	137	zred 11063	. . . . . . . . . . . 12
139	135, 138	suble0d 10225	. . . . . . . . . . 11
140	139	adantr 472	. . . . . . . . . 10 $/\$
141	133, 140	mpbird 240	. . . . . . . . 9 $/\$
142	29, 141	eqbrtrrd 4418	. . . . . . . 8 $/\$
143		dvdsmul1 14401	. . . . . . . . . . . . . . 15 $/\$
144	48, 52, 143	syl2anc 673	. . . . . . . . . . . . . 14
145	144	adantr 472	. . . . . . . . . . . . 13 $/\$
146	145, 115	breqtrrd 4422	. . . . . . . . . . . 12 $/\$
147		gcdcom 14563	. . . . . . . . . . . . . . 15 $/\$
148	30, 48, 147	syl2anc 673	. . . . . . . . . . . . . 14
149	148, 117	eqtr3d 2507	. . . . . . . . . . . . 13
150	149	adantr 472	. . . . . . . . . . . 12 $/\$
151		coprmdvds 14738	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
152	48, 30, 31, 151	syl3anc 1292	. . . . . . . . . . . . 13 $/\$
153	152	adantr 472	. . . . . . . . . . . 12 $/\$ $/\$
154	146, 150, 153	mp2and 693	. . . . . . . . . . 11 $/\$
155		dvdsle 14427	. . . . . . . . . . . . 13 $/\$
156	48, 61, 155	syl2anc 673	. . . . . . . . . . . 12
157	156	adantr 472	. . . . . . . . . . 11 $/\$
158	154, 157	mpd 15	. . . . . . . . . 10 $/\$
159	7, 4, 11, 9	le2sqd 12489	. . . . . . . . . . 11
160	159	adantr 472	. . . . . . . . . 10 $/\$
161	158, 160	mpbid 215	. . . . . . . . 9 $/\$
162	4	resqcld 12480	. . . . . . . . . . 11
163		zsqcl 12383	. . . . . . . . . . . . 13
164	48, 163	syl 17	. . . . . . . . . . . 12
165	164	zred 11063	. . . . . . . . . . 11
166	162, 165	subge0d 10224	. . . . . . . . . 10
167	166	adantr 472	. . . . . . . . 9 $/\$
168	161, 167	mpbird 240	. . . . . . . 8 $/\$
169	135, 138	resubcld 10068	. . . . . . . . . . 11
170	28, 169	eqeltrrd 2550	. . . . . . . . . 10
171		0red 9662	. . . . . . . . . 10
172	170, 171	letri3d 9794	. . . . . . . . 9 $/\$
173	172	adantr 472	. . . . . . . 8 $/\$ $/\$
174	142, 168, 173	mpbir2and 936	. . . . . . 7 $/\$
175	15, 18, 174	subeq0d 10013	. . . . . 6 $/\$
176	5, 8, 10, 12, 175	sq11d 12490	. . . . 5 $/\$
177	2, 176	breqtrrd 4422	. . . 4 $/\$
178		2sqmod.7	. . . . . 6
179	178	adantr 472	. . . . 5 $/\$
180	39	adantr 472	. . . . . 6 $/\$
181	41	adantr 472	. . . . . 6 $/\$
182	19	nn0ge0d 10952	. . . . . . 7
183	182	adantr 472	. . . . . 6 $/\$
184	129	adantr 472	. . . . . 6 $/\$
185	21	adantr 472	. . . . . . 7 $/\$
186	24	adantr 472	. . . . . . 7 $/\$
187	168, 29	breqtrrd 4422	. . . . . . . 8 $/\$
188	169, 171	letri3d 9794	. . . . . . . . 9 $/\$
189	188	adantr 472	. . . . . . . 8 $/\$ $/\$
190	141, 187, 189	mpbir2and 936	. . . . . . 7 $/\$
191	185, 186, 190	subeq0d 10013	. . . . . 6 $/\$
192	180, 181, 183, 184, 191	sq11d 12490	. . . . 5 $/\$
193	179, 192	breqtrrd 4422	. . . 4 $/\$
194	39, 4	letri3d 9794	. . . . 5 $/\$
195	194	adantr 472	. . . 4 $/\$ $/\$
196	177, 193, 195	mpbir2and 936	. . 3 $/\$
197	20	adantr 472	. . . 4 $/\$
198	13	adantr 472	. . . 4 $/\$
199	16	adantr 472	. . . 4 $/\$
200	64	adantr 472	. . . 4 $/\$
201	41	adantr 472	. . . . . . 7 $/\$
202	7	adantr 472	. . . . . . 7 $/\$
203	129	adantr 472	. . . . . . 7 $/\$
204	11	adantr 472	. . . . . . 7 $/\$
205	24	adantr 472	. . . . . . . 8 $/\$
206	17	adantr 472	. . . . . . . 8 $/\$
207		prmnn 14704	. . . . . . . . . . . . 13
208	47, 207	syl 17	. . . . . . . . . . . 12
209	208	nnne0d 10676	. . . . . . . . . . 11
210	209	neneqd 2648	. . . . . . . . . 10
211	210	adantr 472	. . . . . . . . 9 $/\$
212	80, 24, 17	subdid 10095	. . . . . . . . . . . . . . 15
213	80, 24	mulcld 9681	. . . . . . . . . . . . . . . 16
214	21, 24	mulcld 9681	. . . . . . . . . . . . . . . 16
215	80, 17	mulcld 9681	. . . . . . . . . . . . . . . 16
216	14, 17	mulcld 9681	. . . . . . . . . . . . . . . 16
217	17, 24	mulcomd 9682	. . . . . . . . . . . . . . . . . 18
218	25	oveq1d 6323	. . . . . . . . . . . . . . . . . . . 20
219	21, 17	pncan2d 10007	. . . . . . . . . . . . . . . . . . . 20
220	218, 219	eqtr3d 2507	. . . . . . . . . . . . . . . . . . 19
221	220	oveq1d 6323	. . . . . . . . . . . . . . . . . 18
222	26	oveq1d 6323	. . . . . . . . . . . . . . . . . . . 20
223	14, 24	pncan2d 10007	. . . . . . . . . . . . . . . . . . . 20
224	222, 223	eqtr3d 2507	. . . . . . . . . . . . . . . . . . 19
225	224	oveq1d 6323	. . . . . . . . . . . . . . . . . 18
226	217, 221, 225	3eqtr4d 2515	. . . . . . . . . . . . . . . . 17
227	80, 21, 24	subdird 10096	. . . . . . . . . . . . . . . . 17
228	80, 14, 17	subdird 10096	. . . . . . . . . . . . . . . . 17
229	226, 227, 228	3eqtr3d 2513	. . . . . . . . . . . . . . . 16
230	213, 214, 215, 216, 229	subeqxfrd 28396	. . . . . . . . . . . . . . 15
231	212, 230	eqtrd 2505	. . . . . . . . . . . . . 14
232	20, 23	sqmuld 12466	. . . . . . . . . . . . . . 15
233	13, 16	sqmuld 12466	. . . . . . . . . . . . . . 15
234	232, 233	oveq12d 6326	. . . . . . . . . . . . . 14
235	20, 23	mulcld 9681	. . . . . . . . . . . . . . 15
236	13, 16	mulcld 9681	. . . . . . . . . . . . . . 15
237		subsq 12420	. . . . . . . . . . . . . . 15 $/\$
238	235, 236, 237	syl2anc 673	. . . . . . . . . . . . . 14
239	231, 234, 238	3eqtr2d 2511	. . . . . . . . . . . . 13
240	239	adantr 472	. . . . . . . . . . . 12 $/\$
241	235	adantr 472	. . . . . . . . . . . . . 14 $/\$
242		simpll 768	. . . . . . . . . . . . . . . 16 $/\$ $/\$
243		simpr 468	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
244	243	neqned 2650	. . . . . . . . . . . . . . . 16 $/\$ $/\$
245	89, 90	zsubcld 11068	. . . . . . . . . . . . . . . . . . 19
246		dvdssqim 14600	. . . . . . . . . . . . . . . . . . 19 $/\$
247	79, 245, 246	syl2anc 673	. . . . . . . . . . . . . . . . . 18
248	247	imp 436	. . . . . . . . . . . . . . . . 17 $/\$
249	248	adantr 472	. . . . . . . . . . . . . . . 16 $/\$ $/\$
250	95	adantr 472	. . . . . . . . . . . . . . . . . 18 $/\$
251	245	adantr 472	. . . . . . . . . . . . . . . . . . 19 $/\$
252	235	adantr 472	. . . . . . . . . . . . . . . . . . . 20 $/\$
253	236	adantr 472	. . . . . . . . . . . . . . . . . . . 20 $/\$
254		simpr 468	. . . . . . . . . . . . . . . . . . . 20 $/\$
255	252, 253, 254	subne0d 10014	. . . . . . . . . . . . . . . . . . 19 $/\$
256	251, 255	znsqcld 28398	. . . . . . . . . . . . . . . . . 18 $/\$
257		dvdsle 14427	. . . . . . . . . . . . . . . . . 18 $/\$
258	250, 256, 257	syl2anc 673	. . . . . . . . . . . . . . . . 17 $/\$
259	258	imp 436	. . . . . . . . . . . . . . . 16 $/\$ $/\$
260	242, 244, 249, 259	syl21anc 1291	. . . . . . . . . . . . . . 15 $/\$ $/\$
261	39, 41	remulcld 9689	. . . . . . . . . . . . . . . . . . . . . 22
262	4, 7	remulcld 9689	. . . . . . . . . . . . . . . . . . . . . 22
263	261, 262	resubcld 10068	. . . . . . . . . . . . . . . . . . . . 21
264	263	resqcld 12480	. . . . . . . . . . . . . . . . . . . 20
265	61	nnrpd 11362	. . . . . . . . . . . . . . . . . . . . . . 23
266	127, 265	rpmulcld 11380	. . . . . . . . . . . . . . . . . . . . . 22
267	66	nnrpd 11362	. . . . . . . . . . . . . . . . . . . . . . 23
268	57	nnrpd 11362	. . . . . . . . . . . . . . . . . . . . . . 23
269	267, 268	rpmulcld 11380	. . . . . . . . . . . . . . . . . . . . . 22
270	266, 269	rpaddcld 11379	. . . . . . . . . . . . . . . . . . . . 21
271		2z 10993	. . . . . . . . . . . . . . . . . . . . . 22
272	271	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
273	270, 272	rpexpcld 12477	. . . . . . . . . . . . . . . . . . . 20
274	264, 273	ltaddrp2d 11395	. . . . . . . . . . . . . . . . . . 19
275		bhmafibid2 28481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
276	39, 7, 4, 41, 275	syl22anc 1293	. . . . . . . . . . . . . . . . . . . . 21
277	74, 276	eqtr3d 2507	. . . . . . . . . . . . . . . . . . . 20
278	82	oveq2d 6324	. . . . . . . . . . . . . . . . . . . . . 22
279	278	oveq1d 6323	. . . . . . . . . . . . . . . . . . . . 21
280	279	oveq2d 6324	. . . . . . . . . . . . . . . . . . . 20
281	277, 280	eqtr4d 2508	. . . . . . . . . . . . . . . . . . 19
282	274, 281	breqtrrd 4422	. . . . . . . . . . . . . . . . . 18
283	282, 81	breqtrrd 4422	. . . . . . . . . . . . . . . . 17
284	242, 283	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$
285	264, 100	ltnled 9799	. . . . . . . . . . . . . . . . 17
286	242, 285	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$
287	284, 286	mpbid 215	. . . . . . . . . . . . . . 15 $/\$ $/\$
288	260, 287	condan 811	. . . . . . . . . . . . . 14 $/\$
289	241, 288	subeq0bd 10066	. . . . . . . . . . . . 13 $/\$
290	289	oveq2d 6324	. . . . . . . . . . . 12 $/\$
291	235, 236	addcld 9680	. . . . . . . . . . . . . 14
292	291	mul01d 9850	. . . . . . . . . . . . 13
293	292	adantr 472	. . . . . . . . . . . 12 $/\$
294	240, 290, 293	3eqtrd 2509	. . . . . . . . . . 11 $/\$
295	24, 17	subcld 10005	. . . . . . . . . . . . 13
296	80, 295	mul0ord 10284	. . . . . . . . . . . 12 $\/$
297	296	adantr 472	. . . . . . . . . . 11 $/\$ $\/$
298	294, 297	mpbid 215	. . . . . . . . . 10 $/\$ $\/$
299	298	ord 384	. . . . . . . . 9 $/\$
300	211, 299	mpd 15	. . . . . . . 8 $/\$
301	205, 206, 300	subeq0d 10013	. . . . . . 7 $/\$
302	201, 202, 203, 204, 301	sq11d 12490	. . . . . 6 $/\$
303	302	oveq2d 6324	. . . . 5 $/\$
304	303, 288	eqtr3d 2507	. . . 4 $/\$
305	197, 198, 199, 200, 304	mulcan2ad 10270	. . 3 $/\$
306	137, 164	zsubcld 11068	. . . . . 6
307		dvdsmul1 14401	. . . . . 6 $/\$
308	79, 306, 307	syl2anc 673	. . . . 5
309	308, 239	breqtrd 4420	. . . 4
310		euclemma 14744	. . . . 5 $/\$ $/\$ $\/$
311	47, 91, 245, 310	syl3anc 1292	. . . 4 $\/$
312	309, 311	mpbid 215	. . 3 $\/$
313	196, 305, 312	mpjaodan 803	. 2
314	313	oveq1d 6323	. . . . 5
315	314	oveq2d 6324	. . . 4
316	315, 220, 224	3eqtr3d 2513	. . 3
317	7, 41, 11, 129, 316	sq11d 12490	. 2
318	313, 317	jca 541	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $\/$ wo 375 $/\$ wa 376

wceq 1452

wcel 1904

wne 2641 class class class wbr 4395 (class class class)co 6308

cc 9555

cr 9556

cc0 9557

c1 9558

caddc 9560

cmul 9562

clt 9693

cle 9694

cmin 9880

cn 10631

c2 10681

cn0 10893

cz 10961

cexp 12310

cdvds 14382

cgcd 14547

cprime 14701

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-om 6712 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-2o 7201 df-oadd 7204 df-er 7381 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-sup 7974 df-inf 7975 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-3 10691 df-n0 10894 df-z 10962 df-uz 11183 df-rp 11326 df-fl 12061 df-mod 12130 df-seq 12252 df-exp 12311 df-cj 13239 df-re 13240 df-im 13241 df-sqrt 13375 df-abs 13376 df-dvds 14383 df-gcd 14548 df-prm 14702

This theorem is referenced by: 2sqmo 28485

W3C validator