| Step | Hyp | Ref
| Expression |
| 1 | | 2lgslem1a 27435 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2
∥ 𝑃) → {𝑥 ∈ ℤ ∣
∃𝑖 ∈
(1...((𝑃 − 1) /
2))(𝑥 = (𝑖 · 2) ∧ (𝑃 / 2) < (𝑥 mod 𝑃))} = {𝑥 ∈ ℤ ∣ ∃𝑖 ∈ (((⌊‘(𝑃 / 4)) + 1)...((𝑃 − 1) / 2))𝑥 = (𝑖 · 2)}) |
| 2 | 1 | fveq2d 6910 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2
∥ 𝑃) →
(♯‘{𝑥 ∈
ℤ ∣ ∃𝑖
∈ (1...((𝑃 − 1)
/ 2))(𝑥 = (𝑖 · 2) ∧ (𝑃 / 2) < (𝑥 mod 𝑃))}) = (♯‘{𝑥 ∈ ℤ ∣ ∃𝑖 ∈ (((⌊‘(𝑃 / 4)) + 1)...((𝑃 − 1) / 2))𝑥 = (𝑖 · 2)})) |
| 3 | | ovex 7464 |
. . 3
⊢
(((⌊‘(𝑃
/ 4)) + 1)...((𝑃 − 1)
/ 2)) ∈ V |
| 4 | 3 | mptex 7243 |
. . . . 5
⊢ (𝑦 ∈ (((⌊‘(𝑃 / 4)) + 1)...((𝑃 − 1) / 2)) ↦ (𝑦 · 2)) ∈
V |
| 5 | | f1oeq1 6836 |
. . . . 5
⊢ (𝑓 = (𝑦 ∈ (((⌊‘(𝑃 / 4)) + 1)...((𝑃 − 1) / 2)) ↦ (𝑦 · 2)) → (𝑓:(((⌊‘(𝑃 / 4)) + 1)...((𝑃 − 1) / 2))–1-1-onto→{𝑥 ∈ ℤ ∣ ∃𝑖 ∈ (((⌊‘(𝑃 / 4)) + 1)...((𝑃 − 1) / 2))𝑥 = (𝑖 · 2)} ↔ (𝑦 ∈ (((⌊‘(𝑃 / 4)) + 1)...((𝑃 − 1) / 2)) ↦ (𝑦 ·
2)):(((⌊‘(𝑃 /
4)) + 1)...((𝑃 − 1) /
2))–1-1-onto→{𝑥 ∈ ℤ ∣ ∃𝑖 ∈ (((⌊‘(𝑃 / 4)) + 1)...((𝑃 − 1) / 2))𝑥 = (𝑖 · 2)})) |
| 6 | | eqid 2737 |
. . . . . 6
⊢
(((⌊‘(𝑃
/ 4)) + 1)...((𝑃 − 1)
/ 2)) = (((⌊‘(𝑃
/ 4)) + 1)...((𝑃 − 1)
/ 2)) |
| 7 | | eqid 2737 |
. . . . . 6
⊢ (𝑦 ∈ (((⌊‘(𝑃 / 4)) + 1)...((𝑃 − 1) / 2)) ↦ (𝑦 · 2)) = (𝑦 ∈ (((⌊‘(𝑃 / 4)) + 1)...((𝑃 − 1) / 2)) ↦ (𝑦 · 2)) |
| 8 | 6, 7 | 2lgslem1b 27436 |
. . . . 5
⊢ (𝑦 ∈ (((⌊‘(𝑃 / 4)) + 1)...((𝑃 − 1) / 2)) ↦ (𝑦 ·
2)):(((⌊‘(𝑃 /
4)) + 1)...((𝑃 − 1) /
2))–1-1-onto→{𝑥 ∈ ℤ ∣ ∃𝑖 ∈ (((⌊‘(𝑃 / 4)) + 1)...((𝑃 − 1) / 2))𝑥 = (𝑖 · 2)} |
| 9 | 4, 5, 8 | ceqsexv2d 3533 |
. . . 4
⊢
∃𝑓 𝑓:(((⌊‘(𝑃 / 4)) + 1)...((𝑃 − 1) / 2))–1-1-onto→{𝑥 ∈ ℤ ∣ ∃𝑖 ∈ (((⌊‘(𝑃 / 4)) + 1)...((𝑃 − 1) / 2))𝑥 = (𝑖 · 2)} |
| 10 | 9 | a1i 11 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2
∥ 𝑃) →
∃𝑓 𝑓:(((⌊‘(𝑃 / 4)) + 1)...((𝑃 − 1) / 2))–1-1-onto→{𝑥 ∈ ℤ ∣ ∃𝑖 ∈ (((⌊‘(𝑃 / 4)) + 1)...((𝑃 − 1) / 2))𝑥 = (𝑖 · 2)}) |
| 11 | | hasheqf1oi 14390 |
. . 3
⊢
((((⌊‘(𝑃
/ 4)) + 1)...((𝑃 − 1)
/ 2)) ∈ V → (∃𝑓 𝑓:(((⌊‘(𝑃 / 4)) + 1)...((𝑃 − 1) / 2))–1-1-onto→{𝑥 ∈ ℤ ∣ ∃𝑖 ∈ (((⌊‘(𝑃 / 4)) + 1)...((𝑃 − 1) / 2))𝑥 = (𝑖 · 2)} →
(♯‘(((⌊‘(𝑃 / 4)) + 1)...((𝑃 − 1) / 2))) = (♯‘{𝑥 ∈ ℤ ∣
∃𝑖 ∈
(((⌊‘(𝑃 / 4)) +
1)...((𝑃 − 1) /
2))𝑥 = (𝑖 · 2)}))) |
| 12 | 3, 10, 11 | mpsyl 68 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2
∥ 𝑃) →
(♯‘(((⌊‘(𝑃 / 4)) + 1)...((𝑃 − 1) / 2))) = (♯‘{𝑥 ∈ ℤ ∣
∃𝑖 ∈
(((⌊‘(𝑃 / 4)) +
1)...((𝑃 − 1) /
2))𝑥 = (𝑖 · 2)})) |
| 13 | | prmz 16712 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
| 14 | 13 | zred 12722 |
. . . . . . 7
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℝ) |
| 15 | | 4re 12350 |
. . . . . . . 8
⊢ 4 ∈
ℝ |
| 16 | 15 | a1i 11 |
. . . . . . 7
⊢ (𝑃 ∈ ℙ → 4 ∈
ℝ) |
| 17 | | 4ne0 12374 |
. . . . . . . 8
⊢ 4 ≠
0 |
| 18 | 17 | a1i 11 |
. . . . . . 7
⊢ (𝑃 ∈ ℙ → 4 ≠
0) |
| 19 | 14, 16, 18 | redivcld 12095 |
. . . . . 6
⊢ (𝑃 ∈ ℙ → (𝑃 / 4) ∈
ℝ) |
| 20 | 19 | flcld 13838 |
. . . . 5
⊢ (𝑃 ∈ ℙ →
(⌊‘(𝑃 / 4))
∈ ℤ) |
| 21 | 20 | adantr 480 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2
∥ 𝑃) →
(⌊‘(𝑃 / 4))
∈ ℤ) |
| 22 | | oddm1d2 16397 |
. . . . . 6
⊢ (𝑃 ∈ ℤ → (¬ 2
∥ 𝑃 ↔ ((𝑃 − 1) / 2) ∈
ℤ)) |
| 23 | 13, 22 | syl 17 |
. . . . 5
⊢ (𝑃 ∈ ℙ → (¬ 2
∥ 𝑃 ↔ ((𝑃 − 1) / 2) ∈
ℤ)) |
| 24 | 23 | biimpa 476 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2
∥ 𝑃) → ((𝑃 − 1) / 2) ∈
ℤ) |
| 25 | | 2lgslem1c 27437 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2
∥ 𝑃) →
(⌊‘(𝑃 / 4))
≤ ((𝑃 − 1) /
2)) |
| 26 | | eluz2 12884 |
. . . 4
⊢ (((𝑃 − 1) / 2) ∈
(ℤ≥‘(⌊‘(𝑃 / 4))) ↔ ((⌊‘(𝑃 / 4)) ∈ ℤ ∧
((𝑃 − 1) / 2) ∈
ℤ ∧ (⌊‘(𝑃 / 4)) ≤ ((𝑃 − 1) / 2))) |
| 27 | 21, 24, 25, 26 | syl3anbrc 1344 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2
∥ 𝑃) → ((𝑃 − 1) / 2) ∈
(ℤ≥‘(⌊‘(𝑃 / 4)))) |
| 28 | | hashfzp1 14470 |
. . 3
⊢ (((𝑃 − 1) / 2) ∈
(ℤ≥‘(⌊‘(𝑃 / 4))) →
(♯‘(((⌊‘(𝑃 / 4)) + 1)...((𝑃 − 1) / 2))) = (((𝑃 − 1) / 2) −
(⌊‘(𝑃 /
4)))) |
| 29 | 27, 28 | syl 17 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2
∥ 𝑃) →
(♯‘(((⌊‘(𝑃 / 4)) + 1)...((𝑃 − 1) / 2))) = (((𝑃 − 1) / 2) −
(⌊‘(𝑃 /
4)))) |
| 30 | 2, 12, 29 | 3eqtr2d 2783 |
1
⊢ ((𝑃 ∈ ℙ ∧ ¬ 2
∥ 𝑃) →
(♯‘{𝑥 ∈
ℤ ∣ ∃𝑖
∈ (1...((𝑃 − 1)
/ 2))(𝑥 = (𝑖 · 2) ∧ (𝑃 / 2) < (𝑥 mod 𝑃))}) = (((𝑃 − 1) / 2) −
(⌊‘(𝑃 /
4)))) |