2sqreuoplt

Description: There exists a unique decomposition of a prime as a sum of squares of two different nonnegative integers. Ordered pair variant of 2sqreult . (Contributed by AV, 2-Jul-2023)

		Ref	Expression
	Assertion	2sqreuoplt	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 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	2sqreult	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 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 2sqreuoplt

Proof