Metamath Proof Explorer

Theorem 2sqnn

Description: All primes of the form 4 k + 1 are sums of squares of two positive integers. (Contributed by AV, 11-Jun-2023)

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

Proof

Step Hyp Ref Expression
1 2sqnn0 
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> E. a e. NN0 E. b e. NN0 P = ( ( a ^ 2 ) + ( b ^ 2 ) ) )
2 elnn0 
 |-  ( a e. NN0 <-> ( a e. NN \/ a = 0 ) )
3 elnn0 
 |-  ( b e. NN0 <-> ( b e. NN \/ b = 0 ) )
4 oveq1 
 |-  ( x = a -> ( x ^ 2 ) = ( a ^ 2 ) )
5 4 oveq1d 
 |-  ( x = a -> ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( ( a ^ 2 ) + ( y ^ 2 ) ) )
6 5 eqeq2d 
 |-  ( x = a -> ( P = ( ( x ^ 2 ) + ( y ^ 2 ) ) <-> P = ( ( a ^ 2 ) + ( y ^ 2 ) ) ) )
7 oveq1 
 |-  ( y = b -> ( y ^ 2 ) = ( b ^ 2 ) )
8 7 oveq2d 
 |-  ( y = b -> ( ( a ^ 2 ) + ( y ^ 2 ) ) = ( ( a ^ 2 ) + ( b ^ 2 ) ) )
9 8 eqeq2d 
 |-  ( y = b -> ( P = ( ( a ^ 2 ) + ( y ^ 2 ) ) <-> P = ( ( a ^ 2 ) + ( b ^ 2 ) ) ) )
10 6 9 rspc2ev 
 |-  ( ( a e. NN /\ b e. NN /\ P = ( ( a ^ 2 ) + ( b ^ 2 ) ) ) -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
11 10 3expia 
 |-  ( ( a e. NN /\ b e. NN ) -> ( P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
12 11 a1d 
 |-  ( ( a e. NN /\ b e. NN ) -> ( P e. Prime -> ( P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
13 12 expcom 
 |-  ( b e. NN -> ( a e. NN -> ( P e. Prime -> ( P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) ) )
14 sq0i 
 |-  ( a = 0 -> ( a ^ 2 ) = 0 )
15 14 adantr 
 |-  ( ( a = 0 /\ b e. NN ) -> ( a ^ 2 ) = 0 )
16 15 oveq1d 
 |-  ( ( a = 0 /\ b e. NN ) -> ( ( a ^ 2 ) + ( b ^ 2 ) ) = ( 0 + ( b ^ 2 ) ) )
17 nncn 
 |-  ( b e. NN -> b e. CC )
18 17 sqcld 
 |-  ( b e. NN -> ( b ^ 2 ) e. CC )
19 18 addid2d 
 |-  ( b e. NN -> ( 0 + ( b ^ 2 ) ) = ( b ^ 2 ) )
20 19 adantl 
 |-  ( ( a = 0 /\ b e. NN ) -> ( 0 + ( b ^ 2 ) ) = ( b ^ 2 ) )
21 16 20 eqtrd 
 |-  ( ( a = 0 /\ b e. NN ) -> ( ( a ^ 2 ) + ( b ^ 2 ) ) = ( b ^ 2 ) )
22 21 eqeq2d 
 |-  ( ( a = 0 /\ b e. NN ) -> ( P = ( ( a ^ 2 ) + ( b ^ 2 ) ) <-> P = ( b ^ 2 ) ) )
23 eleq1 
 |-  ( P = ( b ^ 2 ) -> ( P e. Prime <-> ( b ^ 2 ) e. Prime ) )
24 23 adantl 
 |-  ( ( b e. NN /\ P = ( b ^ 2 ) ) -> ( P e. Prime <-> ( b ^ 2 ) e. Prime ) )
25 nnz 
 |-  ( b e. NN -> b e. ZZ )
26 sqnprm 
 |-  ( b e. ZZ -> -. ( b ^ 2 ) e. Prime )
27 25 26 syl 
 |-  ( b e. NN -> -. ( b ^ 2 ) e. Prime )
28 27 pm2.21d 
 |-  ( b e. NN -> ( ( b ^ 2 ) e. Prime -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
29 28 adantr 
 |-  ( ( b e. NN /\ P = ( b ^ 2 ) ) -> ( ( b ^ 2 ) e. Prime -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
30 24 29 sylbid 
 |-  ( ( b e. NN /\ P = ( b ^ 2 ) ) -> ( P e. Prime -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
31 30 ex 
 |-  ( b e. NN -> ( P = ( b ^ 2 ) -> ( P e. Prime -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
32 31 adantl 
 |-  ( ( a = 0 /\ b e. NN ) -> ( P = ( b ^ 2 ) -> ( P e. Prime -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
33 22 32 sylbid 
 |-  ( ( a = 0 /\ b e. NN ) -> ( P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> ( P e. Prime -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
34 33 com23 
 |-  ( ( a = 0 /\ b e. NN ) -> ( P e. Prime -> ( P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
35 34 expcom 
 |-  ( b e. NN -> ( a = 0 -> ( P e. Prime -> ( P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) ) )
36 13 35 jaod 
 |-  ( b e. NN -> ( ( a e. NN \/ a = 0 ) -> ( P e. Prime -> ( P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) ) )
37 sq0i 
 |-  ( b = 0 -> ( b ^ 2 ) = 0 )
38 37 adantr 
 |-  ( ( b = 0 /\ a e. NN ) -> ( b ^ 2 ) = 0 )
39 38 oveq2d 
 |-  ( ( b = 0 /\ a e. NN ) -> ( ( a ^ 2 ) + ( b ^ 2 ) ) = ( ( a ^ 2 ) + 0 ) )
40 nncn 
 |-  ( a e. NN -> a e. CC )
41 40 sqcld 
 |-  ( a e. NN -> ( a ^ 2 ) e. CC )
42 41 addid1d 
 |-  ( a e. NN -> ( ( a ^ 2 ) + 0 ) = ( a ^ 2 ) )
43 42 adantl 
 |-  ( ( b = 0 /\ a e. NN ) -> ( ( a ^ 2 ) + 0 ) = ( a ^ 2 ) )
44 39 43 eqtrd 
 |-  ( ( b = 0 /\ a e. NN ) -> ( ( a ^ 2 ) + ( b ^ 2 ) ) = ( a ^ 2 ) )
45 44 eqeq2d 
 |-  ( ( b = 0 /\ a e. NN ) -> ( P = ( ( a ^ 2 ) + ( b ^ 2 ) ) <-> P = ( a ^ 2 ) ) )
46 eleq1 
 |-  ( P = ( a ^ 2 ) -> ( P e. Prime <-> ( a ^ 2 ) e. Prime ) )
47 46 adantl 
 |-  ( ( a e. NN /\ P = ( a ^ 2 ) ) -> ( P e. Prime <-> ( a ^ 2 ) e. Prime ) )
48 nnz 
 |-  ( a e. NN -> a e. ZZ )
49 sqnprm 
 |-  ( a e. ZZ -> -. ( a ^ 2 ) e. Prime )
50 48 49 syl 
 |-  ( a e. NN -> -. ( a ^ 2 ) e. Prime )
51 50 pm2.21d 
 |-  ( a e. NN -> ( ( a ^ 2 ) e. Prime -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
52 51 adantr 
 |-  ( ( a e. NN /\ P = ( a ^ 2 ) ) -> ( ( a ^ 2 ) e. Prime -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
53 47 52 sylbid 
 |-  ( ( a e. NN /\ P = ( a ^ 2 ) ) -> ( P e. Prime -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
54 53 ex 
 |-  ( a e. NN -> ( P = ( a ^ 2 ) -> ( P e. Prime -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
55 54 adantl 
 |-  ( ( b = 0 /\ a e. NN ) -> ( P = ( a ^ 2 ) -> ( P e. Prime -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
56 45 55 sylbid 
 |-  ( ( b = 0 /\ a e. NN ) -> ( P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> ( P e. Prime -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
57 56 com23 
 |-  ( ( b = 0 /\ a e. NN ) -> ( P e. Prime -> ( P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
58 57 ex 
 |-  ( b = 0 -> ( a e. NN -> ( P e. Prime -> ( P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) ) )
59 14 37 oveqan12rd 
 |-  ( ( b = 0 /\ a = 0 ) -> ( ( a ^ 2 ) + ( b ^ 2 ) ) = ( 0 + 0 ) )
60 00id 
 |-  ( 0 + 0 ) = 0
61 59 60 eqtrdi 
 |-  ( ( b = 0 /\ a = 0 ) -> ( ( a ^ 2 ) + ( b ^ 2 ) ) = 0 )
62 61 eqeq2d 
 |-  ( ( b = 0 /\ a = 0 ) -> ( P = ( ( a ^ 2 ) + ( b ^ 2 ) ) <-> P = 0 ) )
63 eleq1 
 |-  ( P = 0 -> ( P e. Prime <-> 0 e. Prime ) )
64 0nprm 
 |-  -. 0 e. Prime
65 64 pm2.21i 
 |-  ( 0 e. Prime -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
66 63 65 syl6bi 
 |-  ( P = 0 -> ( P e. Prime -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
67 62 66 syl6bi 
 |-  ( ( b = 0 /\ a = 0 ) -> ( P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> ( P e. Prime -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
68 67 com23 
 |-  ( ( b = 0 /\ a = 0 ) -> ( P e. Prime -> ( P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
69 68 ex 
 |-  ( b = 0 -> ( a = 0 -> ( P e. Prime -> ( P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) ) )
70 58 69 jaod 
 |-  ( b = 0 -> ( ( a e. NN \/ a = 0 ) -> ( P e. Prime -> ( P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) ) )
71 36 70 jaoi 
 |-  ( ( b e. NN \/ b = 0 ) -> ( ( a e. NN \/ a = 0 ) -> ( P e. Prime -> ( P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) ) )
72 3 71 sylbi 
 |-  ( b e. NN0 -> ( ( a e. NN \/ a = 0 ) -> ( P e. Prime -> ( P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) ) )
73 72 com12 
 |-  ( ( a e. NN \/ a = 0 ) -> ( b e. NN0 -> ( P e. Prime -> ( P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) ) )
74 2 73 sylbi 
 |-  ( a e. NN0 -> ( b e. NN0 -> ( P e. Prime -> ( P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) ) )
75 74 imp 
 |-  ( ( a e. NN0 /\ b e. NN0 ) -> ( P e. Prime -> ( P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
76 75 com12 
 |-  ( P e. Prime -> ( ( a e. NN0 /\ b e. NN0 ) -> ( P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
77 76 adantr 
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> ( ( a e. NN0 /\ b e. NN0 ) -> ( P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
78 77 rexlimdvv 
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> ( E. a e. NN0 E. b e. NN0 P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
79 1 78 mpd 
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> E. x e. NN E. y e. NN P = ( ( x ^ 2 ) + ( y ^ 2 ) ) )