Metamath Proof Explorer

Theorem 2sqreuopb

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 . Alternate ordered pair variant of 2sqreunnltb . (Contributed by AV, 3-Jul-2023)

		Ref	Expression
	Assertion	2sqreuopb	⊢ ( 𝑃 ∈ ℙ → ( ( 𝑃 mod 4 ) = 1 ↔ ∃! 𝑝 ∈ ( ℕ × ℕ ) ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		2sqreuopnnltb	⊢ ( 𝑃 ∈ ℙ → ( ( 𝑃 mod 4 ) = 1 ↔ ∃! 𝑝 ∈ ( ℕ × ℕ ) ( ( 1^st ‘ 𝑝 ) < ( 2^nd ‘ 𝑝 ) ∧ ( ( ( 1^st ‘ 𝑝 ) ↑ 2 ) + ( ( 2^nd ‘ 𝑝 ) ↑ 2 ) ) = 𝑃 ) ) )
2		breq12	⊢ ( ( 𝑎 = ( 1^st ‘ 𝑝 ) ∧ 𝑏 = ( 2^nd ‘ 𝑝 ) ) → ( 𝑎 < 𝑏 ↔ ( 1^st ‘ 𝑝 ) < ( 2^nd ‘ 𝑝 ) ) )
3		simpl	⊢ ( ( 𝑎 = ( 1^st ‘ 𝑝 ) ∧ 𝑏 = ( 2^nd ‘ 𝑝 ) ) → 𝑎 = ( 1^st ‘ 𝑝 ) )
4	3	oveq1d	⊢ ( ( 𝑎 = ( 1^st ‘ 𝑝 ) ∧ 𝑏 = ( 2^nd ‘ 𝑝 ) ) → ( 𝑎 ↑ 2 ) = ( ( 1^st ‘ 𝑝 ) ↑ 2 ) )
5		simpr	⊢ ( ( 𝑎 = ( 1^st ‘ 𝑝 ) ∧ 𝑏 = ( 2^nd ‘ 𝑝 ) ) → 𝑏 = ( 2^nd ‘ 𝑝 ) )
6	5	oveq1d	⊢ ( ( 𝑎 = ( 1^st ‘ 𝑝 ) ∧ 𝑏 = ( 2^nd ‘ 𝑝 ) ) → ( 𝑏 ↑ 2 ) = ( ( 2^nd ‘ 𝑝 ) ↑ 2 ) )
7	4 6	oveq12d	⊢ ( ( 𝑎 = ( 1^st ‘ 𝑝 ) ∧ 𝑏 = ( 2^nd ‘ 𝑝 ) ) → ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = ( ( ( 1^st ‘ 𝑝 ) ↑ 2 ) + ( ( 2^nd ‘ 𝑝 ) ↑ 2 ) ) )
8	7	eqeq1d	⊢ ( ( 𝑎 = ( 1^st ‘ 𝑝 ) ∧ 𝑏 = ( 2^nd ‘ 𝑝 ) ) → ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ↔ ( ( ( 1^st ‘ 𝑝 ) ↑ 2 ) + ( ( 2^nd ‘ 𝑝 ) ↑ 2 ) ) = 𝑃 ) )
9	2 8	anbi12d	⊢ ( ( 𝑎 = ( 1^st ‘ 𝑝 ) ∧ 𝑏 = ( 2^nd ‘ 𝑝 ) ) → ( ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ↔ ( ( 1^st ‘ 𝑝 ) < ( 2^nd ‘ 𝑝 ) ∧ ( ( ( 1^st ‘ 𝑝 ) ↑ 2 ) + ( ( 2^nd ‘ 𝑝 ) ↑ 2 ) ) = 𝑃 ) ) )
10	9	opreuopreu	⊢ ( ∃! 𝑝 ∈ ( ℕ × ℕ ) ( ( 1^st ‘ 𝑝 ) < ( 2^nd ‘ 𝑝 ) ∧ ( ( ( 1^st ‘ 𝑝 ) ↑ 2 ) + ( ( 2^nd ‘ 𝑝 ) ↑ 2 ) ) = 𝑃 ) ↔ ∃! 𝑝 ∈ ( ℕ × ℕ ) ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) )
11	1 10	bitrdi	⊢ ( 𝑃 ∈ ℙ → ( ( 𝑃 mod 4 ) = 1 ↔ ∃! 𝑝 ∈ ( ℕ × ℕ ) ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) ) )