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		oveq1	$$⊢x=if\left(0\le a,a,-a\right)\to x^2={if\left(0\le a,a,-a\right)}^2$$
3	2	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$$
4	3	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)$$
5		oveq1	$$⊢y=if\left(0\le b,b,-b\right)\to y^2={if\left(0\le b,b,-b\right)}^2$$
6	5	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$$
7	6	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)$$
8		elnn0z	$$⊢a\in {\mathbb{N}}_0\leftrightarrow \left(a\in \mathbb{Z}\wedge 0\le a\right)$$
9	8	biimpri	$$⊢\left(a\in \mathbb{Z}\wedge 0\le a\right)\to a\in {\mathbb{N}}_0$$
10		elznn0	$$⊢a\in \mathbb{Z}\leftrightarrow \left(a\in ℝ\wedge \left(a\in {\mathbb{N}}_0\vee -a\in {\mathbb{N}}_0\right)\right)$$
11		nn0ge0	$$⊢a\in {\mathbb{N}}_0\to 0\le a$$
12	11	pm2.24d	$$⊢a\in {\mathbb{N}}_0\to \left(\neg 0\le a\to -a\in {\mathbb{N}}_0\right)$$
13	12	a1i	$$⊢a\in ℝ\to \left(a\in {\mathbb{N}}_0\to \left(\neg 0\le a\to -a\in {\mathbb{N}}_0\right)\right)$$
14		ax1w	$$⊢a\in ℝ\to \left(-a\in {\mathbb{N}}_0\to \left(\neg 0\le a\to -a\in {\mathbb{N}}_0\right)\right)$$
15	13 14	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)$$
16	15	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)$$
17	10 16	sylbi	$$⊢a\in \mathbb{Z}\to \left(\neg 0\le a\to -a\in {\mathbb{N}}_0\right)$$
18	17	imp	$$⊢\left(a\in \mathbb{Z}\wedge \neg 0\le a\right)\to -a\in {\mathbb{N}}_0$$
19	9 18	ifclda	$$⊢a\in \mathbb{Z}\to if\left(0\le a,a,-a\right)\in {\mathbb{N}}_0$$
20	19	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$$
21	20	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$$
22		elnn0z	$$⊢b\in {\mathbb{N}}_0\leftrightarrow \left(b\in \mathbb{Z}\wedge 0\le b\right)$$
23	22	biimpri	$$⊢\left(b\in \mathbb{Z}\wedge 0\le b\right)\to b\in {\mathbb{N}}_0$$
24		elznn0	$$⊢b\in \mathbb{Z}\leftrightarrow \left(b\in ℝ\wedge \left(b\in {\mathbb{N}}_0\vee -b\in {\mathbb{N}}_0\right)\right)$$
25		nn0ge0	$$⊢b\in {\mathbb{N}}_0\to 0\le b$$
26	25	pm2.24d	$$⊢b\in {\mathbb{N}}_0\to \left(\neg 0\le b\to -b\in {\mathbb{N}}_0\right)$$
27	26	a1i	$$⊢b\in ℝ\to \left(b\in {\mathbb{N}}_0\to \left(\neg 0\le b\to -b\in {\mathbb{N}}_0\right)\right)$$
28		ax1w	$$⊢b\in ℝ\to \left(-b\in {\mathbb{N}}_0\to \left(\neg 0\le b\to -b\in {\mathbb{N}}_0\right)\right)$$
29	27 28	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)$$
30	29	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)$$
31	24 30	sylbi	$$⊢b\in \mathbb{Z}\to \left(\neg 0\le b\to -b\in {\mathbb{N}}_0\right)$$
32	31	imp	$$⊢\left(b\in \mathbb{Z}\wedge \neg 0\le b\right)\to -b\in {\mathbb{N}}_0$$
33	23 32	ifclda	$$⊢b\in \mathbb{Z}\to if\left(0\le b,b,-b\right)\in {\mathbb{N}}_0$$
34	33	ad2antlr	$$⊢\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$$
35		elznn0nn	$$⊢a\in \mathbb{Z}\leftrightarrow \left(a\in {\mathbb{N}}_0\vee \left(a\in ℝ\wedge -a\in \mathbb{N}\right)\right)$$
36	11	iftrued	$$⊢a\in {\mathbb{N}}_0\to if\left(0\le a,a,-a\right)=a$$
37	36	eqcomd	$$⊢a\in {\mathbb{N}}_0\to a=if\left(0\le a,a,-a\right)$$
38	37	oveq1d	$$⊢a\in {\mathbb{N}}_0\to a^2={if\left(0\le a,a,-a\right)}^2$$
39		elnnz	$$⊢-a\in \mathbb{N}\leftrightarrow \left(-a\in \mathbb{Z}\wedge 0<-a\right)$$
40		lt0neg1	$$⊢a\in ℝ\to \left(a<0\leftrightarrow 0<-a\right)$$
41		id	$$⊢a\in ℝ\to a\in ℝ$$
42		0red	$$⊢a\in ℝ\to 0\in ℝ$$
43	41 42	ltnled	$$⊢a\in ℝ\to \left(a<0\leftrightarrow \neg 0\le a\right)$$
44	43	biimpd	$$⊢a\in ℝ\to \left(a<0\to \neg 0\le a\right)$$
45	40 44	sylbird	$$⊢a\in ℝ\to \left(0<-a\to \neg 0\le a\right)$$
46	45	com12	$$⊢0<-a\to \left(a\in ℝ\to \neg 0\le a\right)$$
47	39 46	simplbiim	$$⊢-a\in \mathbb{N}\to \left(a\in ℝ\to \neg 0\le a\right)$$
48	47	impcom	$$⊢\left(a\in ℝ\wedge -a\in \mathbb{N}\right)\to \neg 0\le a$$
49	48	iffalsed	$$⊢\left(a\in ℝ\wedge -a\in \mathbb{N}\right)\to if\left(0\le a,a,-a\right)=-a$$
50	49	oveq1d	$$⊢\left(a\in ℝ\wedge -a\in \mathbb{N}\right)\to {if\left(0\le a,a,-a\right)}^2={\left(-a\right)}^2$$
51		recn	$$⊢a\in ℝ\to a\in ℂ$$
52	51	sqnegd	$$⊢a\in ℝ\to {\left(-a\right)}^2=a^2$$
53	52	adantr	$$⊢\left(a\in ℝ\wedge -a\in \mathbb{N}\right)\to {\left(-a\right)}^2=a^2$$
54	50 53	eqtr2d	$$⊢\left(a\in ℝ\wedge -a\in \mathbb{N}\right)\to a^2={if\left(0\le a,a,-a\right)}^2$$
55	38 54	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$$
56	35 55	sylbi	$$⊢a\in \mathbb{Z}\to a^2={if\left(0\le a,a,-a\right)}^2$$
57		elznn0nn	$$⊢b\in \mathbb{Z}\leftrightarrow \left(b\in {\mathbb{N}}_0\vee \left(b\in ℝ\wedge -b\in \mathbb{N}\right)\right)$$
58	25	iftrued	$$⊢b\in {\mathbb{N}}_0\to if\left(0\le b,b,-b\right)=b$$
59	58	eqcomd	$$⊢b\in {\mathbb{N}}_0\to b=if\left(0\le b,b,-b\right)$$
60	59	oveq1d	$$⊢b\in {\mathbb{N}}_0\to b^2={if\left(0\le b,b,-b\right)}^2$$
61		elnnz	$$⊢-b\in \mathbb{N}\leftrightarrow \left(-b\in \mathbb{Z}\wedge 0<-b\right)$$
62		lt0neg1	$$⊢b\in ℝ\to \left(b<0\leftrightarrow 0<-b\right)$$
63		id	$$⊢b\in ℝ\to b\in ℝ$$
64		0red	$$⊢b\in ℝ\to 0\in ℝ$$
65	63 64	ltnled	$$⊢b\in ℝ\to \left(b<0\leftrightarrow \neg 0\le b\right)$$
66	65	biimpd	$$⊢b\in ℝ\to \left(b<0\to \neg 0\le b\right)$$
67	62 66	sylbird	$$⊢b\in ℝ\to \left(0<-b\to \neg 0\le b\right)$$
68	67	com12	$$⊢0<-b\to \left(b\in ℝ\to \neg 0\le b\right)$$
69	61 68	simplbiim	$$⊢-b\in \mathbb{N}\to \left(b\in ℝ\to \neg 0\le b\right)$$
70	69	impcom	$$⊢\left(b\in ℝ\wedge -b\in \mathbb{N}\right)\to \neg 0\le b$$
71	70	iffalsed	$$⊢\left(b\in ℝ\wedge -b\in \mathbb{N}\right)\to if\left(0\le b,b,-b\right)=-b$$
72	71	oveq1d	$$⊢\left(b\in ℝ\wedge -b\in \mathbb{N}\right)\to {if\left(0\le b,b,-b\right)}^2={\left(-b\right)}^2$$
73		recn	$$⊢b\in ℝ\to b\in ℂ$$
74	73	sqnegd	$$⊢b\in ℝ\to {\left(-b\right)}^2=b^2$$
75	74	adantr	$$⊢\left(b\in ℝ\wedge -b\in \mathbb{N}\right)\to {\left(-b\right)}^2=b^2$$
76	72 75	eqtr2d	$$⊢\left(b\in ℝ\wedge -b\in \mathbb{N}\right)\to b^2={if\left(0\le b,b,-b\right)}^2$$
77	60 76	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$$
78	57 77	sylbi	$$⊢b\in \mathbb{Z}\to b^2={if\left(0\le b,b,-b\right)}^2$$
79	56 78	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$$
80	79	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)$$
81	80	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)$$
82	81	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$$
83	4 7 21 34 82	2rspcedvdw	$$⊢\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$$
84	83	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)$$
85	84	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$$
86	1 85	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$$