Metamath Proof Explorer

Theorem 2sqnn0

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

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

Proof

Step Hyp Ref Expression
1 2sq 
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> E. a e. ZZ E. b e. ZZ P = ( ( a ^ 2 ) + ( b ^ 2 ) ) )
2 elnn0z 
 |-  ( a e. NN0 <-> ( a e. ZZ /\ 0 <_ a ) )
3 2 biimpri 
 |-  ( ( a e. ZZ /\ 0 <_ a ) -> a e. NN0 )
4 elznn0 
 |-  ( a e. ZZ <-> ( a e. RR /\ ( a e. NN0 \/ -u a e. NN0 ) ) )
5 nn0ge0 
 |-  ( a e. NN0 -> 0 <_ a )
6 5 pm2.24d 
 |-  ( a e. NN0 -> ( -. 0 <_ a -> -u a e. NN0 ) )
7 6 a1i 
 |-  ( a e. RR -> ( a e. NN0 -> ( -. 0 <_ a -> -u a e. NN0 ) ) )
8 ax-1 
 |-  ( -u a e. NN0 -> ( -. 0 <_ a -> -u a e. NN0 ) )
9 8 a1i 
 |-  ( a e. RR -> ( -u a e. NN0 -> ( -. 0 <_ a -> -u a e. NN0 ) ) )
10 7 9 jaod 
 |-  ( a e. RR -> ( ( a e. NN0 \/ -u a e. NN0 ) -> ( -. 0 <_ a -> -u a e. NN0 ) ) )
11 10 imp 
 |-  ( ( a e. RR /\ ( a e. NN0 \/ -u a e. NN0 ) ) -> ( -. 0 <_ a -> -u a e. NN0 ) )
12 4 11 sylbi 
 |-  ( a e. ZZ -> ( -. 0 <_ a -> -u a e. NN0 ) )
13 12 imp 
 |-  ( ( a e. ZZ /\ -. 0 <_ a ) -> -u a e. NN0 )
14 3 13 ifclda 
 |-  ( a e. ZZ -> if ( 0 <_ a , a , -u a ) e. NN0 )
15 14 adantr 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> if ( 0 <_ a , a , -u a ) e. NN0 )
16 15 adantr 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ P = ( ( a ^ 2 ) + ( b ^ 2 ) ) ) -> if ( 0 <_ a , a , -u a ) e. NN0 )
17 elnn0z 
 |-  ( b e. NN0 <-> ( b e. ZZ /\ 0 <_ b ) )
18 17 biimpri 
 |-  ( ( b e. ZZ /\ 0 <_ b ) -> b e. NN0 )
19 elznn0 
 |-  ( b e. ZZ <-> ( b e. RR /\ ( b e. NN0 \/ -u b e. NN0 ) ) )
20 nn0ge0 
 |-  ( b e. NN0 -> 0 <_ b )
21 20 pm2.24d 
 |-  ( b e. NN0 -> ( -. 0 <_ b -> -u b e. NN0 ) )
22 21 a1i 
 |-  ( b e. RR -> ( b e. NN0 -> ( -. 0 <_ b -> -u b e. NN0 ) ) )
23 ax-1 
 |-  ( -u b e. NN0 -> ( -. 0 <_ b -> -u b e. NN0 ) )
24 23 a1i 
 |-  ( b e. RR -> ( -u b e. NN0 -> ( -. 0 <_ b -> -u b e. NN0 ) ) )
25 22 24 jaod 
 |-  ( b e. RR -> ( ( b e. NN0 \/ -u b e. NN0 ) -> ( -. 0 <_ b -> -u b e. NN0 ) ) )
26 25 imp 
 |-  ( ( b e. RR /\ ( b e. NN0 \/ -u b e. NN0 ) ) -> ( -. 0 <_ b -> -u b e. NN0 ) )
27 19 26 sylbi 
 |-  ( b e. ZZ -> ( -. 0 <_ b -> -u b e. NN0 ) )
28 27 imp 
 |-  ( ( b e. ZZ /\ -. 0 <_ b ) -> -u b e. NN0 )
29 18 28 ifclda 
 |-  ( b e. ZZ -> if ( 0 <_ b , b , -u b ) e. NN0 )
30 29 adantl 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> if ( 0 <_ b , b , -u b ) e. NN0 )
31 30 adantr 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ P = ( ( a ^ 2 ) + ( b ^ 2 ) ) ) -> if ( 0 <_ b , b , -u b ) e. NN0 )
32 elznn0nn 
 |-  ( a e. ZZ <-> ( a e. NN0 \/ ( a e. RR /\ -u a e. NN ) ) )
33 5 iftrued 
 |-  ( a e. NN0 -> if ( 0 <_ a , a , -u a ) = a )
34 33 eqcomd 
 |-  ( a e. NN0 -> a = if ( 0 <_ a , a , -u a ) )
35 34 oveq1d 
 |-  ( a e. NN0 -> ( a ^ 2 ) = ( if ( 0 <_ a , a , -u a ) ^ 2 ) )
36 elnnz 
 |-  ( -u a e. NN <-> ( -u a e. ZZ /\ 0 < -u a ) )
37 lt0neg1 
 |-  ( a e. RR -> ( a < 0 <-> 0 < -u a ) )
38 id 
 |-  ( a e. RR -> a e. RR )
39 0red 
 |-  ( a e. RR -> 0 e. RR )
40 38 39 ltnled 
 |-  ( a e. RR -> ( a < 0 <-> -. 0 <_ a ) )
41 40 biimpd 
 |-  ( a e. RR -> ( a < 0 -> -. 0 <_ a ) )
42 37 41 sylbird 
 |-  ( a e. RR -> ( 0 < -u a -> -. 0 <_ a ) )
43 42 com12 
 |-  ( 0 < -u a -> ( a e. RR -> -. 0 <_ a ) )
44 36 43 simplbiim 
 |-  ( -u a e. NN -> ( a e. RR -> -. 0 <_ a ) )
45 44 impcom 
 |-  ( ( a e. RR /\ -u a e. NN ) -> -. 0 <_ a )
46 45 iffalsed 
 |-  ( ( a e. RR /\ -u a e. NN ) -> if ( 0 <_ a , a , -u a ) = -u a )
47 46 oveq1d 
 |-  ( ( a e. RR /\ -u a e. NN ) -> ( if ( 0 <_ a , a , -u a ) ^ 2 ) = ( -u a ^ 2 ) )
48 recn 
 |-  ( a e. RR -> a e. CC )
49 sqneg 
 |-  ( a e. CC -> ( -u a ^ 2 ) = ( a ^ 2 ) )
50 48 49 syl 
 |-  ( a e. RR -> ( -u a ^ 2 ) = ( a ^ 2 ) )
51 50 adantr 
 |-  ( ( a e. RR /\ -u a e. NN ) -> ( -u a ^ 2 ) = ( a ^ 2 ) )
52 47 51 eqtr2d 
 |-  ( ( a e. RR /\ -u a e. NN ) -> ( a ^ 2 ) = ( if ( 0 <_ a , a , -u a ) ^ 2 ) )
53 35 52 jaoi 
 |-  ( ( a e. NN0 \/ ( a e. RR /\ -u a e. NN ) ) -> ( a ^ 2 ) = ( if ( 0 <_ a , a , -u a ) ^ 2 ) )
54 32 53 sylbi 
 |-  ( a e. ZZ -> ( a ^ 2 ) = ( if ( 0 <_ a , a , -u a ) ^ 2 ) )
55 elznn0nn 
 |-  ( b e. ZZ <-> ( b e. NN0 \/ ( b e. RR /\ -u b e. NN ) ) )
56 20 iftrued 
 |-  ( b e. NN0 -> if ( 0 <_ b , b , -u b ) = b )
57 56 eqcomd 
 |-  ( b e. NN0 -> b = if ( 0 <_ b , b , -u b ) )
58 57 oveq1d 
 |-  ( b e. NN0 -> ( b ^ 2 ) = ( if ( 0 <_ b , b , -u b ) ^ 2 ) )
59 elnnz 
 |-  ( -u b e. NN <-> ( -u b e. ZZ /\ 0 < -u b ) )
60 lt0neg1 
 |-  ( b e. RR -> ( b < 0 <-> 0 < -u b ) )
61 id 
 |-  ( b e. RR -> b e. RR )
62 0red 
 |-  ( b e. RR -> 0 e. RR )
63 61 62 ltnled 
 |-  ( b e. RR -> ( b < 0 <-> -. 0 <_ b ) )
64 63 biimpd 
 |-  ( b e. RR -> ( b < 0 -> -. 0 <_ b ) )
65 60 64 sylbird 
 |-  ( b e. RR -> ( 0 < -u b -> -. 0 <_ b ) )
66 65 com12 
 |-  ( 0 < -u b -> ( b e. RR -> -. 0 <_ b ) )
67 59 66 simplbiim 
 |-  ( -u b e. NN -> ( b e. RR -> -. 0 <_ b ) )
68 67 impcom 
 |-  ( ( b e. RR /\ -u b e. NN ) -> -. 0 <_ b )
69 68 iffalsed 
 |-  ( ( b e. RR /\ -u b e. NN ) -> if ( 0 <_ b , b , -u b ) = -u b )
70 69 oveq1d 
 |-  ( ( b e. RR /\ -u b e. NN ) -> ( if ( 0 <_ b , b , -u b ) ^ 2 ) = ( -u b ^ 2 ) )
71 recn 
 |-  ( b e. RR -> b e. CC )
72 sqneg 
 |-  ( b e. CC -> ( -u b ^ 2 ) = ( b ^ 2 ) )
73 71 72 syl 
 |-  ( b e. RR -> ( -u b ^ 2 ) = ( b ^ 2 ) )
74 73 adantr 
 |-  ( ( b e. RR /\ -u b e. NN ) -> ( -u b ^ 2 ) = ( b ^ 2 ) )
75 70 74 eqtr2d 
 |-  ( ( b e. RR /\ -u b e. NN ) -> ( b ^ 2 ) = ( if ( 0 <_ b , b , -u b ) ^ 2 ) )
76 58 75 jaoi 
 |-  ( ( b e. NN0 \/ ( b e. RR /\ -u b e. NN ) ) -> ( b ^ 2 ) = ( if ( 0 <_ b , b , -u b ) ^ 2 ) )
77 55 76 sylbi 
 |-  ( b e. ZZ -> ( b ^ 2 ) = ( if ( 0 <_ b , b , -u b ) ^ 2 ) )
78 54 77 oveqan12d 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( ( a ^ 2 ) + ( b ^ 2 ) ) = ( ( if ( 0 <_ a , a , -u a ) ^ 2 ) + ( if ( 0 <_ b , b , -u b ) ^ 2 ) ) )
79 78 eqeq2d 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( P = ( ( a ^ 2 ) + ( b ^ 2 ) ) <-> P = ( ( if ( 0 <_ a , a , -u a ) ^ 2 ) + ( if ( 0 <_ b , b , -u b ) ^ 2 ) ) ) )
80 79 biimpd 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> P = ( ( if ( 0 <_ a , a , -u a ) ^ 2 ) + ( if ( 0 <_ b , b , -u b ) ^ 2 ) ) ) )
81 80 imp 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ P = ( ( a ^ 2 ) + ( b ^ 2 ) ) ) -> P = ( ( if ( 0 <_ a , a , -u a ) ^ 2 ) + ( if ( 0 <_ b , b , -u b ) ^ 2 ) ) )
82 oveq1 
 |-  ( x = if ( 0 <_ a , a , -u a ) -> ( x ^ 2 ) = ( if ( 0 <_ a , a , -u a ) ^ 2 ) )
83 82 oveq1d 
 |-  ( x = if ( 0 <_ a , a , -u a ) -> ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( ( if ( 0 <_ a , a , -u a ) ^ 2 ) + ( y ^ 2 ) ) )
84 83 eqeq2d 
 |-  ( x = if ( 0 <_ a , a , -u a ) -> ( P = ( ( x ^ 2 ) + ( y ^ 2 ) ) <-> P = ( ( if ( 0 <_ a , a , -u a ) ^ 2 ) + ( y ^ 2 ) ) ) )
85 oveq1 
 |-  ( y = if ( 0 <_ b , b , -u b ) -> ( y ^ 2 ) = ( if ( 0 <_ b , b , -u b ) ^ 2 ) )
86 85 oveq2d 
 |-  ( y = if ( 0 <_ b , b , -u b ) -> ( ( if ( 0 <_ a , a , -u a ) ^ 2 ) + ( y ^ 2 ) ) = ( ( if ( 0 <_ a , a , -u a ) ^ 2 ) + ( if ( 0 <_ b , b , -u b ) ^ 2 ) ) )
87 86 eqeq2d 
 |-  ( y = if ( 0 <_ b , b , -u b ) -> ( P = ( ( if ( 0 <_ a , a , -u a ) ^ 2 ) + ( y ^ 2 ) ) <-> P = ( ( if ( 0 <_ a , a , -u a ) ^ 2 ) + ( if ( 0 <_ b , b , -u b ) ^ 2 ) ) ) )
88 84 87 rspc2ev 
 |-  ( ( if ( 0 <_ a , a , -u a ) e. NN0 /\ if ( 0 <_ b , b , -u b ) e. NN0 /\ P = ( ( if ( 0 <_ a , a , -u a ) ^ 2 ) + ( if ( 0 <_ b , b , -u b ) ^ 2 ) ) ) -> E. x e. NN0 E. y e. NN0 P = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
89 16 31 81 88 syl3anc 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ P = ( ( a ^ 2 ) + ( b ^ 2 ) ) ) -> E. x e. NN0 E. y e. NN0 P = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
90 89 ex 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> E. x e. NN0 E. y e. NN0 P = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
91 90 rexlimivv 
 |-  ( E. a e. ZZ E. b e. ZZ P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> E. x e. NN0 E. y e. NN0 P = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
92 1 91 syl 
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> E. x e. NN0 E. y e. NN0 P = ( ( x ^ 2 ) + ( y ^ 2 ) ) )