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 ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℕ0 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )

Proof

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