# Metamath Proof Explorer

## 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 }↔\left({a}\le {b}\wedge {{a}}^{2}+{{b}}^{2}={P}\right)$
Assertion 2sqreu ${⊢}\left({P}\in ℙ\wedge {P}\mathrm{mod}4=1\right)\to \left(\exists !{a}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {b}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists !{b}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {a}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{\phi }\right)$

### Proof

Step Hyp Ref Expression
1 2sqreu.1 ${⊢}{\phi }↔\left({a}\le {b}\wedge {{a}}^{2}+{{b}}^{2}={P}\right)$
2 2sqreulem1 ${⊢}\left({P}\in ℙ\wedge {P}\mathrm{mod}4=1\right)\to \exists !{a}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists !{b}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\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)↔{\phi }$
4 3 reubii ${⊢}\exists !{b}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({a}\le {b}\wedge {{a}}^{2}+{{b}}^{2}={P}\right)↔\exists !{b}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{\phi }$
5 4 reubii ${⊢}\exists !{a}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists !{b}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({a}\le {b}\wedge {{a}}^{2}+{{b}}^{2}={P}\right)↔\exists !{a}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists !{b}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{\phi }$
6 1 2sqreulem4 ${⊢}\forall {a}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{b}\in {ℕ}_{0}{\phi }$
7 2reu1 ${⊢}\forall {a}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{b}\in {ℕ}_{0}{\phi }\to \left(\exists !{a}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists !{b}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\exists !{a}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {b}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists !{b}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {a}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
8 6 7 mp1i ${⊢}\left({P}\in ℙ\wedge {P}\mathrm{mod}4=1\right)\to \left(\exists !{a}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists !{b}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\exists !{a}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {b}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists !{b}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {a}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
9 5 8 syl5bb ${⊢}\left({P}\in ℙ\wedge {P}\mathrm{mod}4=1\right)\to \left(\exists !{a}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists !{b}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({a}\le {b}\wedge {{a}}^{2}+{{b}}^{2}={P}\right)↔\left(\exists !{a}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {b}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists !{b}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {a}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
10 2 9 mpbid ${⊢}\left({P}\in ℙ\wedge {P}\mathrm{mod}4=1\right)\to \left(\exists !{a}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {b}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists !{b}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {a}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{\phi }\right)$