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 P mod 4 = 1 x 0 y 0 P = x 2 + y 2

Proof

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