Theorem sq2reunnltb

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 . Double restricted existential uniqueness variant of 2sqreunnltb . (Contributed by AV, 5-Jul-2023)

	Ref	Expression
Assertion	sq2reunnltb	|- ( P e. Prime -> ( ( P mod 4 ) = 1 <-> E! a e. NN , b e. NN ( a < b /\ ( ( a ^ 2 ) + ( b ^ 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 e. Prime -> ( ( P mod 4 ) = 1 <-> ( E! a e. NN E. b e. NN ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) /\ E! b e. NN E. a e. NN ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) ) )
3		df-2reu	|- ( E! a e. NN , b e. NN ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) <-> ( E! a e. NN E. b e. NN ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) /\ E! b e. NN E. a e. NN ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) )
4	2 3	bitr4di	|- ( P e. Prime -> ( ( P mod 4 ) = 1 <-> E! a e. NN , b e. NN ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) )