Metamath Proof Explorer

Theorem 2lgsoddprm

Description: The second supplement to the law of quadratic reciprocity for odd primes (common representation, see theorem 9.5 in ApostolNT p. 181): The Legendre symbol for 2 at an odd prime is minus one to the power of the square of the odd prime minus one divided by eight ( ( 2 /L P ) = -1^(((P^2)-1)/8) ). (Contributed by AV, 20-Jul-2021)

Ref Expression
Assertion 2lgsoddprm 
|- ( P e. ( Prime \ { 2 } ) -> ( 2 /L P ) = ( -u 1 ^ ( ( ( P ^ 2 ) - 1 ) / 8 ) ) )

Proof

Step Hyp Ref Expression
1 eldifi 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. Prime )
2 2lgs 
 |-  ( P e. Prime -> ( ( 2 /L P ) = 1 <-> ( P mod 8 ) e. { 1 , 7 } ) )
3 1 2 syl 
 |-  ( P e. ( Prime \ { 2 } ) -> ( ( 2 /L P ) = 1 <-> ( P mod 8 ) e. { 1 , 7 } ) )
4 simpl 
 |-  ( ( ( 2 /L P ) = 1 /\ ( ( P mod 8 ) e. { 1 , 7 } /\ P e. ( Prime \ { 2 } ) ) ) -> ( 2 /L P ) = 1 )
5 eqcom 
 |-  ( 1 = ( -u 1 ^ ( ( ( P ^ 2 ) - 1 ) / 8 ) ) <-> ( -u 1 ^ ( ( ( P ^ 2 ) - 1 ) / 8 ) ) = 1 )
6 5 a1i 
 |-  ( P e. ( Prime \ { 2 } ) -> ( 1 = ( -u 1 ^ ( ( ( P ^ 2 ) - 1 ) / 8 ) ) <-> ( -u 1 ^ ( ( ( P ^ 2 ) - 1 ) / 8 ) ) = 1 ) )
7 nnoddn2prm 
 |-  ( P e. ( Prime \ { 2 } ) -> ( P e. NN /\ -. 2 || P ) )
8 nnz 
 |-  ( P e. NN -> P e. ZZ )
9 8 anim1i 
 |-  ( ( P e. NN /\ -. 2 || P ) -> ( P e. ZZ /\ -. 2 || P ) )
10 7 9 syl 
 |-  ( P e. ( Prime \ { 2 } ) -> ( P e. ZZ /\ -. 2 || P ) )
11 sqoddm1div8z 
 |-  ( ( P e. ZZ /\ -. 2 || P ) -> ( ( ( P ^ 2 ) - 1 ) / 8 ) e. ZZ )
12 10 11 syl 
 |-  ( P e. ( Prime \ { 2 } ) -> ( ( ( P ^ 2 ) - 1 ) / 8 ) e. ZZ )
13 m1exp1 
 |-  ( ( ( ( P ^ 2 ) - 1 ) / 8 ) e. ZZ -> ( ( -u 1 ^ ( ( ( P ^ 2 ) - 1 ) / 8 ) ) = 1 <-> 2 || ( ( ( P ^ 2 ) - 1 ) / 8 ) ) )
14 12 13 syl 
 |-  ( P e. ( Prime \ { 2 } ) -> ( ( -u 1 ^ ( ( ( P ^ 2 ) - 1 ) / 8 ) ) = 1 <-> 2 || ( ( ( P ^ 2 ) - 1 ) / 8 ) ) )
15 2lgsoddprmlem4 
 |-  ( ( P e. ZZ /\ -. 2 || P ) -> ( 2 || ( ( ( P ^ 2 ) - 1 ) / 8 ) <-> ( P mod 8 ) e. { 1 , 7 } ) )
16 10 15 syl 
 |-  ( P e. ( Prime \ { 2 } ) -> ( 2 || ( ( ( P ^ 2 ) - 1 ) / 8 ) <-> ( P mod 8 ) e. { 1 , 7 } ) )
17 6 14 16 3bitrd 
 |-  ( P e. ( Prime \ { 2 } ) -> ( 1 = ( -u 1 ^ ( ( ( P ^ 2 ) - 1 ) / 8 ) ) <-> ( P mod 8 ) e. { 1 , 7 } ) )
18 17 biimparc 
 |-  ( ( ( P mod 8 ) e. { 1 , 7 } /\ P e. ( Prime \ { 2 } ) ) -> 1 = ( -u 1 ^ ( ( ( P ^ 2 ) - 1 ) / 8 ) ) )
19 18 adantl 
 |-  ( ( ( 2 /L P ) = 1 /\ ( ( P mod 8 ) e. { 1 , 7 } /\ P e. ( Prime \ { 2 } ) ) ) -> 1 = ( -u 1 ^ ( ( ( P ^ 2 ) - 1 ) / 8 ) ) )
20 4 19 eqtrd 
 |-  ( ( ( 2 /L P ) = 1 /\ ( ( P mod 8 ) e. { 1 , 7 } /\ P e. ( Prime \ { 2 } ) ) ) -> ( 2 /L P ) = ( -u 1 ^ ( ( ( P ^ 2 ) - 1 ) / 8 ) ) )
21 20 exp32 
 |-  ( ( 2 /L P ) = 1 -> ( ( P mod 8 ) e. { 1 , 7 } -> ( P e. ( Prime \ { 2 } ) -> ( 2 /L P ) = ( -u 1 ^ ( ( ( P ^ 2 ) - 1 ) / 8 ) ) ) ) )
22 2z 
 |-  2 e. ZZ
23 prmz 
 |-  ( P e. Prime -> P e. ZZ )
24 1 23 syl 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. ZZ )
25 lgscl1 
 |-  ( ( 2 e. ZZ /\ P e. ZZ ) -> ( 2 /L P ) e. { -u 1 , 0 , 1 } )
26 22 24 25 sylancr 
 |-  ( P e. ( Prime \ { 2 } ) -> ( 2 /L P ) e. { -u 1 , 0 , 1 } )
27 ovex 
 |-  ( 2 /L P ) e. _V
28 27 eltp 
 |-  ( ( 2 /L P ) e. { -u 1 , 0 , 1 } <-> ( ( 2 /L P ) = -u 1 \/ ( 2 /L P ) = 0 \/ ( 2 /L P ) = 1 ) )
29 simpl 
 |-  ( ( ( 2 /L P ) = -u 1 /\ ( P e. ( Prime \ { 2 } ) /\ -. ( P mod 8 ) e. { 1 , 7 } ) ) -> ( 2 /L P ) = -u 1 )
30 16 notbid 
 |-  ( P e. ( Prime \ { 2 } ) -> ( -. 2 || ( ( ( P ^ 2 ) - 1 ) / 8 ) <-> -. ( P mod 8 ) e. { 1 , 7 } ) )
31 30 biimpar 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ -. ( P mod 8 ) e. { 1 , 7 } ) -> -. 2 || ( ( ( P ^ 2 ) - 1 ) / 8 ) )
32 m1expo 
 |-  ( ( ( ( ( P ^ 2 ) - 1 ) / 8 ) e. ZZ /\ -. 2 || ( ( ( P ^ 2 ) - 1 ) / 8 ) ) -> ( -u 1 ^ ( ( ( P ^ 2 ) - 1 ) / 8 ) ) = -u 1 )
33 12 31 32 syl2an2r 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ -. ( P mod 8 ) e. { 1 , 7 } ) -> ( -u 1 ^ ( ( ( P ^ 2 ) - 1 ) / 8 ) ) = -u 1 )
34 33 eqcomd 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ -. ( P mod 8 ) e. { 1 , 7 } ) -> -u 1 = ( -u 1 ^ ( ( ( P ^ 2 ) - 1 ) / 8 ) ) )
35 34 adantl 
 |-  ( ( ( 2 /L P ) = -u 1 /\ ( P e. ( Prime \ { 2 } ) /\ -. ( P mod 8 ) e. { 1 , 7 } ) ) -> -u 1 = ( -u 1 ^ ( ( ( P ^ 2 ) - 1 ) / 8 ) ) )
36 29 35 eqtrd 
 |-  ( ( ( 2 /L P ) = -u 1 /\ ( P e. ( Prime \ { 2 } ) /\ -. ( P mod 8 ) e. { 1 , 7 } ) ) -> ( 2 /L P ) = ( -u 1 ^ ( ( ( P ^ 2 ) - 1 ) / 8 ) ) )
37 36 a1d 
 |-  ( ( ( 2 /L P ) = -u 1 /\ ( P e. ( Prime \ { 2 } ) /\ -. ( P mod 8 ) e. { 1 , 7 } ) ) -> ( -. ( 2 /L P ) = 1 -> ( 2 /L P ) = ( -u 1 ^ ( ( ( P ^ 2 ) - 1 ) / 8 ) ) ) )
38 37 exp32 
 |-  ( ( 2 /L P ) = -u 1 -> ( P e. ( Prime \ { 2 } ) -> ( -. ( P mod 8 ) e. { 1 , 7 } -> ( -. ( 2 /L P ) = 1 -> ( 2 /L P ) = ( -u 1 ^ ( ( ( P ^ 2 ) - 1 ) / 8 ) ) ) ) ) )
39 eldifsn 
 |-  ( P e. ( Prime \ { 2 } ) <-> ( P e. Prime /\ P =/= 2 ) )
40 simpr 
 |-  ( ( P e. Prime /\ P =/= 2 ) -> P =/= 2 )
41 40 necomd 
 |-  ( ( P e. Prime /\ P =/= 2 ) -> 2 =/= P )
42 39 41 sylbi 
 |-  ( P e. ( Prime \ { 2 } ) -> 2 =/= P )
43 2prm 
 |-  2 e. Prime
44 prmrp 
 |-  ( ( 2 e. Prime /\ P e. Prime ) -> ( ( 2 gcd P ) = 1 <-> 2 =/= P ) )
45 43 1 44 sylancr 
 |-  ( P e. ( Prime \ { 2 } ) -> ( ( 2 gcd P ) = 1 <-> 2 =/= P ) )
46 42 45 mpbird 
 |-  ( P e. ( Prime \ { 2 } ) -> ( 2 gcd P ) = 1 )
47 lgsne0 
 |-  ( ( 2 e. ZZ /\ P e. ZZ ) -> ( ( 2 /L P ) =/= 0 <-> ( 2 gcd P ) = 1 ) )
48 22 24 47 sylancr 
 |-  ( P e. ( Prime \ { 2 } ) -> ( ( 2 /L P ) =/= 0 <-> ( 2 gcd P ) = 1 ) )
49 46 48 mpbird 
 |-  ( P e. ( Prime \ { 2 } ) -> ( 2 /L P ) =/= 0 )
50 eqneqall 
 |-  ( ( 2 /L P ) = 0 -> ( ( 2 /L P ) =/= 0 -> ( -. ( P mod 8 ) e. { 1 , 7 } -> ( -. ( 2 /L P ) = 1 -> ( 2 /L P ) = ( -u 1 ^ ( ( ( P ^ 2 ) - 1 ) / 8 ) ) ) ) ) )
51 49 50 syl5 
 |-  ( ( 2 /L P ) = 0 -> ( P e. ( Prime \ { 2 } ) -> ( -. ( P mod 8 ) e. { 1 , 7 } -> ( -. ( 2 /L P ) = 1 -> ( 2 /L P ) = ( -u 1 ^ ( ( ( P ^ 2 ) - 1 ) / 8 ) ) ) ) ) )
52 pm2.24 
 |-  ( ( 2 /L P ) = 1 -> ( -. ( 2 /L P ) = 1 -> ( 2 /L P ) = ( -u 1 ^ ( ( ( P ^ 2 ) - 1 ) / 8 ) ) ) )
53 52 2a1d 
 |-  ( ( 2 /L P ) = 1 -> ( P e. ( Prime \ { 2 } ) -> ( -. ( P mod 8 ) e. { 1 , 7 } -> ( -. ( 2 /L P ) = 1 -> ( 2 /L P ) = ( -u 1 ^ ( ( ( P ^ 2 ) - 1 ) / 8 ) ) ) ) ) )
54 38 51 53 3jaoi 
 |-  ( ( ( 2 /L P ) = -u 1 \/ ( 2 /L P ) = 0 \/ ( 2 /L P ) = 1 ) -> ( P e. ( Prime \ { 2 } ) -> ( -. ( P mod 8 ) e. { 1 , 7 } -> ( -. ( 2 /L P ) = 1 -> ( 2 /L P ) = ( -u 1 ^ ( ( ( P ^ 2 ) - 1 ) / 8 ) ) ) ) ) )
55 28 54 sylbi 
 |-  ( ( 2 /L P ) e. { -u 1 , 0 , 1 } -> ( P e. ( Prime \ { 2 } ) -> ( -. ( P mod 8 ) e. { 1 , 7 } -> ( -. ( 2 /L P ) = 1 -> ( 2 /L P ) = ( -u 1 ^ ( ( ( P ^ 2 ) - 1 ) / 8 ) ) ) ) ) )
56 26 55 mpcom 
 |-  ( P e. ( Prime \ { 2 } ) -> ( -. ( P mod 8 ) e. { 1 , 7 } -> ( -. ( 2 /L P ) = 1 -> ( 2 /L P ) = ( -u 1 ^ ( ( ( P ^ 2 ) - 1 ) / 8 ) ) ) ) )
57 56 com13 
 |-  ( -. ( 2 /L P ) = 1 -> ( -. ( P mod 8 ) e. { 1 , 7 } -> ( P e. ( Prime \ { 2 } ) -> ( 2 /L P ) = ( -u 1 ^ ( ( ( P ^ 2 ) - 1 ) / 8 ) ) ) ) )
58 21 57 bija 
 |-  ( ( ( 2 /L P ) = 1 <-> ( P mod 8 ) e. { 1 , 7 } ) -> ( P e. ( Prime \ { 2 } ) -> ( 2 /L P ) = ( -u 1 ^ ( ( ( P ^ 2 ) - 1 ) / 8 ) ) ) )
59 3 58 mpcom 
 |-  ( P e. ( Prime \ { 2 } ) -> ( 2 /L P ) = ( -u 1 ^ ( ( ( P ^ 2 ) - 1 ) / 8 ) ) )