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