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 syl6bi
 |-  ( ( a = 1 /\ b = 1 ) -> ( a < b -> ( P mod 4 ) = 1 ) )
14 8 13 syl6bi
 |-  ( ( 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 ) ) )