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 biimtrdi ⊢ ( 𝑃 = 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 biimtrdi ⊢ ( ¬ ( 𝑃 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 } ) )