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 ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 2 /L 𝑃 ) = ( - 1 ↑ ( ( ( 𝑃 ↑ 2 ) − 1 ) / 8 ) ) )

Proof

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