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∈ℙ∧Pmod4=1→∃x∈ℕ0∃y∈ℕ0P=x2+y2

Proof

Step Hyp Ref Expression
1 2sq ⊢P∈ℙ∧Pmod4=1→∃a∈ℤ∃b∈ℤP=a2+b2
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∈ℤ→if0≤aa−a∈ℕ0
15 14 adantr ⊢a∈ℤ∧b∈ℤ→if0≤aa−a∈ℕ0
16 15 adantr ⊢a∈ℤ∧b∈ℤ∧P=a2+b2→if0≤aa−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∈ℤ→if0≤bb−b∈ℕ0
30 29 adantl ⊢a∈ℤ∧b∈ℤ→if0≤bb−b∈ℕ0
31 30 adantr ⊢a∈ℤ∧b∈ℤ∧P=a2+b2→if0≤bb−b∈ℕ0
32 elznn0nn ⊢a∈ℤ↔a∈ℕ0∨a∈ℝ∧−a∈ℕ
33 5 iftrued ⊢a∈ℕ0→if0≤aa−a=a
34 33 eqcomd ⊢a∈ℕ0→a=if0≤aa−a
35 34 oveq1d ⊢a∈ℕ0→a2=if0≤aa−a2
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∈ℕ→if0≤aa−a=−a
47 46 oveq1d ⊢a∈ℝ∧−a∈ℕ→if0≤aa−a2=−a2
48 recn ⊢a∈ℝ→a∈ℂ
49 sqneg ⊢a∈ℂ→−a2=a2
50 48 49 syl ⊢a∈ℝ→−a2=a2
51 50 adantr ⊢a∈ℝ∧−a∈ℕ→−a2=a2
52 47 51 eqtr2d ⊢a∈ℝ∧−a∈ℕ→a2=if0≤aa−a2
53 35 52 jaoi ⊢a∈ℕ0∨a∈ℝ∧−a∈ℕ→a2=if0≤aa−a2
54 32 53 sylbi ⊢a∈ℤ→a2=if0≤aa−a2
55 elznn0nn ⊢b∈ℤ↔b∈ℕ0∨b∈ℝ∧−b∈ℕ
56 20 iftrued ⊢b∈ℕ0→if0≤bb−b=b
57 56 eqcomd ⊢b∈ℕ0→b=if0≤bb−b
58 57 oveq1d ⊢b∈ℕ0→b2=if0≤bb−b2
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∈ℕ→if0≤bb−b=−b
70 69 oveq1d ⊢b∈ℝ∧−b∈ℕ→if0≤bb−b2=−b2
71 recn ⊢b∈ℝ→b∈ℂ
72 sqneg ⊢b∈ℂ→−b2=b2
73 71 72 syl ⊢b∈ℝ→−b2=b2
74 73 adantr ⊢b∈ℝ∧−b∈ℕ→−b2=b2
75 70 74 eqtr2d ⊢b∈ℝ∧−b∈ℕ→b2=if0≤bb−b2
76 58 75 jaoi ⊢b∈ℕ0∨b∈ℝ∧−b∈ℕ→b2=if0≤bb−b2
77 55 76 sylbi ⊢b∈ℤ→b2=if0≤bb−b2
78 54 77 oveqan12d ⊢a∈ℤ∧b∈ℤ→a2+b2=if0≤aa−a2+if0≤bb−b2
79 78 eqeq2d ⊢a∈ℤ∧b∈ℤ→P=a2+b2↔P=if0≤aa−a2+if0≤bb−b2
80 79 biimpd ⊢a∈ℤ∧b∈ℤ→P=a2+b2→P=if0≤aa−a2+if0≤bb−b2
81 80 imp ⊢a∈ℤ∧b∈ℤ∧P=a2+b2→P=if0≤aa−a2+if0≤bb−b2
82 oveq1 ⊢x=if0≤aa−a→x2=if0≤aa−a2
83 82 oveq1d ⊢x=if0≤aa−a→x2+y2=if0≤aa−a2+y2
84 83 eqeq2d ⊢x=if0≤aa−a→P=x2+y2↔P=if0≤aa−a2+y2
85 oveq1 ⊢y=if0≤bb−b→y2=if0≤bb−b2
86 85 oveq2d ⊢y=if0≤bb−b→if0≤aa−a2+y2=if0≤aa−a2+if0≤bb−b2
87 86 eqeq2d ⊢y=if0≤bb−b→P=if0≤aa−a2+y2↔P=if0≤aa−a2+if0≤bb−b2
88 84 87 rspc2ev ⊢if0≤aa−a∈ℕ0∧if0≤bb−b∈ℕ0∧P=if0≤aa−a2+if0≤bb−b2→∃x∈ℕ0∃y∈ℕ0P=x2+y2
89 16 31 81 88 syl3anc ⊢a∈ℤ∧b∈ℤ∧P=a2+b2→∃x∈ℕ0∃y∈ℕ0P=x2+y2
90 89 ex ⊢a∈ℤ∧b∈ℤ→P=a2+b2→∃x∈ℕ0∃y∈ℕ0P=x2+y2
91 90 rexlimivv ⊢∃a∈ℤ∃b∈ℤP=a2+b2→∃x∈ℕ0∃y∈ℕ0P=x2+y2
92 1 91 syl ⊢P∈ℙ∧Pmod4=1→∃x∈ℕ0∃y∈ℕ0P=x2+y2