Theorem 2sqreu

Description: There exists a unique decomposition of a prime of the form 4 k + 1 as a sum of squares of two nonnegative integers. See 2sqnn0 for the existence of such a decomposition. (Contributed by AV, 4-Jun-2023) (Revised by AV, 25-Jun-2023)

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