# 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 syl6bb
` |-  ( 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 ) )`