Theorem 2sqreuopltb

Description: There exists a unique decomposition of a prime as a sum of squares of two different nonnegative integers iff P == 1 (mod 4). Ordered pair variant of 2sqreultb . (Contributed by AV, 3-Jul-2023)

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

Proof

Step	Hyp	Ref	Expression
1		biid	$$⊢\left(a<b\wedge a^2+b^2=P\right)\leftrightarrow \left(a<b\wedge a^2+b^2=P\right)$$
2	1	2sqreultb	$$⊢P\in \mathbb{P}\to \left(P\mathrm{mod}4=1\leftrightarrow \left(\exists !a\in {\mathbb{N}}_0\exists b\in {\mathbb{N}}_0\left(a<b\wedge a^2+b^2=P\right)\wedge \exists !b\in {\mathbb{N}}_0\exists a\in {\mathbb{N}}_0\left(a<b\wedge a^2+b^2=P\right)\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)<2^{nd}\left(p\right)\leftrightarrow 1^{st}\left(⟨a,b⟩\right)<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)<2^{nd}\left(⟨a,b⟩\right)\leftrightarrow a<b$$
11	5 10	bitrdi	$$⊢p=⟨a,b⟩\to \left(1^{st}\left(p\right)<2^{nd}\left(p\right)\leftrightarrow a<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)<2^{nd}\left(p\right)\wedge {1^{st}\left(p\right)}^2+{2^{nd}\left(p\right)}^2=P\right)\leftrightarrow \left(a<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)<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<b\wedge a^2+b^2=P\right)\wedge \exists !b\in {\mathbb{N}}_0\exists a\in {\mathbb{N}}_0\left(a<b\wedge a^2+b^2=P\right)\right)$$
20	2 19	bitr4di	$$⊢P\in \mathbb{P}\to \left(P\mathrm{mod}4=1\leftrightarrow \exists !p\in \left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\left(1^{st}\left(p\right)<2^{nd}\left(p\right)\wedge {1^{st}\left(p\right)}^2+{2^{nd}\left(p\right)}^2=P\right)\right)$$