Theorem 2sqreultb

Description: There exists a unique decomposition of a prime as a sum of squares of two different nonnegative integers iff P == 1 (mod 4). (Contributed by AV, 10-Jun-2023) The prime needs not be odd, as observed by WL. (Revised by AV, 25-Jun-2023)

	Ref	Expression
Hypothesis	2sqreult.1	$$⊢\phi \leftrightarrow \left(a<b\wedge a^2+b^2=P\right)$$
Assertion	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\phi \wedge \exists !b\in {\mathbb{N}}_0\exists a\in {\mathbb{N}}_0\phi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		2sqreult.1	$$⊢\phi \leftrightarrow \left(a<b\wedge a^2+b^2=P\right)$$
2		2sqreultblem	$$⊢P\in \mathbb{P}\to \left(P\mathrm{mod}4=1\leftrightarrow \exists !a\in {\mathbb{N}}_0\exists !b\in {\mathbb{N}}_0\left(a<b\wedge a^2+b^2=P\right)\right)$$
3	1	bicomi	$$⊢\left(a<b\wedge a^2+b^2=P\right)\leftrightarrow \phi$$
4	3	reubii	$$⊢\exists !b\in {\mathbb{N}}_0\left(a<b\wedge a^2+b^2=P\right)\leftrightarrow \exists !b\in {\mathbb{N}}_0\phi$$
5	4	reubii	$$⊢\exists !a\in {\mathbb{N}}_0\exists !b\in {\mathbb{N}}_0\left(a<b\wedge a^2+b^2=P\right)\leftrightarrow \exists !a\in {\mathbb{N}}_0\exists !b\in {\mathbb{N}}_0\phi$$
6	5	a1i	$$⊢P\in \mathbb{P}\to \left(\exists !a\in {\mathbb{N}}_0\exists !b\in {\mathbb{N}}_0\left(a<b\wedge a^2+b^2=P\right)\leftrightarrow \exists !a\in {\mathbb{N}}_0\exists !b\in {\mathbb{N}}_0\phi \right)$$
7	1	2sqreulem4	$$⊢\forall a\in {\mathbb{N}}_0{\exists }^{*}b\in {\mathbb{N}}_0\phi$$
8		2reu1	$$⊢\forall a\in {\mathbb{N}}_0{\exists }^{*}b\in {\mathbb{N}}_0\phi \to \left(\exists !a\in {\mathbb{N}}_0\exists !b\in {\mathbb{N}}_0\phi \leftrightarrow \left(\exists !a\in {\mathbb{N}}_0\exists b\in {\mathbb{N}}_0\phi \wedge \exists !b\in {\mathbb{N}}_0\exists a\in {\mathbb{N}}_0\phi \right)\right)$$
9	7 8	mp1i	$$⊢P\in \mathbb{P}\to \left(\exists !a\in {\mathbb{N}}_0\exists !b\in {\mathbb{N}}_0\phi \leftrightarrow \left(\exists !a\in {\mathbb{N}}_0\exists b\in {\mathbb{N}}_0\phi \wedge \exists !b\in {\mathbb{N}}_0\exists a\in {\mathbb{N}}_0\phi \right)\right)$$
10	2 6 9	3bitrd	$$⊢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\phi \wedge \exists !b\in {\mathbb{N}}_0\exists a\in {\mathbb{N}}_0\phi \right)\right)$$