Metamath Proof Explorer


Theorem 2sqreuopb

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 . Alternate ordered pair variant of 2sqreunnltb . (Contributed by AV, 3-Jul-2023)

Ref Expression
Assertion 2sqreuopb P P mod 4 = 1 ∃! p × a b p = a b a < b a 2 + b 2 = P

Proof

Step Hyp Ref Expression
1 2sqreuopnnltb P P mod 4 = 1 ∃! p × 1 st p < 2 nd p 1 st p 2 + 2 nd p 2 = P
2 breq12 a = 1 st p b = 2 nd p a < b 1 st p < 2 nd p
3 simpl a = 1 st p b = 2 nd p a = 1 st p
4 3 oveq1d a = 1 st p b = 2 nd p a 2 = 1 st p 2
5 simpr a = 1 st p b = 2 nd p b = 2 nd p
6 5 oveq1d a = 1 st p b = 2 nd p b 2 = 2 nd p 2
7 4 6 oveq12d a = 1 st p b = 2 nd p a 2 + b 2 = 1 st p 2 + 2 nd p 2
8 7 eqeq1d a = 1 st p b = 2 nd p a 2 + b 2 = P 1 st p 2 + 2 nd p 2 = P
9 2 8 anbi12d a = 1 st p b = 2 nd p a < b a 2 + b 2 = P 1 st p < 2 nd p 1 st p 2 + 2 nd p 2 = P
10 9 opreuopreu ∃! p × 1 st p < 2 nd p 1 st p 2 + 2 nd p 2 = P ∃! p × a b p = a b a < b a 2 + b 2 = P
11 1 10 bitrdi P P mod 4 = 1 ∃! p × a b p = a b a < b a 2 + b 2 = P