Metamath Proof Explorer

Theorem sq2reunnltb

Description: There exists a unique decomposition of a prime as a sum of squares of two different positive integers iff the prime is of the form 4 k + 1 . Double restricted existential uniqueness variant of 2sqreunnltb . (Contributed by AV, 5-Jul-2023)

Ref Expression
Assertion sq2reunnltb ⊢ P ∈ ℙ → P mod 4 = 1 ↔ ∃! a ∈ ℕ , b ∈ ℕ a < b ∧ a 2 + b 2 = P

Proof

Step Hyp Ref Expression
1 biid ⊢ a < b ∧ a 2 + b 2 = P ↔ a < b ∧ a 2 + b 2 = P
2 1 2sqreunnltb ⊢ P ∈ ℙ → P mod 4 = 1 ↔ ∃! a ∈ ℕ ∃ b ∈ ℕ a < b ∧ a 2 + b 2 = P ∧ ∃! b ∈ ℕ ∃ a ∈ ℕ a < b ∧ a 2 + b 2 = P
3 df-2reu ⊢ ∃! a ∈ ℕ , b ∈ ℕ a < b ∧ a 2 + b 2 = P ↔ ∃! a ∈ ℕ ∃ b ∈ ℕ a < b ∧ a 2 + b 2 = P ∧ ∃! b ∈ ℕ ∃ a ∈ ℕ a < b ∧ a 2 + b 2 = P
4 2 3 bitr4di ⊢ P ∈ ℙ → P mod 4 = 1 ↔ ∃! a ∈ ℕ , b ∈ ℕ a < b ∧ a 2 + b 2 = P