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

Proof

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