Theorem 2sqreu

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

	Ref	Expression
Hypothesis	2sqreu.1	⊢ ( 𝜑 ↔ ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) )
Assertion	2sqreu	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → ( ∃! 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 𝜑 ∧ ∃! 𝑏 ∈ ℕ0 ∃ 𝑎 ∈ ℕ0 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		2sqreu.1	⊢ ( 𝜑 ↔ ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) )
2		2sqreulem1	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 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	1	2sqreulem4	⊢ ∀ 𝑎 ∈ ℕ0 ∃* 𝑏 ∈ ℕ0 𝜑
7		2reu1	⊢ ( ∀ 𝑎 ∈ ℕ0 ∃* 𝑏 ∈ ℕ0 𝜑 → ( ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 𝜑 ↔ ( ∃! 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 𝜑 ∧ ∃! 𝑏 ∈ ℕ0 ∃ 𝑎 ∈ ℕ0 𝜑 ) ) )
8	6 7	mp1i	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → ( ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 𝜑 ↔ ( ∃! 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 𝜑 ∧ ∃! 𝑏 ∈ ℕ0 ∃ 𝑎 ∈ ℕ0 𝜑 ) ) )
9	5 8	syl5bb	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → ( ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ↔ ( ∃! 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 𝜑 ∧ ∃! 𝑏 ∈ ℕ0 ∃ 𝑎 ∈ ℕ0 𝜑 ) ) )
10	2 9	mpbid	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → ( ∃! 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 𝜑 ∧ ∃! 𝑏 ∈ ℕ0 ∃ 𝑎 ∈ ℕ0 𝜑 ) )