Metamath Proof Explorer

Theorem 2sqreunn

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

Ref Expression
Hypothesis 2sqreu.1 ⊢ φ ↔ a ≤ b ∧ a 2 + b 2 = P
Assertion 2sqreunn ⊢ P ∈ ℙ ∧ P mod 4 = 1 → ∃! a ∈ ℕ ∃ b ∈ ℕ φ ∧ ∃! b ∈ ℕ ∃ a ∈ ℕ φ

Proof

Step Hyp Ref Expression
1 2sqreu.1 ⊢ φ ↔ a ≤ b ∧ a 2 + b 2 = P
2 2sqreunnlem1 ⊢ P ∈ ℙ ∧ P mod 4 = 1 → ∃! a ∈ ℕ ∃! b ∈ ℕ a ≤ b ∧ a 2 + b 2 = P
3 1 bicomi ⊢ a ≤ b ∧ a 2 + b 2 = P ↔ φ
4 3 reubii ⊢ ∃! b ∈ ℕ a ≤ b ∧ a 2 + b 2 = P ↔ ∃! b ∈ ℕ φ
5 4 reubii ⊢ ∃! a ∈ ℕ ∃! b ∈ ℕ a ≤ b ∧ a 2 + b 2 = P ↔ ∃! a ∈ ℕ ∃! b ∈ ℕ φ
6 1 2sqreunnlem2 ⊢ ∀ a ∈ ℕ ∃* b ∈ ℕ φ
7 2reu1 ⊢ ∀ a ∈ ℕ ∃* b ∈ ℕ φ → ∃! a ∈ ℕ ∃! b ∈ ℕ φ ↔ ∃! a ∈ ℕ ∃ b ∈ ℕ φ ∧ ∃! b ∈ ℕ ∃ a ∈ ℕ φ
8 6 7 mp1i ⊢ P ∈ ℙ ∧ P mod 4 = 1 → ∃! a ∈ ℕ ∃! b ∈ ℕ φ ↔ ∃! a ∈ ℕ ∃ b ∈ ℕ φ ∧ ∃! b ∈ ℕ ∃ a ∈ ℕ φ
9 5 8 bitrid ⊢ P ∈ ℙ ∧ P mod 4 = 1 → ∃! a ∈ ℕ ∃! b ∈ ℕ a ≤ b ∧ a 2 + b 2 = P ↔ ∃! a ∈ ℕ ∃ b ∈ ℕ φ ∧ ∃! b ∈ ℕ ∃ a ∈ ℕ φ
10 2 9 mpbid ⊢ P ∈ ℙ ∧ P mod 4 = 1 → ∃! a ∈ ℕ ∃ b ∈ ℕ φ ∧ ∃! b ∈ ℕ ∃ a ∈ ℕ φ