Theorem 2sqreuopb

Description: There exists a unique decomposition of a prime as a sum of squares of two different positive integers iff the prime is of the form 4 k + 1 . Alternate ordered pair variant of 2sqreunnltb . (Contributed by AV, 3-Jul-2023)

	Ref	Expression
Assertion	2sqreuopb	$$⊢P\in \mathbb{P}\to \left(P\mathrm{mod}4=1\leftrightarrow \exists !p\in \left(\mathbb{N}\times \mathbb{N}\right)\exists a\exists b\left(p=⟨a,b⟩\wedge \left(a<b\wedge a^2+b^2=P\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		2sqreuopnnltb	$$⊢P\in \mathbb{P}\to \left(P\mathrm{mod}4=1\leftrightarrow \exists !p\in \left(\mathbb{N}\times \mathbb{N}\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)$$
2		breq12	$$⊢\left(a=1^{st}\left(p\right)\wedge b=2^{nd}\left(p\right)\right)\to \left(a<b\leftrightarrow 1^{st}\left(p\right)<2^{nd}\left(p\right)\right)$$
3		simpl	$$⊢\left(a=1^{st}\left(p\right)\wedge b=2^{nd}\left(p\right)\right)\to a=1^{st}\left(p\right)$$
4	3	oveq1d	$$⊢\left(a=1^{st}\left(p\right)\wedge b=2^{nd}\left(p\right)\right)\to a^2={1^{st}\left(p\right)}^2$$
5		simpr	$$⊢\left(a=1^{st}\left(p\right)\wedge b=2^{nd}\left(p\right)\right)\to b=2^{nd}\left(p\right)$$
6	5	oveq1d	$$⊢\left(a=1^{st}\left(p\right)\wedge b=2^{nd}\left(p\right)\right)\to b^2={2^{nd}\left(p\right)}^2$$
7	4 6	oveq12d	$$⊢\left(a=1^{st}\left(p\right)\wedge b=2^{nd}\left(p\right)\right)\to a^2+b^2={1^{st}\left(p\right)}^2+{2^{nd}\left(p\right)}^2$$
8	7	eqeq1d	$$⊢\left(a=1^{st}\left(p\right)\wedge b=2^{nd}\left(p\right)\right)\to \left(a^2+b^2=P\leftrightarrow {1^{st}\left(p\right)}^2+{2^{nd}\left(p\right)}^2=P\right)$$
9	2 8	anbi12d	$$⊢\left(a=1^{st}\left(p\right)\wedge b=2^{nd}\left(p\right)\right)\to \left(\left(a<b\wedge a^2+b^2=P\right)\leftrightarrow \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)$$
10	9	opreuopreu	$$⊢\exists !p\in \left(\mathbb{N}\times \mathbb{N}\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 \exists !p\in \left(\mathbb{N}\times \mathbb{N}\right)\exists a\exists b\left(p=⟨a,b⟩\wedge \left(a<b\wedge a^2+b^2=P\right)\right)$$
11	1 10	bitrdi	$$⊢P\in \mathbb{P}\to \left(P\mathrm{mod}4=1\leftrightarrow \exists !p\in \left(\mathbb{N}\times \mathbb{N}\right)\exists a\exists b\left(p=⟨a,b⟩\wedge \left(a<b\wedge a^2+b^2=P\right)\right)\right)$$