Metamath Proof Explorer

Theorem 2lgs

Description: The second supplement to the law of quadratic reciprocity (for the Legendre symbol extended to arbitrary primes as second argument). Two is a square modulo a prime P iff P == +- 1 (mod 8 ), see first case of theorem 9.5 in ApostolNT p. 181. This theorem justifies our definition of ( N /L 2 ) ( lgs2 ) to some degree, by demanding that reciprocity extend to the case Q = 2 . (Proposed by Mario Carneiro, 19-Jun-2015.) (Contributed by AV, 16-Jul-2021)

Ref Expression
Assertion 2lgs 
|- ( P e. Prime -> ( ( 2 /L P ) = 1 <-> ( P mod 8 ) e. { 1 , 7 } ) )

Proof

Step Hyp Ref Expression
1 prm2orodd 
 |-  ( P e. Prime -> ( P = 2 \/ -. 2 || P ) )
2 2lgslem4 
 |-  ( ( 2 /L 2 ) = 1 <-> ( 2 mod 8 ) e. { 1 , 7 } )
3 2 a1i 
 |-  ( P = 2 -> ( ( 2 /L 2 ) = 1 <-> ( 2 mod 8 ) e. { 1 , 7 } ) )
4 oveq2 
 |-  ( P = 2 -> ( 2 /L P ) = ( 2 /L 2 ) )
5 4 eqeq1d 
 |-  ( P = 2 -> ( ( 2 /L P ) = 1 <-> ( 2 /L 2 ) = 1 ) )
6 oveq1 
 |-  ( P = 2 -> ( P mod 8 ) = ( 2 mod 8 ) )
7 6 eleq1d 
 |-  ( P = 2 -> ( ( P mod 8 ) e. { 1 , 7 } <-> ( 2 mod 8 ) e. { 1 , 7 } ) )
8 3 5 7 3bitr4d 
 |-  ( P = 2 -> ( ( 2 /L P ) = 1 <-> ( P mod 8 ) e. { 1 , 7 } ) )
9 8 a1d 
 |-  ( P = 2 -> ( P e. Prime -> ( ( 2 /L P ) = 1 <-> ( P mod 8 ) e. { 1 , 7 } ) ) )
10 2prm 
 |-  2 e. Prime
11 prmnn 
 |-  ( P e. Prime -> P e. NN )
12 dvdsprime 
 |-  ( ( 2 e. Prime /\ P e. NN ) -> ( P || 2 <-> ( P = 2 \/ P = 1 ) ) )
13 10 11 12 sylancr 
 |-  ( P e. Prime -> ( P || 2 <-> ( P = 2 \/ P = 1 ) ) )
14 z2even 
 |-  2 || 2
15 breq2 
 |-  ( P = 2 -> ( 2 || P <-> 2 || 2 ) )
16 14 15 mpbiri 
 |-  ( P = 2 -> 2 || P )
17 16 a1d 
 |-  ( P = 2 -> ( P e. Prime -> 2 || P ) )
18 eleq1 
 |-  ( P = 1 -> ( P e. Prime <-> 1 e. Prime ) )
19 1nprm 
 |-  -. 1 e. Prime
20 19 pm2.21i 
 |-  ( 1 e. Prime -> 2 || P )
21 18 20 biimtrdi 
 |-  ( P = 1 -> ( P e. Prime -> 2 || P ) )
22 17 21 jaoi 
 |-  ( ( P = 2 \/ P = 1 ) -> ( P e. Prime -> 2 || P ) )
23 22 com12 
 |-  ( P e. Prime -> ( ( P = 2 \/ P = 1 ) -> 2 || P ) )
24 13 23 sylbid 
 |-  ( P e. Prime -> ( P || 2 -> 2 || P ) )
25 24 con3dimp 
 |-  ( ( P e. Prime /\ -. 2 || P ) -> -. P || 2 )
26 2z 
 |-  2 e. ZZ
27 25 26 jctil 
 |-  ( ( P e. Prime /\ -. 2 || P ) -> ( 2 e. ZZ /\ -. P || 2 ) )
28 2lgslem1 
 |-  ( ( P e. Prime /\ -. 2 || P ) -> ( # ` { x e. ZZ | E. i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( x = ( i x. 2 ) /\ ( P / 2 ) < ( x mod P ) ) } ) = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) )
29 28 eqcomd 
 |-  ( ( P e. Prime /\ -. 2 || P ) -> ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) = ( # ` { x e. ZZ | E. i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( x = ( i x. 2 ) /\ ( P / 2 ) < ( x mod P ) ) } ) )
30 nnoddn2prmb 
 |-  ( P e. ( Prime \ { 2 } ) <-> ( P e. Prime /\ -. 2 || P ) )
31 30 biimpri 
 |-  ( ( P e. Prime /\ -. 2 || P ) -> P e. ( Prime \ { 2 } ) )
32 31 3ad2ant1 
 |-  ( ( ( P e. Prime /\ -. 2 || P ) /\ ( 2 e. ZZ /\ -. P || 2 ) /\ ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) = ( # ` { x e. ZZ | E. i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( x = ( i x. 2 ) /\ ( P / 2 ) < ( x mod P ) ) } ) ) -> P e. ( Prime \ { 2 } ) )
33 eqid 
 |-  ( ( P - 1 ) / 2 ) = ( ( P - 1 ) / 2 )
34 eqid 
 |-  ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> if ( ( y x. 2 ) < ( P / 2 ) , ( y x. 2 ) , ( P - ( y x. 2 ) ) ) ) = ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> if ( ( y x. 2 ) < ( P / 2 ) , ( y x. 2 ) , ( P - ( y x. 2 ) ) ) )
35 eqid 
 |-  ( |_ ` ( P / 4 ) ) = ( |_ ` ( P / 4 ) )
36 eqid 
 |-  ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )
37 32 33 34 35 36 gausslemma2d 
 |-  ( ( ( P e. Prime /\ -. 2 || P ) /\ ( 2 e. ZZ /\ -. P || 2 ) /\ ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) = ( # ` { x e. ZZ | E. i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( x = ( i x. 2 ) /\ ( P / 2 ) < ( x mod P ) ) } ) ) -> ( 2 /L P ) = ( -u 1 ^ ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) ) )
38 37 eqeq1d 
 |-  ( ( ( P e. Prime /\ -. 2 || P ) /\ ( 2 e. ZZ /\ -. P || 2 ) /\ ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) = ( # ` { x e. ZZ | E. i e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( x = ( i x. 2 ) /\ ( P / 2 ) < ( x mod P ) ) } ) ) -> ( ( 2 /L P ) = 1 <-> ( -u 1 ^ ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) ) = 1 ) )
39 27 29 38 mpd3an23 
 |-  ( ( P e. Prime /\ -. 2 || P ) -> ( ( 2 /L P ) = 1 <-> ( -u 1 ^ ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) ) = 1 ) )
40 36 2lgslem2 
 |-  ( ( P e. Prime /\ -. 2 || P ) -> ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) e. ZZ )
41 m1exp1 
 |-  ( ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) e. ZZ -> ( ( -u 1 ^ ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) ) = 1 <-> 2 || ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) ) )
42 40 41 syl 
 |-  ( ( P e. Prime /\ -. 2 || P ) -> ( ( -u 1 ^ ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) ) = 1 <-> 2 || ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) ) )
43 2nn 
 |-  2 e. NN
44 dvdsval3 
 |-  ( ( 2 e. NN /\ ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) e. ZZ ) -> ( 2 || ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) <-> ( ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) mod 2 ) = 0 ) )
45 43 40 44 sylancr 
 |-  ( ( P e. Prime /\ -. 2 || P ) -> ( 2 || ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) <-> ( ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) mod 2 ) = 0 ) )
46 36 2lgslem3 
 |-  ( ( P e. NN /\ -. 2 || P ) -> ( ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) mod 2 ) = if ( ( P mod 8 ) e. { 1 , 7 } , 0 , 1 ) )
47 11 46 sylan 
 |-  ( ( P e. Prime /\ -. 2 || P ) -> ( ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) mod 2 ) = if ( ( P mod 8 ) e. { 1 , 7 } , 0 , 1 ) )
48 47 eqeq1d 
 |-  ( ( P e. Prime /\ -. 2 || P ) -> ( ( ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) mod 2 ) = 0 <-> if ( ( P mod 8 ) e. { 1 , 7 } , 0 , 1 ) = 0 ) )
49 ax-1 
 |-  ( ( P mod 8 ) e. { 1 , 7 } -> ( if ( ( P mod 8 ) e. { 1 , 7 } , 0 , 1 ) = 0 -> ( P mod 8 ) e. { 1 , 7 } ) )
50 iffalse 
 |-  ( -. ( P mod 8 ) e. { 1 , 7 } -> if ( ( P mod 8 ) e. { 1 , 7 } , 0 , 1 ) = 1 )
51 50 eqeq1d 
 |-  ( -. ( P mod 8 ) e. { 1 , 7 } -> ( if ( ( P mod 8 ) e. { 1 , 7 } , 0 , 1 ) = 0 <-> 1 = 0 ) )
52 ax-1ne0 
 |-  1 =/= 0
53 eqneqall 
 |-  ( 1 = 0 -> ( 1 =/= 0 -> ( P mod 8 ) e. { 1 , 7 } ) )
54 52 53 mpi 
 |-  ( 1 = 0 -> ( P mod 8 ) e. { 1 , 7 } )
55 51 54 biimtrdi 
 |-  ( -. ( P mod 8 ) e. { 1 , 7 } -> ( if ( ( P mod 8 ) e. { 1 , 7 } , 0 , 1 ) = 0 -> ( P mod 8 ) e. { 1 , 7 } ) )
56 49 55 pm2.61i 
 |-  ( if ( ( P mod 8 ) e. { 1 , 7 } , 0 , 1 ) = 0 -> ( P mod 8 ) e. { 1 , 7 } )
57 iftrue 
 |-  ( ( P mod 8 ) e. { 1 , 7 } -> if ( ( P mod 8 ) e. { 1 , 7 } , 0 , 1 ) = 0 )
58 56 57 impbii 
 |-  ( if ( ( P mod 8 ) e. { 1 , 7 } , 0 , 1 ) = 0 <-> ( P mod 8 ) e. { 1 , 7 } )
59 58 a1i 
 |-  ( ( P e. Prime /\ -. 2 || P ) -> ( if ( ( P mod 8 ) e. { 1 , 7 } , 0 , 1 ) = 0 <-> ( P mod 8 ) e. { 1 , 7 } ) )
60 45 48 59 3bitrd 
 |-  ( ( P e. Prime /\ -. 2 || P ) -> ( 2 || ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) <-> ( P mod 8 ) e. { 1 , 7 } ) )
61 39 42 60 3bitrd 
 |-  ( ( P e. Prime /\ -. 2 || P ) -> ( ( 2 /L P ) = 1 <-> ( P mod 8 ) e. { 1 , 7 } ) )
62 61 expcom 
 |-  ( -. 2 || P -> ( P e. Prime -> ( ( 2 /L P ) = 1 <-> ( P mod 8 ) e. { 1 , 7 } ) ) )
63 9 62 jaoi 
 |-  ( ( P = 2 \/ -. 2 || P ) -> ( P e. Prime -> ( ( 2 /L P ) = 1 <-> ( P mod 8 ) e. { 1 , 7 } ) ) )
64 1 63 mpcom 
 |-  ( P e. Prime -> ( ( 2 /L P ) = 1 <-> ( P mod 8 ) e. { 1 , 7 } ) )