Theorem 2sqreultb

Description: There exists a unique decomposition of a prime as a sum of squares of two different nonnegative integers iff P == 1 (mod 4). (Contributed by AV, 10-Jun-2023) The prime needs not be odd, as observed by WL. (Revised by AV, 25-Jun-2023)

	Ref	Expression
Hypothesis	2sqreult.1	|- ( ph <-> ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )
Assertion	2sqreultb	|- ( P e. Prime -> ( ( P mod 4 ) = 1 <-> ( E! a e. NN0 E. b e. NN0 ph /\ E! b e. NN0 E. a e. NN0 ph ) ) )

Proof

Step	Hyp	Ref	Expression
1		2sqreult.1	|- ( ph <-> ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )
2		2sqreultblem	|- ( P e. Prime -> ( ( P mod 4 ) = 1 <-> E! a e. NN0 E! b e. NN0 ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) )
3	1	bicomi	|- ( ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) <-> ph )
4	3	reubii	|- ( E! b e. NN0 ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) <-> E! b e. NN0 ph )
5	4	reubii	|- ( E! a e. NN0 E! b e. NN0 ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) <-> E! a e. NN0 E! b e. NN0 ph )
6	5	a1i	|- ( P e. Prime -> ( E! a e. NN0 E! b e. NN0 ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) <-> E! a e. NN0 E! b e. NN0 ph ) )
7	1	2sqreulem4	|- A. a e. NN0 E* b e. NN0 ph
8		2reu1	|- ( A. a e. NN0 E* b e. NN0 ph -> ( E! a e. NN0 E! b e. NN0 ph <-> ( E! a e. NN0 E. b e. NN0 ph /\ E! b e. NN0 E. a e. NN0 ph ) ) )
9	7 8	mp1i	|- ( P e. Prime -> ( E! a e. NN0 E! b e. NN0 ph <-> ( E! a e. NN0 E. b e. NN0 ph /\ E! b e. NN0 E. a e. NN0 ph ) ) )
10	2 6 9	3bitrd	|- ( P e. Prime -> ( ( P mod 4 ) = 1 <-> ( E! a e. NN0 E. b e. NN0 ph /\ E! b e. NN0 E. a e. NN0 ph ) ) )