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 e. Prime -> ( ( P mod 4 ) = 1 <-> E! p e. ( NN X. NN ) E. a E. b ( p = <. a , b >. /\ ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		2sqreuopnnltb	|- ( P e. Prime -> ( ( P mod 4 ) = 1 <-> E! p e. ( NN X. NN ) ( ( 1st ` p ) < ( 2nd ` p ) /\ ( ( ( 1st ` p ) ^ 2 ) + ( ( 2nd ` p ) ^ 2 ) ) = P ) ) )
2		breq12	|- ( ( a = ( 1st ` p ) /\ b = ( 2nd ` p ) ) -> ( a < b <-> ( 1st ` p ) < ( 2nd ` p ) ) )
3		simpl	|- ( ( a = ( 1st ` p ) /\ b = ( 2nd ` p ) ) -> a = ( 1st ` p ) )
4	3	oveq1d	|- ( ( a = ( 1st ` p ) /\ b = ( 2nd ` p ) ) -> ( a ^ 2 ) = ( ( 1st ` p ) ^ 2 ) )
5		simpr	|- ( ( a = ( 1st ` p ) /\ b = ( 2nd ` p ) ) -> b = ( 2nd ` p ) )
6	5	oveq1d	|- ( ( a = ( 1st ` p ) /\ b = ( 2nd ` p ) ) -> ( b ^ 2 ) = ( ( 2nd ` p ) ^ 2 ) )
7	4 6	oveq12d	|- ( ( a = ( 1st ` p ) /\ b = ( 2nd ` p ) ) -> ( ( a ^ 2 ) + ( b ^ 2 ) ) = ( ( ( 1st ` p ) ^ 2 ) + ( ( 2nd ` p ) ^ 2 ) ) )
8	7	eqeq1d	|- ( ( a = ( 1st ` p ) /\ b = ( 2nd ` p ) ) -> ( ( ( a ^ 2 ) + ( b ^ 2 ) ) = P <-> ( ( ( 1st ` p ) ^ 2 ) + ( ( 2nd ` p ) ^ 2 ) ) = P ) )
9	2 8	anbi12d	|- ( ( a = ( 1st ` p ) /\ b = ( 2nd ` p ) ) -> ( ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) <-> ( ( 1st ` p ) < ( 2nd ` p ) /\ ( ( ( 1st ` p ) ^ 2 ) + ( ( 2nd ` p ) ^ 2 ) ) = P ) ) )
10	9	opreuopreu	|- ( E! p e. ( NN X. NN ) ( ( 1st ` p ) < ( 2nd ` p ) /\ ( ( ( 1st ` p ) ^ 2 ) + ( ( 2nd ` p ) ^ 2 ) ) = P ) <-> E! p e. ( NN X. NN ) E. a E. b ( p = <. a , b >. /\ ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) )
11	1 10	bitrdi	|- ( P e. Prime -> ( ( P mod 4 ) = 1 <-> E! p e. ( NN X. NN ) E. a E. b ( p = <. a , b >. /\ ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) ) )