2sqreuopnn

Description: There exists a unique decomposition of a prime of the form 4 k + 1 as a sum of squares of two positive integers. Ordered pair variant of 2sqreunn . (Contributed by AV, 2-Jul-2023)

		Ref	Expression
	Assertion	2sqreuopnn	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → ∃! 𝑝 ∈ ( ℕ × ℕ ) ( ( 1^st ‘ 𝑝 ) ≤ ( 2^nd ‘ 𝑝 ) ∧ ( ( ( 1^st ‘ 𝑝 ) ↑ 2 ) + ( ( 2^nd ‘ 𝑝 ) ↑ 2 ) ) = 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		biid	⊢ ( ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ↔ ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) )
2	1	2sqreunn	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → ( ∃! 𝑎 ∈ ℕ ∃ 𝑏 ∈ ℕ ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ∧ ∃! 𝑏 ∈ ℕ ∃ 𝑎 ∈ ℕ ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) )
3		fveq2	⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 1^st ‘ 𝑝 ) = ( 1^st ‘ ⟨ 𝑎 , 𝑏 ⟩ ) )
4		fveq2	⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 2^nd ‘ 𝑝 ) = ( 2^nd ‘ ⟨ 𝑎 , 𝑏 ⟩ ) )
5	3 4	breq12d	⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 1^st ‘ 𝑝 ) ≤ ( 2^nd ‘ 𝑝 ) ↔ ( 1^st ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ≤ ( 2^nd ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) )
6		vex	⊢ 𝑎 ∈ V
7		vex	⊢ 𝑏 ∈ V
8	6 7	op1st	⊢ ( 1^st ‘ ⟨ 𝑎 , 𝑏 ⟩ ) = 𝑎
9	6 7	op2nd	⊢ ( 2^nd ‘ ⟨ 𝑎 , 𝑏 ⟩ ) = 𝑏
10	8 9	breq12i	⊢ ( ( 1^st ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ≤ ( 2^nd ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ↔ 𝑎 ≤ 𝑏 )
11	5 10	bitrdi	⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 1^st ‘ 𝑝 ) ≤ ( 2^nd ‘ 𝑝 ) ↔ 𝑎 ≤ 𝑏 ) )
12	6 7	op1std	⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 1^st ‘ 𝑝 ) = 𝑎 )
13	12	oveq1d	⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 1^st ‘ 𝑝 ) ↑ 2 ) = ( 𝑎 ↑ 2 ) )
14	6 7	op2ndd	⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 2^nd ‘ 𝑝 ) = 𝑏 )
15	14	oveq1d	⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 2^nd ‘ 𝑝 ) ↑ 2 ) = ( 𝑏 ↑ 2 ) )
16	13 15	oveq12d	⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( ( 1^st ‘ 𝑝 ) ↑ 2 ) + ( ( 2^nd ‘ 𝑝 ) ↑ 2 ) ) = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) )
17	16	eqeq1d	⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( ( ( 1^st ‘ 𝑝 ) ↑ 2 ) + ( ( 2^nd ‘ 𝑝 ) ↑ 2 ) ) = 𝑃 ↔ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) )
18	11 17	anbi12d	⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( ( 1^st ‘ 𝑝 ) ≤ ( 2^nd ‘ 𝑝 ) ∧ ( ( ( 1^st ‘ 𝑝 ) ↑ 2 ) + ( ( 2^nd ‘ 𝑝 ) ↑ 2 ) ) = 𝑃 ) ↔ ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) )
19	18	opreu2reurex	⊢ ( ∃! 𝑝 ∈ ( ℕ × ℕ ) ( ( 1^st ‘ 𝑝 ) ≤ ( 2^nd ‘ 𝑝 ) ∧ ( ( ( 1^st ‘ 𝑝 ) ↑ 2 ) + ( ( 2^nd ‘ 𝑝 ) ↑ 2 ) ) = 𝑃 ) ↔ ( ∃! 𝑎 ∈ ℕ ∃ 𝑏 ∈ ℕ ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ∧ ∃! 𝑏 ∈ ℕ ∃ 𝑎 ∈ ℕ ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) )
20	2 19	sylibr	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → ∃! 𝑝 ∈ ( ℕ × ℕ ) ( ( 1^st ‘ 𝑝 ) ≤ ( 2^nd ‘ 𝑝 ) ∧ ( ( ( 1^st ‘ 𝑝 ) ↑ 2 ) + ( ( 2^nd ‘ 𝑝 ) ↑ 2 ) ) = 𝑃 ) )

Metamath Proof Explorer

Theorem 2sqreuopnn

Proof