Metamath Proof Explorer

Theorem 2sqreunnltblem

Description: Lemma for 2sqreunnltb . (Contributed by AV, 11-Jun-2023) The prime needs not be odd, as observed by WL. (Revised by AV, 18-Jun-2023)

Ref Expression
Assertion 2sqreunnltblem 
|- ( P e. Prime -> ( ( P mod 4 ) = 1 <-> E! a e. NN E! b e. NN ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) )

Proof

Step Hyp Ref Expression
1 2sqreunnltlem 
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> E! a e. NN E! b e. NN ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )
2 1 ex 
 |-  ( P e. Prime -> ( ( P mod 4 ) = 1 -> E! a e. NN E! b e. NN ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) )
3 2reu2rex 
 |-  ( E! a e. NN E! b e. NN ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> E. a e. NN E. b e. NN ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )
4 eqeq2 
 |-  ( P = 2 -> ( ( ( a ^ 2 ) + ( b ^ 2 ) ) = P <-> ( ( a ^ 2 ) + ( b ^ 2 ) ) = 2 ) )
5 4 adantr 
 |-  ( ( P = 2 /\ ( a e. NN /\ b e. NN ) ) -> ( ( ( a ^ 2 ) + ( b ^ 2 ) ) = P <-> ( ( a ^ 2 ) + ( b ^ 2 ) ) = 2 ) )
6 nnnn0 
 |-  ( a e. NN -> a e. NN0 )
7 nnnn0 
 |-  ( b e. NN -> b e. NN0 )
8 2sq2 
 |-  ( ( a e. NN0 /\ b e. NN0 ) -> ( ( ( a ^ 2 ) + ( b ^ 2 ) ) = 2 <-> ( a = 1 /\ b = 1 ) ) )
9 6 7 8 syl2an 
 |-  ( ( a e. NN /\ b e. NN ) -> ( ( ( a ^ 2 ) + ( b ^ 2 ) ) = 2 <-> ( a = 1 /\ b = 1 ) ) )
10 breq12 
 |-  ( ( a = 1 /\ b = 1 ) -> ( a < b <-> 1 < 1 ) )
11 1re 
 |-  1 e. RR
12 11 ltnri 
 |-  -. 1 < 1
13 12 pm2.21i 
 |-  ( 1 < 1 -> ( P mod 4 ) = 1 )
14 10 13 syl6bi 
 |-  ( ( a = 1 /\ b = 1 ) -> ( a < b -> ( P mod 4 ) = 1 ) )
15 9 14 syl6bi 
 |-  ( ( a e. NN /\ b e. NN ) -> ( ( ( a ^ 2 ) + ( b ^ 2 ) ) = 2 -> ( a < b -> ( P mod 4 ) = 1 ) ) )
16 15 adantl 
 |-  ( ( P = 2 /\ ( a e. NN /\ b e. NN ) ) -> ( ( ( a ^ 2 ) + ( b ^ 2 ) ) = 2 -> ( a < b -> ( P mod 4 ) = 1 ) ) )
17 5 16 sylbid 
 |-  ( ( P = 2 /\ ( a e. NN /\ b e. NN ) ) -> ( ( ( a ^ 2 ) + ( b ^ 2 ) ) = P -> ( a < b -> ( P mod 4 ) = 1 ) ) )
18 17 impcomd 
 |-  ( ( P = 2 /\ ( a e. NN /\ b e. NN ) ) -> ( ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> ( P mod 4 ) = 1 ) )
19 18 rexlimdvva 
 |-  ( P = 2 -> ( E. a e. NN E. b e. NN ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> ( P mod 4 ) = 1 ) )
20 3 19 syl5 
 |-  ( P = 2 -> ( E! a e. NN E! b e. NN ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> ( P mod 4 ) = 1 ) )
21 20 a1d 
 |-  ( P = 2 -> ( P e. Prime -> ( E! a e. NN E! b e. NN ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> ( P mod 4 ) = 1 ) ) )
22 nnssz 
 |-  NN C_ ZZ
23 id 
 |-  ( ( ( a ^ 2 ) + ( b ^ 2 ) ) = P -> ( ( a ^ 2 ) + ( b ^ 2 ) ) = P )
24 23 eqcomd 
 |-  ( ( ( a ^ 2 ) + ( b ^ 2 ) ) = P -> P = ( ( a ^ 2 ) + ( b ^ 2 ) ) )
25 24 adantl 
 |-  ( ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> P = ( ( a ^ 2 ) + ( b ^ 2 ) ) )
26 25 reximi 
 |-  ( E. b e. NN ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> E. b e. NN P = ( ( a ^ 2 ) + ( b ^ 2 ) ) )
27 26 reximi 
 |-  ( E. a e. NN E. b e. NN ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> E. a e. NN E. b e. NN P = ( ( a ^ 2 ) + ( b ^ 2 ) ) )
28 ssrexv 
 |-  ( NN C_ ZZ -> ( E. b e. NN P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> E. b e. ZZ P = ( ( a ^ 2 ) + ( b ^ 2 ) ) ) )
29 22 28 ax-mp 
 |-  ( E. b e. NN P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> E. b e. ZZ P = ( ( a ^ 2 ) + ( b ^ 2 ) ) )
30 29 reximi 
 |-  ( E. a e. NN E. b e. NN P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> E. a e. NN E. b e. ZZ P = ( ( a ^ 2 ) + ( b ^ 2 ) ) )
31 3 27 30 3syl 
 |-  ( E! a e. NN E! b e. NN ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> E. a e. NN E. b e. ZZ P = ( ( a ^ 2 ) + ( b ^ 2 ) ) )
32 ssrexv 
 |-  ( NN C_ ZZ -> ( E. a e. NN E. b e. ZZ P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> E. a e. ZZ E. b e. ZZ P = ( ( a ^ 2 ) + ( b ^ 2 ) ) ) )
33 22 31 32 mpsyl 
 |-  ( E! a e. NN E! b e. NN ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> E. a e. ZZ E. b e. ZZ P = ( ( a ^ 2 ) + ( b ^ 2 ) ) )
34 33 adantl 
 |-  ( ( P e. Prime /\ E! a e. NN E! b e. NN ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) -> E. a e. ZZ E. b e. ZZ P = ( ( a ^ 2 ) + ( b ^ 2 ) ) )
35 2sqb 
 |-  ( P e. Prime -> ( E. a e. ZZ E. b e. ZZ P = ( ( a ^ 2 ) + ( b ^ 2 ) ) <-> ( P = 2 \/ ( P mod 4 ) = 1 ) ) )
36 35 adantr 
 |-  ( ( P e. Prime /\ E! a e. NN E! b e. NN ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) -> ( E. a e. ZZ E. b e. ZZ P = ( ( a ^ 2 ) + ( b ^ 2 ) ) <-> ( P = 2 \/ ( P mod 4 ) = 1 ) ) )
37 34 36 mpbid 
 |-  ( ( P e. Prime /\ E! a e. NN E! b e. NN ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) -> ( P = 2 \/ ( P mod 4 ) = 1 ) )
38 37 ord 
 |-  ( ( P e. Prime /\ E! a e. NN E! b e. NN ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) -> ( -. P = 2 -> ( P mod 4 ) = 1 ) )
39 38 expcom 
 |-  ( E! a e. NN E! b e. NN ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> ( P e. Prime -> ( -. P = 2 -> ( P mod 4 ) = 1 ) ) )
40 39 com13 
 |-  ( -. P = 2 -> ( P e. Prime -> ( E! a e. NN E! b e. NN ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> ( P mod 4 ) = 1 ) ) )
41 21 40 pm2.61i 
 |-  ( P e. Prime -> ( E! a e. NN E! b e. NN ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> ( P mod 4 ) = 1 ) )
42 2 41 impbid 
 |-  ( P e. Prime -> ( ( P mod 4 ) = 1 <-> E! a e. NN E! b e. NN ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) )