# Metamath Proof Explorer

## Theorem 2sqreuopnn

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

Ref Expression
Assertion 2sqreuopnn ${⊢}\left({P}\in ℙ\wedge {P}\mathrm{mod}4=1\right)\to \exists !{p}\in \left(ℕ×ℕ\right)\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({p}\right)\le {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}\le {b}\wedge {{a}}^{2}+{{b}}^{2}={P}\right)↔\left({a}\le {b}\wedge {{a}}^{2}+{{b}}^{2}={P}\right)$
2 1 2sqreunn ${⊢}\left({P}\in ℙ\wedge {P}\mathrm{mod}4=1\right)\to \left(\exists !{a}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {b}\in ℕ\phantom{\rule{.4em}{0ex}}\left({a}\le {b}\wedge {{a}}^{2}+{{b}}^{2}={P}\right)\wedge \exists !{b}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\left({a}\le {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)\le {2}^{nd}\left({p}\right)↔{1}^{st}\left(⟨{a},{b}⟩\right)\le {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)\le {2}^{nd}\left(⟨{a},{b}⟩\right)↔{a}\le {b}$
11 5 10 syl6bb ${⊢}{p}=⟨{a},{b}⟩\to \left({1}^{st}\left({p}\right)\le {2}^{nd}\left({p}\right)↔{a}\le {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}↔{{a}}^{2}+{{b}}^{2}={P}\right)$
18 11 17 anbi12d ${⊢}{p}=⟨{a},{b}⟩\to \left(\left({1}^{st}\left({p}\right)\le {2}^{nd}\left({p}\right)\wedge {{1}^{st}\left({p}\right)}^{2}+{{2}^{nd}\left({p}\right)}^{2}={P}\right)↔\left({a}\le {b}\wedge {{a}}^{2}+{{b}}^{2}={P}\right)\right)$
19 18 opreu2reurex ${⊢}\exists !{p}\in \left(ℕ×ℕ\right)\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({p}\right)\le {2}^{nd}\left({p}\right)\wedge {{1}^{st}\left({p}\right)}^{2}+{{2}^{nd}\left({p}\right)}^{2}={P}\right)↔\left(\exists !{a}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {b}\in ℕ\phantom{\rule{.4em}{0ex}}\left({a}\le {b}\wedge {{a}}^{2}+{{b}}^{2}={P}\right)\wedge \exists !{b}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\left({a}\le {b}\wedge {{a}}^{2}+{{b}}^{2}={P}\right)\right)$
20 2 19 sylibr ${⊢}\left({P}\in ℙ\wedge {P}\mathrm{mod}4=1\right)\to \exists !{p}\in \left(ℕ×ℕ\right)\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({p}\right)\le {2}^{nd}\left({p}\right)\wedge {{1}^{st}\left({p}\right)}^{2}+{{2}^{nd}\left({p}\right)}^{2}={P}\right)$