Metamath Proof Explorer


Theorem 2sqreunnltb

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 . (Contributed by AV, 11-Jun-2023) The prime needs not be odd, as observed by WL. (Revised by AV, 25-Jun-2023)

Ref Expression
Hypothesis 2sqreult.1 φ a < b a 2 + b 2 = P
Assertion 2sqreunnltb P P mod 4 = 1 ∃! a b φ ∃! b a φ

Proof

Step Hyp Ref Expression
1 2sqreult.1 φ a < b a 2 + b 2 = P
2 2sqreunnltblem P P mod 4 = 1 ∃! a ∃! b a < b a 2 + b 2 = P
3 1 bicomi a < b a 2 + b 2 = P φ
4 3 reubii ∃! b a < b a 2 + b 2 = P ∃! b φ
5 4 reubii ∃! a ∃! b a < b a 2 + b 2 = P ∃! a ∃! b φ
6 1 2sqreunnlem2 a * b φ
7 2reu1 a * b φ ∃! a ∃! b φ ∃! a b φ ∃! b a φ
8 6 7 ax-mp ∃! a ∃! b φ ∃! a b φ ∃! b a φ
9 5 8 bitri ∃! a ∃! b a < b a 2 + b 2 = P ∃! a b φ ∃! b a φ
10 2 9 bitrdi P P mod 4 = 1 ∃! a b φ ∃! b a φ