Metamath Proof Explorer

Theorem 2sqreultb

Description: There exists a unique decomposition of a prime as a sum of squares of two different nonnegative integers iff P == 1 (mod 4). (Contributed by AV, 10-Jun-2023) The prime needs not be odd, as observed by WL. (Revised by AV, 25-Jun-2023)

Ref Expression
Hypothesis 2sqreult.1 ⊢ φ ↔ a < b ∧ a 2 + b 2 = P
Assertion 2sqreultb ⊢ P ∈ ℙ → P mod 4 = 1 ↔ ∃! a ∈ ℕ 0 ∃ b ∈ ℕ 0 φ ∧ ∃! b ∈ ℕ 0 ∃ a ∈ ℕ 0 φ

Proof

Step Hyp Ref Expression
1 2sqreult.1 ⊢ φ ↔ a < b ∧ a 2 + b 2 = P
2 2sqreultblem ⊢ P ∈ ℙ → P mod 4 = 1 ↔ ∃! a ∈ ℕ 0 ∃! b ∈ ℕ 0 a < b ∧ a 2 + b 2 = P
3 1 bicomi ⊢ a < b ∧ a 2 + b 2 = P ↔ φ
4 3 reubii ⊢ ∃! b ∈ ℕ 0 a < b ∧ a 2 + b 2 = P ↔ ∃! b ∈ ℕ 0 φ
5 4 reubii ⊢ ∃! a ∈ ℕ 0 ∃! b ∈ ℕ 0 a < b ∧ a 2 + b 2 = P ↔ ∃! a ∈ ℕ 0 ∃! b ∈ ℕ 0 φ
6 5 a1i ⊢ P ∈ ℙ → ∃! a ∈ ℕ 0 ∃! b ∈ ℕ 0 a < b ∧ a 2 + b 2 = P ↔ ∃! a ∈ ℕ 0 ∃! b ∈ ℕ 0 φ
7 1 2sqreulem4 ⊢ ∀ a ∈ ℕ 0 ∃* b ∈ ℕ 0 φ
8 2reu1 ⊢ ∀ a ∈ ℕ 0 ∃* b ∈ ℕ 0 φ → ∃! a ∈ ℕ 0 ∃! b ∈ ℕ 0 φ ↔ ∃! a ∈ ℕ 0 ∃ b ∈ ℕ 0 φ ∧ ∃! b ∈ ℕ 0 ∃ a ∈ ℕ 0 φ
9 7 8 mp1i ⊢ P ∈ ℙ → ∃! a ∈ ℕ 0 ∃! b ∈ ℕ 0 φ ↔ ∃! a ∈ ℕ 0 ∃ b ∈ ℕ 0 φ ∧ ∃! b ∈ ℕ 0 ∃ a ∈ ℕ 0 φ
10 2 6 9 3bitrd ⊢ P ∈ ℙ → P mod 4 = 1 ↔ ∃! a ∈ ℕ 0 ∃ b ∈ ℕ 0 φ ∧ ∃! b ∈ ℕ 0 ∃ a ∈ ℕ 0 φ