Metamath Proof Explorer

Theorem 2sqreultblem

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

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

Proof

Step Hyp Ref Expression
1 2sqreultlem 
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> E! a e. NN0 E! b e. NN0 ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )
2 1 ex 
 |-  ( P e. Prime -> ( ( P mod 4 ) = 1 -> E! a e. NN0 E! b e. NN0 ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) )
3 2reu2rex 
 |-  ( E! a e. NN0 E! b e. NN0 ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> E. a e. NN0 E. b e. NN0 ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )
4 elsni 
 |-  ( P e. { 2 } -> P = 2 )
5 eqeq2 
 |-  ( P = 2 -> ( ( ( a ^ 2 ) + ( b ^ 2 ) ) = P <-> ( ( a ^ 2 ) + ( b ^ 2 ) ) = 2 ) )
6 5 anbi2d 
 |-  ( P = 2 -> ( ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) <-> ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = 2 ) ) )
7 6 adantl 
 |-  ( ( ( a e. NN0 /\ b e. NN0 ) /\ P = 2 ) -> ( ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) <-> ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = 2 ) ) )
8 2sq2 
 |-  ( ( a e. NN0 /\ b e. NN0 ) -> ( ( ( a ^ 2 ) + ( b ^ 2 ) ) = 2 <-> ( a = 1 /\ b = 1 ) ) )
9 breq12 
 |-  ( ( a = 1 /\ b = 1 ) -> ( a < b <-> 1 < 1 ) )
10 1re 
 |-  1 e. RR
11 10 ltnri 
 |-  -. 1 < 1
12 11 pm2.21i 
 |-  ( 1 < 1 -> ( P mod 4 ) = 1 )
13 9 12 biimtrdi 
 |-  ( ( a = 1 /\ b = 1 ) -> ( a < b -> ( P mod 4 ) = 1 ) )
14 8 13 biimtrdi 
 |-  ( ( a e. NN0 /\ b e. NN0 ) -> ( ( ( a ^ 2 ) + ( b ^ 2 ) ) = 2 -> ( a < b -> ( P mod 4 ) = 1 ) ) )
15 14 impcomd 
 |-  ( ( a e. NN0 /\ b e. NN0 ) -> ( ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = 2 ) -> ( P mod 4 ) = 1 ) )
16 15 adantr 
 |-  ( ( ( a e. NN0 /\ b e. NN0 ) /\ P = 2 ) -> ( ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = 2 ) -> ( P mod 4 ) = 1 ) )
17 7 16 sylbid 
 |-  ( ( ( a e. NN0 /\ b e. NN0 ) /\ P = 2 ) -> ( ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> ( P mod 4 ) = 1 ) )
18 17 ex 
 |-  ( ( a e. NN0 /\ b e. NN0 ) -> ( P = 2 -> ( ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> ( P mod 4 ) = 1 ) ) )
19 18 com23 
 |-  ( ( a e. NN0 /\ b e. NN0 ) -> ( ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> ( P = 2 -> ( P mod 4 ) = 1 ) ) )
20 19 rexlimivv 
 |-  ( E. a e. NN0 E. b e. NN0 ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> ( P = 2 -> ( P mod 4 ) = 1 ) )
21 3 4 20 syl2imc 
 |-  ( P e. { 2 } -> ( E! a e. NN0 E! b e. NN0 ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> ( P mod 4 ) = 1 ) )
22 21 a1d 
 |-  ( P e. { 2 } -> ( P e. Prime -> ( E! a e. NN0 E! b e. NN0 ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> ( P mod 4 ) = 1 ) ) )
23 eldif 
 |-  ( P e. ( Prime \ { 2 } ) <-> ( P e. Prime /\ -. P e. { 2 } ) )
24 eldifsnneq 
 |-  ( P e. ( Prime \ { 2 } ) -> -. P = 2 )
25 nn0ssz 
 |-  NN0 C_ ZZ
26 id 
 |-  ( ( ( a ^ 2 ) + ( b ^ 2 ) ) = P -> ( ( a ^ 2 ) + ( b ^ 2 ) ) = P )
27 26 eqcomd 
 |-  ( ( ( a ^ 2 ) + ( b ^ 2 ) ) = P -> P = ( ( a ^ 2 ) + ( b ^ 2 ) ) )
28 27 adantl 
 |-  ( ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> P = ( ( a ^ 2 ) + ( b ^ 2 ) ) )
29 28 reximi 
 |-  ( E. b e. NN0 ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> E. b e. NN0 P = ( ( a ^ 2 ) + ( b ^ 2 ) ) )
30 29 reximi 
 |-  ( E. a e. NN0 E. b e. NN0 ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> E. a e. NN0 E. b e. NN0 P = ( ( a ^ 2 ) + ( b ^ 2 ) ) )
31 ssrexv 
 |-  ( NN0 C_ ZZ -> ( E. b e. NN0 P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> E. b e. ZZ P = ( ( a ^ 2 ) + ( b ^ 2 ) ) ) )
32 25 31 ax-mp 
 |-  ( E. b e. NN0 P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> E. b e. ZZ P = ( ( a ^ 2 ) + ( b ^ 2 ) ) )
33 32 reximi 
 |-  ( E. a e. NN0 E. b e. NN0 P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> E. a e. NN0 E. b e. ZZ P = ( ( a ^ 2 ) + ( b ^ 2 ) ) )
34 3 30 33 3syl 
 |-  ( E! a e. NN0 E! b e. NN0 ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> E. a e. NN0 E. b e. ZZ P = ( ( a ^ 2 ) + ( b ^ 2 ) ) )
35 ssrexv 
 |-  ( NN0 C_ ZZ -> ( E. a e. NN0 E. b e. ZZ P = ( ( a ^ 2 ) + ( b ^ 2 ) ) -> E. a e. ZZ E. b e. ZZ P = ( ( a ^ 2 ) + ( b ^ 2 ) ) ) )
36 25 34 35 mpsyl 
 |-  ( E! a e. NN0 E! b e. NN0 ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> E. a e. ZZ E. b e. ZZ P = ( ( a ^ 2 ) + ( b ^ 2 ) ) )
37 36 adantl 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ E! a e. NN0 E! b e. NN0 ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) -> E. a e. ZZ E. b e. ZZ P = ( ( a ^ 2 ) + ( b ^ 2 ) ) )
38 eldifi 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. Prime )
39 38 adantr 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ E! a e. NN0 E! b e. NN0 ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) -> P e. Prime )
40 2sqb 
 |-  ( P e. Prime -> ( E. a e. ZZ E. b e. ZZ P = ( ( a ^ 2 ) + ( b ^ 2 ) ) <-> ( P = 2 \/ ( P mod 4 ) = 1 ) ) )
41 39 40 syl 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ E! a e. NN0 E! b e. NN0 ( 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 ) ) )
42 37 41 mpbid 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ E! a e. NN0 E! b e. NN0 ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) -> ( P = 2 \/ ( P mod 4 ) = 1 ) )
43 42 ord 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ E! a e. NN0 E! b e. NN0 ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) -> ( -. P = 2 -> ( P mod 4 ) = 1 ) )
44 43 ex 
 |-  ( P e. ( Prime \ { 2 } ) -> ( E! a e. NN0 E! b e. NN0 ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> ( -. P = 2 -> ( P mod 4 ) = 1 ) ) )
45 24 44 mpid 
 |-  ( P e. ( Prime \ { 2 } ) -> ( E! a e. NN0 E! b e. NN0 ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> ( P mod 4 ) = 1 ) )
46 23 45 sylbir 
 |-  ( ( P e. Prime /\ -. P e. { 2 } ) -> ( E! a e. NN0 E! b e. NN0 ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> ( P mod 4 ) = 1 ) )
47 46 expcom 
 |-  ( -. P e. { 2 } -> ( P e. Prime -> ( E! a e. NN0 E! b e. NN0 ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> ( P mod 4 ) = 1 ) ) )
48 22 47 pm2.61i 
 |-  ( P e. Prime -> ( E! a e. NN0 E! b e. NN0 ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) -> ( P mod 4 ) = 1 ) )
49 2 48 impbid 
 |-  ( P e. Prime -> ( ( P mod 4 ) = 1 <-> E! a e. NN0 E! b e. NN0 ( a < b /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) ) )