Metamath Proof Explorer

Theorem 2sqnn

Description: All primes of the form 4 k + 1 are sums of squares of two positive integers. (Contributed by AV, 11-Jun-2023)

Ref Expression
Assertion 2sqnn ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )

Proof

Step Hyp Ref Expression
1 2sqnn0 ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → ∃ 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) )
2 elnn0 ⊢ ( 𝑎 ∈ ℕ0 ↔ ( 𝑎 ∈ ℕ ∨ 𝑎 = 0 ) )
3 elnn0 ⊢ ( 𝑏 ∈ ℕ0 ↔ ( 𝑏 ∈ ℕ ∨ 𝑏 = 0 ) )
4 oveq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 ↑ 2 ) = ( 𝑎 ↑ 2 ) )
5 4 oveq1d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( ( 𝑎 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
6 5 eqeq2d ⊢ ( 𝑥 = 𝑎 → ( 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ↔ 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
7 oveq1 ⊢ ( 𝑦 = 𝑏 → ( 𝑦 ↑ 2 ) = ( 𝑏 ↑ 2 ) )
8 7 oveq2d ⊢ ( 𝑦 = 𝑏 → ( ( 𝑎 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) )
9 8 eqeq2d ⊢ ( 𝑦 = 𝑏 → ( 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ↔ 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) ) )
10 6 9 rspc2ev ⊢ ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ∧ 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
11 10 3expia ⊢ ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) → ( 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
12 11 a1d ⊢ ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) → ( 𝑃 ∈ ℙ → ( 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) )
13 12 expcom ⊢ ( 𝑏 ∈ ℕ → ( 𝑎 ∈ ℕ → ( 𝑃 ∈ ℙ → ( 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) ) )
14 sq0i ⊢ ( 𝑎 = 0 → ( 𝑎 ↑ 2 ) = 0 )
15 14 adantr ⊢ ( ( 𝑎 = 0 ∧ 𝑏 ∈ ℕ ) → ( 𝑎 ↑ 2 ) = 0 )
16 15 oveq1d ⊢ ( ( 𝑎 = 0 ∧ 𝑏 ∈ ℕ ) → ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = ( 0 + ( 𝑏 ↑ 2 ) ) )
17 nncn ⊢ ( 𝑏 ∈ ℕ → 𝑏 ∈ ℂ )
18 17 sqcld ⊢ ( 𝑏 ∈ ℕ → ( 𝑏 ↑ 2 ) ∈ ℂ )
19 18 addlidd ⊢ ( 𝑏 ∈ ℕ → ( 0 + ( 𝑏 ↑ 2 ) ) = ( 𝑏 ↑ 2 ) )
20 19 adantl ⊢ ( ( 𝑎 = 0 ∧ 𝑏 ∈ ℕ ) → ( 0 + ( 𝑏 ↑ 2 ) ) = ( 𝑏 ↑ 2 ) )
21 16 20 eqtrd ⊢ ( ( 𝑎 = 0 ∧ 𝑏 ∈ ℕ ) → ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = ( 𝑏 ↑ 2 ) )
22 21 eqeq2d ⊢ ( ( 𝑎 = 0 ∧ 𝑏 ∈ ℕ ) → ( 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) ↔ 𝑃 = ( 𝑏 ↑ 2 ) ) )
23 eleq1 ⊢ ( 𝑃 = ( 𝑏 ↑ 2 ) → ( 𝑃 ∈ ℙ ↔ ( 𝑏 ↑ 2 ) ∈ ℙ ) )
24 23 adantl ⊢ ( ( 𝑏 ∈ ℕ ∧ 𝑃 = ( 𝑏 ↑ 2 ) ) → ( 𝑃 ∈ ℙ ↔ ( 𝑏 ↑ 2 ) ∈ ℙ ) )
25 nnz ⊢ ( 𝑏 ∈ ℕ → 𝑏 ∈ ℤ )
26 sqnprm ⊢ ( 𝑏 ∈ ℤ → ¬ ( 𝑏 ↑ 2 ) ∈ ℙ )
27 25 26 syl ⊢ ( 𝑏 ∈ ℕ → ¬ ( 𝑏 ↑ 2 ) ∈ ℙ )
28 27 pm2.21d ⊢ ( 𝑏 ∈ ℕ → ( ( 𝑏 ↑ 2 ) ∈ ℙ → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
29 28 adantr ⊢ ( ( 𝑏 ∈ ℕ ∧ 𝑃 = ( 𝑏 ↑ 2 ) ) → ( ( 𝑏 ↑ 2 ) ∈ ℙ → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
30 24 29 sylbid ⊢ ( ( 𝑏 ∈ ℕ ∧ 𝑃 = ( 𝑏 ↑ 2 ) ) → ( 𝑃 ∈ ℙ → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
31 30 ex ⊢ ( 𝑏 ∈ ℕ → ( 𝑃 = ( 𝑏 ↑ 2 ) → ( 𝑃 ∈ ℙ → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) )
32 31 adantl ⊢ ( ( 𝑎 = 0 ∧ 𝑏 ∈ ℕ ) → ( 𝑃 = ( 𝑏 ↑ 2 ) → ( 𝑃 ∈ ℙ → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) )
33 22 32 sylbid ⊢ ( ( 𝑎 = 0 ∧ 𝑏 ∈ ℕ ) → ( 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) → ( 𝑃 ∈ ℙ → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) )
34 33 com23 ⊢ ( ( 𝑎 = 0 ∧ 𝑏 ∈ ℕ ) → ( 𝑃 ∈ ℙ → ( 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) )
35 34 expcom ⊢ ( 𝑏 ∈ ℕ → ( 𝑎 = 0 → ( 𝑃 ∈ ℙ → ( 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) ) )
36 13 35 jaod ⊢ ( 𝑏 ∈ ℕ → ( ( 𝑎 ∈ ℕ ∨ 𝑎 = 0 ) → ( 𝑃 ∈ ℙ → ( 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) ) )
37 sq0i ⊢ ( 𝑏 = 0 → ( 𝑏 ↑ 2 ) = 0 )
38 37 adantr ⊢ ( ( 𝑏 = 0 ∧ 𝑎 ∈ ℕ ) → ( 𝑏 ↑ 2 ) = 0 )
39 38 oveq2d ⊢ ( ( 𝑏 = 0 ∧ 𝑎 ∈ ℕ ) → ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = ( ( 𝑎 ↑ 2 ) + 0 ) )
40 nncn ⊢ ( 𝑎 ∈ ℕ → 𝑎 ∈ ℂ )
41 40 sqcld ⊢ ( 𝑎 ∈ ℕ → ( 𝑎 ↑ 2 ) ∈ ℂ )
42 41 addridd ⊢ ( 𝑎 ∈ ℕ → ( ( 𝑎 ↑ 2 ) + 0 ) = ( 𝑎 ↑ 2 ) )
43 42 adantl ⊢ ( ( 𝑏 = 0 ∧ 𝑎 ∈ ℕ ) → ( ( 𝑎 ↑ 2 ) + 0 ) = ( 𝑎 ↑ 2 ) )
44 39 43 eqtrd ⊢ ( ( 𝑏 = 0 ∧ 𝑎 ∈ ℕ ) → ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = ( 𝑎 ↑ 2 ) )
45 44 eqeq2d ⊢ ( ( 𝑏 = 0 ∧ 𝑎 ∈ ℕ ) → ( 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) ↔ 𝑃 = ( 𝑎 ↑ 2 ) ) )
46 eleq1 ⊢ ( 𝑃 = ( 𝑎 ↑ 2 ) → ( 𝑃 ∈ ℙ ↔ ( 𝑎 ↑ 2 ) ∈ ℙ ) )
47 46 adantl ⊢ ( ( 𝑎 ∈ ℕ ∧ 𝑃 = ( 𝑎 ↑ 2 ) ) → ( 𝑃 ∈ ℙ ↔ ( 𝑎 ↑ 2 ) ∈ ℙ ) )
48 nnz ⊢ ( 𝑎 ∈ ℕ → 𝑎 ∈ ℤ )
49 sqnprm ⊢ ( 𝑎 ∈ ℤ → ¬ ( 𝑎 ↑ 2 ) ∈ ℙ )
50 48 49 syl ⊢ ( 𝑎 ∈ ℕ → ¬ ( 𝑎 ↑ 2 ) ∈ ℙ )
51 50 pm2.21d ⊢ ( 𝑎 ∈ ℕ → ( ( 𝑎 ↑ 2 ) ∈ ℙ → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
52 51 adantr ⊢ ( ( 𝑎 ∈ ℕ ∧ 𝑃 = ( 𝑎 ↑ 2 ) ) → ( ( 𝑎 ↑ 2 ) ∈ ℙ → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
53 47 52 sylbid ⊢ ( ( 𝑎 ∈ ℕ ∧ 𝑃 = ( 𝑎 ↑ 2 ) ) → ( 𝑃 ∈ ℙ → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
54 53 ex ⊢ ( 𝑎 ∈ ℕ → ( 𝑃 = ( 𝑎 ↑ 2 ) → ( 𝑃 ∈ ℙ → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) )
55 54 adantl ⊢ ( ( 𝑏 = 0 ∧ 𝑎 ∈ ℕ ) → ( 𝑃 = ( 𝑎 ↑ 2 ) → ( 𝑃 ∈ ℙ → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) )
56 45 55 sylbid ⊢ ( ( 𝑏 = 0 ∧ 𝑎 ∈ ℕ ) → ( 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) → ( 𝑃 ∈ ℙ → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) )
57 56 com23 ⊢ ( ( 𝑏 = 0 ∧ 𝑎 ∈ ℕ ) → ( 𝑃 ∈ ℙ → ( 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) )
58 57 ex ⊢ ( 𝑏 = 0 → ( 𝑎 ∈ ℕ → ( 𝑃 ∈ ℙ → ( 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) ) )
59 14 37 oveqan12rd ⊢ ( ( 𝑏 = 0 ∧ 𝑎 = 0 ) → ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = ( 0 + 0 ) )
60 00id ⊢ ( 0 + 0 ) = 0
61 59 60 eqtrdi ⊢ ( ( 𝑏 = 0 ∧ 𝑎 = 0 ) → ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 0 )
62 61 eqeq2d ⊢ ( ( 𝑏 = 0 ∧ 𝑎 = 0 ) → ( 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) ↔ 𝑃 = 0 ) )
63 eleq1 ⊢ ( 𝑃 = 0 → ( 𝑃 ∈ ℙ ↔ 0 ∈ ℙ ) )
64 0nprm ⊢ ¬ 0 ∈ ℙ
65 64 pm2.21i ⊢ ( 0 ∈ ℙ → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
66 63 65 biimtrdi ⊢ ( 𝑃 = 0 → ( 𝑃 ∈ ℙ → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
67 62 66 biimtrdi ⊢ ( ( 𝑏 = 0 ∧ 𝑎 = 0 ) → ( 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) → ( 𝑃 ∈ ℙ → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) )
68 67 com23 ⊢ ( ( 𝑏 = 0 ∧ 𝑎 = 0 ) → ( 𝑃 ∈ ℙ → ( 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) )
69 68 ex ⊢ ( 𝑏 = 0 → ( 𝑎 = 0 → ( 𝑃 ∈ ℙ → ( 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) ) )
70 58 69 jaod ⊢ ( 𝑏 = 0 → ( ( 𝑎 ∈ ℕ ∨ 𝑎 = 0 ) → ( 𝑃 ∈ ℙ → ( 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) ) )
71 36 70 jaoi ⊢ ( ( 𝑏 ∈ ℕ ∨ 𝑏 = 0 ) → ( ( 𝑎 ∈ ℕ ∨ 𝑎 = 0 ) → ( 𝑃 ∈ ℙ → ( 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) ) )
72 3 71 sylbi ⊢ ( 𝑏 ∈ ℕ0 → ( ( 𝑎 ∈ ℕ ∨ 𝑎 = 0 ) → ( 𝑃 ∈ ℙ → ( 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) ) )
73 72 com12 ⊢ ( ( 𝑎 ∈ ℕ ∨ 𝑎 = 0 ) → ( 𝑏 ∈ ℕ0 → ( 𝑃 ∈ ℙ → ( 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) ) )
74 2 73 sylbi ⊢ ( 𝑎 ∈ ℕ0 → ( 𝑏 ∈ ℕ0 → ( 𝑃 ∈ ℙ → ( 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) ) )
75 74 imp ⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) → ( 𝑃 ∈ ℙ → ( 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) )
76 75 com12 ⊢ ( 𝑃 ∈ ℙ → ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) → ( 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) )
77 76 adantr ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) → ( 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) )
78 77 rexlimdvv ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → ( ∃ 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 𝑃 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
79 1 78 mpd ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )