Step | Hyp | Ref
| Expression |
1 | | fveq2 5496 |
. . . . . . . 8
⊢ (𝑥 = 0 →
(ℤ≥‘𝑥) =
(ℤ≥‘0)) |
2 | | fveq2 5496 |
. . . . . . . . . 10
⊢ (𝑥 = 0 → (!‘𝑥) =
(!‘0)) |
3 | 2 | oveq2d 5869 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (𝑃 pCnt (!‘𝑥)) = (𝑃 pCnt (!‘0))) |
4 | | fvoveq1 5876 |
. . . . . . . . . 10
⊢ (𝑥 = 0 →
(⌊‘(𝑥 / (𝑃↑𝑘))) = (⌊‘(0 / (𝑃↑𝑘)))) |
5 | 4 | sumeq2sdv 11333 |
. . . . . . . . 9
⊢ (𝑥 = 0 → Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) = Σ𝑘 ∈ (1...𝑚)(⌊‘(0 / (𝑃↑𝑘)))) |
6 | 3, 5 | eqeq12d 2185 |
. . . . . . . 8
⊢ (𝑥 = 0 → ((𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) ↔ (𝑃 pCnt (!‘0)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(0 / (𝑃↑𝑘))))) |
7 | 1, 6 | raleqbidv 2677 |
. . . . . . 7
⊢ (𝑥 = 0 → (∀𝑚 ∈
(ℤ≥‘𝑥)(𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) ↔ ∀𝑚 ∈
(ℤ≥‘0)(𝑃 pCnt (!‘0)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(0 / (𝑃↑𝑘))))) |
8 | 7 | imbi2d 229 |
. . . . . 6
⊢ (𝑥 = 0 → ((𝑃 ∈ ℙ → ∀𝑚 ∈
(ℤ≥‘𝑥)(𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘)))) ↔ (𝑃 ∈ ℙ → ∀𝑚 ∈
(ℤ≥‘0)(𝑃 pCnt (!‘0)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(0 / (𝑃↑𝑘)))))) |
9 | | fveq2 5496 |
. . . . . . . 8
⊢ (𝑥 = 𝑛 → (ℤ≥‘𝑥) =
(ℤ≥‘𝑛)) |
10 | | fveq2 5496 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑛 → (!‘𝑥) = (!‘𝑛)) |
11 | 10 | oveq2d 5869 |
. . . . . . . . 9
⊢ (𝑥 = 𝑛 → (𝑃 pCnt (!‘𝑥)) = (𝑃 pCnt (!‘𝑛))) |
12 | | fvoveq1 5876 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑛 → (⌊‘(𝑥 / (𝑃↑𝑘))) = (⌊‘(𝑛 / (𝑃↑𝑘)))) |
13 | 12 | sumeq2sdv 11333 |
. . . . . . . . 9
⊢ (𝑥 = 𝑛 → Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘)))) |
14 | 11, 13 | eqeq12d 2185 |
. . . . . . . 8
⊢ (𝑥 = 𝑛 → ((𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) ↔ (𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))))) |
15 | 9, 14 | raleqbidv 2677 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (∀𝑚 ∈ (ℤ≥‘𝑥)(𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) ↔ ∀𝑚 ∈ (ℤ≥‘𝑛)(𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))))) |
16 | 15 | imbi2d 229 |
. . . . . 6
⊢ (𝑥 = 𝑛 → ((𝑃 ∈ ℙ → ∀𝑚 ∈
(ℤ≥‘𝑥)(𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘)))) ↔ (𝑃 ∈ ℙ → ∀𝑚 ∈
(ℤ≥‘𝑛)(𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘)))))) |
17 | | fveq2 5496 |
. . . . . . . 8
⊢ (𝑥 = (𝑛 + 1) →
(ℤ≥‘𝑥) = (ℤ≥‘(𝑛 + 1))) |
18 | | fveq2 5496 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑛 + 1) → (!‘𝑥) = (!‘(𝑛 + 1))) |
19 | 18 | oveq2d 5869 |
. . . . . . . . 9
⊢ (𝑥 = (𝑛 + 1) → (𝑃 pCnt (!‘𝑥)) = (𝑃 pCnt (!‘(𝑛 + 1)))) |
20 | | fvoveq1 5876 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑛 + 1) → (⌊‘(𝑥 / (𝑃↑𝑘))) = (⌊‘((𝑛 + 1) / (𝑃↑𝑘)))) |
21 | 20 | sumeq2sdv 11333 |
. . . . . . . . 9
⊢ (𝑥 = (𝑛 + 1) → Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘)))) |
22 | 19, 21 | eqeq12d 2185 |
. . . . . . . 8
⊢ (𝑥 = (𝑛 + 1) → ((𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) ↔ (𝑃 pCnt (!‘(𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))))) |
23 | 17, 22 | raleqbidv 2677 |
. . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → (∀𝑚 ∈ (ℤ≥‘𝑥)(𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) ↔ ∀𝑚 ∈ (ℤ≥‘(𝑛 + 1))(𝑃 pCnt (!‘(𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))))) |
24 | 23 | imbi2d 229 |
. . . . . 6
⊢ (𝑥 = (𝑛 + 1) → ((𝑃 ∈ ℙ → ∀𝑚 ∈
(ℤ≥‘𝑥)(𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘)))) ↔ (𝑃 ∈ ℙ → ∀𝑚 ∈
(ℤ≥‘(𝑛 + 1))(𝑃 pCnt (!‘(𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘)))))) |
25 | | fveq2 5496 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → (ℤ≥‘𝑥) =
(ℤ≥‘𝑁)) |
26 | | fveq2 5496 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑁 → (!‘𝑥) = (!‘𝑁)) |
27 | 26 | oveq2d 5869 |
. . . . . . . . 9
⊢ (𝑥 = 𝑁 → (𝑃 pCnt (!‘𝑥)) = (𝑃 pCnt (!‘𝑁))) |
28 | | fvoveq1 5876 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑁 → (⌊‘(𝑥 / (𝑃↑𝑘))) = (⌊‘(𝑁 / (𝑃↑𝑘)))) |
29 | 28 | sumeq2sdv 11333 |
. . . . . . . . 9
⊢ (𝑥 = 𝑁 → Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑁 / (𝑃↑𝑘)))) |
30 | 27, 29 | eqeq12d 2185 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → ((𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) ↔ (𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑁 / (𝑃↑𝑘))))) |
31 | 25, 30 | raleqbidv 2677 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (∀𝑚 ∈ (ℤ≥‘𝑥)(𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) ↔ ∀𝑚 ∈ (ℤ≥‘𝑁)(𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑁 / (𝑃↑𝑘))))) |
32 | 31 | imbi2d 229 |
. . . . . 6
⊢ (𝑥 = 𝑁 → ((𝑃 ∈ ℙ → ∀𝑚 ∈
(ℤ≥‘𝑥)(𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘)))) ↔ (𝑃 ∈ ℙ → ∀𝑚 ∈
(ℤ≥‘𝑁)(𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑁 / (𝑃↑𝑘)))))) |
33 | | 1zzd 9239 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝑚 ∈
(ℤ≥‘0)) → 1 ∈ ℤ) |
34 | | eluzelz 9496 |
. . . . . . . . . . 11
⊢ (𝑚 ∈
(ℤ≥‘0) → 𝑚 ∈ ℤ) |
35 | 34 | adantl 275 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝑚 ∈
(ℤ≥‘0)) → 𝑚 ∈ ℤ) |
36 | 33, 35 | fzfigd 10387 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝑚 ∈
(ℤ≥‘0)) → (1...𝑚) ∈ Fin) |
37 | | isumz 11352 |
. . . . . . . . . 10
⊢ (((1
∈ ℤ ∧ (1...𝑚) ⊆ (ℤ≥‘1)
∧ ∀𝑗 ∈
(ℤ≥‘1)DECID 𝑗 ∈ (1...𝑚)) ∨ (1...𝑚) ∈ Fin) → Σ𝑘 ∈ (1...𝑚)0 = 0) |
38 | 37 | olcs 731 |
. . . . . . . . 9
⊢
((1...𝑚) ∈ Fin
→ Σ𝑘 ∈
(1...𝑚)0 =
0) |
39 | 36, 38 | syl 14 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑚 ∈
(ℤ≥‘0)) → Σ𝑘 ∈ (1...𝑚)0 = 0) |
40 | | 0nn0 9150 |
. . . . . . . . . 10
⊢ 0 ∈
ℕ0 |
41 | | elfznn 10010 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1...𝑚) → 𝑘 ∈ ℕ) |
42 | 41 | nnnn0d 9188 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...𝑚) → 𝑘 ∈ ℕ0) |
43 | | nn0uz 9521 |
. . . . . . . . . . . 12
⊢
ℕ0 = (ℤ≥‘0) |
44 | 42, 43 | eleqtrdi 2263 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...𝑚) → 𝑘 ∈
(ℤ≥‘0)) |
45 | 44 | adantl 275 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝑚 ∈
(ℤ≥‘0)) ∧ 𝑘 ∈ (1...𝑚)) → 𝑘 ∈
(ℤ≥‘0)) |
46 | | simpll 524 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝑚 ∈
(ℤ≥‘0)) ∧ 𝑘 ∈ (1...𝑚)) → 𝑃 ∈ ℙ) |
47 | | pcfaclem 12301 |
. . . . . . . . . 10
⊢ ((0
∈ ℕ0 ∧ 𝑘 ∈ (ℤ≥‘0)
∧ 𝑃 ∈ ℙ)
→ (⌊‘(0 / (𝑃↑𝑘))) = 0) |
48 | 40, 45, 46, 47 | mp3an2i 1337 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝑚 ∈
(ℤ≥‘0)) ∧ 𝑘 ∈ (1...𝑚)) → (⌊‘(0 / (𝑃↑𝑘))) = 0) |
49 | 48 | sumeq2dv 11331 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑚 ∈
(ℤ≥‘0)) → Σ𝑘 ∈ (1...𝑚)(⌊‘(0 / (𝑃↑𝑘))) = Σ𝑘 ∈ (1...𝑚)0) |
50 | | fac0 10662 |
. . . . . . . . . . 11
⊢
(!‘0) = 1 |
51 | 50 | oveq2i 5864 |
. . . . . . . . . 10
⊢ (𝑃 pCnt (!‘0)) = (𝑃 pCnt 1) |
52 | | pc1 12259 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → (𝑃 pCnt 1) = 0) |
53 | 51, 52 | eqtrid 2215 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → (𝑃 pCnt (!‘0)) =
0) |
54 | 53 | adantr 274 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑚 ∈
(ℤ≥‘0)) → (𝑃 pCnt (!‘0)) = 0) |
55 | 39, 49, 54 | 3eqtr4rd 2214 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑚 ∈
(ℤ≥‘0)) → (𝑃 pCnt (!‘0)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(0 / (𝑃↑𝑘)))) |
56 | 55 | ralrimiva 2543 |
. . . . . 6
⊢ (𝑃 ∈ ℙ →
∀𝑚 ∈
(ℤ≥‘0)(𝑃 pCnt (!‘0)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(0 / (𝑃↑𝑘)))) |
57 | | nn0z 9232 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℤ) |
58 | 57 | adantr 274 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
→ 𝑛 ∈
ℤ) |
59 | | uzid 9501 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
(ℤ≥‘𝑛)) |
60 | | peano2uz 9542 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(ℤ≥‘𝑛) → (𝑛 + 1) ∈
(ℤ≥‘𝑛)) |
61 | 58, 59, 60 | 3syl 17 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
→ (𝑛 + 1) ∈
(ℤ≥‘𝑛)) |
62 | | uzss 9507 |
. . . . . . . . . 10
⊢ ((𝑛 + 1) ∈
(ℤ≥‘𝑛) → (ℤ≥‘(𝑛 + 1)) ⊆
(ℤ≥‘𝑛)) |
63 | | ssralv 3211 |
. . . . . . . . . 10
⊢
((ℤ≥‘(𝑛 + 1)) ⊆
(ℤ≥‘𝑛) → (∀𝑚 ∈ (ℤ≥‘𝑛)(𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) → ∀𝑚 ∈ (ℤ≥‘(𝑛 + 1))(𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))))) |
64 | 61, 62, 63 | 3syl 17 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
→ (∀𝑚 ∈
(ℤ≥‘𝑛)(𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) → ∀𝑚 ∈ (ℤ≥‘(𝑛 + 1))(𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))))) |
65 | | oveq1 5860 |
. . . . . . . . . . 11
⊢ ((𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) → ((𝑃 pCnt (!‘𝑛)) + (𝑃 pCnt (𝑛 + 1))) = (Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) + (𝑃 pCnt (𝑛 + 1)))) |
66 | | simpll 524 |
. . . . . . . . . . . . . . 15
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → 𝑛 ∈ ℕ0) |
67 | | facp1 10664 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ0
→ (!‘(𝑛 + 1)) =
((!‘𝑛) ·
(𝑛 + 1))) |
68 | 66, 67 | syl 14 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (!‘(𝑛 + 1)) = ((!‘𝑛) · (𝑛 + 1))) |
69 | 68 | oveq2d 5869 |
. . . . . . . . . . . . 13
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃 pCnt (!‘(𝑛 + 1))) = (𝑃 pCnt ((!‘𝑛) · (𝑛 + 1)))) |
70 | | simplr 525 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → 𝑃 ∈ ℙ) |
71 | | faccl 10669 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ0
→ (!‘𝑛) ∈
ℕ) |
72 | | nnz 9231 |
. . . . . . . . . . . . . . . 16
⊢
((!‘𝑛) ∈
ℕ → (!‘𝑛)
∈ ℤ) |
73 | | nnne0 8906 |
. . . . . . . . . . . . . . . 16
⊢
((!‘𝑛) ∈
ℕ → (!‘𝑛)
≠ 0) |
74 | 72, 73 | jca 304 |
. . . . . . . . . . . . . . 15
⊢
((!‘𝑛) ∈
ℕ → ((!‘𝑛)
∈ ℤ ∧ (!‘𝑛) ≠ 0)) |
75 | 66, 71, 74 | 3syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((!‘𝑛) ∈ ℤ ∧ (!‘𝑛) ≠ 0)) |
76 | | nn0p1nn 9174 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ0
→ (𝑛 + 1) ∈
ℕ) |
77 | | nnz 9231 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 + 1) ∈ ℕ →
(𝑛 + 1) ∈
ℤ) |
78 | | nnne0 8906 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 + 1) ∈ ℕ →
(𝑛 + 1) ≠
0) |
79 | 77, 78 | jca 304 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 + 1) ∈ ℕ →
((𝑛 + 1) ∈ ℤ
∧ (𝑛 + 1) ≠
0)) |
80 | 66, 76, 79 | 3syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((𝑛 + 1) ∈ ℤ ∧ (𝑛 + 1) ≠ 0)) |
81 | | pcmul 12255 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧
((!‘𝑛) ∈ ℤ
∧ (!‘𝑛) ≠ 0)
∧ ((𝑛 + 1) ∈
ℤ ∧ (𝑛 + 1) ≠
0)) → (𝑃 pCnt
((!‘𝑛) ·
(𝑛 + 1))) = ((𝑃 pCnt (!‘𝑛)) + (𝑃 pCnt (𝑛 + 1)))) |
82 | 70, 75, 80, 81 | syl3anc 1233 |
. . . . . . . . . . . . 13
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃 pCnt ((!‘𝑛) · (𝑛 + 1))) = ((𝑃 pCnt (!‘𝑛)) + (𝑃 pCnt (𝑛 + 1)))) |
83 | 69, 82 | eqtr2d 2204 |
. . . . . . . . . . . 12
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((𝑃 pCnt (!‘𝑛)) + (𝑃 pCnt (𝑛 + 1))) = (𝑃 pCnt (!‘(𝑛 + 1)))) |
84 | 66 | adantr 274 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → 𝑛 ∈ ℕ0) |
85 | 84 | nn0zd 9332 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → 𝑛 ∈ ℤ) |
86 | | prmnn 12064 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
87 | 86 | ad2antlr 486 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → 𝑃 ∈ ℕ) |
88 | | nnexpcl 10489 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑃↑𝑘) ∈
ℕ) |
89 | 87, 42, 88 | syl2an 287 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → (𝑃↑𝑘) ∈ ℕ) |
90 | | fldivp1 12300 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℤ ∧ (𝑃↑𝑘) ∈ ℕ) →
((⌊‘((𝑛 + 1) /
(𝑃↑𝑘))) − (⌊‘(𝑛 / (𝑃↑𝑘)))) = if((𝑃↑𝑘) ∥ (𝑛 + 1), 1, 0)) |
91 | 85, 89, 90 | syl2anc 409 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → ((⌊‘((𝑛 + 1) / (𝑃↑𝑘))) − (⌊‘(𝑛 / (𝑃↑𝑘)))) = if((𝑃↑𝑘) ∥ (𝑛 + 1), 1, 0)) |
92 | | elfzuz 9977 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ (1...𝑚) → 𝑘 ∈
(ℤ≥‘1)) |
93 | 66, 76 | syl 14 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑛 + 1) ∈ ℕ) |
94 | 70, 93 | pccld 12254 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃 pCnt (𝑛 + 1)) ∈
ℕ0) |
95 | 94 | nn0zd 9332 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃 pCnt (𝑛 + 1)) ∈ ℤ) |
96 | | elfz5 9973 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈
(ℤ≥‘1) ∧ (𝑃 pCnt (𝑛 + 1)) ∈ ℤ) → (𝑘 ∈ (1...(𝑃 pCnt (𝑛 + 1))) ↔ 𝑘 ≤ (𝑃 pCnt (𝑛 + 1)))) |
97 | 92, 95, 96 | syl2anr 288 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → (𝑘 ∈ (1...(𝑃 pCnt (𝑛 + 1))) ↔ 𝑘 ≤ (𝑃 pCnt (𝑛 + 1)))) |
98 | | simpllr 529 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → 𝑃 ∈ ℙ) |
99 | 84, 76 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → (𝑛 + 1) ∈ ℕ) |
100 | 99 | nnzd 9333 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → (𝑛 + 1) ∈ ℤ) |
101 | 42 | adantl 275 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → 𝑘 ∈ ℕ0) |
102 | | pcdvdsb 12273 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ ℙ ∧ (𝑛 + 1) ∈ ℤ ∧ 𝑘 ∈ ℕ0)
→ (𝑘 ≤ (𝑃 pCnt (𝑛 + 1)) ↔ (𝑃↑𝑘) ∥ (𝑛 + 1))) |
103 | 98, 100, 101, 102 | syl3anc 1233 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → (𝑘 ≤ (𝑃 pCnt (𝑛 + 1)) ↔ (𝑃↑𝑘) ∥ (𝑛 + 1))) |
104 | 97, 103 | bitr2d 188 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → ((𝑃↑𝑘) ∥ (𝑛 + 1) ↔ 𝑘 ∈ (1...(𝑃 pCnt (𝑛 + 1))))) |
105 | 104 | ifbid 3547 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → if((𝑃↑𝑘) ∥ (𝑛 + 1), 1, 0) = if(𝑘 ∈ (1...(𝑃 pCnt (𝑛 + 1))), 1, 0)) |
106 | 91, 105 | eqtrd 2203 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → ((⌊‘((𝑛 + 1) / (𝑃↑𝑘))) − (⌊‘(𝑛 / (𝑃↑𝑘)))) = if(𝑘 ∈ (1...(𝑃 pCnt (𝑛 + 1))), 1, 0)) |
107 | 106 | sumeq2dv 11331 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → Σ𝑘 ∈ (1...𝑚)((⌊‘((𝑛 + 1) / (𝑃↑𝑘))) − (⌊‘(𝑛 / (𝑃↑𝑘)))) = Σ𝑘 ∈ (1...𝑚)if(𝑘 ∈ (1...(𝑃 pCnt (𝑛 + 1))), 1, 0)) |
108 | | 1zzd 9239 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → 1 ∈
ℤ) |
109 | | eluzelz 9496 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈
(ℤ≥‘(𝑛 + 1)) → 𝑚 ∈ ℤ) |
110 | 109 | adantl 275 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → 𝑚 ∈ ℤ) |
111 | 108, 110 | fzfigd 10387 |
. . . . . . . . . . . . . . 15
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (1...𝑚) ∈ Fin) |
112 | | znq 9583 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑛 + 1) ∈ ℤ ∧
(𝑃↑𝑘) ∈ ℕ) → ((𝑛 + 1) / (𝑃↑𝑘)) ∈ ℚ) |
113 | 100, 89, 112 | syl2anc 409 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → ((𝑛 + 1) / (𝑃↑𝑘)) ∈ ℚ) |
114 | 113 | flqcld 10233 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → (⌊‘((𝑛 + 1) / (𝑃↑𝑘))) ∈ ℤ) |
115 | 114 | zcnd 9335 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → (⌊‘((𝑛 + 1) / (𝑃↑𝑘))) ∈ ℂ) |
116 | | znq 9583 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ ℤ ∧ (𝑃↑𝑘) ∈ ℕ) → (𝑛 / (𝑃↑𝑘)) ∈ ℚ) |
117 | 85, 89, 116 | syl2anc 409 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → (𝑛 / (𝑃↑𝑘)) ∈ ℚ) |
118 | 117 | flqcld 10233 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → (⌊‘(𝑛 / (𝑃↑𝑘))) ∈ ℤ) |
119 | 118 | zcnd 9335 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → (⌊‘(𝑛 / (𝑃↑𝑘))) ∈ ℂ) |
120 | 111, 115,
119 | fsumsub 11415 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → Σ𝑘 ∈ (1...𝑚)((⌊‘((𝑛 + 1) / (𝑃↑𝑘))) − (⌊‘(𝑛 / (𝑃↑𝑘)))) = (Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))) − Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))))) |
121 | 94 | nn0red 9189 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃 pCnt (𝑛 + 1)) ∈ ℝ) |
122 | 66 | nn0red 9189 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → 𝑛 ∈ ℝ) |
123 | | peano2re 8055 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℝ → (𝑛 + 1) ∈
ℝ) |
124 | 122, 123 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑛 + 1) ∈ ℝ) |
125 | 110 | zred 9334 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → 𝑚 ∈ ℝ) |
126 | 93 | nnzd 9333 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑛 + 1) ∈ ℤ) |
127 | | zdcle 9288 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 pCnt (𝑛 + 1)) ∈ ℤ ∧ (𝑛 + 1) ∈ ℤ) →
DECID (𝑃
pCnt (𝑛 + 1)) ≤ (𝑛 + 1)) |
128 | 95, 126, 127 | syl2anc 409 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → DECID (𝑃 pCnt (𝑛 + 1)) ≤ (𝑛 + 1)) |
129 | | zletric 9256 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑃 pCnt (𝑛 + 1)) ∈ ℤ ∧ (𝑛 + 1) ∈ ℤ) →
((𝑃 pCnt (𝑛 + 1)) ≤ (𝑛 + 1) ∨ (𝑛 + 1) ≤ (𝑃 pCnt (𝑛 + 1)))) |
130 | 95, 126, 129 | syl2anc 409 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((𝑃 pCnt (𝑛 + 1)) ≤ (𝑛 + 1) ∨ (𝑛 + 1) ≤ (𝑃 pCnt (𝑛 + 1)))) |
131 | 130 | ord 719 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (¬ (𝑃 pCnt (𝑛 + 1)) ≤ (𝑛 + 1) → (𝑛 + 1) ≤ (𝑃 pCnt (𝑛 + 1)))) |
132 | 93 | nnnn0d 9188 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑛 + 1) ∈
ℕ0) |
133 | | pcdvdsb 12273 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃 ∈ ℙ ∧ (𝑛 + 1) ∈ ℤ ∧
(𝑛 + 1) ∈
ℕ0) → ((𝑛 + 1) ≤ (𝑃 pCnt (𝑛 + 1)) ↔ (𝑃↑(𝑛 + 1)) ∥ (𝑛 + 1))) |
134 | 70, 126, 132, 133 | syl3anc 1233 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((𝑛 + 1) ≤ (𝑃 pCnt (𝑛 + 1)) ↔ (𝑃↑(𝑛 + 1)) ∥ (𝑛 + 1))) |
135 | 87, 132 | nnexpcld 10631 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃↑(𝑛 + 1)) ∈ ℕ) |
136 | 135 | nnzd 9333 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃↑(𝑛 + 1)) ∈ ℤ) |
137 | | dvdsle 11804 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑃↑(𝑛 + 1)) ∈ ℤ ∧ (𝑛 + 1) ∈ ℕ) →
((𝑃↑(𝑛 + 1)) ∥ (𝑛 + 1) → (𝑃↑(𝑛 + 1)) ≤ (𝑛 + 1))) |
138 | 136, 93, 137 | syl2anc 409 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((𝑃↑(𝑛 + 1)) ∥ (𝑛 + 1) → (𝑃↑(𝑛 + 1)) ≤ (𝑛 + 1))) |
139 | 135 | nnred 8891 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃↑(𝑛 + 1)) ∈ ℝ) |
140 | 139, 124 | lenltd 8037 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((𝑃↑(𝑛 + 1)) ≤ (𝑛 + 1) ↔ ¬ (𝑛 + 1) < (𝑃↑(𝑛 + 1)))) |
141 | 138, 140 | sylibd 148 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((𝑃↑(𝑛 + 1)) ∥ (𝑛 + 1) → ¬ (𝑛 + 1) < (𝑃↑(𝑛 + 1)))) |
142 | 134, 141 | sylbid 149 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((𝑛 + 1) ≤ (𝑃 pCnt (𝑛 + 1)) → ¬ (𝑛 + 1) < (𝑃↑(𝑛 + 1)))) |
143 | 131, 142 | syld 45 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (¬ (𝑃 pCnt (𝑛 + 1)) ≤ (𝑛 + 1) → ¬ (𝑛 + 1) < (𝑃↑(𝑛 + 1)))) |
144 | | prmuz2 12085 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
145 | 144 | ad2antlr 486 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → 𝑃 ∈
(ℤ≥‘2)) |
146 | | bernneq3 10598 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑛 + 1) ∈ ℕ0) →
(𝑛 + 1) < (𝑃↑(𝑛 + 1))) |
147 | 145, 132,
146 | syl2anc 409 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑛 + 1) < (𝑃↑(𝑛 + 1))) |
148 | | condc 848 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(DECID (𝑃 pCnt (𝑛 + 1)) ≤ (𝑛 + 1) → ((¬ (𝑃 pCnt (𝑛 + 1)) ≤ (𝑛 + 1) → ¬ (𝑛 + 1) < (𝑃↑(𝑛 + 1))) → ((𝑛 + 1) < (𝑃↑(𝑛 + 1)) → (𝑃 pCnt (𝑛 + 1)) ≤ (𝑛 + 1)))) |
149 | 128, 143,
147, 148 | syl3c 63 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃 pCnt (𝑛 + 1)) ≤ (𝑛 + 1)) |
150 | | eluzle 9499 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈
(ℤ≥‘(𝑛 + 1)) → (𝑛 + 1) ≤ 𝑚) |
151 | 150 | adantl 275 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑛 + 1) ≤ 𝑚) |
152 | 121, 124,
125, 149, 151 | letrd 8043 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃 pCnt (𝑛 + 1)) ≤ 𝑚) |
153 | | eluz 9500 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 pCnt (𝑛 + 1)) ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑚 ∈
(ℤ≥‘(𝑃 pCnt (𝑛 + 1))) ↔ (𝑃 pCnt (𝑛 + 1)) ≤ 𝑚)) |
154 | 95, 110, 153 | syl2anc 409 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑚 ∈ (ℤ≥‘(𝑃 pCnt (𝑛 + 1))) ↔ (𝑃 pCnt (𝑛 + 1)) ≤ 𝑚)) |
155 | 152, 154 | mpbird 166 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → 𝑚 ∈ (ℤ≥‘(𝑃 pCnt (𝑛 + 1)))) |
156 | | fzss2 10020 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈
(ℤ≥‘(𝑃 pCnt (𝑛 + 1))) → (1...(𝑃 pCnt (𝑛 + 1))) ⊆ (1...𝑚)) |
157 | 155, 156 | syl 14 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (1...(𝑃 pCnt (𝑛 + 1))) ⊆ (1...𝑚)) |
158 | | elfzelz 9981 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (1...𝑚) → 𝑗 ∈ ℤ) |
159 | 158 | adantl 275 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑗 ∈ (1...𝑚)) → 𝑗 ∈ ℤ) |
160 | | 1zzd 9239 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑗 ∈ (1...𝑚)) → 1 ∈ ℤ) |
161 | 95 | adantr 274 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑗 ∈ (1...𝑚)) → (𝑃 pCnt (𝑛 + 1)) ∈ ℤ) |
162 | | fzdcel 9996 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ ℤ ∧ 1 ∈
ℤ ∧ (𝑃 pCnt
(𝑛 + 1)) ∈ ℤ)
→ DECID 𝑗 ∈ (1...(𝑃 pCnt (𝑛 + 1)))) |
163 | 159, 160,
161, 162 | syl3anc 1233 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑗 ∈ (1...𝑚)) → DECID 𝑗 ∈ (1...(𝑃 pCnt (𝑛 + 1)))) |
164 | 163 | ralrimiva 2543 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ∀𝑗 ∈ (1...𝑚)DECID 𝑗 ∈ (1...(𝑃 pCnt (𝑛 + 1)))) |
165 | | sumhashdc 12299 |
. . . . . . . . . . . . . . . 16
⊢
(((1...𝑚) ∈ Fin
∧ (1...(𝑃 pCnt (𝑛 + 1))) ⊆ (1...𝑚) ∧ ∀𝑗 ∈ (1...𝑚)DECID 𝑗 ∈ (1...(𝑃 pCnt (𝑛 + 1)))) → Σ𝑘 ∈ (1...𝑚)if(𝑘 ∈ (1...(𝑃 pCnt (𝑛 + 1))), 1, 0) = (♯‘(1...(𝑃 pCnt (𝑛 + 1))))) |
166 | 111, 157,
164, 165 | syl3anc 1233 |
. . . . . . . . . . . . . . 15
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → Σ𝑘 ∈ (1...𝑚)if(𝑘 ∈ (1...(𝑃 pCnt (𝑛 + 1))), 1, 0) = (♯‘(1...(𝑃 pCnt (𝑛 + 1))))) |
167 | | hashfz1 10717 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 pCnt (𝑛 + 1)) ∈ ℕ0 →
(♯‘(1...(𝑃 pCnt
(𝑛 + 1)))) = (𝑃 pCnt (𝑛 + 1))) |
168 | 94, 167 | syl 14 |
. . . . . . . . . . . . . . 15
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (♯‘(1...(𝑃 pCnt (𝑛 + 1)))) = (𝑃 pCnt (𝑛 + 1))) |
169 | 166, 168 | eqtrd 2203 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → Σ𝑘 ∈ (1...𝑚)if(𝑘 ∈ (1...(𝑃 pCnt (𝑛 + 1))), 1, 0) = (𝑃 pCnt (𝑛 + 1))) |
170 | 107, 120,
169 | 3eqtr3d 2211 |
. . . . . . . . . . . . 13
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))) − Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘)))) = (𝑃 pCnt (𝑛 + 1))) |
171 | 111, 115 | fsumcl 11363 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))) ∈ ℂ) |
172 | 111, 119 | fsumcl 11363 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) ∈ ℂ) |
173 | 94 | nn0cnd 9190 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃 pCnt (𝑛 + 1)) ∈ ℂ) |
174 | 171, 172,
173 | subaddd 8248 |
. . . . . . . . . . . . 13
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))) − Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘)))) = (𝑃 pCnt (𝑛 + 1)) ↔ (Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) + (𝑃 pCnt (𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))))) |
175 | 170, 174 | mpbid 146 |
. . . . . . . . . . . 12
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) + (𝑃 pCnt (𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘)))) |
176 | 83, 175 | eqeq12d 2185 |
. . . . . . . . . . 11
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (((𝑃 pCnt (!‘𝑛)) + (𝑃 pCnt (𝑛 + 1))) = (Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) + (𝑃 pCnt (𝑛 + 1))) ↔ (𝑃 pCnt (!‘(𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))))) |
177 | 65, 176 | syl5ib 153 |
. . . . . . . . . 10
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) → (𝑃 pCnt (!‘(𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))))) |
178 | 177 | ralimdva 2537 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
→ (∀𝑚 ∈
(ℤ≥‘(𝑛 + 1))(𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) → ∀𝑚 ∈ (ℤ≥‘(𝑛 + 1))(𝑃 pCnt (!‘(𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))))) |
179 | 64, 178 | syld 45 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
→ (∀𝑚 ∈
(ℤ≥‘𝑛)(𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) → ∀𝑚 ∈ (ℤ≥‘(𝑛 + 1))(𝑃 pCnt (!‘(𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))))) |
180 | 179 | ex 114 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0
→ (𝑃 ∈ ℙ
→ (∀𝑚 ∈
(ℤ≥‘𝑛)(𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) → ∀𝑚 ∈ (ℤ≥‘(𝑛 + 1))(𝑃 pCnt (!‘(𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘)))))) |
181 | 180 | a2d 26 |
. . . . . 6
⊢ (𝑛 ∈ ℕ0
→ ((𝑃 ∈ ℙ
→ ∀𝑚 ∈
(ℤ≥‘𝑛)(𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘)))) → (𝑃 ∈ ℙ → ∀𝑚 ∈
(ℤ≥‘(𝑛 + 1))(𝑃 pCnt (!‘(𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘)))))) |
182 | 8, 16, 24, 32, 56, 181 | nn0ind 9326 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (𝑃 ∈ ℙ
→ ∀𝑚 ∈
(ℤ≥‘𝑁)(𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑁 / (𝑃↑𝑘))))) |
183 | 182 | imp 123 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
→ ∀𝑚 ∈
(ℤ≥‘𝑁)(𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑁 / (𝑃↑𝑘)))) |
184 | | oveq2 5861 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → (1...𝑚) = (1...𝑀)) |
185 | 184 | sumeq1d 11329 |
. . . . . 6
⊢ (𝑚 = 𝑀 → Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑁 / (𝑃↑𝑘))) = Σ𝑘 ∈ (1...𝑀)(⌊‘(𝑁 / (𝑃↑𝑘)))) |
186 | 185 | eqeq2d 2182 |
. . . . 5
⊢ (𝑚 = 𝑀 → ((𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑁 / (𝑃↑𝑘))) ↔ (𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑀)(⌊‘(𝑁 / (𝑃↑𝑘))))) |
187 | 186 | rspcv 2830 |
. . . 4
⊢ (𝑀 ∈
(ℤ≥‘𝑁) → (∀𝑚 ∈ (ℤ≥‘𝑁)(𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑁 / (𝑃↑𝑘))) → (𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑀)(⌊‘(𝑁 / (𝑃↑𝑘))))) |
188 | 183, 187 | syl5 32 |
. . 3
⊢ (𝑀 ∈
(ℤ≥‘𝑁) → ((𝑁 ∈ ℕ0 ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑀)(⌊‘(𝑁 / (𝑃↑𝑘))))) |
189 | 188 | 3impib 1196 |
. 2
⊢ ((𝑀 ∈
(ℤ≥‘𝑁) ∧ 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑀)(⌊‘(𝑁 / (𝑃↑𝑘)))) |
190 | 189 | 3com12 1202 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
(ℤ≥‘𝑁) ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑀)(⌊‘(𝑁 / (𝑃↑𝑘)))) |