Theorem 2sqreuop

Description: There exists a unique decomposition of a prime of the form 4 k + 1 as a sum of squares of two nonnegative integers. Ordered pair variant of 2sqreu . (Contributed by AV, 2-Jul-2023)

	Ref	Expression
Assertion	2sqreuop	$$⊢\left(P\in \mathbb{P}\wedge P\mathrm{mod}4=1\right)\to \exists !p\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\left(1^{st}\left(p\right)\le 2^{nd}\left(p\right)\wedge {1^{st}\left(p\right)}^2+{2^{nd}\left(p\right)}^2=P\right)$$

Proof

Step	Hyp	Ref	Expression
1		biid	$$⊢\left(a\le b\wedge a^2+b^2=P\right)\leftrightarrow \left(a\le b\wedge a^2+b^2=P\right)$$
2	1	2sqreu	$$⊢\left(P\in \mathbb{P}\wedge P\mathrm{mod}4=1\right)\to \left(\exists !a\in {\mathbb{N}}_0\exists b\in {\mathbb{N}}_0\left(a\le b\wedge a^2+b^2=P\right)\wedge \exists !b\in {\mathbb{N}}_0\exists a\in {\mathbb{N}}_0\left(a\le b\wedge a^2+b^2=P\right)\right)$$
3		fveq2	$$⊢p=⟨a,b⟩\to 1^{st}\left(p\right)=1^{st}\left(⟨a,b⟩\right)$$
4		fveq2	$$⊢p=⟨a,b⟩\to 2^{nd}\left(p\right)=2^{nd}\left(⟨a,b⟩\right)$$
5	3 4	breq12d	$$⊢p=⟨a,b⟩\to \left(1^{st}\left(p\right)\le 2^{nd}\left(p\right)\leftrightarrow 1^{st}\left(⟨a,b⟩\right)\le 2^{nd}\left(⟨a,b⟩\right)\right)$$
6		vex	$$⊢a\in \mathrm{V}$$
7		vex	$$⊢b\in \mathrm{V}$$
8	6 7	op1st	$$⊢1^{st}\left(⟨a,b⟩\right)=a$$
9	6 7	op2nd	$$⊢2^{nd}\left(⟨a,b⟩\right)=b$$
10	8 9	breq12i	$$⊢1^{st}\left(⟨a,b⟩\right)\le 2^{nd}\left(⟨a,b⟩\right)\leftrightarrow a\le b$$
11	5 10	bitrdi	$$⊢p=⟨a,b⟩\to \left(1^{st}\left(p\right)\le 2^{nd}\left(p\right)\leftrightarrow a\le b\right)$$
12	6 7	op1std	$$⊢p=⟨a,b⟩\to 1^{st}\left(p\right)=a$$
13	12	oveq1d	$$⊢p=⟨a,b⟩\to {1^{st}\left(p\right)}^2=a^2$$
14	6 7	op2ndd	$$⊢p=⟨a,b⟩\to 2^{nd}\left(p\right)=b$$
15	14	oveq1d	$$⊢p=⟨a,b⟩\to {2^{nd}\left(p\right)}^2=b^2$$
16	13 15	oveq12d	$$⊢p=⟨a,b⟩\to {1^{st}\left(p\right)}^2+{2^{nd}\left(p\right)}^2=a^2+b^2$$
17	16	eqeq1d	$$⊢p=⟨a,b⟩\to \left({1^{st}\left(p\right)}^2+{2^{nd}\left(p\right)}^2=P\leftrightarrow a^2+b^2=P\right)$$
18	11 17	anbi12d	$$⊢p=⟨a,b⟩\to \left(\left(1^{st}\left(p\right)\le 2^{nd}\left(p\right)\wedge {1^{st}\left(p\right)}^2+{2^{nd}\left(p\right)}^2=P\right)\leftrightarrow \left(a\le b\wedge a^2+b^2=P\right)\right)$$
19	18	opreu2reurex	$$⊢\exists !p\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\left(1^{st}\left(p\right)\le 2^{nd}\left(p\right)\wedge {1^{st}\left(p\right)}^2+{2^{nd}\left(p\right)}^2=P\right)\leftrightarrow \left(\exists !a\in {\mathbb{N}}_0\exists b\in {\mathbb{N}}_0\left(a\le b\wedge a^2+b^2=P\right)\wedge \exists !b\in {\mathbb{N}}_0\exists a\in {\mathbb{N}}_0\left(a\le b\wedge a^2+b^2=P\right)\right)$$
20	2 19	sylibr	$$⊢\left(P\in \mathbb{P}\wedge P\mathrm{mod}4=1\right)\to \exists !p\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\left(1^{st}\left(p\right)\le 2^{nd}\left(p\right)\wedge {1^{st}\left(p\right)}^2+{2^{nd}\left(p\right)}^2=P\right)$$