Metamath Proof Explorer


Theorem 2sqb

Description: The converse to 2sq . (Contributed by Mario Carneiro, 20-Jun-2015)

Ref Expression
Assertion 2sqb PxyP=x2+y2P=2Pmod4=1

Proof

Step Hyp Ref Expression
1 df-ne P2¬P=2
2 prmz PP
3 2 ad3antrrr PP2xyP=x2+y2P
4 simplrr PP2xyP=x2+y2y
5 bezout PyabPgcdy=Pa+yb
6 3 4 5 syl2anc PP2xyP=x2+y2abPgcdy=Pa+yb
7 simplll PP2xyP=x2+y2abPgcdy=Pa+ybPP2
8 simpllr PP2xyP=x2+y2abPgcdy=Pa+ybxy
9 simplr PP2xyP=x2+y2abPgcdy=Pa+ybP=x2+y2
10 simprll PP2xyP=x2+y2abPgcdy=Pa+yba
11 simprlr PP2xyP=x2+y2abPgcdy=Pa+ybb
12 simprr PP2xyP=x2+y2abPgcdy=Pa+ybPgcdy=Pa+yb
13 7 8 9 10 11 12 2sqblem PP2xyP=x2+y2abPgcdy=Pa+ybPmod4=1
14 13 expr PP2xyP=x2+y2abPgcdy=Pa+ybPmod4=1
15 14 rexlimdvva PP2xyP=x2+y2abPgcdy=Pa+ybPmod4=1
16 6 15 mpd PP2xyP=x2+y2Pmod4=1
17 16 ex PP2xyP=x2+y2Pmod4=1
18 17 rexlimdvva PP2xyP=x2+y2Pmod4=1
19 18 impancom PxyP=x2+y2P2Pmod4=1
20 1 19 biimtrrid PxyP=x2+y2¬P=2Pmod4=1
21 20 orrd PxyP=x2+y2P=2Pmod4=1
22 1z 1
23 oveq1 x=1x2=12
24 sq1 12=1
25 23 24 eqtrdi x=1x2=1
26 25 oveq1d x=1x2+y2=1+y2
27 26 eqeq2d x=1P=x2+y2P=1+y2
28 oveq1 y=1y2=12
29 28 24 eqtrdi y=1y2=1
30 29 oveq2d y=11+y2=1+1
31 1p1e2 1+1=2
32 30 31 eqtrdi y=11+y2=2
33 32 eqeq2d y=1P=1+y2P=2
34 27 33 rspc2ev 11P=2xyP=x2+y2
35 22 22 34 mp3an12 P=2xyP=x2+y2
36 35 adantl PP=2xyP=x2+y2
37 2sq PPmod4=1xyP=x2+y2
38 36 37 jaodan PP=2Pmod4=1xyP=x2+y2
39 21 38 impbida PxyP=x2+y2P=2Pmod4=1