Theorem 2sqreunn

Description: There exists a unique decomposition of a prime of the form 4 k + 1 as a sum of squares of two positive integers. See 2sqnn for the existence of such a decomposition. (Contributed by AV, 11-Jun-2023) (Revised by AV, 25-Jun-2023)

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

Proof

Step	Hyp	Ref	Expression
1		2sqreu.1	|- ( ph <-> ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )
2		2sqreunnlem1	|- ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> E! a e. NN E! b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )
3	1	bicomi	|- ( ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) <-> ph )
4	3	reubii	|- ( E! b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) <-> E! b e. NN ph )
5	4	reubii	|- ( E! a e. NN E! b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) <-> E! a e. NN E! b e. NN ph )
6	1	2sqreunnlem2	|- A. a e. NN E* b e. NN ph
7		2reu1	|- ( A. a e. NN E* b e. NN ph -> ( E! a e. NN E! b e. NN ph <-> ( E! a e. NN E. b e. NN ph /\ E! b e. NN E. a e. NN ph ) ) )
8	6 7	mp1i	|- ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> ( E! a e. NN E! b e. NN ph <-> ( E! a e. NN E. b e. NN ph /\ E! b e. NN E. a e. NN ph ) ) )
9	5 8	syl5bb	|- ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> ( E! a e. NN E! b e. NN ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) <-> ( E! a e. NN E. b e. NN ph /\ E! b e. NN E. a e. NN ph ) ) )
10	2 9	mpbid	|- ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> ( E! a e. NN E. b e. NN ph /\ E! b e. NN E. a e. NN ph ) )