Theorem 2sqreuopnnlt

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

	Ref	Expression
Assertion	2sqreuopnnlt	$$⊢\left(P\in \mathbb{P}\wedge P\mathrm{mod}4=1\right)\to \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)$$

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	2sqreunnlt	$$⊢\left(P\in \mathbb{P}\wedge P\mathrm{mod}4=1\right)\to \left(\exists !a\in \mathbb{N}\exists b\in \mathbb{N}\left(a<b\wedge a^2+b^2=P\right)\wedge \exists !b\in \mathbb{N}\exists a\in \mathbb{N}\left(a<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)<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}\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 \left(\exists !a\in \mathbb{N}\exists b\in \mathbb{N}\left(a<b\wedge a^2+b^2=P\right)\wedge \exists !b\in \mathbb{N}\exists a\in \mathbb{N}\left(a<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}\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)$$