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 ( ๐‘ƒ โˆˆ โ„™ โ†’ ( ( 2 /L ๐‘ƒ ) = 1 โ†” ( ๐‘ƒ mod 8 ) โˆˆ { 1 , 7 } ) )

Proof

Step Hyp Ref Expression
1 prm2orodd โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ( ๐‘ƒ = 2 โˆจ ยฌ 2 โˆฅ ๐‘ƒ ) )
2 2lgslem4 โŠข ( ( 2 /L 2 ) = 1 โ†” ( 2 mod 8 ) โˆˆ { 1 , 7 } )
3 2 a1i โŠข ( ๐‘ƒ = 2 โ†’ ( ( 2 /L 2 ) = 1 โ†” ( 2 mod 8 ) โˆˆ { 1 , 7 } ) )
4 oveq2 โŠข ( ๐‘ƒ = 2 โ†’ ( 2 /L ๐‘ƒ ) = ( 2 /L 2 ) )
5 4 eqeq1d โŠข ( ๐‘ƒ = 2 โ†’ ( ( 2 /L ๐‘ƒ ) = 1 โ†” ( 2 /L 2 ) = 1 ) )
6 oveq1 โŠข ( ๐‘ƒ = 2 โ†’ ( ๐‘ƒ mod 8 ) = ( 2 mod 8 ) )
7 6 eleq1d โŠข ( ๐‘ƒ = 2 โ†’ ( ( ๐‘ƒ mod 8 ) โˆˆ { 1 , 7 } โ†” ( 2 mod 8 ) โˆˆ { 1 , 7 } ) )
8 3 5 7 3bitr4d โŠข ( ๐‘ƒ = 2 โ†’ ( ( 2 /L ๐‘ƒ ) = 1 โ†” ( ๐‘ƒ mod 8 ) โˆˆ { 1 , 7 } ) )
9 8 a1d โŠข ( ๐‘ƒ = 2 โ†’ ( ๐‘ƒ โˆˆ โ„™ โ†’ ( ( 2 /L ๐‘ƒ ) = 1 โ†” ( ๐‘ƒ mod 8 ) โˆˆ { 1 , 7 } ) ) )
10 2prm โŠข 2 โˆˆ โ„™
11 prmnn โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„• )
12 dvdsprime โŠข ( ( 2 โˆˆ โ„™ โˆง ๐‘ƒ โˆˆ โ„• ) โ†’ ( ๐‘ƒ โˆฅ 2 โ†” ( ๐‘ƒ = 2 โˆจ ๐‘ƒ = 1 ) ) )
13 10 11 12 sylancr โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ( ๐‘ƒ โˆฅ 2 โ†” ( ๐‘ƒ = 2 โˆจ ๐‘ƒ = 1 ) ) )
14 z2even โŠข 2 โˆฅ 2
15 breq2 โŠข ( ๐‘ƒ = 2 โ†’ ( 2 โˆฅ ๐‘ƒ โ†” 2 โˆฅ 2 ) )
16 14 15 mpbiri โŠข ( ๐‘ƒ = 2 โ†’ 2 โˆฅ ๐‘ƒ )
17 16 a1d โŠข ( ๐‘ƒ = 2 โ†’ ( ๐‘ƒ โˆˆ โ„™ โ†’ 2 โˆฅ ๐‘ƒ ) )
18 eleq1 โŠข ( ๐‘ƒ = 1 โ†’ ( ๐‘ƒ โˆˆ โ„™ โ†” 1 โˆˆ โ„™ ) )
19 1nprm โŠข ยฌ 1 โˆˆ โ„™
20 19 pm2.21i โŠข ( 1 โˆˆ โ„™ โ†’ 2 โˆฅ ๐‘ƒ )
21 18 20 syl6bi โŠข ( ๐‘ƒ = 1 โ†’ ( ๐‘ƒ โˆˆ โ„™ โ†’ 2 โˆฅ ๐‘ƒ ) )
22 17 21 jaoi โŠข ( ( ๐‘ƒ = 2 โˆจ ๐‘ƒ = 1 ) โ†’ ( ๐‘ƒ โˆˆ โ„™ โ†’ 2 โˆฅ ๐‘ƒ ) )
23 22 com12 โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ( ( ๐‘ƒ = 2 โˆจ ๐‘ƒ = 1 ) โ†’ 2 โˆฅ ๐‘ƒ ) )
24 13 23 sylbid โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ( ๐‘ƒ โˆฅ 2 โ†’ 2 โˆฅ ๐‘ƒ ) )
25 24 con3dimp โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ยฌ 2 โˆฅ ๐‘ƒ ) โ†’ ยฌ ๐‘ƒ โˆฅ 2 )
26 2z โŠข 2 โˆˆ โ„ค
27 25 26 jctil โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ยฌ 2 โˆฅ ๐‘ƒ ) โ†’ ( 2 โˆˆ โ„ค โˆง ยฌ ๐‘ƒ โˆฅ 2 ) )
28 2lgslem1 โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ยฌ 2 โˆฅ ๐‘ƒ ) โ†’ ( โ™ฏ โ€˜ { ๐‘ฅ โˆˆ โ„ค โˆฃ โˆƒ ๐‘– โˆˆ ( 1 ... ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) ( ๐‘ฅ = ( ๐‘– ยท 2 ) โˆง ( ๐‘ƒ / 2 ) < ( ๐‘ฅ mod ๐‘ƒ ) ) } ) = ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆ’ ( โŒŠ โ€˜ ( ๐‘ƒ / 4 ) ) ) )
29 28 eqcomd โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ยฌ 2 โˆฅ ๐‘ƒ ) โ†’ ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆ’ ( โŒŠ โ€˜ ( ๐‘ƒ / 4 ) ) ) = ( โ™ฏ โ€˜ { ๐‘ฅ โˆˆ โ„ค โˆฃ โˆƒ ๐‘– โˆˆ ( 1 ... ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) ( ๐‘ฅ = ( ๐‘– ยท 2 ) โˆง ( ๐‘ƒ / 2 ) < ( ๐‘ฅ mod ๐‘ƒ ) ) } ) )
30 nnoddn2prmb โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†” ( ๐‘ƒ โˆˆ โ„™ โˆง ยฌ 2 โˆฅ ๐‘ƒ ) )
31 30 biimpri โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ยฌ 2 โˆฅ ๐‘ƒ ) โ†’ ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) )
32 31 3ad2ant1 โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ยฌ 2 โˆฅ ๐‘ƒ ) โˆง ( 2 โˆˆ โ„ค โˆง ยฌ ๐‘ƒ โˆฅ 2 ) โˆง ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆ’ ( โŒŠ โ€˜ ( ๐‘ƒ / 4 ) ) ) = ( โ™ฏ โ€˜ { ๐‘ฅ โˆˆ โ„ค โˆฃ โˆƒ ๐‘– โˆˆ ( 1 ... ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) ( ๐‘ฅ = ( ๐‘– ยท 2 ) โˆง ( ๐‘ƒ / 2 ) < ( ๐‘ฅ mod ๐‘ƒ ) ) } ) ) โ†’ ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) )
33 eqid โŠข ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) = ( ( ๐‘ƒ โˆ’ 1 ) / 2 )
34 eqid โŠข ( ๐‘ฆ โˆˆ ( 1 ... ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) โ†ฆ if ( ( ๐‘ฆ ยท 2 ) < ( ๐‘ƒ / 2 ) , ( ๐‘ฆ ยท 2 ) , ( ๐‘ƒ โˆ’ ( ๐‘ฆ ยท 2 ) ) ) ) = ( ๐‘ฆ โˆˆ ( 1 ... ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) โ†ฆ if ( ( ๐‘ฆ ยท 2 ) < ( ๐‘ƒ / 2 ) , ( ๐‘ฆ ยท 2 ) , ( ๐‘ƒ โˆ’ ( ๐‘ฆ ยท 2 ) ) ) )
35 eqid โŠข ( โŒŠ โ€˜ ( ๐‘ƒ / 4 ) ) = ( โŒŠ โ€˜ ( ๐‘ƒ / 4 ) )
36 eqid โŠข ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆ’ ( โŒŠ โ€˜ ( ๐‘ƒ / 4 ) ) ) = ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆ’ ( โŒŠ โ€˜ ( ๐‘ƒ / 4 ) ) )
37 32 33 34 35 36 gausslemma2d โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ยฌ 2 โˆฅ ๐‘ƒ ) โˆง ( 2 โˆˆ โ„ค โˆง ยฌ ๐‘ƒ โˆฅ 2 ) โˆง ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆ’ ( โŒŠ โ€˜ ( ๐‘ƒ / 4 ) ) ) = ( โ™ฏ โ€˜ { ๐‘ฅ โˆˆ โ„ค โˆฃ โˆƒ ๐‘– โˆˆ ( 1 ... ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) ( ๐‘ฅ = ( ๐‘– ยท 2 ) โˆง ( ๐‘ƒ / 2 ) < ( ๐‘ฅ mod ๐‘ƒ ) ) } ) ) โ†’ ( 2 /L ๐‘ƒ ) = ( - 1 โ†‘ ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆ’ ( โŒŠ โ€˜ ( ๐‘ƒ / 4 ) ) ) ) )
38 37 eqeq1d โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ยฌ 2 โˆฅ ๐‘ƒ ) โˆง ( 2 โˆˆ โ„ค โˆง ยฌ ๐‘ƒ โˆฅ 2 ) โˆง ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆ’ ( โŒŠ โ€˜ ( ๐‘ƒ / 4 ) ) ) = ( โ™ฏ โ€˜ { ๐‘ฅ โˆˆ โ„ค โˆฃ โˆƒ ๐‘– โˆˆ ( 1 ... ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) ) ( ๐‘ฅ = ( ๐‘– ยท 2 ) โˆง ( ๐‘ƒ / 2 ) < ( ๐‘ฅ mod ๐‘ƒ ) ) } ) ) โ†’ ( ( 2 /L ๐‘ƒ ) = 1 โ†” ( - 1 โ†‘ ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆ’ ( โŒŠ โ€˜ ( ๐‘ƒ / 4 ) ) ) ) = 1 ) )
39 27 29 38 mpd3an23 โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ยฌ 2 โˆฅ ๐‘ƒ ) โ†’ ( ( 2 /L ๐‘ƒ ) = 1 โ†” ( - 1 โ†‘ ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆ’ ( โŒŠ โ€˜ ( ๐‘ƒ / 4 ) ) ) ) = 1 ) )
40 36 2lgslem2 โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ยฌ 2 โˆฅ ๐‘ƒ ) โ†’ ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆ’ ( โŒŠ โ€˜ ( ๐‘ƒ / 4 ) ) ) โˆˆ โ„ค )
41 m1exp1 โŠข ( ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆ’ ( โŒŠ โ€˜ ( ๐‘ƒ / 4 ) ) ) โˆˆ โ„ค โ†’ ( ( - 1 โ†‘ ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆ’ ( โŒŠ โ€˜ ( ๐‘ƒ / 4 ) ) ) ) = 1 โ†” 2 โˆฅ ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆ’ ( โŒŠ โ€˜ ( ๐‘ƒ / 4 ) ) ) ) )
42 40 41 syl โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ยฌ 2 โˆฅ ๐‘ƒ ) โ†’ ( ( - 1 โ†‘ ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆ’ ( โŒŠ โ€˜ ( ๐‘ƒ / 4 ) ) ) ) = 1 โ†” 2 โˆฅ ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆ’ ( โŒŠ โ€˜ ( ๐‘ƒ / 4 ) ) ) ) )
43 2nn โŠข 2 โˆˆ โ„•
44 dvdsval3 โŠข ( ( 2 โˆˆ โ„• โˆง ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆ’ ( โŒŠ โ€˜ ( ๐‘ƒ / 4 ) ) ) โˆˆ โ„ค ) โ†’ ( 2 โˆฅ ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆ’ ( โŒŠ โ€˜ ( ๐‘ƒ / 4 ) ) ) โ†” ( ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆ’ ( โŒŠ โ€˜ ( ๐‘ƒ / 4 ) ) ) mod 2 ) = 0 ) )
45 43 40 44 sylancr โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ยฌ 2 โˆฅ ๐‘ƒ ) โ†’ ( 2 โˆฅ ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆ’ ( โŒŠ โ€˜ ( ๐‘ƒ / 4 ) ) ) โ†” ( ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆ’ ( โŒŠ โ€˜ ( ๐‘ƒ / 4 ) ) ) mod 2 ) = 0 ) )
46 36 2lgslem3 โŠข ( ( ๐‘ƒ โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘ƒ ) โ†’ ( ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆ’ ( โŒŠ โ€˜ ( ๐‘ƒ / 4 ) ) ) mod 2 ) = if ( ( ๐‘ƒ mod 8 ) โˆˆ { 1 , 7 } , 0 , 1 ) )
47 11 46 sylan โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ยฌ 2 โˆฅ ๐‘ƒ ) โ†’ ( ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆ’ ( โŒŠ โ€˜ ( ๐‘ƒ / 4 ) ) ) mod 2 ) = if ( ( ๐‘ƒ mod 8 ) โˆˆ { 1 , 7 } , 0 , 1 ) )
48 47 eqeq1d โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ยฌ 2 โˆฅ ๐‘ƒ ) โ†’ ( ( ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆ’ ( โŒŠ โ€˜ ( ๐‘ƒ / 4 ) ) ) mod 2 ) = 0 โ†” if ( ( ๐‘ƒ mod 8 ) โˆˆ { 1 , 7 } , 0 , 1 ) = 0 ) )
49 ax-1 โŠข ( ( ๐‘ƒ mod 8 ) โˆˆ { 1 , 7 } โ†’ ( if ( ( ๐‘ƒ mod 8 ) โˆˆ { 1 , 7 } , 0 , 1 ) = 0 โ†’ ( ๐‘ƒ mod 8 ) โˆˆ { 1 , 7 } ) )
50 iffalse โŠข ( ยฌ ( ๐‘ƒ mod 8 ) โˆˆ { 1 , 7 } โ†’ if ( ( ๐‘ƒ mod 8 ) โˆˆ { 1 , 7 } , 0 , 1 ) = 1 )
51 50 eqeq1d โŠข ( ยฌ ( ๐‘ƒ mod 8 ) โˆˆ { 1 , 7 } โ†’ ( if ( ( ๐‘ƒ mod 8 ) โˆˆ { 1 , 7 } , 0 , 1 ) = 0 โ†” 1 = 0 ) )
52 ax-1ne0 โŠข 1 โ‰  0
53 eqneqall โŠข ( 1 = 0 โ†’ ( 1 โ‰  0 โ†’ ( ๐‘ƒ mod 8 ) โˆˆ { 1 , 7 } ) )
54 52 53 mpi โŠข ( 1 = 0 โ†’ ( ๐‘ƒ mod 8 ) โˆˆ { 1 , 7 } )
55 51 54 syl6bi โŠข ( ยฌ ( ๐‘ƒ mod 8 ) โˆˆ { 1 , 7 } โ†’ ( if ( ( ๐‘ƒ mod 8 ) โˆˆ { 1 , 7 } , 0 , 1 ) = 0 โ†’ ( ๐‘ƒ mod 8 ) โˆˆ { 1 , 7 } ) )
56 49 55 pm2.61i โŠข ( if ( ( ๐‘ƒ mod 8 ) โˆˆ { 1 , 7 } , 0 , 1 ) = 0 โ†’ ( ๐‘ƒ mod 8 ) โˆˆ { 1 , 7 } )
57 iftrue โŠข ( ( ๐‘ƒ mod 8 ) โˆˆ { 1 , 7 } โ†’ if ( ( ๐‘ƒ mod 8 ) โˆˆ { 1 , 7 } , 0 , 1 ) = 0 )
58 56 57 impbii โŠข ( if ( ( ๐‘ƒ mod 8 ) โˆˆ { 1 , 7 } , 0 , 1 ) = 0 โ†” ( ๐‘ƒ mod 8 ) โˆˆ { 1 , 7 } )
59 58 a1i โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ยฌ 2 โˆฅ ๐‘ƒ ) โ†’ ( if ( ( ๐‘ƒ mod 8 ) โˆˆ { 1 , 7 } , 0 , 1 ) = 0 โ†” ( ๐‘ƒ mod 8 ) โˆˆ { 1 , 7 } ) )
60 45 48 59 3bitrd โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ยฌ 2 โˆฅ ๐‘ƒ ) โ†’ ( 2 โˆฅ ( ( ( ๐‘ƒ โˆ’ 1 ) / 2 ) โˆ’ ( โŒŠ โ€˜ ( ๐‘ƒ / 4 ) ) ) โ†” ( ๐‘ƒ mod 8 ) โˆˆ { 1 , 7 } ) )
61 39 42 60 3bitrd โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ยฌ 2 โˆฅ ๐‘ƒ ) โ†’ ( ( 2 /L ๐‘ƒ ) = 1 โ†” ( ๐‘ƒ mod 8 ) โˆˆ { 1 , 7 } ) )
62 61 expcom โŠข ( ยฌ 2 โˆฅ ๐‘ƒ โ†’ ( ๐‘ƒ โˆˆ โ„™ โ†’ ( ( 2 /L ๐‘ƒ ) = 1 โ†” ( ๐‘ƒ mod 8 ) โˆˆ { 1 , 7 } ) ) )
63 9 62 jaoi โŠข ( ( ๐‘ƒ = 2 โˆจ ยฌ 2 โˆฅ ๐‘ƒ ) โ†’ ( ๐‘ƒ โˆˆ โ„™ โ†’ ( ( 2 /L ๐‘ƒ ) = 1 โ†” ( ๐‘ƒ mod 8 ) โˆˆ { 1 , 7 } ) ) )
64 1 63 mpcom โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ( ( 2 /L ๐‘ƒ ) = 1 โ†” ( ๐‘ƒ mod 8 ) โˆˆ { 1 , 7 } ) )