Metamath Proof Explorer

Theorem 2sqreuop

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

Ref Expression
Assertion 2sqreuop 
|- ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> E! p e. ( NN0 X. NN0 ) ( ( 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 2sqreu 
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> ( E! a e. NN0 E. b e. NN0 ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) /\ E! b e. NN0 E. a e. NN0 ( 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. ( NN0 X. NN0 ) ( ( 1st ` p ) <_ ( 2nd ` p ) /\ ( ( ( 1st ` p ) ^ 2 ) + ( ( 2nd ` p ) ^ 2 ) ) = P ) <-> ( E! a e. NN0 E. b e. NN0 ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) /\ E! b e. NN0 E. a e. NN0 ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) )
20 2 19 sylibr 
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> E! p e. ( NN0 X. NN0 ) ( ( 1st ` p ) <_ ( 2nd ` p ) /\ ( ( ( 1st ` p ) ^ 2 ) + ( ( 2nd ` p ) ^ 2 ) ) = P ) )