Metamath Proof Explorer

Theorem 2sqreuopnnlt

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

Ref Expression
Assertion 2sqreuopnnlt ⊢ P ∈ ℙ ∧ P mod 4 = 1 → ∃! p ∈ ℕ × ℕ 1 st ⁡ p < 2 nd ⁡ p ∧ 1 st ⁡ p 2 + 2 nd ⁡ p 2 = P

Proof

Step Hyp Ref Expression
1 biid ⊢ a < b ∧ a 2 + b 2 = P ↔ a < b ∧ a 2 + b 2 = P
2 1 2sqreunnlt ⊢ P ∈ ℙ ∧ P mod 4 = 1 → ∃! a ∈ ℕ ∃ b ∈ ℕ a < b ∧ a 2 + b 2 = P ∧ ∃! b ∈ ℕ ∃ a ∈ ℕ a < b ∧ a 2 + b 2 = P
3 fveq2 ⊢ p = a b → 1 st ⁡ p = 1 st ⁡ a b
4 fveq2 ⊢ p = a b → 2 nd ⁡ p = 2 nd ⁡ a b
5 3 4 breq12d ⊢ p = a b → 1 st ⁡ p < 2 nd ⁡ p ↔ 1 st ⁡ a b < 2 nd ⁡ a b
6 vex ⊢ a ∈ V
7 vex ⊢ b ∈ V
8 6 7 op1st ⊢ 1 st ⁡ a b = a
9 6 7 op2nd ⊢ 2 nd ⁡ a b = b
10 8 9 breq12i ⊢ 1 st ⁡ a b < 2 nd ⁡ a b ↔ a < b
11 5 10 bitrdi ⊢ p = a b → 1 st ⁡ p < 2 nd ⁡ p ↔ a < b
12 6 7 op1std ⊢ p = a b → 1 st ⁡ p = a
13 12 oveq1d ⊢ p = a b → 1 st ⁡ p 2 = a 2
14 6 7 op2ndd ⊢ p = a b → 2 nd ⁡ p = b
15 14 oveq1d ⊢ p = a b → 2 nd ⁡ p 2 = b 2
16 13 15 oveq12d ⊢ p = a b → 1 st ⁡ p 2 + 2 nd ⁡ p 2 = a 2 + b 2
17 16 eqeq1d ⊢ p = a b → 1 st ⁡ p 2 + 2 nd ⁡ p 2 = P ↔ a 2 + b 2 = P
18 11 17 anbi12d ⊢ p = a b → 1 st ⁡ p < 2 nd ⁡ p ∧ 1 st ⁡ p 2 + 2 nd ⁡ p 2 = P ↔ a < b ∧ a 2 + b 2 = P
19 18 opreu2reurex ⊢ ∃! p ∈ ℕ × ℕ 1 st ⁡ p < 2 nd ⁡ p ∧ 1 st ⁡ p 2 + 2 nd ⁡ p 2 = P ↔ ∃! a ∈ ℕ ∃ b ∈ ℕ a < b ∧ a 2 + b 2 = P ∧ ∃! b ∈ ℕ ∃ a ∈ ℕ a < b ∧ a 2 + b 2 = P
20 2 19 sylibr ⊢ P ∈ ℙ ∧ P mod 4 = 1 → ∃! p ∈ ℕ × ℕ 1 st ⁡ p < 2 nd ⁡ p ∧ 1 st ⁡ p 2 + 2 nd ⁡ p 2 = P