Metamath Proof Explorer


Theorem 2sqmod

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)

Ref Expression
Hypotheses 2sqmod.1 φP
2sqmod.2 φA0
2sqmod.3 φB0
2sqmod.4 φC0
2sqmod.5 φD0
2sqmod.6 φAB
2sqmod.7 φCD
2sqmod.8 φA2+B2=P
2sqmod.9 φC2+D2=P
Assertion 2sqmod φA=CB=D

Proof

Step Hyp Ref Expression
1 2sqmod.1 φP
2 2sqmod.2 φA0
3 2sqmod.3 φB0
4 2sqmod.4 φC0
5 2sqmod.5 φD0
6 2sqmod.6 φAB
7 2sqmod.7 φCD
8 2sqmod.8 φA2+B2=P
9 2sqmod.9 φC2+D2=P
10 6 adantr φPAD+CBAB
11 4 nn0red φC
12 11 adantr φPAD+CBC
13 3 nn0red φB
14 13 adantr φPAD+CBB
15 4 nn0ge0d φ0C
16 15 adantr φPAD+CB0C
17 3 nn0ge0d φ0B
18 17 adantr φPAD+CB0B
19 4 nn0cnd φC
20 19 sqcld φC2
21 20 adantr φPAD+CBC2
22 3 nn0cnd φB
23 22 sqcld φB2
24 23 adantr φPAD+CBB2
25 2 nn0cnd φA
26 25 sqcld φA2
27 5 nn0cnd φD
28 27 sqcld φD2
29 8 9 eqtr4d φA2+B2=C2+D2
30 26 23 20 28 29 subaddeqd φA2D2=C2B2
31 30 adantr φPAD+CBA2D2=C2B2
32 2 nn0zd φA
33 4 nn0zd φC
34 dvdsmul1 ACAAC
35 32 33 34 syl2anc φAAC
36 35 adantr φPAD+CBAAC
37 25 19 mulcld φAC
38 37 adantr φPAD+CBAC
39 22 27 mulcld φBD
40 39 adantr φPAD+CBBD
41 2 nn0red φA
42 41 11 remulcld φAC
43 5 nn0red φD
44 13 43 remulcld φBD
45 42 44 resubcld φACBD
46 45 recnd φACBD
47 46 adantr φPAD+CBACBD
48 45 sqge0d φ0ACBD2
49 3 nn0zd φB
50 1 32 49 8 2sqn0 φA0
51 elnnne0 AA0A0
52 2 50 51 sylanbrc φA
53 5 nn0zd φD
54 28 20 addcomd φD2+C2=C2+D2
55 54 9 eqtrd φD2+C2=P
56 1 53 33 55 2sqn0 φD0
57 elnnne0 DD0D0
58 5 56 57 sylanbrc φD
59 52 58 nnmulcld φAD
60 1 33 53 9 2sqn0 φC0
61 elnnne0 CC0C0
62 4 60 61 sylanbrc φC
63 23 26 addcomd φB2+A2=A2+B2
64 63 8 eqtrd φB2+A2=P
65 1 49 32 64 2sqn0 φB0
66 elnnne0 BB0B0
67 3 65 66 sylanbrc φB
68 62 67 nnmulcld φCB
69 59 68 nnaddcld φAD+CB
70 69 nnsqcld φAD+CB2
71 70 nnred φAD+CB2
72 45 resqcld φACBD2
73 71 72 addge02d φ0ACBD2AD+CB2ACBD2+AD+CB2
74 48 73 mpbid φAD+CB2ACBD2+AD+CB2
75 8 9 oveq12d φA2+B2C2+D2=PP
76 bhmafibid1 ABCDA2+B2C2+D2=ACBD2+AD+BC2
77 41 13 11 43 76 syl22anc φA2+B2C2+D2=ACBD2+AD+BC2
78 75 77 eqtr3d φPP=ACBD2+AD+BC2
79 prmz PP
80 1 79 syl φP
81 80 zcnd φP
82 81 sqvald φP2=PP
83 19 22 mulcomd φCB=BC
84 83 oveq2d φAD+CB=AD+BC
85 84 oveq1d φAD+CB2=AD+BC2
86 85 oveq2d φACBD2+AD+CB2=ACBD2+AD+BC2
87 78 82 86 3eqtr4d φP2=ACBD2+AD+CB2
88 74 87 breqtrrd φAD+CB2P2
89 88 adantr φPAD+CBAD+CB2P2
90 32 53 zmulcld φAD
91 33 49 zmulcld φCB
92 90 91 zaddcld φAD+CB
93 dvdssqim PAD+CBPAD+CBP2AD+CB2
94 80 92 93 syl2anc φPAD+CBP2AD+CB2
95 zsqcl PP2
96 80 95 syl φP2
97 dvdsle P2AD+CB2P2AD+CB2P2AD+CB2
98 96 70 97 syl2anc φP2AD+CB2P2AD+CB2
99 94 98 syld φPAD+CBP2AD+CB2
100 99 imp φPAD+CBP2AD+CB2
101 96 zred φP2
102 71 101 letri3d φAD+CB2=P2AD+CB2P2P2AD+CB2
103 102 adantr φPAD+CBAD+CB2=P2AD+CB2P2P2AD+CB2
104 89 100 103 mpbir2and φPAD+CBAD+CB2=P2
105 87 adantr φPAD+CBP2=ACBD2+AD+CB2
106 104 105 eqtr2d φPAD+CBACBD2+AD+CB2=AD+CB2
107 71 recnd φAD+CB2
108 72 recnd φACBD2
109 107 107 108 subadd2d φAD+CB2AD+CB2=ACBD2ACBD2+AD+CB2=AD+CB2
110 109 adantr φPAD+CBAD+CB2AD+CB2=ACBD2ACBD2+AD+CB2=AD+CB2
111 106 110 mpbird φPAD+CBAD+CB2AD+CB2=ACBD2
112 107 subidd φAD+CB2AD+CB2=0
113 112 adantr φPAD+CBAD+CB2AD+CB2=0
114 111 113 eqtr3d φPAD+CBACBD2=0
115 47 114 sqeq0d φPAD+CBACBD=0
116 38 40 115 subeq0d φPAD+CBAC=BD
117 36 116 breqtrd φPAD+CBABD
118 1 32 49 8 2sqcoprm φAgcdB=1
119 118 adantr φPAD+CBAgcdB=1
120 coprmdvds ABDABDAgcdB=1AD
121 32 49 53 120 syl3anc φABDAgcdB=1AD
122 121 adantr φPAD+CBABDAgcdB=1AD
123 117 119 122 mp2and φPAD+CBAD
124 dvdsle ADADAD
125 32 58 124 syl2anc φADAD
126 125 adantr φPAD+CBADAD
127 123 126 mpd φPAD+CBAD
128 52 nnrpd φA+
129 128 rprege0d φA0A
130 5 nn0ge0d φ0D
131 le2sq A0AD0DADA2D2
132 129 43 130 131 syl12anc φADA2D2
133 132 adantr φPAD+CBADA2D2
134 127 133 mpbid φPAD+CBA2D2
135 52 nnsqcld φA2
136 135 nnred φA2
137 zsqcl DD2
138 53 137 syl φD2
139 138 zred φD2
140 136 139 suble0d φA2D20A2D2
141 140 adantr φPAD+CBA2D20A2D2
142 134 141 mpbird φPAD+CBA2D20
143 31 142 eqbrtrrd φPAD+CBC2B20
144 dvdsmul1 BDBBD
145 49 53 144 syl2anc φBBD
146 145 adantr φPAD+CBBBD
147 146 116 breqtrrd φPAD+CBBAC
148 32 49 gcdcomd φAgcdB=BgcdA
149 148 118 eqtr3d φBgcdA=1
150 149 adantr φPAD+CBBgcdA=1
151 coprmdvds BACBACBgcdA=1BC
152 49 32 33 151 syl3anc φBACBgcdA=1BC
153 152 adantr φPAD+CBBACBgcdA=1BC
154 147 150 153 mp2and φPAD+CBBC
155 dvdsle BCBCBC
156 49 62 155 syl2anc φBCBC
157 156 adantr φPAD+CBBCBC
158 154 157 mpd φPAD+CBBC
159 13 11 17 15 le2sqd φBCB2C2
160 159 adantr φPAD+CBBCB2C2
161 158 160 mpbid φPAD+CBB2C2
162 11 resqcld φC2
163 zsqcl BB2
164 49 163 syl φB2
165 164 zred φB2
166 162 165 subge0d φ0C2B2B2C2
167 166 adantr φPAD+CB0C2B2B2C2
168 161 167 mpbird φPAD+CB0C2B2
169 136 139 resubcld φA2D2
170 30 169 eqeltrrd φC2B2
171 0red φ0
172 170 171 letri3d φC2B2=0C2B200C2B2
173 172 adantr φPAD+CBC2B2=0C2B200C2B2
174 143 168 173 mpbir2and φPAD+CBC2B2=0
175 21 24 174 subeq0d φPAD+CBC2=B2
176 12 14 16 18 175 sq11d φPAD+CBC=B
177 10 176 breqtrrd φPAD+CBAC
178 7 adantr φPAD+CBCD
179 41 adantr φPAD+CBA
180 43 adantr φPAD+CBD
181 2 nn0ge0d φ0A
182 181 adantr φPAD+CB0A
183 130 adantr φPAD+CB0D
184 26 adantr φPAD+CBA2
185 28 adantr φPAD+CBD2
186 168 31 breqtrrd φPAD+CB0A2D2
187 169 171 letri3d φA2D2=0A2D200A2D2
188 187 adantr φPAD+CBA2D2=0A2D200A2D2
189 142 186 188 mpbir2and φPAD+CBA2D2=0
190 184 185 189 subeq0d φPAD+CBA2=D2
191 179 180 182 183 190 sq11d φPAD+CBA=D
192 178 191 breqtrrd φPAD+CBCA
193 41 11 letri3d φA=CACCA
194 193 adantr φPAD+CBA=CACCA
195 177 192 194 mpbir2and φPAD+CBA=C
196 25 adantr φPADCBA
197 19 adantr φPADCBC
198 22 adantr φPADCBB
199 65 adantr φPADCBB0
200 43 adantr φPADCBD
201 13 adantr φPADCBB
202 130 adantr φPADCB0D
203 17 adantr φPADCB0B
204 28 adantr φPADCBD2
205 23 adantr φPADCBB2
206 prmnn PP
207 1 206 syl φP
208 207 nnne0d φP0
209 208 neneqd φ¬P=0
210 209 adantr φPADCB¬P=0
211 81 28 23 subdid φPD2B2=PD2PB2
212 81 28 mulcld φPD2
213 26 28 mulcld φA2D2
214 81 23 mulcld φPB2
215 20 23 mulcld φC2B2
216 23 28 mulcomd φB2D2=D2B2
217 8 oveq1d φA2+B2-A2=PA2
218 26 23 pncan2d φA2+B2-A2=B2
219 217 218 eqtr3d φPA2=B2
220 219 oveq1d φPA2D2=B2D2
221 9 oveq1d φC2+D2-C2=PC2
222 20 28 pncan2d φC2+D2-C2=D2
223 221 222 eqtr3d φPC2=D2
224 223 oveq1d φPC2B2=D2B2
225 216 220 224 3eqtr4d φPA2D2=PC2B2
226 81 26 28 subdird φPA2D2=PD2A2D2
227 81 20 23 subdird φPC2B2=PB2C2B2
228 225 226 227 3eqtr3d φPD2A2D2=PB2C2B2
229 212 213 214 215 228 subeqxfrd φPD2PB2=A2D2C2B2
230 211 229 eqtrd φPD2B2=A2D2C2B2
231 25 27 sqmuld φAD2=A2D2
232 19 22 sqmuld φCB2=C2B2
233 231 232 oveq12d φAD2CB2=A2D2C2B2
234 25 27 mulcld φAD
235 19 22 mulcld φCB
236 subsq ADCBAD2CB2=AD+CBADCB
237 234 235 236 syl2anc φAD2CB2=AD+CBADCB
238 230 233 237 3eqtr2d φPD2B2=AD+CBADCB
239 238 adantr φPADCBPD2B2=AD+CBADCB
240 234 adantr φPADCBAD
241 simpll φPADCB¬AD=CBφ
242 simpr φPADCB¬AD=CB¬AD=CB
243 242 neqned φPADCB¬AD=CBADCB
244 90 91 zsubcld φADCB
245 dvdssqim PADCBPADCBP2ADCB2
246 80 244 245 syl2anc φPADCBP2ADCB2
247 246 imp φPADCBP2ADCB2
248 247 adantr φPADCB¬AD=CBP2ADCB2
249 96 adantr φADCBP2
250 244 adantr φADCBADCB
251 234 adantr φADCBAD
252 235 adantr φADCBCB
253 simpr φADCBADCB
254 251 252 253 subne0d φADCBADCB0
255 250 254 znsqcld φADCBADCB2
256 dvdsle P2ADCB2P2ADCB2P2ADCB2
257 249 255 256 syl2anc φADCBP2ADCB2P2ADCB2
258 257 imp φADCBP2ADCB2P2ADCB2
259 241 243 248 258 syl21anc φPADCB¬AD=CBP2ADCB2
260 41 43 remulcld φAD
261 11 13 remulcld φCB
262 260 261 resubcld φADCB
263 262 resqcld φADCB2
264 62 nnrpd φC+
265 128 264 rpmulcld φAC+
266 67 nnrpd φB+
267 58 nnrpd φD+
268 266 267 rpmulcld φBD+
269 265 268 rpaddcld φAC+BD+
270 2z 2
271 270 a1i φ2
272 269 271 rpexpcld φAC+BD2+
273 263 272 ltaddrp2d φADCB2<AC+BD2+ADCB2
274 bhmafibid2 ABCDA2+B2C2+D2=AC+BD2+ADBC2
275 41 13 11 43 274 syl22anc φA2+B2C2+D2=AC+BD2+ADBC2
276 75 275 eqtr3d φPP=AC+BD2+ADBC2
277 83 oveq2d φADCB=ADBC
278 277 oveq1d φADCB2=ADBC2
279 278 oveq2d φAC+BD2+ADCB2=AC+BD2+ADBC2
280 276 279 eqtr4d φPP=AC+BD2+ADCB2
281 273 280 breqtrrd φADCB2<PP
282 281 82 breqtrrd φADCB2<P2
283 241 282 syl φPADCB¬AD=CBADCB2<P2
284 263 101 ltnled φADCB2<P2¬P2ADCB2
285 241 284 syl φPADCB¬AD=CBADCB2<P2¬P2ADCB2
286 283 285 mpbid φPADCB¬AD=CB¬P2ADCB2
287 259 286 condan φPADCBAD=CB
288 240 287 subeq0bd φPADCBADCB=0
289 288 oveq2d φPADCBAD+CBADCB=AD+CB0
290 234 235 addcld φAD+CB
291 290 mul01d φAD+CB0=0
292 291 adantr φPADCBAD+CB0=0
293 239 289 292 3eqtrd φPADCBPD2B2=0
294 28 23 subcld φD2B2
295 81 294 mul0ord φPD2B2=0P=0D2B2=0
296 295 adantr φPADCBPD2B2=0P=0D2B2=0
297 293 296 mpbid φPADCBP=0D2B2=0
298 297 ord φPADCB¬P=0D2B2=0
299 210 298 mpd φPADCBD2B2=0
300 204 205 299 subeq0d φPADCBD2=B2
301 200 201 202 203 300 sq11d φPADCBD=B
302 301 oveq2d φPADCBAD=AB
303 302 287 eqtr3d φPADCBAB=CB
304 196 197 198 199 303 mulcan2ad φPADCBA=C
305 138 164 zsubcld φD2B2
306 dvdsmul1 PD2B2PPD2B2
307 80 305 306 syl2anc φPPD2B2
308 307 238 breqtrd φPAD+CBADCB
309 euclemma PAD+CBADCBPAD+CBADCBPAD+CBPADCB
310 1 92 244 309 syl3anc φPAD+CBADCBPAD+CBPADCB
311 308 310 mpbid φPAD+CBPADCB
312 195 304 311 mpjaodan φA=C
313 312 oveq1d φA2=C2
314 313 oveq2d φPA2=PC2
315 314 219 223 3eqtr3d φB2=D2
316 13 43 17 130 315 sq11d φB=D
317 312 316 jca φA=CB=D