# 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}\in ℙ\to \left(2{/}_{L}{P}=1↔{P}\mathrm{mod}8\in \left\{1,7\right\}\right)$

### Proof

Step Hyp Ref Expression
1 prm2orodd ${⊢}{P}\in ℙ\to \left({P}=2\vee ¬2\parallel {P}\right)$
2 2lgslem4 ${⊢}2{/}_{L}2=1↔2\mathrm{mod}8\in \left\{1,7\right\}$
3 2 a1i ${⊢}{P}=2\to \left(2{/}_{L}2=1↔2\mathrm{mod}8\in \left\{1,7\right\}\right)$
4 oveq2 ${⊢}{P}=2\to 2{/}_{L}{P}=2{/}_{L}2$
5 4 eqeq1d ${⊢}{P}=2\to \left(2{/}_{L}{P}=1↔2{/}_{L}2=1\right)$
6 oveq1 ${⊢}{P}=2\to {P}\mathrm{mod}8=2\mathrm{mod}8$
7 6 eleq1d ${⊢}{P}=2\to \left({P}\mathrm{mod}8\in \left\{1,7\right\}↔2\mathrm{mod}8\in \left\{1,7\right\}\right)$
8 3 5 7 3bitr4d ${⊢}{P}=2\to \left(2{/}_{L}{P}=1↔{P}\mathrm{mod}8\in \left\{1,7\right\}\right)$
9 8 a1d ${⊢}{P}=2\to \left({P}\in ℙ\to \left(2{/}_{L}{P}=1↔{P}\mathrm{mod}8\in \left\{1,7\right\}\right)\right)$
10 2prm ${⊢}2\in ℙ$
11 prmnn ${⊢}{P}\in ℙ\to {P}\in ℕ$
12 dvdsprime ${⊢}\left(2\in ℙ\wedge {P}\in ℕ\right)\to \left({P}\parallel 2↔\left({P}=2\vee {P}=1\right)\right)$
13 10 11 12 sylancr ${⊢}{P}\in ℙ\to \left({P}\parallel 2↔\left({P}=2\vee {P}=1\right)\right)$
14 z2even ${⊢}2\parallel 2$
15 breq2 ${⊢}{P}=2\to \left(2\parallel {P}↔2\parallel 2\right)$
16 14 15 mpbiri ${⊢}{P}=2\to 2\parallel {P}$
17 16 a1d ${⊢}{P}=2\to \left({P}\in ℙ\to 2\parallel {P}\right)$
18 eleq1 ${⊢}{P}=1\to \left({P}\in ℙ↔1\in ℙ\right)$
19 1nprm ${⊢}¬1\in ℙ$
20 19 pm2.21i ${⊢}1\in ℙ\to 2\parallel {P}$
21 18 20 syl6bi ${⊢}{P}=1\to \left({P}\in ℙ\to 2\parallel {P}\right)$
22 17 21 jaoi ${⊢}\left({P}=2\vee {P}=1\right)\to \left({P}\in ℙ\to 2\parallel {P}\right)$
23 22 com12 ${⊢}{P}\in ℙ\to \left(\left({P}=2\vee {P}=1\right)\to 2\parallel {P}\right)$
24 13 23 sylbid ${⊢}{P}\in ℙ\to \left({P}\parallel 2\to 2\parallel {P}\right)$
25 24 con3dimp ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to ¬{P}\parallel 2$
26 2z ${⊢}2\in ℤ$
27 25 26 jctil ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to \left(2\in ℤ\wedge ¬{P}\parallel 2\right)$
28 2lgslem1 ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to \left|\left\{{x}\in ℤ|\exists {i}\in \left(1\dots \frac{{P}-1}{2}\right)\phantom{\rule{.4em}{0ex}}\left({x}={i}\cdot 2\wedge \frac{{P}}{2}<{x}\mathrm{mod}{P}\right)\right\}\right|=\left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋$
29 28 eqcomd ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to \left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋=\left|\left\{{x}\in ℤ|\exists {i}\in \left(1\dots \frac{{P}-1}{2}\right)\phantom{\rule{.4em}{0ex}}\left({x}={i}\cdot 2\wedge \frac{{P}}{2}<{x}\mathrm{mod}{P}\right)\right\}\right|$
30 nnoddn2prmb ${⊢}{P}\in \left(ℙ\setminus \left\{2\right\}\right)↔\left({P}\in ℙ\wedge ¬2\parallel {P}\right)$
31 30 biimpri ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to {P}\in \left(ℙ\setminus \left\{2\right\}\right)$
32 31 3ad2ant1 ${⊢}\left(\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\wedge \left(2\in ℤ\wedge ¬{P}\parallel 2\right)\wedge \left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋=\left|\left\{{x}\in ℤ|\exists {i}\in \left(1\dots \frac{{P}-1}{2}\right)\phantom{\rule{.4em}{0ex}}\left({x}={i}\cdot 2\wedge \frac{{P}}{2}<{x}\mathrm{mod}{P}\right)\right\}\right|\right)\to {P}\in \left(ℙ\setminus \left\{2\right\}\right)$
33 eqid ${⊢}\frac{{P}-1}{2}=\frac{{P}-1}{2}$
34 eqid ${⊢}\left({y}\in \left(1\dots \frac{{P}-1}{2}\right)⟼if\left({y}\cdot 2<\frac{{P}}{2},{y}\cdot 2,{P}-{y}\cdot 2\right)\right)=\left({y}\in \left(1\dots \frac{{P}-1}{2}\right)⟼if\left({y}\cdot 2<\frac{{P}}{2},{y}\cdot 2,{P}-{y}\cdot 2\right)\right)$
35 eqid ${⊢}⌊\frac{{P}}{4}⌋=⌊\frac{{P}}{4}⌋$
36 eqid ${⊢}\left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋=\left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋$
37 32 33 34 35 36 gausslemma2d ${⊢}\left(\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\wedge \left(2\in ℤ\wedge ¬{P}\parallel 2\right)\wedge \left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋=\left|\left\{{x}\in ℤ|\exists {i}\in \left(1\dots \frac{{P}-1}{2}\right)\phantom{\rule{.4em}{0ex}}\left({x}={i}\cdot 2\wedge \frac{{P}}{2}<{x}\mathrm{mod}{P}\right)\right\}\right|\right)\to 2{/}_{L}{P}={\left(-1\right)}^{\left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋}$
38 37 eqeq1d ${⊢}\left(\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\wedge \left(2\in ℤ\wedge ¬{P}\parallel 2\right)\wedge \left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋=\left|\left\{{x}\in ℤ|\exists {i}\in \left(1\dots \frac{{P}-1}{2}\right)\phantom{\rule{.4em}{0ex}}\left({x}={i}\cdot 2\wedge \frac{{P}}{2}<{x}\mathrm{mod}{P}\right)\right\}\right|\right)\to \left(2{/}_{L}{P}=1↔{\left(-1\right)}^{\left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋}=1\right)$
39 27 29 38 mpd3an23 ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to \left(2{/}_{L}{P}=1↔{\left(-1\right)}^{\left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋}=1\right)$
40 36 2lgslem2 ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to \left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋\in ℤ$
41 m1exp1 ${⊢}\left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋\in ℤ\to \left({\left(-1\right)}^{\left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋}=1↔2\parallel \left(\left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋\right)\right)$
42 40 41 syl ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to \left({\left(-1\right)}^{\left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋}=1↔2\parallel \left(\left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋\right)\right)$
43 2nn ${⊢}2\in ℕ$
44 dvdsval3 ${⊢}\left(2\in ℕ\wedge \left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋\in ℤ\right)\to \left(2\parallel \left(\left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋\right)↔\left(\left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋\right)\mathrm{mod}2=0\right)$
45 43 40 44 sylancr ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to \left(2\parallel \left(\left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋\right)↔\left(\left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋\right)\mathrm{mod}2=0\right)$
46 36 2lgslem3 ${⊢}\left({P}\in ℕ\wedge ¬2\parallel {P}\right)\to \left(\left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋\right)\mathrm{mod}2=if\left({P}\mathrm{mod}8\in \left\{1,7\right\},0,1\right)$
47 11 46 sylan ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to \left(\left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋\right)\mathrm{mod}2=if\left({P}\mathrm{mod}8\in \left\{1,7\right\},0,1\right)$
48 47 eqeq1d ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to \left(\left(\left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋\right)\mathrm{mod}2=0↔if\left({P}\mathrm{mod}8\in \left\{1,7\right\},0,1\right)=0\right)$
49 ax-1 ${⊢}{P}\mathrm{mod}8\in \left\{1,7\right\}\to \left(if\left({P}\mathrm{mod}8\in \left\{1,7\right\},0,1\right)=0\to {P}\mathrm{mod}8\in \left\{1,7\right\}\right)$
50 iffalse ${⊢}¬{P}\mathrm{mod}8\in \left\{1,7\right\}\to if\left({P}\mathrm{mod}8\in \left\{1,7\right\},0,1\right)=1$
51 50 eqeq1d ${⊢}¬{P}\mathrm{mod}8\in \left\{1,7\right\}\to \left(if\left({P}\mathrm{mod}8\in \left\{1,7\right\},0,1\right)=0↔1=0\right)$
52 ax-1ne0 ${⊢}1\ne 0$
53 eqneqall ${⊢}1=0\to \left(1\ne 0\to {P}\mathrm{mod}8\in \left\{1,7\right\}\right)$
54 52 53 mpi ${⊢}1=0\to {P}\mathrm{mod}8\in \left\{1,7\right\}$
55 51 54 syl6bi ${⊢}¬{P}\mathrm{mod}8\in \left\{1,7\right\}\to \left(if\left({P}\mathrm{mod}8\in \left\{1,7\right\},0,1\right)=0\to {P}\mathrm{mod}8\in \left\{1,7\right\}\right)$
56 49 55 pm2.61i ${⊢}if\left({P}\mathrm{mod}8\in \left\{1,7\right\},0,1\right)=0\to {P}\mathrm{mod}8\in \left\{1,7\right\}$
57 iftrue ${⊢}{P}\mathrm{mod}8\in \left\{1,7\right\}\to if\left({P}\mathrm{mod}8\in \left\{1,7\right\},0,1\right)=0$
58 56 57 impbii ${⊢}if\left({P}\mathrm{mod}8\in \left\{1,7\right\},0,1\right)=0↔{P}\mathrm{mod}8\in \left\{1,7\right\}$
59 58 a1i ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to \left(if\left({P}\mathrm{mod}8\in \left\{1,7\right\},0,1\right)=0↔{P}\mathrm{mod}8\in \left\{1,7\right\}\right)$
60 45 48 59 3bitrd ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to \left(2\parallel \left(\left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋\right)↔{P}\mathrm{mod}8\in \left\{1,7\right\}\right)$
61 39 42 60 3bitrd ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to \left(2{/}_{L}{P}=1↔{P}\mathrm{mod}8\in \left\{1,7\right\}\right)$
62 61 expcom ${⊢}¬2\parallel {P}\to \left({P}\in ℙ\to \left(2{/}_{L}{P}=1↔{P}\mathrm{mod}8\in \left\{1,7\right\}\right)\right)$
63 9 62 jaoi ${⊢}\left({P}=2\vee ¬2\parallel {P}\right)\to \left({P}\in ℙ\to \left(2{/}_{L}{P}=1↔{P}\mathrm{mod}8\in \left\{1,7\right\}\right)\right)$
64 1 63 mpcom ${⊢}{P}\in ℙ\to \left(2{/}_{L}{P}=1↔{P}\mathrm{mod}8\in \left\{1,7\right\}\right)$