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	$$⊢\left(P\in \mathbb{P}\wedge P\mathrm{mod}4=1\right)\to \exists x\in {\mathbb{N}}_0\exists y\in {\mathbb{N}}_{0}P=x^2+y^2$$

Proof

Step	Hyp	Ref	Expression
1		2sq	$$⊢\left(P\in \mathbb{P}\wedge P\mathrm{mod}4=1\right)\to \exists a\in \mathbb{Z}\exists b\in \mathbb{Z}P=a^2+b^2$$
2		elnn0z	$$⊢a\in {\mathbb{N}}_0\leftrightarrow \left(a\in \mathbb{Z}\wedge 0\le a\right)$$
3	2	biimpri	$$⊢\left(a\in \mathbb{Z}\wedge 0\le a\right)\to a\in {\mathbb{N}}_0$$
4		elznn0	$$⊢a\in \mathbb{Z}\leftrightarrow \left(a\in ℝ\wedge \left(a\in {\mathbb{N}}_0\vee -a\in {\mathbb{N}}_0\right)\right)$$
5		nn0ge0	$$⊢a\in {\mathbb{N}}_0\to 0\le a$$
6	5	pm2.24d	$$⊢a\in {\mathbb{N}}_0\to \left(\neg 0\le a\to -a\in {\mathbb{N}}_0\right)$$
7	6	a1i	$$⊢a\in ℝ\to \left(a\in {\mathbb{N}}_0\to \left(\neg 0\le a\to -a\in {\mathbb{N}}_0\right)\right)$$
8		ax-1	$$⊢-a\in {\mathbb{N}}_0\to \left(\neg 0\le a\to -a\in {\mathbb{N}}_0\right)$$
9	8	a1i	$$⊢a\in ℝ\to \left(-a\in {\mathbb{N}}_0\to \left(\neg 0\le a\to -a\in {\mathbb{N}}_0\right)\right)$$
10	7 9	jaod	$$⊢a\in ℝ\to \left(\left(a\in {\mathbb{N}}_0\vee -a\in {\mathbb{N}}_0\right)\to \left(\neg 0\le a\to -a\in {\mathbb{N}}_0\right)\right)$$
11	10	imp	$$⊢\left(a\in ℝ\wedge \left(a\in {\mathbb{N}}_0\vee -a\in {\mathbb{N}}_0\right)\right)\to \left(\neg 0\le a\to -a\in {\mathbb{N}}_0\right)$$
12	4 11	sylbi	$$⊢a\in \mathbb{Z}\to \left(\neg 0\le a\to -a\in {\mathbb{N}}_0\right)$$
13	12	imp	$$⊢\left(a\in \mathbb{Z}\wedge \neg 0\le a\right)\to -a\in {\mathbb{N}}_0$$
14	3 13	ifclda	$$⊢a\in \mathbb{Z}\to if\left(0\le a,a,-a\right)\in {\mathbb{N}}_0$$
15	14	adantr	$$⊢\left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\to if\left(0\le a,a,-a\right)\in {\mathbb{N}}_0$$
16	15	adantr	$$⊢\left(\left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\wedge P=a^2+b^2\right)\to if\left(0\le a,a,-a\right)\in {\mathbb{N}}_0$$
17		elnn0z	$$⊢b\in {\mathbb{N}}_0\leftrightarrow \left(b\in \mathbb{Z}\wedge 0\le b\right)$$
18	17	biimpri	$$⊢\left(b\in \mathbb{Z}\wedge 0\le b\right)\to b\in {\mathbb{N}}_0$$
19		elznn0	$$⊢b\in \mathbb{Z}\leftrightarrow \left(b\in ℝ\wedge \left(b\in {\mathbb{N}}_0\vee -b\in {\mathbb{N}}_0\right)\right)$$
20		nn0ge0	$$⊢b\in {\mathbb{N}}_0\to 0\le b$$
21	20	pm2.24d	$$⊢b\in {\mathbb{N}}_0\to \left(\neg 0\le b\to -b\in {\mathbb{N}}_0\right)$$
22	21	a1i	$$⊢b\in ℝ\to \left(b\in {\mathbb{N}}_0\to \left(\neg 0\le b\to -b\in {\mathbb{N}}_0\right)\right)$$
23		ax-1	$$⊢-b\in {\mathbb{N}}_0\to \left(\neg 0\le b\to -b\in {\mathbb{N}}_0\right)$$
24	23	a1i	$$⊢b\in ℝ\to \left(-b\in {\mathbb{N}}_0\to \left(\neg 0\le b\to -b\in {\mathbb{N}}_0\right)\right)$$
25	22 24	jaod	$$⊢b\in ℝ\to \left(\left(b\in {\mathbb{N}}_0\vee -b\in {\mathbb{N}}_0\right)\to \left(\neg 0\le b\to -b\in {\mathbb{N}}_0\right)\right)$$
26	25	imp	$$⊢\left(b\in ℝ\wedge \left(b\in {\mathbb{N}}_0\vee -b\in {\mathbb{N}}_0\right)\right)\to \left(\neg 0\le b\to -b\in {\mathbb{N}}_0\right)$$
27	19 26	sylbi	$$⊢b\in \mathbb{Z}\to \left(\neg 0\le b\to -b\in {\mathbb{N}}_0\right)$$
28	27	imp	$$⊢\left(b\in \mathbb{Z}\wedge \neg 0\le b\right)\to -b\in {\mathbb{N}}_0$$
29	18 28	ifclda	$$⊢b\in \mathbb{Z}\to if\left(0\le b,b,-b\right)\in {\mathbb{N}}_0$$
30	29	adantl	$$⊢\left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\to if\left(0\le b,b,-b\right)\in {\mathbb{N}}_0$$
31	30	adantr	$$⊢\left(\left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\wedge P=a^2+b^2\right)\to if\left(0\le b,b,-b\right)\in {\mathbb{N}}_0$$
32		elznn0nn	$$⊢a\in \mathbb{Z}\leftrightarrow \left(a\in {\mathbb{N}}_0\vee \left(a\in ℝ\wedge -a\in \mathbb{N}\right)\right)$$
33	5	iftrued	$$⊢a\in {\mathbb{N}}_0\to if\left(0\le a,a,-a\right)=a$$
34	33	eqcomd	$$⊢a\in {\mathbb{N}}_0\to a=if\left(0\le a,a,-a\right)$$
35	34	oveq1d	$$⊢a\in {\mathbb{N}}_0\to a^2={if\left(0\le a,a,-a\right)}^2$$
36		elnnz	$$⊢-a\in \mathbb{N}\leftrightarrow \left(-a\in \mathbb{Z}\wedge 0<-a\right)$$
37		lt0neg1	$$⊢a\in ℝ\to \left(a<0\leftrightarrow 0<-a\right)$$
38		id	$$⊢a\in ℝ\to a\in ℝ$$
39		0red	$$⊢a\in ℝ\to 0\in ℝ$$
40	38 39	ltnled	$$⊢a\in ℝ\to \left(a<0\leftrightarrow \neg 0\le a\right)$$
41	40	biimpd	$$⊢a\in ℝ\to \left(a<0\to \neg 0\le a\right)$$
42	37 41	sylbird	$$⊢a\in ℝ\to \left(0<-a\to \neg 0\le a\right)$$
43	42	com12	$$⊢0<-a\to \left(a\in ℝ\to \neg 0\le a\right)$$
44	36 43	simplbiim	$$⊢-a\in \mathbb{N}\to \left(a\in ℝ\to \neg 0\le a\right)$$
45	44	impcom	$$⊢\left(a\in ℝ\wedge -a\in \mathbb{N}\right)\to \neg 0\le a$$
46	45	iffalsed	$$⊢\left(a\in ℝ\wedge -a\in \mathbb{N}\right)\to if\left(0\le a,a,-a\right)=-a$$
47	46	oveq1d	$$⊢\left(a\in ℝ\wedge -a\in \mathbb{N}\right)\to {if\left(0\le a,a,-a\right)}^2={\left(-a\right)}^2$$
48		recn	$$⊢a\in ℝ\to a\in ℂ$$
49		sqneg	$$⊢a\in ℂ\to {\left(-a\right)}^2=a^2$$
50	48 49	syl	$$⊢a\in ℝ\to {\left(-a\right)}^2=a^2$$
51	50	adantr	$$⊢\left(a\in ℝ\wedge -a\in \mathbb{N}\right)\to {\left(-a\right)}^2=a^2$$
52	47 51	eqtr2d	$$⊢\left(a\in ℝ\wedge -a\in \mathbb{N}\right)\to a^2={if\left(0\le a,a,-a\right)}^2$$
53	35 52	jaoi	$$⊢\left(a\in {\mathbb{N}}_0\vee \left(a\in ℝ\wedge -a\in \mathbb{N}\right)\right)\to a^2={if\left(0\le a,a,-a\right)}^2$$
54	32 53	sylbi	$$⊢a\in \mathbb{Z}\to a^2={if\left(0\le a,a,-a\right)}^2$$
55		elznn0nn	$$⊢b\in \mathbb{Z}\leftrightarrow \left(b\in {\mathbb{N}}_0\vee \left(b\in ℝ\wedge -b\in \mathbb{N}\right)\right)$$
56	20	iftrued	$$⊢b\in {\mathbb{N}}_0\to if\left(0\le b,b,-b\right)=b$$
57	56	eqcomd	$$⊢b\in {\mathbb{N}}_0\to b=if\left(0\le b,b,-b\right)$$
58	57	oveq1d	$$⊢b\in {\mathbb{N}}_0\to b^2={if\left(0\le b,b,-b\right)}^2$$
59		elnnz	$$⊢-b\in \mathbb{N}\leftrightarrow \left(-b\in \mathbb{Z}\wedge 0<-b\right)$$
60		lt0neg1	$$⊢b\in ℝ\to \left(b<0\leftrightarrow 0<-b\right)$$
61		id	$$⊢b\in ℝ\to b\in ℝ$$
62		0red	$$⊢b\in ℝ\to 0\in ℝ$$
63	61 62	ltnled	$$⊢b\in ℝ\to \left(b<0\leftrightarrow \neg 0\le b\right)$$
64	63	biimpd	$$⊢b\in ℝ\to \left(b<0\to \neg 0\le b\right)$$
65	60 64	sylbird	$$⊢b\in ℝ\to \left(0<-b\to \neg 0\le b\right)$$
66	65	com12	$$⊢0<-b\to \left(b\in ℝ\to \neg 0\le b\right)$$
67	59 66	simplbiim	$$⊢-b\in \mathbb{N}\to \left(b\in ℝ\to \neg 0\le b\right)$$
68	67	impcom	$$⊢\left(b\in ℝ\wedge -b\in \mathbb{N}\right)\to \neg 0\le b$$
69	68	iffalsed	$$⊢\left(b\in ℝ\wedge -b\in \mathbb{N}\right)\to if\left(0\le b,b,-b\right)=-b$$
70	69	oveq1d	$$⊢\left(b\in ℝ\wedge -b\in \mathbb{N}\right)\to {if\left(0\le b,b,-b\right)}^2={\left(-b\right)}^2$$
71		recn	$$⊢b\in ℝ\to b\in ℂ$$
72		sqneg	$$⊢b\in ℂ\to {\left(-b\right)}^2=b^2$$
73	71 72	syl	$$⊢b\in ℝ\to {\left(-b\right)}^2=b^2$$
74	73	adantr	$$⊢\left(b\in ℝ\wedge -b\in \mathbb{N}\right)\to {\left(-b\right)}^2=b^2$$
75	70 74	eqtr2d	$$⊢\left(b\in ℝ\wedge -b\in \mathbb{N}\right)\to b^2={if\left(0\le b,b,-b\right)}^2$$
76	58 75	jaoi	$$⊢\left(b\in {\mathbb{N}}_0\vee \left(b\in ℝ\wedge -b\in \mathbb{N}\right)\right)\to b^2={if\left(0\le b,b,-b\right)}^2$$
77	55 76	sylbi	$$⊢b\in \mathbb{Z}\to b^2={if\left(0\le b,b,-b\right)}^2$$
78	54 77	oveqan12d	$$⊢\left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\to a^2+b^2={if\left(0\le a,a,-a\right)}^2+{if\left(0\le b,b,-b\right)}^2$$
79	78	eqeq2d	$$⊢\left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\to \left(P=a^2+b^2\leftrightarrow P={if\left(0\le a,a,-a\right)}^2+{if\left(0\le b,b,-b\right)}^2\right)$$
80	79	biimpd	$$⊢\left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\to \left(P=a^2+b^2\to P={if\left(0\le a,a,-a\right)}^2+{if\left(0\le b,b,-b\right)}^2\right)$$
81	80	imp	$$⊢\left(\left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\wedge P=a^2+b^2\right)\to P={if\left(0\le a,a,-a\right)}^2+{if\left(0\le b,b,-b\right)}^2$$
82		oveq1	$$⊢x=if\left(0\le a,a,-a\right)\to x^2={if\left(0\le a,a,-a\right)}^2$$
83	82	oveq1d	$$⊢x=if\left(0\le a,a,-a\right)\to x^2+y^2={if\left(0\le a,a,-a\right)}^2+y^2$$
84	83	eqeq2d	$$⊢x=if\left(0\le a,a,-a\right)\to \left(P=x^2+y^2\leftrightarrow P={if\left(0\le a,a,-a\right)}^2+y^2\right)$$
85		oveq1	$$⊢y=if\left(0\le b,b,-b\right)\to y^2={if\left(0\le b,b,-b\right)}^2$$
86	85	oveq2d	$$⊢y=if\left(0\le b,b,-b\right)\to {if\left(0\le a,a,-a\right)}^2+y^2={if\left(0\le a,a,-a\right)}^2+{if\left(0\le b,b,-b\right)}^2$$
87	86	eqeq2d	$$⊢y=if\left(0\le b,b,-b\right)\to \left(P={if\left(0\le a,a,-a\right)}^2+y^2\leftrightarrow P={if\left(0\le a,a,-a\right)}^2+{if\left(0\le b,b,-b\right)}^2\right)$$
88	84 87	rspc2ev	$$⊢\left(if\left(0\le a,a,-a\right)\in {\mathbb{N}}_0\wedge if\left(0\le b,b,-b\right)\in {\mathbb{N}}_0\wedge P={if\left(0\le a,a,-a\right)}^2+{if\left(0\le b,b,-b\right)}^2\right)\to \exists x\in {\mathbb{N}}_0\exists y\in {\mathbb{N}}_{0}P=x^2+y^2$$
89	16 31 81 88	syl3anc	$$⊢\left(\left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\wedge P=a^2+b^2\right)\to \exists x\in {\mathbb{N}}_0\exists y\in {\mathbb{N}}_{0}P=x^2+y^2$$
90	89	ex	$$⊢\left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\to \left(P=a^2+b^2\to \exists x\in {\mathbb{N}}_0\exists y\in {\mathbb{N}}_{0}P=x^2+y^2\right)$$
91	90	rexlimivv	$$⊢\exists a\in \mathbb{Z}\exists b\in \mathbb{Z}P=a^2+b^2\to \exists x\in {\mathbb{N}}_0\exists y\in {\mathbb{N}}_{0}P=x^2+y^2$$
92	1 91	syl	$$⊢\left(P\in \mathbb{P}\wedge P\mathrm{mod}4=1\right)\to \exists x\in {\mathbb{N}}_0\exists y\in {\mathbb{N}}_{0}P=x^2+y^2$$