| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | prm2orodd 16729 | . 2
⊢ (𝑃 ∈ ℙ → (𝑃 = 2 ∨ ¬ 2 ∥ 𝑃)) | 
| 2 |  | 2lgslem4 27451 | . . . . . 6
⊢ ((2
/L 2) = 1 ↔ (2 mod 8) ∈ {1, 7}) | 
| 3 | 2 | a1i 11 | . . . . 5
⊢ (𝑃 = 2 → ((2
/L 2) = 1 ↔ (2 mod 8) ∈ {1, 7})) | 
| 4 |  | oveq2 7440 | . . . . . 6
⊢ (𝑃 = 2 → (2
/L 𝑃) =
(2 /L 2)) | 
| 5 | 4 | eqeq1d 2738 | . . . . 5
⊢ (𝑃 = 2 → ((2
/L 𝑃) = 1
↔ (2 /L 2) = 1)) | 
| 6 |  | oveq1 7439 | . . . . . 6
⊢ (𝑃 = 2 → (𝑃 mod 8) = (2 mod 8)) | 
| 7 | 6 | eleq1d 2825 | . . . . 5
⊢ (𝑃 = 2 → ((𝑃 mod 8) ∈ {1, 7} ↔ (2 mod 8)
∈ {1, 7})) | 
| 8 | 3, 5, 7 | 3bitr4d 311 | . . . 4
⊢ (𝑃 = 2 → ((2
/L 𝑃) = 1
↔ (𝑃 mod 8) ∈ {1,
7})) | 
| 9 | 8 | a1d 25 | . . 3
⊢ (𝑃 = 2 → (𝑃 ∈ ℙ → ((2
/L 𝑃) = 1
↔ (𝑃 mod 8) ∈ {1,
7}))) | 
| 10 |  | 2prm 16730 | . . . . . . . . . 10
⊢ 2 ∈
ℙ | 
| 11 |  | prmnn 16712 | . . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) | 
| 12 |  | dvdsprime 16725 | . . . . . . . . . 10
⊢ ((2
∈ ℙ ∧ 𝑃
∈ ℕ) → (𝑃
∥ 2 ↔ (𝑃 = 2
∨ 𝑃 =
1))) | 
| 13 | 10, 11, 12 | sylancr 587 | . . . . . . . . 9
⊢ (𝑃 ∈ ℙ → (𝑃 ∥ 2 ↔ (𝑃 = 2 ∨ 𝑃 = 1))) | 
| 14 |  | z2even 16408 | . . . . . . . . . . . . 13
⊢ 2 ∥
2 | 
| 15 |  | breq2 5146 | . . . . . . . . . . . . 13
⊢ (𝑃 = 2 → (2 ∥ 𝑃 ↔ 2 ∥
2)) | 
| 16 | 14, 15 | mpbiri 258 | . . . . . . . . . . . 12
⊢ (𝑃 = 2 → 2 ∥ 𝑃) | 
| 17 | 16 | a1d 25 | . . . . . . . . . . 11
⊢ (𝑃 = 2 → (𝑃 ∈ ℙ → 2 ∥ 𝑃)) | 
| 18 |  | eleq1 2828 | . . . . . . . . . . . 12
⊢ (𝑃 = 1 → (𝑃 ∈ ℙ ↔ 1 ∈
ℙ)) | 
| 19 |  | 1nprm 16717 | . . . . . . . . . . . . 13
⊢  ¬ 1
∈ ℙ | 
| 20 | 19 | pm2.21i 119 | . . . . . . . . . . . 12
⊢ (1 ∈
ℙ → 2 ∥ 𝑃) | 
| 21 | 18, 20 | biimtrdi 253 | . . . . . . . . . . 11
⊢ (𝑃 = 1 → (𝑃 ∈ ℙ → 2 ∥ 𝑃)) | 
| 22 | 17, 21 | jaoi 857 | . . . . . . . . . 10
⊢ ((𝑃 = 2 ∨ 𝑃 = 1) → (𝑃 ∈ ℙ → 2 ∥ 𝑃)) | 
| 23 | 22 | com12 32 | . . . . . . . . 9
⊢ (𝑃 ∈ ℙ → ((𝑃 = 2 ∨ 𝑃 = 1) → 2 ∥ 𝑃)) | 
| 24 | 13, 23 | sylbid 240 | . . . . . . . 8
⊢ (𝑃 ∈ ℙ → (𝑃 ∥ 2 → 2 ∥
𝑃)) | 
| 25 | 24 | con3dimp 408 | . . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2
∥ 𝑃) → ¬
𝑃 ∥
2) | 
| 26 |  | 2z 12651 | . . . . . . 7
⊢ 2 ∈
ℤ | 
| 27 | 25, 26 | jctil 519 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2
∥ 𝑃) → (2 ∈
ℤ ∧ ¬ 𝑃
∥ 2)) | 
| 28 |  | 2lgslem1 27439 | . . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2
∥ 𝑃) →
(♯‘{𝑥 ∈
ℤ ∣ ∃𝑖
∈ (1...((𝑃 − 1)
/ 2))(𝑥 = (𝑖 · 2) ∧ (𝑃 / 2) < (𝑥 mod 𝑃))}) = (((𝑃 − 1) / 2) −
(⌊‘(𝑃 /
4)))) | 
| 29 | 28 | eqcomd 2742 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2
∥ 𝑃) → (((𝑃 − 1) / 2) −
(⌊‘(𝑃 / 4))) =
(♯‘{𝑥 ∈
ℤ ∣ ∃𝑖
∈ (1...((𝑃 − 1)
/ 2))(𝑥 = (𝑖 · 2) ∧ (𝑃 / 2) < (𝑥 mod 𝑃))})) | 
| 30 |  | nnoddn2prmb 16852 | . . . . . . . . . 10
⊢ (𝑃 ∈ (ℙ ∖ {2})
↔ (𝑃 ∈ ℙ
∧ ¬ 2 ∥ 𝑃)) | 
| 31 | 30 | biimpri 228 | . . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2
∥ 𝑃) → 𝑃 ∈ (ℙ ∖
{2})) | 
| 32 | 31 | 3ad2ant1 1133 | . . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ ¬ 2
∥ 𝑃) ∧ (2 ∈
ℤ ∧ ¬ 𝑃
∥ 2) ∧ (((𝑃
− 1) / 2) − (⌊‘(𝑃 / 4))) = (♯‘{𝑥 ∈ ℤ ∣ ∃𝑖 ∈ (1...((𝑃 − 1) / 2))(𝑥 = (𝑖 · 2) ∧ (𝑃 / 2) < (𝑥 mod 𝑃))})) → 𝑃 ∈ (ℙ ∖
{2})) | 
| 33 |  | eqid 2736 | . . . . . . . 8
⊢ ((𝑃 − 1) / 2) = ((𝑃 − 1) /
2) | 
| 34 |  | eqid 2736 | . . . . . . . 8
⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ↦ if((𝑦 · 2) < (𝑃 / 2), (𝑦 · 2), (𝑃 − (𝑦 · 2)))) = (𝑦 ∈ (1...((𝑃 − 1) / 2)) ↦ if((𝑦 · 2) < (𝑃 / 2), (𝑦 · 2), (𝑃 − (𝑦 · 2)))) | 
| 35 |  | eqid 2736 | . . . . . . . 8
⊢
(⌊‘(𝑃 /
4)) = (⌊‘(𝑃 /
4)) | 
| 36 |  | eqid 2736 | . . . . . . . 8
⊢ (((𝑃 − 1) / 2) −
(⌊‘(𝑃 / 4))) =
(((𝑃 − 1) / 2)
− (⌊‘(𝑃 /
4))) | 
| 37 | 32, 33, 34, 35, 36 | gausslemma2d 27419 | . . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ ¬ 2
∥ 𝑃) ∧ (2 ∈
ℤ ∧ ¬ 𝑃
∥ 2) ∧ (((𝑃
− 1) / 2) − (⌊‘(𝑃 / 4))) = (♯‘{𝑥 ∈ ℤ ∣ ∃𝑖 ∈ (1...((𝑃 − 1) / 2))(𝑥 = (𝑖 · 2) ∧ (𝑃 / 2) < (𝑥 mod 𝑃))})) → (2 /L 𝑃) = (-1↑(((𝑃 − 1) / 2) −
(⌊‘(𝑃 /
4))))) | 
| 38 | 37 | eqeq1d 2738 | . . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ ¬ 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 1464 | . . . . 5
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2
∥ 𝑃) → ((2
/L 𝑃) = 1
↔ (-1↑(((𝑃
− 1) / 2) − (⌊‘(𝑃 / 4)))) = 1)) | 
| 40 | 36 | 2lgslem2 27440 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2
∥ 𝑃) → (((𝑃 − 1) / 2) −
(⌊‘(𝑃 / 4)))
∈ ℤ) | 
| 41 |  | m1exp1 16414 | . . . . . 6
⊢ ((((𝑃 − 1) / 2) −
(⌊‘(𝑃 / 4)))
∈ ℤ → ((-1↑(((𝑃 − 1) / 2) −
(⌊‘(𝑃 / 4)))) =
1 ↔ 2 ∥ (((𝑃
− 1) / 2) − (⌊‘(𝑃 / 4))))) | 
| 42 | 40, 41 | syl 17 | . . . . 5
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2
∥ 𝑃) →
((-1↑(((𝑃 − 1) /
2) − (⌊‘(𝑃 / 4)))) = 1 ↔ 2 ∥ (((𝑃 − 1) / 2) −
(⌊‘(𝑃 /
4))))) | 
| 43 |  | 2nn 12340 | . . . . . . 7
⊢ 2 ∈
ℕ | 
| 44 |  | dvdsval3 16295 | . . . . . . 7
⊢ ((2
∈ ℕ ∧ (((𝑃
− 1) / 2) − (⌊‘(𝑃 / 4))) ∈ ℤ) → (2 ∥
(((𝑃 − 1) / 2)
− (⌊‘(𝑃 /
4))) ↔ ((((𝑃 −
1) / 2) − (⌊‘(𝑃 / 4))) mod 2) = 0)) | 
| 45 | 43, 40, 44 | sylancr 587 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2
∥ 𝑃) → (2
∥ (((𝑃 − 1) /
2) − (⌊‘(𝑃 / 4))) ↔ ((((𝑃 − 1) / 2) −
(⌊‘(𝑃 / 4)))
mod 2) = 0)) | 
| 46 | 36 | 2lgslem3 27449 | . . . . . . . 8
⊢ ((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) → ((((𝑃 − 1) / 2) −
(⌊‘(𝑃 / 4)))
mod 2) = if((𝑃 mod 8)
∈ {1, 7}, 0, 1)) | 
| 47 | 11, 46 | sylan 580 | . . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2
∥ 𝑃) → ((((𝑃 − 1) / 2) −
(⌊‘(𝑃 / 4)))
mod 2) = if((𝑃 mod 8)
∈ {1, 7}, 0, 1)) | 
| 48 | 47 | eqeq1d 2738 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2
∥ 𝑃) →
(((((𝑃 − 1) / 2)
− (⌊‘(𝑃 /
4))) mod 2) = 0 ↔ if((𝑃 mod 8) ∈ {1, 7}, 0, 1) =
0)) | 
| 49 |  | ax-1 6 | . . . . . . . . 9
⊢ ((𝑃 mod 8) ∈ {1, 7} →
(if((𝑃 mod 8) ∈ {1,
7}, 0, 1) = 0 → (𝑃 mod
8) ∈ {1, 7})) | 
| 50 |  | iffalse 4533 | . . . . . . . . . . 11
⊢ (¬
(𝑃 mod 8) ∈ {1, 7}
→ if((𝑃 mod 8) ∈
{1, 7}, 0, 1) = 1) | 
| 51 | 50 | eqeq1d 2738 | . . . . . . . . . 10
⊢ (¬
(𝑃 mod 8) ∈ {1, 7}
→ (if((𝑃 mod 8) ∈
{1, 7}, 0, 1) = 0 ↔ 1 = 0)) | 
| 52 |  | ax-1ne0 11225 | . . . . . . . . . . 11
⊢ 1 ≠
0 | 
| 53 |  | eqneqall 2950 | . . . . . . . . . . 11
⊢ (1 = 0
→ (1 ≠ 0 → (𝑃
mod 8) ∈ {1, 7})) | 
| 54 | 52, 53 | mpi 20 | . . . . . . . . . 10
⊢ (1 = 0
→ (𝑃 mod 8) ∈ {1,
7}) | 
| 55 | 51, 54 | biimtrdi 253 | . . . . . . . . 9
⊢ (¬
(𝑃 mod 8) ∈ {1, 7}
→ (if((𝑃 mod 8) ∈
{1, 7}, 0, 1) = 0 → (𝑃
mod 8) ∈ {1, 7})) | 
| 56 | 49, 55 | pm2.61i 182 | . . . . . . . 8
⊢
(if((𝑃 mod 8) ∈
{1, 7}, 0, 1) = 0 → (𝑃
mod 8) ∈ {1, 7}) | 
| 57 |  | iftrue 4530 | . . . . . . . 8
⊢ ((𝑃 mod 8) ∈ {1, 7} →
if((𝑃 mod 8) ∈ {1, 7},
0, 1) = 0) | 
| 58 | 56, 57 | impbii 209 | . . . . . . 7
⊢
(if((𝑃 mod 8) ∈
{1, 7}, 0, 1) = 0 ↔ (𝑃
mod 8) ∈ {1, 7}) | 
| 59 | 58 | a1i 11 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2
∥ 𝑃) →
(if((𝑃 mod 8) ∈ {1,
7}, 0, 1) = 0 ↔ (𝑃 mod
8) ∈ {1, 7})) | 
| 60 | 45, 48, 59 | 3bitrd 305 | . . . . 5
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2
∥ 𝑃) → (2
∥ (((𝑃 − 1) /
2) − (⌊‘(𝑃 / 4))) ↔ (𝑃 mod 8) ∈ {1, 7})) | 
| 61 | 39, 42, 60 | 3bitrd 305 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2
∥ 𝑃) → ((2
/L 𝑃) = 1
↔ (𝑃 mod 8) ∈ {1,
7})) | 
| 62 | 61 | expcom 413 | . . 3
⊢ (¬ 2
∥ 𝑃 → (𝑃 ∈ ℙ → ((2
/L 𝑃) = 1
↔ (𝑃 mod 8) ∈ {1,
7}))) | 
| 63 | 9, 62 | jaoi 857 | . 2
⊢ ((𝑃 = 2 ∨ ¬ 2 ∥ 𝑃) → (𝑃 ∈ ℙ → ((2
/L 𝑃) = 1
↔ (𝑃 mod 8) ∈ {1,
7}))) | 
| 64 | 1, 63 | mpcom 38 | 1
⊢ (𝑃 ∈ ℙ → ((2
/L 𝑃) = 1
↔ (𝑃 mod 8) ∈ {1,
7})) |