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∧a2+b2=P
Assertion 2sqreunn ⊢P∈ℙ∧Pmod4=1→∃!a∈ℕ∃b∈ℕφ∧∃!b∈ℕ∃a∈ℕφ

Proof

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