Metamath Proof Explorer

Theorem 2sq

Description: All primes of the form 4 k + 1 are sums of two squares. This is Metamath 100 proof #20. (Contributed by Mario Carneiro, 20-Jun-2015)

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

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ran ( w e. Z[i] |-> ( ( abs ` w ) ^ 2 ) ) = ran ( w e. Z[i] |-> ( ( abs ` w ) ^ 2 ) )
2 oveq1 
 |-  ( a = x -> ( a gcd b ) = ( x gcd b ) )
3 2 eqeq1d 
 |-  ( a = x -> ( ( a gcd b ) = 1 <-> ( x gcd b ) = 1 ) )
4 oveq1 
 |-  ( a = x -> ( a ^ 2 ) = ( x ^ 2 ) )
5 4 oveq1d 
 |-  ( a = x -> ( ( a ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( b ^ 2 ) ) )
6 5 eqeq2d 
 |-  ( a = x -> ( z = ( ( a ^ 2 ) + ( b ^ 2 ) ) <-> z = ( ( x ^ 2 ) + ( b ^ 2 ) ) ) )
7 3 6 anbi12d 
 |-  ( a = x -> ( ( ( a gcd b ) = 1 /\ z = ( ( a ^ 2 ) + ( b ^ 2 ) ) ) <-> ( ( x gcd b ) = 1 /\ z = ( ( x ^ 2 ) + ( b ^ 2 ) ) ) ) )
8 oveq2 
 |-  ( b = y -> ( x gcd b ) = ( x gcd y ) )
9 8 eqeq1d 
 |-  ( b = y -> ( ( x gcd b ) = 1 <-> ( x gcd y ) = 1 ) )
10 oveq1 
 |-  ( b = y -> ( b ^ 2 ) = ( y ^ 2 ) )
11 10 oveq2d 
 |-  ( b = y -> ( ( x ^ 2 ) + ( b ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
12 11 eqeq2d 
 |-  ( b = y -> ( z = ( ( x ^ 2 ) + ( b ^ 2 ) ) <-> z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
13 9 12 anbi12d 
 |-  ( b = y -> ( ( ( x gcd b ) = 1 /\ z = ( ( x ^ 2 ) + ( b ^ 2 ) ) ) <-> ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
14 7 13 cbvrex2vw 
 |-  ( E. a e. ZZ E. b e. ZZ ( ( a gcd b ) = 1 /\ z = ( ( a ^ 2 ) + ( b ^ 2 ) ) ) <-> E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
15 14 abbii 
 |-  { z | E. a e. ZZ E. b e. ZZ ( ( a gcd b ) = 1 /\ z = ( ( a ^ 2 ) + ( b ^ 2 ) ) ) } = { z | E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) }
16 1 15 2sqlem11 
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> P e. ran ( w e. Z[i] |-> ( ( abs ` w ) ^ 2 ) ) )
17 1 2sqlem2 
 |-  ( P e. ran ( w e. Z[i] |-> ( ( abs ` w ) ^ 2 ) ) <-> E. x e. ZZ E. y e. ZZ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
18 16 17 sylib 
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> E. x e. ZZ E. y e. ZZ P = ( ( x ^ 2 ) + ( y ^ 2 ) ) )