Metamath Proof Explorer

Theorem 2sqlem11

Description: Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015)

Ref Expression
Hypotheses 2sq.1 
|- S = ran ( w e. Z[i] |-> ( ( abs ` w ) ^ 2 ) )
2sqlem7.2 
|- Y = { z | E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) }
Assertion 2sqlem11 
|- ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> P e. S )

Proof

Step Hyp Ref Expression
1 2sq.1 
 |-  S = ran ( w e. Z[i] |-> ( ( abs ` w ) ^ 2 ) )
2 2sqlem7.2 
 |-  Y = { z | E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) }
3 simpr 
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> ( P mod 4 ) = 1 )
4 simpl 
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> P e. Prime )
5 1ne2 
 |-  1 =/= 2
6 5 necomi 
 |-  2 =/= 1
7 oveq1 
 |-  ( P = 2 -> ( P mod 4 ) = ( 2 mod 4 ) )
8 2re 
 |-  2 e. RR
9 4re 
 |-  4 e. RR
10 4pos 
 |-  0 < 4
11 9 10 elrpii 
 |-  4 e. RR+
12 0le2 
 |-  0 <_ 2
13 2lt4 
 |-  2 < 4
14 modid 
 |-  ( ( ( 2 e. RR /\ 4 e. RR+ ) /\ ( 0 <_ 2 /\ 2 < 4 ) ) -> ( 2 mod 4 ) = 2 )
15 8 11 12 13 14 mp4an 
 |-  ( 2 mod 4 ) = 2
16 7 15 eqtrdi 
 |-  ( P = 2 -> ( P mod 4 ) = 2 )
17 16 neeq1d 
 |-  ( P = 2 -> ( ( P mod 4 ) =/= 1 <-> 2 =/= 1 ) )
18 6 17 mpbiri 
 |-  ( P = 2 -> ( P mod 4 ) =/= 1 )
19 18 necon2i 
 |-  ( ( P mod 4 ) = 1 -> P =/= 2 )
20 3 19 syl 
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> P =/= 2 )
21 eldifsn 
 |-  ( P e. ( Prime \ { 2 } ) <-> ( P e. Prime /\ P =/= 2 ) )
22 4 20 21 sylanbrc 
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> P e. ( Prime \ { 2 } ) )
23 m1lgs 
 |-  ( P e. ( Prime \ { 2 } ) -> ( ( -u 1 /L P ) = 1 <-> ( P mod 4 ) = 1 ) )
24 22 23 syl 
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> ( ( -u 1 /L P ) = 1 <-> ( P mod 4 ) = 1 ) )
25 3 24 mpbird 
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> ( -u 1 /L P ) = 1 )
26 neg1z 
 |-  -u 1 e. ZZ
27 lgsqr 
 |-  ( ( -u 1 e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( -u 1 /L P ) = 1 <-> ( -. P || -u 1 /\ E. n e. ZZ P || ( ( n ^ 2 ) - -u 1 ) ) ) )
28 26 22 27 sylancr 
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> ( ( -u 1 /L P ) = 1 <-> ( -. P || -u 1 /\ E. n e. ZZ P || ( ( n ^ 2 ) - -u 1 ) ) ) )
29 25 28 mpbid 
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> ( -. P || -u 1 /\ E. n e. ZZ P || ( ( n ^ 2 ) - -u 1 ) ) )
30 29 simprd 
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> E. n e. ZZ P || ( ( n ^ 2 ) - -u 1 ) )
31 simprl 
 |-  ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ ( n e. ZZ /\ P || ( ( n ^ 2 ) - -u 1 ) ) ) -> n e. ZZ )
32 1zzd 
 |-  ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ ( n e. ZZ /\ P || ( ( n ^ 2 ) - -u 1 ) ) ) -> 1 e. ZZ )
33 gcd1 
 |-  ( n e. ZZ -> ( n gcd 1 ) = 1 )
34 33 ad2antrl 
 |-  ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ ( n e. ZZ /\ P || ( ( n ^ 2 ) - -u 1 ) ) ) -> ( n gcd 1 ) = 1 )
35 eqidd 
 |-  ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ ( n e. ZZ /\ P || ( ( n ^ 2 ) - -u 1 ) ) ) -> ( ( n ^ 2 ) + 1 ) = ( ( n ^ 2 ) + 1 ) )
36 oveq1 
 |-  ( x = n -> ( x gcd y ) = ( n gcd y ) )
37 36 eqeq1d 
 |-  ( x = n -> ( ( x gcd y ) = 1 <-> ( n gcd y ) = 1 ) )
38 oveq1 
 |-  ( x = n -> ( x ^ 2 ) = ( n ^ 2 ) )
39 38 oveq1d 
 |-  ( x = n -> ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( ( n ^ 2 ) + ( y ^ 2 ) ) )
40 39 eqeq2d 
 |-  ( x = n -> ( ( ( n ^ 2 ) + 1 ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) <-> ( ( n ^ 2 ) + 1 ) = ( ( n ^ 2 ) + ( y ^ 2 ) ) ) )
41 37 40 anbi12d 
 |-  ( x = n -> ( ( ( x gcd y ) = 1 /\ ( ( n ^ 2 ) + 1 ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) <-> ( ( n gcd y ) = 1 /\ ( ( n ^ 2 ) + 1 ) = ( ( n ^ 2 ) + ( y ^ 2 ) ) ) ) )
42 oveq2 
 |-  ( y = 1 -> ( n gcd y ) = ( n gcd 1 ) )
43 42 eqeq1d 
 |-  ( y = 1 -> ( ( n gcd y ) = 1 <-> ( n gcd 1 ) = 1 ) )
44 oveq1 
 |-  ( y = 1 -> ( y ^ 2 ) = ( 1 ^ 2 ) )
45 sq1 
 |-  ( 1 ^ 2 ) = 1
46 44 45 eqtrdi 
 |-  ( y = 1 -> ( y ^ 2 ) = 1 )
47 46 oveq2d 
 |-  ( y = 1 -> ( ( n ^ 2 ) + ( y ^ 2 ) ) = ( ( n ^ 2 ) + 1 ) )
48 47 eqeq2d 
 |-  ( y = 1 -> ( ( ( n ^ 2 ) + 1 ) = ( ( n ^ 2 ) + ( y ^ 2 ) ) <-> ( ( n ^ 2 ) + 1 ) = ( ( n ^ 2 ) + 1 ) ) )
49 43 48 anbi12d 
 |-  ( y = 1 -> ( ( ( n gcd y ) = 1 /\ ( ( n ^ 2 ) + 1 ) = ( ( n ^ 2 ) + ( y ^ 2 ) ) ) <-> ( ( n gcd 1 ) = 1 /\ ( ( n ^ 2 ) + 1 ) = ( ( n ^ 2 ) + 1 ) ) ) )
50 41 49 rspc2ev 
 |-  ( ( n e. ZZ /\ 1 e. ZZ /\ ( ( n gcd 1 ) = 1 /\ ( ( n ^ 2 ) + 1 ) = ( ( n ^ 2 ) + 1 ) ) ) -> E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ ( ( n ^ 2 ) + 1 ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
51 31 32 34 35 50 syl112anc 
 |-  ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ ( n e. ZZ /\ P || ( ( n ^ 2 ) - -u 1 ) ) ) -> E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ ( ( n ^ 2 ) + 1 ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
52 ovex 
 |-  ( ( n ^ 2 ) + 1 ) e. _V
53 eqeq1 
 |-  ( z = ( ( n ^ 2 ) + 1 ) -> ( z = ( ( x ^ 2 ) + ( y ^ 2 ) ) <-> ( ( n ^ 2 ) + 1 ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
54 53 anbi2d 
 |-  ( z = ( ( n ^ 2 ) + 1 ) -> ( ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) <-> ( ( x gcd y ) = 1 /\ ( ( n ^ 2 ) + 1 ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
55 54 2rexbidv 
 |-  ( z = ( ( n ^ 2 ) + 1 ) -> ( E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) <-> E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ ( ( n ^ 2 ) + 1 ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
56 52 55 2 elab2 
 |-  ( ( ( n ^ 2 ) + 1 ) e. Y <-> E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ ( ( n ^ 2 ) + 1 ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
57 51 56 sylibr 
 |-  ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ ( n e. ZZ /\ P || ( ( n ^ 2 ) - -u 1 ) ) ) -> ( ( n ^ 2 ) + 1 ) e. Y )
58 prmnn 
 |-  ( P e. Prime -> P e. NN )
59 58 ad2antrr 
 |-  ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ ( n e. ZZ /\ P || ( ( n ^ 2 ) - -u 1 ) ) ) -> P e. NN )
60 simprr 
 |-  ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ ( n e. ZZ /\ P || ( ( n ^ 2 ) - -u 1 ) ) ) -> P || ( ( n ^ 2 ) - -u 1 ) )
61 31 zcnd 
 |-  ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ ( n e. ZZ /\ P || ( ( n ^ 2 ) - -u 1 ) ) ) -> n e. CC )
62 61 sqcld 
 |-  ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ ( n e. ZZ /\ P || ( ( n ^ 2 ) - -u 1 ) ) ) -> ( n ^ 2 ) e. CC )
63 ax-1cn 
 |-  1 e. CC
64 subneg 
 |-  ( ( ( n ^ 2 ) e. CC /\ 1 e. CC ) -> ( ( n ^ 2 ) - -u 1 ) = ( ( n ^ 2 ) + 1 ) )
65 62 63 64 sylancl 
 |-  ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ ( n e. ZZ /\ P || ( ( n ^ 2 ) - -u 1 ) ) ) -> ( ( n ^ 2 ) - -u 1 ) = ( ( n ^ 2 ) + 1 ) )
66 60 65 breqtrd 
 |-  ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ ( n e. ZZ /\ P || ( ( n ^ 2 ) - -u 1 ) ) ) -> P || ( ( n ^ 2 ) + 1 ) )
67 1 2 2sqlem10 
 |-  ( ( ( ( n ^ 2 ) + 1 ) e. Y /\ P e. NN /\ P || ( ( n ^ 2 ) + 1 ) ) -> P e. S )
68 57 59 66 67 syl3anc 
 |-  ( ( ( P e. Prime /\ ( P mod 4 ) = 1 ) /\ ( n e. ZZ /\ P || ( ( n ^ 2 ) - -u 1 ) ) ) -> P e. S )
69 30 68 rexlimddv 
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 1 ) -> P e. S )