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

Proof

Step	Hyp	Ref	Expression
1		biid	⊢ ( ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ↔ ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) )
2	1	2sqreunnltb	⊢ ( 𝑃 ∈ ℙ → ( ( 𝑃 mod 4 ) = 1 ↔ ( ∃! 𝑎 ∈ ℕ ∃ 𝑏 ∈ ℕ ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ∧ ∃! 𝑏 ∈ ℕ ∃ 𝑎 ∈ ℕ ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) ) )
3		df-2reu	⊢ ( ∃! 𝑎 ∈ ℕ , 𝑏 ∈ ℕ ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ↔ ( ∃! 𝑎 ∈ ℕ ∃ 𝑏 ∈ ℕ ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ∧ ∃! 𝑏 ∈ ℕ ∃ 𝑎 ∈ ℕ ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) )
4	2 3	bitr4di	⊢ ( 𝑃 ∈ ℙ → ( ( 𝑃 mod 4 ) = 1 ↔ ∃! 𝑎 ∈ ℕ , 𝑏 ∈ ℕ ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) )