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