Metamath Proof Explorer

Theorem 2sqreuop

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

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

Proof

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