Metamath Proof Explorer

Theorem 2sqmo

Description: There exists at most one decomposition of a prime as a sum of two squares. See 2sqb for the existence of such a decomposition. (Contributed by Thierry Arnoux, 2-Feb-2020)

Ref Expression
Assertion 2sqmo 
|- ( P e. Prime -> E* a e. NN0 E. b e. NN0 ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )

Proof

Step Hyp Ref Expression
1 nfv 
 |-  F/ b ( ( P e. Prime /\ a e. NN0 ) /\ c e. NN0 )
2 nfre1 
 |-  F/ b E. b e. NN0 ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P )
3 1 2 nfan 
 |-  F/ b ( ( ( P e. Prime /\ a e. NN0 ) /\ c e. NN0 ) /\ E. b e. NN0 ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )
4 nfv 
 |-  F/ b d e. NN0
5 3 4 nfan 
 |-  F/ b ( ( ( ( P e. Prime /\ a e. NN0 ) /\ c e. NN0 ) /\ E. b e. NN0 ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) /\ d e. NN0 )
6 nfv 
 |-  F/ b c <_ d
7 5 6 nfan 
 |-  F/ b ( ( ( ( ( P e. Prime /\ a e. NN0 ) /\ c e. NN0 ) /\ E. b e. NN0 ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) /\ d e. NN0 ) /\ c <_ d )
8 nfv 
 |-  F/ b ( ( c ^ 2 ) + ( d ^ 2 ) ) = P
9 7 8 nfan 
 |-  F/ b ( ( ( ( ( ( P e. Prime /\ a e. NN0 ) /\ c e. NN0 ) /\ E. b e. NN0 ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) /\ d e. NN0 ) /\ c <_ d ) /\ ( ( c ^ 2 ) + ( d ^ 2 ) ) = P )
10 simp-8l 
 |-  ( ( ( ( ( ( ( ( ( P e. Prime /\ a e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ c <_ d ) /\ ( ( c ^ 2 ) + ( d ^ 2 ) ) = P ) /\ b e. NN0 ) /\ a <_ b ) /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> P e. Prime )
11 simp-8r 
 |-  ( ( ( ( ( ( ( ( ( P e. Prime /\ a e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ c <_ d ) /\ ( ( c ^ 2 ) + ( d ^ 2 ) ) = P ) /\ b e. NN0 ) /\ a <_ b ) /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> a e. NN0 )
12 simpllr 
 |-  ( ( ( ( ( ( ( ( ( P e. Prime /\ a e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ c <_ d ) /\ ( ( c ^ 2 ) + ( d ^ 2 ) ) = P ) /\ b e. NN0 ) /\ a <_ b ) /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> b e. NN0 )
13 simp-7r 
 |-  ( ( ( ( ( ( ( ( ( P e. Prime /\ a e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ c <_ d ) /\ ( ( c ^ 2 ) + ( d ^ 2 ) ) = P ) /\ b e. NN0 ) /\ a <_ b ) /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> c e. NN0 )
14 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( P e. Prime /\ a e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ c <_ d ) /\ ( ( c ^ 2 ) + ( d ^ 2 ) ) = P ) /\ b e. NN0 ) /\ a <_ b ) /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> d e. NN0 )
15 simplr 
 |-  ( ( ( ( ( ( ( ( ( P e. Prime /\ a e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ c <_ d ) /\ ( ( c ^ 2 ) + ( d ^ 2 ) ) = P ) /\ b e. NN0 ) /\ a <_ b ) /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> a <_ b )
16 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( P e. Prime /\ a e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ c <_ d ) /\ ( ( c ^ 2 ) + ( d ^ 2 ) ) = P ) /\ b e. NN0 ) /\ a <_ b ) /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> c <_ d )
17 simpr 
 |-  ( ( ( ( ( ( ( ( ( P e. Prime /\ a e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ c <_ d ) /\ ( ( c ^ 2 ) + ( d ^ 2 ) ) = P ) /\ b e. NN0 ) /\ a <_ b ) /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> ( ( a ^ 2 ) + ( b ^ 2 ) ) = P )
18 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( P e. Prime /\ a e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ c <_ d ) /\ ( ( c ^ 2 ) + ( d ^ 2 ) ) = P ) /\ b e. NN0 ) /\ a <_ b ) /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> ( ( c ^ 2 ) + ( d ^ 2 ) ) = P )
19 10 11 12 13 14 15 16 17 18 2sqmod 
 |-  ( ( ( ( ( ( ( ( ( P e. Prime /\ a e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ c <_ d ) /\ ( ( c ^ 2 ) + ( d ^ 2 ) ) = P ) /\ b e. NN0 ) /\ a <_ b ) /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> ( a = c /\ b = d ) )
20 19 simpld 
 |-  ( ( ( ( ( ( ( ( ( P e. Prime /\ a e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ c <_ d ) /\ ( ( c ^ 2 ) + ( d ^ 2 ) ) = P ) /\ b e. NN0 ) /\ a <_ b ) /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> a = c )
21 20 anasss 
 |-  ( ( ( ( ( ( ( ( P e. Prime /\ a e. NN0 ) /\ c e. NN0 ) /\ d e. NN0 ) /\ c <_ d ) /\ ( ( c ^ 2 ) + ( d ^ 2 ) ) = P ) /\ b e. NN0 ) /\ ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) -> a = c )
22 21 adantl5r 
 |-  ( ( ( ( ( ( ( ( ( P e. Prime /\ a e. NN0 ) /\ c e. NN0 ) /\ E. b e. NN0 ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) /\ d e. NN0 ) /\ c <_ d ) /\ ( ( c ^ 2 ) + ( d ^ 2 ) ) = P ) /\ b e. NN0 ) /\ ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) -> a = c )
23 simp-4r 
 |-  ( ( ( ( ( ( ( P e. Prime /\ a e. NN0 ) /\ c e. NN0 ) /\ E. b e. NN0 ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) /\ d e. NN0 ) /\ c <_ d ) /\ ( ( c ^ 2 ) + ( d ^ 2 ) ) = P ) -> E. b e. NN0 ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )
24 9 22 23 r19.29af 
 |-  ( ( ( ( ( ( ( P e. Prime /\ a e. NN0 ) /\ c e. NN0 ) /\ E. b e. NN0 ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) /\ d e. NN0 ) /\ c <_ d ) /\ ( ( c ^ 2 ) + ( d ^ 2 ) ) = P ) -> a = c )
25 24 anasss 
 |-  ( ( ( ( ( ( P e. Prime /\ a e. NN0 ) /\ c e. NN0 ) /\ E. b e. NN0 ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) /\ d e. NN0 ) /\ ( c <_ d /\ ( ( c ^ 2 ) + ( d ^ 2 ) ) = P ) ) -> a = c )
26 25 r19.29an 
 |-  ( ( ( ( ( P e. Prime /\ a e. NN0 ) /\ c e. NN0 ) /\ E. b e. NN0 ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) /\ E. d e. NN0 ( c <_ d /\ ( ( c ^ 2 ) + ( d ^ 2 ) ) = P ) ) -> a = c )
27 26 expl 
 |-  ( ( ( P e. Prime /\ a e. NN0 ) /\ c e. NN0 ) -> ( ( E. b e. NN0 ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) /\ E. d e. NN0 ( c <_ d /\ ( ( c ^ 2 ) + ( d ^ 2 ) ) = P ) ) -> a = c ) )
28 27 ralrimiva 
 |-  ( ( P e. Prime /\ a e. NN0 ) -> A. c e. NN0 ( ( E. b e. NN0 ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) /\ E. d e. NN0 ( c <_ d /\ ( ( c ^ 2 ) + ( d ^ 2 ) ) = P ) ) -> a = c ) )
29 28 ralrimiva 
 |-  ( P e. Prime -> A. a e. NN0 A. c e. NN0 ( ( E. b e. NN0 ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) /\ E. d e. NN0 ( c <_ d /\ ( ( c ^ 2 ) + ( d ^ 2 ) ) = P ) ) -> a = c ) )
30 breq12 
 |-  ( ( a = c /\ b = d ) -> ( a <_ b <-> c <_ d ) )
31 simpl 
 |-  ( ( a = c /\ b = d ) -> a = c )
32 31 oveq1d 
 |-  ( ( a = c /\ b = d ) -> ( a ^ 2 ) = ( c ^ 2 ) )
33 simpr 
 |-  ( ( a = c /\ b = d ) -> b = d )
34 33 oveq1d 
 |-  ( ( a = c /\ b = d ) -> ( b ^ 2 ) = ( d ^ 2 ) )
35 32 34 oveq12d 
 |-  ( ( a = c /\ b = d ) -> ( ( a ^ 2 ) + ( b ^ 2 ) ) = ( ( c ^ 2 ) + ( d ^ 2 ) ) )
36 35 eqeq1d 
 |-  ( ( a = c /\ b = d ) -> ( ( ( a ^ 2 ) + ( b ^ 2 ) ) = P <-> ( ( c ^ 2 ) + ( d ^ 2 ) ) = P ) )
37 30 36 anbi12d 
 |-  ( ( a = c /\ b = d ) -> ( ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) <-> ( c <_ d /\ ( ( c ^ 2 ) + ( d ^ 2 ) ) = P ) ) )
38 37 cbvrexdva 
 |-  ( a = c -> ( E. b e. NN0 ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) <-> E. d e. NN0 ( c <_ d /\ ( ( c ^ 2 ) + ( d ^ 2 ) ) = P ) ) )
39 38 rmo4 
 |-  ( E* a e. NN0 E. b e. NN0 ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) <-> A. a e. NN0 A. c e. NN0 ( ( E. b e. NN0 ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) /\ E. d e. NN0 ( c <_ d /\ ( ( c ^ 2 ) + ( d ^ 2 ) ) = P ) ) -> a = c ) )
40 29 39 sylibr 
 |-  ( P e. Prime -> E* a e. NN0 E. b e. NN0 ( a <_ b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )