Metamath Proof Explorer

Theorem 2sqb

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

Ref Expression
Assertion 2sqb 
|- ( P e. Prime -> ( E. x e. ZZ E. y e. ZZ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) <-> ( P = 2 \/ ( P mod 4 ) = 1 ) ) )

Proof

Step Hyp Ref Expression
1 df-ne 
 |-  ( P =/= 2 <-> -. P = 2 )
2 prmz 
 |-  ( P e. Prime -> P e. ZZ )
3 2 ad3antrrr 
 |-  ( ( ( ( P e. Prime /\ P =/= 2 ) /\ ( x e. ZZ /\ y e. ZZ ) ) /\ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> P e. ZZ )
4 simplrr 
 |-  ( ( ( ( P e. Prime /\ P =/= 2 ) /\ ( x e. ZZ /\ y e. ZZ ) ) /\ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> y e. ZZ )
5 bezout 
 |-  ( ( P e. ZZ /\ y e. ZZ ) -> E. a e. ZZ E. b e. ZZ ( P gcd y ) = ( ( P x. a ) + ( y x. b ) ) )
6 3 4 5 syl2anc 
 |-  ( ( ( ( P e. Prime /\ P =/= 2 ) /\ ( x e. ZZ /\ y e. ZZ ) ) /\ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> E. a e. ZZ E. b e. ZZ ( P gcd y ) = ( ( P x. a ) + ( y x. b ) ) )
7 simplll 
 |-  ( ( ( ( ( P e. Prime /\ P =/= 2 ) /\ ( x e. ZZ /\ y e. ZZ ) ) /\ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( P gcd y ) = ( ( P x. a ) + ( y x. b ) ) ) ) -> ( P e. Prime /\ P =/= 2 ) )
8 simpllr 
 |-  ( ( ( ( ( P e. Prime /\ P =/= 2 ) /\ ( x e. ZZ /\ y e. ZZ ) ) /\ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( P gcd y ) = ( ( P x. a ) + ( y x. b ) ) ) ) -> ( x e. ZZ /\ y e. ZZ ) )
9 simplr 
 |-  ( ( ( ( ( P e. Prime /\ P =/= 2 ) /\ ( x e. ZZ /\ y e. ZZ ) ) /\ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( P gcd y ) = ( ( P x. a ) + ( y x. b ) ) ) ) -> P = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
10 simprll 
 |-  ( ( ( ( ( P e. Prime /\ P =/= 2 ) /\ ( x e. ZZ /\ y e. ZZ ) ) /\ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( P gcd y ) = ( ( P x. a ) + ( y x. b ) ) ) ) -> a e. ZZ )
11 simprlr 
 |-  ( ( ( ( ( P e. Prime /\ P =/= 2 ) /\ ( x e. ZZ /\ y e. ZZ ) ) /\ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( P gcd y ) = ( ( P x. a ) + ( y x. b ) ) ) ) -> b e. ZZ )
12 simprr 
 |-  ( ( ( ( ( P e. Prime /\ P =/= 2 ) /\ ( x e. ZZ /\ y e. ZZ ) ) /\ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( P gcd y ) = ( ( P x. a ) + ( y x. b ) ) ) ) -> ( P gcd y ) = ( ( P x. a ) + ( y x. b ) ) )
13 7 8 9 10 11 12 2sqblem 
 |-  ( ( ( ( ( P e. Prime /\ P =/= 2 ) /\ ( x e. ZZ /\ y e. ZZ ) ) /\ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( P gcd y ) = ( ( P x. a ) + ( y x. b ) ) ) ) -> ( P mod 4 ) = 1 )
14 13 expr 
 |-  ( ( ( ( ( P e. Prime /\ P =/= 2 ) /\ ( x e. ZZ /\ y e. ZZ ) ) /\ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( P gcd y ) = ( ( P x. a ) + ( y x. b ) ) -> ( P mod 4 ) = 1 ) )
15 14 rexlimdvva 
 |-  ( ( ( ( P e. Prime /\ P =/= 2 ) /\ ( x e. ZZ /\ y e. ZZ ) ) /\ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> ( E. a e. ZZ E. b e. ZZ ( P gcd y ) = ( ( P x. a ) + ( y x. b ) ) -> ( P mod 4 ) = 1 ) )
16 6 15 mpd 
 |-  ( ( ( ( P e. Prime /\ P =/= 2 ) /\ ( x e. ZZ /\ y e. ZZ ) ) /\ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> ( P mod 4 ) = 1 )
17 16 ex 
 |-  ( ( ( P e. Prime /\ P =/= 2 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( P = ( ( x ^ 2 ) + ( y ^ 2 ) ) -> ( P mod 4 ) = 1 ) )
18 17 rexlimdvva 
 |-  ( ( P e. Prime /\ P =/= 2 ) -> ( E. x e. ZZ E. y e. ZZ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) -> ( P mod 4 ) = 1 ) )
19 18 impancom 
 |-  ( ( P e. Prime /\ E. x e. ZZ E. y e. ZZ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> ( P =/= 2 -> ( P mod 4 ) = 1 ) )
20 1 19 biimtrrid 
 |-  ( ( P e. Prime /\ E. x e. ZZ E. y e. ZZ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> ( -. P = 2 -> ( P mod 4 ) = 1 ) )
21 20 orrd 
 |-  ( ( P e. Prime /\ E. x e. ZZ E. y e. ZZ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> ( P = 2 \/ ( P mod 4 ) = 1 ) )
22 1z 
 |-  1 e. ZZ
23 oveq1 
 |-  ( x = 1 -> ( x ^ 2 ) = ( 1 ^ 2 ) )
24 sq1 
 |-  ( 1 ^ 2 ) = 1
25 23 24 eqtrdi 
 |-  ( x = 1 -> ( x ^ 2 ) = 1 )
26 25 oveq1d 
 |-  ( x = 1 -> ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( 1 + ( y ^ 2 ) ) )
27 26 eqeq2d 
 |-  ( x = 1 -> ( P = ( ( x ^ 2 ) + ( y ^ 2 ) ) <-> P = ( 1 + ( y ^ 2 ) ) ) )
28 oveq1 
 |-  ( y = 1 -> ( y ^ 2 ) = ( 1 ^ 2 ) )
29 28 24 eqtrdi 
 |-  ( y = 1 -> ( y ^ 2 ) = 1 )
30 29 oveq2d 
 |-  ( y = 1 -> ( 1 + ( y ^ 2 ) ) = ( 1 + 1 ) )
31 1p1e2 
 |-  ( 1 + 1 ) = 2
32 30 31 eqtrdi 
 |-  ( y = 1 -> ( 1 + ( y ^ 2 ) ) = 2 )
33 32 eqeq2d 
 |-  ( y = 1 -> ( P = ( 1 + ( y ^ 2 ) ) <-> P = 2 ) )
34 27 33 rspc2ev 
 |-  ( ( 1 e. ZZ /\ 1 e. ZZ /\ P = 2 ) -> E. x e. ZZ E. y e. ZZ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
35 22 22 34 mp3an12 
 |-  ( P = 2 -> E. x e. ZZ E. y e. ZZ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
36 35 adantl 
 |-  ( ( P e. Prime /\ P = 2 ) -> E. x e. ZZ E. y e. ZZ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
37 2sq 
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> E. x e. ZZ E. y e. ZZ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
38 36 37 jaodan 
 |-  ( ( P e. Prime /\ ( P = 2 \/ ( P mod 4 ) = 1 ) ) -> E. x e. ZZ E. y e. ZZ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
39 21 38 impbida 
 |-  ( P e. Prime -> ( E. x e. ZZ E. y e. ZZ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) <-> ( P = 2 \/ ( P mod 4 ) = 1 ) ) )