Metamath Proof Explorer


Theorem 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 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 2sqreunn 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