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 ) ) ) |