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∈ℙ∖2→2/LP=−1P2−18

Proof

Step Hyp Ref Expression
1 eldifi ⊢P∈ℙ∖2→P∈ℙ
2 2lgs ⊢P∈ℙ→2/LP=1↔Pmod8∈17
3 1 2 syl ⊢P∈ℙ∖2→2/LP=1↔Pmod8∈17
4 simpl ⊢2/LP=1∧Pmod8∈17∧P∈ℙ∖2→2/LP=1
5 eqcom ⊢1=−1P2−18↔−1P2−18=1
6 5 a1i ⊢P∈ℙ∖2→1=−1P2−18↔−1P2−18=1
7 nnoddn2prm ⊢P∈ℙ∖2→P∈ℕ∧¬2∥P
8 nnz ⊢P∈ℕ→P∈ℤ
9 8 anim1i ⊢P∈ℕ∧¬2∥P→P∈ℤ∧¬2∥P
10 7 9 syl ⊢P∈ℙ∖2→P∈ℤ∧¬2∥P
11 sqoddm1div8z ⊢P∈ℤ∧¬2∥P→P2−18∈ℤ
12 10 11 syl ⊢P∈ℙ∖2→P2−18∈ℤ
13 m1exp1 ⊢P2−18∈ℤ→−1P2−18=1↔2∥P2−18
14 12 13 syl ⊢P∈ℙ∖2→−1P2−18=1↔2∥P2−18
15 2lgsoddprmlem4 ⊢P∈ℤ∧¬2∥P→2∥P2−18↔Pmod8∈17
16 10 15 syl ⊢P∈ℙ∖2→2∥P2−18↔Pmod8∈17
17 6 14 16 3bitrd ⊢P∈ℙ∖2→1=−1P2−18↔Pmod8∈17
18 17 biimparc ⊢Pmod8∈17∧P∈ℙ∖2→1=−1P2−18
19 18 adantl ⊢2/LP=1∧Pmod8∈17∧P∈ℙ∖2→1=−1P2−18
20 4 19 eqtrd ⊢2/LP=1∧Pmod8∈17∧P∈ℙ∖2→2/LP=−1P2−18
21 20 exp32 ⊢2/LP=1→Pmod8∈17→P∈ℙ∖2→2/LP=−1P2−18
22 2z ⊢2∈ℤ
23 prmz ⊢P∈ℙ→P∈ℤ
24 1 23 syl ⊢P∈ℙ∖2→P∈ℤ
25 lgscl1 ⊢2∈ℤ∧P∈ℤ→2/LP∈−101
26 22 24 25 sylancr ⊢P∈ℙ∖2→2/LP∈−101
27 ovex ⊢2/LP∈V
28 27 eltp ⊢2/LP∈−101↔2/LP=−1∨2/LP=0∨2/LP=1
29 simpl ⊢2/LP=−1∧P∈ℙ∖2∧¬Pmod8∈17→2/LP=−1
30 16 notbid ⊢P∈ℙ∖2→¬2∥P2−18↔¬Pmod8∈17
31 30 biimpar ⊢P∈ℙ∖2∧¬Pmod8∈17→¬2∥P2−18
32 m1expo ⊢P2−18∈ℤ∧¬2∥P2−18→−1P2−18=−1
33 12 31 32 syl2an2r ⊢P∈ℙ∖2∧¬Pmod8∈17→−1P2−18=−1
34 33 eqcomd ⊢P∈ℙ∖2∧¬Pmod8∈17→−1=−1P2−18
35 34 adantl ⊢2/LP=−1∧P∈ℙ∖2∧¬Pmod8∈17→−1=−1P2−18
36 29 35 eqtrd ⊢2/LP=−1∧P∈ℙ∖2∧¬Pmod8∈17→2/LP=−1P2−18
37 36 a1d ⊢2/LP=−1∧P∈ℙ∖2∧¬Pmod8∈17→¬2/LP=1→2/LP=−1P2−18
38 37 exp32 ⊢2/LP=−1→P∈ℙ∖2→¬Pmod8∈17→¬2/LP=1→2/LP=−1P2−18
39 eldifsn ⊢P∈ℙ∖2↔P∈ℙ∧P≠2
40 simpr ⊢P∈ℙ∧P≠2→P≠2
41 40 necomd ⊢P∈ℙ∧P≠2→2≠P
42 39 41 sylbi ⊢P∈ℙ∖2→2≠P
43 2prm ⊢2∈ℙ
44 prmrp ⊢2∈ℙ∧P∈ℙ→2gcdP=1↔2≠P
45 43 1 44 sylancr ⊢P∈ℙ∖2→2gcdP=1↔2≠P
46 42 45 mpbird ⊢P∈ℙ∖2→2gcdP=1
47 lgsne0 ⊢2∈ℤ∧P∈ℤ→2/LP≠0↔2gcdP=1
48 22 24 47 sylancr ⊢P∈ℙ∖2→2/LP≠0↔2gcdP=1
49 46 48 mpbird ⊢P∈ℙ∖2→2/LP≠0
50 eqneqall ⊢2/LP=0→2/LP≠0→¬Pmod8∈17→¬2/LP=1→2/LP=−1P2−18
51 49 50 syl5 ⊢2/LP=0→P∈ℙ∖2→¬Pmod8∈17→¬2/LP=1→2/LP=−1P2−18
52 pm2.24 ⊢2/LP=1→¬2/LP=1→2/LP=−1P2−18
53 52 2a1d ⊢2/LP=1→P∈ℙ∖2→¬Pmod8∈17→¬2/LP=1→2/LP=−1P2−18
54 38 51 53 3jaoi ⊢2/LP=−1∨2/LP=0∨2/LP=1→P∈ℙ∖2→¬Pmod8∈17→¬2/LP=1→2/LP=−1P2−18
55 28 54 sylbi ⊢2/LP∈−101→P∈ℙ∖2→¬Pmod8∈17→¬2/LP=1→2/LP=−1P2−18
56 26 55 mpcom ⊢P∈ℙ∖2→¬Pmod8∈17→¬2/LP=1→2/LP=−1P2−18
57 56 com13 ⊢¬2/LP=1→¬Pmod8∈17→P∈ℙ∖2→2/LP=−1P2−18
58 21 57 bija ⊢2/LP=1↔Pmod8∈17→P∈ℙ∖2→2/LP=−1P2−18
59 3 58 mpcom ⊢P∈ℙ∖2→2/LP=−1P2−18