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 ( 𝜑 ↔ ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) )
Assertion 2sqreultb ( 𝑃 ∈ ℙ → ( ( 𝑃 mod 4 ) = 1 ↔ ( ∃! 𝑎 ∈ ℕ0𝑏 ∈ ℕ0 𝜑 ∧ ∃! 𝑏 ∈ ℕ0𝑎 ∈ ℕ0 𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 2sqreult.1 ( 𝜑 ↔ ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) )
2 2sqreultblem ( 𝑃 ∈ ℙ → ( ( 𝑃 mod 4 ) = 1 ↔ ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) )
3 1 bicomi ( ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ↔ 𝜑 )
4 3 reubii ( ∃! 𝑏 ∈ ℕ0 ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ↔ ∃! 𝑏 ∈ ℕ0 𝜑 )
5 4 reubii ( ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ↔ ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 𝜑 )
6 5 a1i ( 𝑃 ∈ ℙ → ( ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ↔ ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 𝜑 ) )
7 1 2sqreulem4 𝑎 ∈ ℕ0 ∃* 𝑏 ∈ ℕ0 𝜑
8 2reu1 ( ∀ 𝑎 ∈ ℕ0 ∃* 𝑏 ∈ ℕ0 𝜑 → ( ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 𝜑 ↔ ( ∃! 𝑎 ∈ ℕ0𝑏 ∈ ℕ0 𝜑 ∧ ∃! 𝑏 ∈ ℕ0𝑎 ∈ ℕ0 𝜑 ) ) )
9 7 8 mp1i ( 𝑃 ∈ ℙ → ( ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 𝜑 ↔ ( ∃! 𝑎 ∈ ℕ0𝑏 ∈ ℕ0 𝜑 ∧ ∃! 𝑏 ∈ ℕ0𝑎 ∈ ℕ0 𝜑 ) ) )
10 2 6 9 3bitrd ( 𝑃 ∈ ℙ → ( ( 𝑃 mod 4 ) = 1 ↔ ( ∃! 𝑎 ∈ ℕ0𝑏 ∈ ℕ0 𝜑 ∧ ∃! 𝑏 ∈ ℕ0𝑎 ∈ ℕ0 𝜑 ) ) )