Theorem 2sqreult

Description: There exists a unique decomposition of a prime as a sum of squares of two different nonnegative integers. (Contributed by AV, 8-Jun-2023) (Proposed by GL, 8-Jun-2023.) (Revised by AV, 25-Jun-2023)

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

Proof

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