Metamath Proof Explorer


Theorem 2sqreuopnnltb

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

Ref Expression
Assertion 2sqreuopnnltb 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 2sqreunnltb 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 bitr4di P P mod 4 = 1 ∃! p × 1 st p < 2 nd p 1 st p 2 + 2 nd p 2 = P