Theorem 2sqreuopnnlt

Description: There exists a unique decomposition of a prime of the form 4 k + 1 as a sum of squares of two different positive integers. Ordered pair variant of 2sqreunnlt . (Contributed by AV, 3-Jul-2023)

	Ref	Expression
Assertion	2sqreuopnnlt	|- ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> E! p e. ( NN X. NN ) ( ( 1st ` p ) < ( 2nd ` p ) /\ ( ( ( 1st ` p ) ^ 2 ) + ( ( 2nd ` p ) ^ 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	2sqreunnlt	|- ( ( 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		fveq2	|- ( p = <. a , b >. -> ( 1st ` p ) = ( 1st ` <. a , b >. ) )
4		fveq2	|- ( p = <. a , b >. -> ( 2nd ` p ) = ( 2nd ` <. a , b >. ) )
5	3 4	breq12d	|- ( p = <. a , b >. -> ( ( 1st ` p ) < ( 2nd ` p ) <-> ( 1st ` <. a , b >. ) < ( 2nd ` <. a , b >. ) ) )
6		vex	|- a e. _V
7		vex	|- b e. _V
8	6 7	op1st	|- ( 1st ` <. a , b >. ) = a
9	6 7	op2nd	|- ( 2nd ` <. a , b >. ) = b
10	8 9	breq12i	|- ( ( 1st ` <. a , b >. ) < ( 2nd ` <. a , b >. ) <-> a < b )
11	5 10	bitrdi	|- ( p = <. a , b >. -> ( ( 1st ` p ) < ( 2nd ` p ) <-> a < b ) )
12	6 7	op1std	|- ( p = <. a , b >. -> ( 1st ` p ) = a )
13	12	oveq1d	|- ( p = <. a , b >. -> ( ( 1st ` p ) ^ 2 ) = ( a ^ 2 ) )
14	6 7	op2ndd	|- ( p = <. a , b >. -> ( 2nd ` p ) = b )
15	14	oveq1d	|- ( p = <. a , b >. -> ( ( 2nd ` p ) ^ 2 ) = ( b ^ 2 ) )
16	13 15	oveq12d	|- ( p = <. a , b >. -> ( ( ( 1st ` p ) ^ 2 ) + ( ( 2nd ` p ) ^ 2 ) ) = ( ( a ^ 2 ) + ( b ^ 2 ) ) )
17	16	eqeq1d	|- ( p = <. a , b >. -> ( ( ( ( 1st ` p ) ^ 2 ) + ( ( 2nd ` p ) ^ 2 ) ) = P <-> ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )
18	11 17	anbi12d	|- ( p = <. a , b >. -> ( ( ( 1st ` p ) < ( 2nd ` p ) /\ ( ( ( 1st ` p ) ^ 2 ) + ( ( 2nd ` p ) ^ 2 ) ) = P ) <-> ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) )
19	18	opreu2reurex	|- ( E! p e. ( NN X. NN ) ( ( 1st ` p ) < ( 2nd ` p ) /\ ( ( ( 1st ` p ) ^ 2 ) + ( ( 2nd ` p ) ^ 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 ) ) )
20	2 19	sylibr	|- ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> E! p e. ( NN X. NN ) ( ( 1st ` p ) < ( 2nd ` p ) /\ ( ( ( 1st ` p ) ^ 2 ) + ( ( 2nd ` p ) ^ 2 ) ) = P ) )