Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑥 = 0 →
(ℤ≥‘𝑥) =
(ℤ≥‘0)) |
2 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑥 = 0 → (!‘𝑥) =
(!‘0)) |
3 | 2 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (𝑃 pCnt (!‘𝑥)) = (𝑃 pCnt (!‘0))) |
4 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑥 = 0 → (𝑥 / (𝑃↑𝑘)) = (0 / (𝑃↑𝑘))) |
5 | 4 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑥 = 0 →
(⌊‘(𝑥 / (𝑃↑𝑘))) = (⌊‘(0 / (𝑃↑𝑘)))) |
6 | 5 | sumeq2sdv 14435 |
. . . . . . . . 9
⊢ (𝑥 = 0 → Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) = Σ𝑘 ∈ (1...𝑚)(⌊‘(0 / (𝑃↑𝑘)))) |
7 | 3, 6 | eqeq12d 2637 |
. . . . . . . 8
⊢ (𝑥 = 0 → ((𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) ↔ (𝑃 pCnt (!‘0)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(0 / (𝑃↑𝑘))))) |
8 | 1, 7 | raleqbidv 3152 |
. . . . . . 7
⊢ (𝑥 = 0 → (∀𝑚 ∈
(ℤ≥‘𝑥)(𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) ↔ ∀𝑚 ∈
(ℤ≥‘0)(𝑃 pCnt (!‘0)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(0 / (𝑃↑𝑘))))) |
9 | 8 | imbi2d 330 |
. . . . . 6
⊢ (𝑥 = 0 → ((𝑃 ∈ ℙ → ∀𝑚 ∈
(ℤ≥‘𝑥)(𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘)))) ↔ (𝑃 ∈ ℙ → ∀𝑚 ∈
(ℤ≥‘0)(𝑃 pCnt (!‘0)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(0 / (𝑃↑𝑘)))))) |
10 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑥 = 𝑛 → (ℤ≥‘𝑥) =
(ℤ≥‘𝑛)) |
11 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑛 → (!‘𝑥) = (!‘𝑛)) |
12 | 11 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝑥 = 𝑛 → (𝑃 pCnt (!‘𝑥)) = (𝑃 pCnt (!‘𝑛))) |
13 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑛 → (𝑥 / (𝑃↑𝑘)) = (𝑛 / (𝑃↑𝑘))) |
14 | 13 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑛 → (⌊‘(𝑥 / (𝑃↑𝑘))) = (⌊‘(𝑛 / (𝑃↑𝑘)))) |
15 | 14 | sumeq2sdv 14435 |
. . . . . . . . 9
⊢ (𝑥 = 𝑛 → Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘)))) |
16 | 12, 15 | eqeq12d 2637 |
. . . . . . . 8
⊢ (𝑥 = 𝑛 → ((𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) ↔ (𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))))) |
17 | 10, 16 | raleqbidv 3152 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (∀𝑚 ∈ (ℤ≥‘𝑥)(𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) ↔ ∀𝑚 ∈ (ℤ≥‘𝑛)(𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))))) |
18 | 17 | imbi2d 330 |
. . . . . 6
⊢ (𝑥 = 𝑛 → ((𝑃 ∈ ℙ → ∀𝑚 ∈
(ℤ≥‘𝑥)(𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘)))) ↔ (𝑃 ∈ ℙ → ∀𝑚 ∈
(ℤ≥‘𝑛)(𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘)))))) |
19 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑥 = (𝑛 + 1) →
(ℤ≥‘𝑥) = (ℤ≥‘(𝑛 + 1))) |
20 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑛 + 1) → (!‘𝑥) = (!‘(𝑛 + 1))) |
21 | 20 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝑥 = (𝑛 + 1) → (𝑃 pCnt (!‘𝑥)) = (𝑃 pCnt (!‘(𝑛 + 1)))) |
22 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑛 + 1) → (𝑥 / (𝑃↑𝑘)) = ((𝑛 + 1) / (𝑃↑𝑘))) |
23 | 22 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑛 + 1) → (⌊‘(𝑥 / (𝑃↑𝑘))) = (⌊‘((𝑛 + 1) / (𝑃↑𝑘)))) |
24 | 23 | sumeq2sdv 14435 |
. . . . . . . . 9
⊢ (𝑥 = (𝑛 + 1) → Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘)))) |
25 | 21, 24 | eqeq12d 2637 |
. . . . . . . 8
⊢ (𝑥 = (𝑛 + 1) → ((𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) ↔ (𝑃 pCnt (!‘(𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))))) |
26 | 19, 25 | raleqbidv 3152 |
. . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → (∀𝑚 ∈ (ℤ≥‘𝑥)(𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) ↔ ∀𝑚 ∈ (ℤ≥‘(𝑛 + 1))(𝑃 pCnt (!‘(𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))))) |
27 | 26 | imbi2d 330 |
. . . . . 6
⊢ (𝑥 = (𝑛 + 1) → ((𝑃 ∈ ℙ → ∀𝑚 ∈
(ℤ≥‘𝑥)(𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘)))) ↔ (𝑃 ∈ ℙ → ∀𝑚 ∈
(ℤ≥‘(𝑛 + 1))(𝑃 pCnt (!‘(𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘)))))) |
28 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → (ℤ≥‘𝑥) =
(ℤ≥‘𝑁)) |
29 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑁 → (!‘𝑥) = (!‘𝑁)) |
30 | 29 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝑥 = 𝑁 → (𝑃 pCnt (!‘𝑥)) = (𝑃 pCnt (!‘𝑁))) |
31 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑁 → (𝑥 / (𝑃↑𝑘)) = (𝑁 / (𝑃↑𝑘))) |
32 | 31 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑁 → (⌊‘(𝑥 / (𝑃↑𝑘))) = (⌊‘(𝑁 / (𝑃↑𝑘)))) |
33 | 32 | sumeq2sdv 14435 |
. . . . . . . . 9
⊢ (𝑥 = 𝑁 → Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑁 / (𝑃↑𝑘)))) |
34 | 30, 33 | eqeq12d 2637 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → ((𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) ↔ (𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑁 / (𝑃↑𝑘))))) |
35 | 28, 34 | raleqbidv 3152 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (∀𝑚 ∈ (ℤ≥‘𝑥)(𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) ↔ ∀𝑚 ∈ (ℤ≥‘𝑁)(𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑁 / (𝑃↑𝑘))))) |
36 | 35 | imbi2d 330 |
. . . . . 6
⊢ (𝑥 = 𝑁 → ((𝑃 ∈ ℙ → ∀𝑚 ∈
(ℤ≥‘𝑥)(𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘)))) ↔ (𝑃 ∈ ℙ → ∀𝑚 ∈
(ℤ≥‘𝑁)(𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑁 / (𝑃↑𝑘)))))) |
37 | | fzfid 12772 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝑚 ∈
(ℤ≥‘0)) → (1...𝑚) ∈ Fin) |
38 | | sumz 14453 |
. . . . . . . . . 10
⊢
(((1...𝑚) ⊆
(ℤ≥‘1) ∨ (1...𝑚) ∈ Fin) → Σ𝑘 ∈ (1...𝑚)0 = 0) |
39 | 38 | olcs 410 |
. . . . . . . . 9
⊢
((1...𝑚) ∈ Fin
→ Σ𝑘 ∈
(1...𝑚)0 =
0) |
40 | 37, 39 | syl 17 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑚 ∈
(ℤ≥‘0)) → Σ𝑘 ∈ (1...𝑚)0 = 0) |
41 | | 0nn0 11307 |
. . . . . . . . . . 11
⊢ 0 ∈
ℕ0 |
42 | 41 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝑚 ∈
(ℤ≥‘0)) ∧ 𝑘 ∈ (1...𝑚)) → 0 ∈
ℕ0) |
43 | | elfznn 12370 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1...𝑚) → 𝑘 ∈ ℕ) |
44 | 43 | nnnn0d 11351 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...𝑚) → 𝑘 ∈ ℕ0) |
45 | | nn0uz 11722 |
. . . . . . . . . . . 12
⊢
ℕ0 = (ℤ≥‘0) |
46 | 44, 45 | syl6eleq 2711 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...𝑚) → 𝑘 ∈
(ℤ≥‘0)) |
47 | 46 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝑚 ∈
(ℤ≥‘0)) ∧ 𝑘 ∈ (1...𝑚)) → 𝑘 ∈
(ℤ≥‘0)) |
48 | | simpll 790 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝑚 ∈
(ℤ≥‘0)) ∧ 𝑘 ∈ (1...𝑚)) → 𝑃 ∈ ℙ) |
49 | | pcfaclem 15602 |
. . . . . . . . . 10
⊢ ((0
∈ ℕ0 ∧ 𝑘 ∈ (ℤ≥‘0)
∧ 𝑃 ∈ ℙ)
→ (⌊‘(0 / (𝑃↑𝑘))) = 0) |
50 | 42, 47, 48, 49 | syl3anc 1326 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝑚 ∈
(ℤ≥‘0)) ∧ 𝑘 ∈ (1...𝑚)) → (⌊‘(0 / (𝑃↑𝑘))) = 0) |
51 | 50 | sumeq2dv 14433 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑚 ∈
(ℤ≥‘0)) → Σ𝑘 ∈ (1...𝑚)(⌊‘(0 / (𝑃↑𝑘))) = Σ𝑘 ∈ (1...𝑚)0) |
52 | | fac0 13063 |
. . . . . . . . . . 11
⊢
(!‘0) = 1 |
53 | 52 | oveq2i 6661 |
. . . . . . . . . 10
⊢ (𝑃 pCnt (!‘0)) = (𝑃 pCnt 1) |
54 | | pc1 15560 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → (𝑃 pCnt 1) = 0) |
55 | 53, 54 | syl5eq 2668 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → (𝑃 pCnt (!‘0)) =
0) |
56 | 55 | adantr 481 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑚 ∈
(ℤ≥‘0)) → (𝑃 pCnt (!‘0)) = 0) |
57 | 40, 51, 56 | 3eqtr4rd 2667 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑚 ∈
(ℤ≥‘0)) → (𝑃 pCnt (!‘0)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(0 / (𝑃↑𝑘)))) |
58 | 57 | ralrimiva 2966 |
. . . . . 6
⊢ (𝑃 ∈ ℙ →
∀𝑚 ∈
(ℤ≥‘0)(𝑃 pCnt (!‘0)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(0 / (𝑃↑𝑘)))) |
59 | | nn0z 11400 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℤ) |
60 | 59 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
→ 𝑛 ∈
ℤ) |
61 | | uzid 11702 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
(ℤ≥‘𝑛)) |
62 | | peano2uz 11741 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(ℤ≥‘𝑛) → (𝑛 + 1) ∈
(ℤ≥‘𝑛)) |
63 | 60, 61, 62 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
→ (𝑛 + 1) ∈
(ℤ≥‘𝑛)) |
64 | | uzss 11708 |
. . . . . . . . . 10
⊢ ((𝑛 + 1) ∈
(ℤ≥‘𝑛) → (ℤ≥‘(𝑛 + 1)) ⊆
(ℤ≥‘𝑛)) |
65 | | ssralv 3666 |
. . . . . . . . . 10
⊢
((ℤ≥‘(𝑛 + 1)) ⊆
(ℤ≥‘𝑛) → (∀𝑚 ∈ (ℤ≥‘𝑛)(𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) → ∀𝑚 ∈ (ℤ≥‘(𝑛 + 1))(𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))))) |
66 | 63, 64, 65 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
→ (∀𝑚 ∈
(ℤ≥‘𝑛)(𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) → ∀𝑚 ∈ (ℤ≥‘(𝑛 + 1))(𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))))) |
67 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ ((𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) → ((𝑃 pCnt (!‘𝑛)) + (𝑃 pCnt (𝑛 + 1))) = (Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) + (𝑃 pCnt (𝑛 + 1)))) |
68 | | simpll 790 |
. . . . . . . . . . . . . . 15
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → 𝑛 ∈ ℕ0) |
69 | | facp1 13065 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ0
→ (!‘(𝑛 + 1)) =
((!‘𝑛) ·
(𝑛 + 1))) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (!‘(𝑛 + 1)) = ((!‘𝑛) · (𝑛 + 1))) |
71 | 70 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃 pCnt (!‘(𝑛 + 1))) = (𝑃 pCnt ((!‘𝑛) · (𝑛 + 1)))) |
72 | | simplr 792 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → 𝑃 ∈ ℙ) |
73 | | faccl 13070 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ0
→ (!‘𝑛) ∈
ℕ) |
74 | | nnz 11399 |
. . . . . . . . . . . . . . . 16
⊢
((!‘𝑛) ∈
ℕ → (!‘𝑛)
∈ ℤ) |
75 | | nnne0 11053 |
. . . . . . . . . . . . . . . 16
⊢
((!‘𝑛) ∈
ℕ → (!‘𝑛)
≠ 0) |
76 | 74, 75 | jca 554 |
. . . . . . . . . . . . . . 15
⊢
((!‘𝑛) ∈
ℕ → ((!‘𝑛)
∈ ℤ ∧ (!‘𝑛) ≠ 0)) |
77 | 68, 73, 76 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((!‘𝑛) ∈ ℤ ∧ (!‘𝑛) ≠ 0)) |
78 | | nn0p1nn 11332 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ0
→ (𝑛 + 1) ∈
ℕ) |
79 | | nnz 11399 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 + 1) ∈ ℕ →
(𝑛 + 1) ∈
ℤ) |
80 | | nnne0 11053 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 + 1) ∈ ℕ →
(𝑛 + 1) ≠
0) |
81 | 79, 80 | jca 554 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 + 1) ∈ ℕ →
((𝑛 + 1) ∈ ℤ
∧ (𝑛 + 1) ≠
0)) |
82 | 68, 78, 81 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((𝑛 + 1) ∈ ℤ ∧ (𝑛 + 1) ≠ 0)) |
83 | | pcmul 15556 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧
((!‘𝑛) ∈ ℤ
∧ (!‘𝑛) ≠ 0)
∧ ((𝑛 + 1) ∈
ℤ ∧ (𝑛 + 1) ≠
0)) → (𝑃 pCnt
((!‘𝑛) ·
(𝑛 + 1))) = ((𝑃 pCnt (!‘𝑛)) + (𝑃 pCnt (𝑛 + 1)))) |
84 | 72, 77, 82, 83 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃 pCnt ((!‘𝑛) · (𝑛 + 1))) = ((𝑃 pCnt (!‘𝑛)) + (𝑃 pCnt (𝑛 + 1)))) |
85 | 71, 84 | eqtr2d 2657 |
. . . . . . . . . . . 12
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((𝑃 pCnt (!‘𝑛)) + (𝑃 pCnt (𝑛 + 1))) = (𝑃 pCnt (!‘(𝑛 + 1)))) |
86 | 68 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → 𝑛 ∈ ℕ0) |
87 | 86 | nn0zd 11480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → 𝑛 ∈ ℤ) |
88 | | prmnn 15388 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
89 | 88 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → 𝑃 ∈ ℕ) |
90 | | nnexpcl 12873 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑃↑𝑘) ∈
ℕ) |
91 | 89, 44, 90 | syl2an 494 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → (𝑃↑𝑘) ∈ ℕ) |
92 | | fldivp1 15601 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℤ ∧ (𝑃↑𝑘) ∈ ℕ) →
((⌊‘((𝑛 + 1) /
(𝑃↑𝑘))) − (⌊‘(𝑛 / (𝑃↑𝑘)))) = if((𝑃↑𝑘) ∥ (𝑛 + 1), 1, 0)) |
93 | 87, 91, 92 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → ((⌊‘((𝑛 + 1) / (𝑃↑𝑘))) − (⌊‘(𝑛 / (𝑃↑𝑘)))) = if((𝑃↑𝑘) ∥ (𝑛 + 1), 1, 0)) |
94 | | elfzuz 12338 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ (1...𝑚) → 𝑘 ∈
(ℤ≥‘1)) |
95 | 68, 78 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑛 + 1) ∈ ℕ) |
96 | 72, 95 | pccld 15555 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃 pCnt (𝑛 + 1)) ∈
ℕ0) |
97 | 96 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃 pCnt (𝑛 + 1)) ∈ ℤ) |
98 | | elfz5 12334 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈
(ℤ≥‘1) ∧ (𝑃 pCnt (𝑛 + 1)) ∈ ℤ) → (𝑘 ∈ (1...(𝑃 pCnt (𝑛 + 1))) ↔ 𝑘 ≤ (𝑃 pCnt (𝑛 + 1)))) |
99 | 94, 97, 98 | syl2anr 495 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → (𝑘 ∈ (1...(𝑃 pCnt (𝑛 + 1))) ↔ 𝑘 ≤ (𝑃 pCnt (𝑛 + 1)))) |
100 | | simpllr 799 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → 𝑃 ∈ ℙ) |
101 | 86, 78 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → (𝑛 + 1) ∈ ℕ) |
102 | 101 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → (𝑛 + 1) ∈ ℤ) |
103 | 44 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → 𝑘 ∈ ℕ0) |
104 | | pcdvdsb 15573 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ ℙ ∧ (𝑛 + 1) ∈ ℤ ∧ 𝑘 ∈ ℕ0)
→ (𝑘 ≤ (𝑃 pCnt (𝑛 + 1)) ↔ (𝑃↑𝑘) ∥ (𝑛 + 1))) |
105 | 100, 102,
103, 104 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → (𝑘 ≤ (𝑃 pCnt (𝑛 + 1)) ↔ (𝑃↑𝑘) ∥ (𝑛 + 1))) |
106 | 99, 105 | bitr2d 269 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → ((𝑃↑𝑘) ∥ (𝑛 + 1) ↔ 𝑘 ∈ (1...(𝑃 pCnt (𝑛 + 1))))) |
107 | 106 | ifbid 4108 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → if((𝑃↑𝑘) ∥ (𝑛 + 1), 1, 0) = if(𝑘 ∈ (1...(𝑃 pCnt (𝑛 + 1))), 1, 0)) |
108 | 93, 107 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → ((⌊‘((𝑛 + 1) / (𝑃↑𝑘))) − (⌊‘(𝑛 / (𝑃↑𝑘)))) = if(𝑘 ∈ (1...(𝑃 pCnt (𝑛 + 1))), 1, 0)) |
109 | 108 | sumeq2dv 14433 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → Σ𝑘 ∈ (1...𝑚)((⌊‘((𝑛 + 1) / (𝑃↑𝑘))) − (⌊‘(𝑛 / (𝑃↑𝑘)))) = Σ𝑘 ∈ (1...𝑚)if(𝑘 ∈ (1...(𝑃 pCnt (𝑛 + 1))), 1, 0)) |
110 | | fzfid 12772 |
. . . . . . . . . . . . . . 15
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (1...𝑚) ∈ Fin) |
111 | 68 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → 𝑛 ∈ ℝ) |
112 | | peano2re 10209 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℝ → (𝑛 + 1) ∈
ℝ) |
113 | 111, 112 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑛 + 1) ∈ ℝ) |
114 | 113 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → (𝑛 + 1) ∈ ℝ) |
115 | 114, 91 | nndivred 11069 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → ((𝑛 + 1) / (𝑃↑𝑘)) ∈ ℝ) |
116 | 115 | flcld 12599 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → (⌊‘((𝑛 + 1) / (𝑃↑𝑘))) ∈ ℤ) |
117 | 116 | zcnd 11483 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → (⌊‘((𝑛 + 1) / (𝑃↑𝑘))) ∈ ℂ) |
118 | 111 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → 𝑛 ∈ ℝ) |
119 | 118, 91 | nndivred 11069 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → (𝑛 / (𝑃↑𝑘)) ∈ ℝ) |
120 | 119 | flcld 12599 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → (⌊‘(𝑛 / (𝑃↑𝑘))) ∈ ℤ) |
121 | 120 | zcnd 11483 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → (⌊‘(𝑛 / (𝑃↑𝑘))) ∈ ℂ) |
122 | 110, 117,
121 | fsumsub 14520 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → Σ𝑘 ∈ (1...𝑚)((⌊‘((𝑛 + 1) / (𝑃↑𝑘))) − (⌊‘(𝑛 / (𝑃↑𝑘)))) = (Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))) − Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))))) |
123 | | fzfi 12771 |
. . . . . . . . . . . . . . . 16
⊢
(1...𝑚) ∈
Fin |
124 | 96 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃 pCnt (𝑛 + 1)) ∈ ℝ) |
125 | | eluzelz 11697 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 ∈
(ℤ≥‘(𝑛 + 1)) → 𝑚 ∈ ℤ) |
126 | 125 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → 𝑚 ∈ ℤ) |
127 | 126 | zred 11482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → 𝑚 ∈ ℝ) |
128 | | prmuz2 15408 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
129 | 128 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → 𝑃 ∈
(ℤ≥‘2)) |
130 | 95 | nnnn0d 11351 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑛 + 1) ∈
ℕ0) |
131 | | bernneq3 12992 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑛 + 1) ∈ ℕ0) →
(𝑛 + 1) < (𝑃↑(𝑛 + 1))) |
132 | 129, 130,
131 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑛 + 1) < (𝑃↑(𝑛 + 1))) |
133 | 124, 113 | letrid 10189 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((𝑃 pCnt (𝑛 + 1)) ≤ (𝑛 + 1) ∨ (𝑛 + 1) ≤ (𝑃 pCnt (𝑛 + 1)))) |
134 | 133 | ord 392 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (¬ (𝑃 pCnt (𝑛 + 1)) ≤ (𝑛 + 1) → (𝑛 + 1) ≤ (𝑃 pCnt (𝑛 + 1)))) |
135 | 95 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑛 + 1) ∈ ℤ) |
136 | | pcdvdsb 15573 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃 ∈ ℙ ∧ (𝑛 + 1) ∈ ℤ ∧
(𝑛 + 1) ∈
ℕ0) → ((𝑛 + 1) ≤ (𝑃 pCnt (𝑛 + 1)) ↔ (𝑃↑(𝑛 + 1)) ∥ (𝑛 + 1))) |
137 | 72, 135, 130, 136 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((𝑛 + 1) ≤ (𝑃 pCnt (𝑛 + 1)) ↔ (𝑃↑(𝑛 + 1)) ∥ (𝑛 + 1))) |
138 | 89, 130 | nnexpcld 13030 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃↑(𝑛 + 1)) ∈ ℕ) |
139 | 138 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃↑(𝑛 + 1)) ∈ ℤ) |
140 | | dvdsle 15032 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑃↑(𝑛 + 1)) ∈ ℤ ∧ (𝑛 + 1) ∈ ℕ) →
((𝑃↑(𝑛 + 1)) ∥ (𝑛 + 1) → (𝑃↑(𝑛 + 1)) ≤ (𝑛 + 1))) |
141 | 139, 95, 140 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((𝑃↑(𝑛 + 1)) ∥ (𝑛 + 1) → (𝑃↑(𝑛 + 1)) ≤ (𝑛 + 1))) |
142 | 138 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃↑(𝑛 + 1)) ∈ ℝ) |
143 | 142, 113 | lenltd 10183 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((𝑃↑(𝑛 + 1)) ≤ (𝑛 + 1) ↔ ¬ (𝑛 + 1) < (𝑃↑(𝑛 + 1)))) |
144 | 141, 143 | sylibd 229 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((𝑃↑(𝑛 + 1)) ∥ (𝑛 + 1) → ¬ (𝑛 + 1) < (𝑃↑(𝑛 + 1)))) |
145 | 137, 144 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((𝑛 + 1) ≤ (𝑃 pCnt (𝑛 + 1)) → ¬ (𝑛 + 1) < (𝑃↑(𝑛 + 1)))) |
146 | 134, 145 | syld 47 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (¬ (𝑃 pCnt (𝑛 + 1)) ≤ (𝑛 + 1) → ¬ (𝑛 + 1) < (𝑃↑(𝑛 + 1)))) |
147 | 132, 146 | mt4d 152 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃 pCnt (𝑛 + 1)) ≤ (𝑛 + 1)) |
148 | | eluzle 11700 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈
(ℤ≥‘(𝑛 + 1)) → (𝑛 + 1) ≤ 𝑚) |
149 | 148 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑛 + 1) ≤ 𝑚) |
150 | 124, 113,
127, 147, 149 | letrd 10194 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃 pCnt (𝑛 + 1)) ≤ 𝑚) |
151 | | eluz 11701 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 pCnt (𝑛 + 1)) ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑚 ∈
(ℤ≥‘(𝑃 pCnt (𝑛 + 1))) ↔ (𝑃 pCnt (𝑛 + 1)) ≤ 𝑚)) |
152 | 97, 126, 151 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑚 ∈ (ℤ≥‘(𝑃 pCnt (𝑛 + 1))) ↔ (𝑃 pCnt (𝑛 + 1)) ≤ 𝑚)) |
153 | 150, 152 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → 𝑚 ∈ (ℤ≥‘(𝑃 pCnt (𝑛 + 1)))) |
154 | | fzss2 12381 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈
(ℤ≥‘(𝑃 pCnt (𝑛 + 1))) → (1...(𝑃 pCnt (𝑛 + 1))) ⊆ (1...𝑚)) |
155 | 153, 154 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (1...(𝑃 pCnt (𝑛 + 1))) ⊆ (1...𝑚)) |
156 | | sumhash 15600 |
. . . . . . . . . . . . . . . 16
⊢
(((1...𝑚) ∈ Fin
∧ (1...(𝑃 pCnt (𝑛 + 1))) ⊆ (1...𝑚)) → Σ𝑘 ∈ (1...𝑚)if(𝑘 ∈ (1...(𝑃 pCnt (𝑛 + 1))), 1, 0) = (#‘(1...(𝑃 pCnt (𝑛 + 1))))) |
157 | 123, 155,
156 | sylancr 695 |
. . . . . . . . . . . . . . 15
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → Σ𝑘 ∈ (1...𝑚)if(𝑘 ∈ (1...(𝑃 pCnt (𝑛 + 1))), 1, 0) = (#‘(1...(𝑃 pCnt (𝑛 + 1))))) |
158 | | hashfz1 13134 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 pCnt (𝑛 + 1)) ∈ ℕ0 →
(#‘(1...(𝑃 pCnt
(𝑛 + 1)))) = (𝑃 pCnt (𝑛 + 1))) |
159 | 96, 158 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (#‘(1...(𝑃 pCnt (𝑛 + 1)))) = (𝑃 pCnt (𝑛 + 1))) |
160 | 157, 159 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → Σ𝑘 ∈ (1...𝑚)if(𝑘 ∈ (1...(𝑃 pCnt (𝑛 + 1))), 1, 0) = (𝑃 pCnt (𝑛 + 1))) |
161 | 109, 122,
160 | 3eqtr3d 2664 |
. . . . . . . . . . . . 13
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))) − Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘)))) = (𝑃 pCnt (𝑛 + 1))) |
162 | 110, 117 | fsumcl 14464 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))) ∈ ℂ) |
163 | 110, 121 | fsumcl 14464 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) ∈ ℂ) |
164 | 124 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃 pCnt (𝑛 + 1)) ∈ ℂ) |
165 | 162, 163,
164 | subaddd 10410 |
. . . . . . . . . . . . 13
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))) − Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘)))) = (𝑃 pCnt (𝑛 + 1)) ↔ (Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) + (𝑃 pCnt (𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))))) |
166 | 161, 165 | mpbid 222 |
. . . . . . . . . . . 12
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) + (𝑃 pCnt (𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘)))) |
167 | 85, 166 | eqeq12d 2637 |
. . . . . . . . . . 11
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (((𝑃 pCnt (!‘𝑛)) + (𝑃 pCnt (𝑛 + 1))) = (Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) + (𝑃 pCnt (𝑛 + 1))) ↔ (𝑃 pCnt (!‘(𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))))) |
168 | 67, 167 | syl5ib 234 |
. . . . . . . . . 10
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) → (𝑃 pCnt (!‘(𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))))) |
169 | 168 | ralimdva 2962 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
→ (∀𝑚 ∈
(ℤ≥‘(𝑛 + 1))(𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) → ∀𝑚 ∈ (ℤ≥‘(𝑛 + 1))(𝑃 pCnt (!‘(𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))))) |
170 | 66, 169 | syld 47 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
→ (∀𝑚 ∈
(ℤ≥‘𝑛)(𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) → ∀𝑚 ∈ (ℤ≥‘(𝑛 + 1))(𝑃 pCnt (!‘(𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))))) |
171 | 170 | ex 450 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0
→ (𝑃 ∈ ℙ
→ (∀𝑚 ∈
(ℤ≥‘𝑛)(𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) → ∀𝑚 ∈ (ℤ≥‘(𝑛 + 1))(𝑃 pCnt (!‘(𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘)))))) |
172 | 171 | a2d 29 |
. . . . . 6
⊢ (𝑛 ∈ ℕ0
→ ((𝑃 ∈ ℙ
→ ∀𝑚 ∈
(ℤ≥‘𝑛)(𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘)))) → (𝑃 ∈ ℙ → ∀𝑚 ∈
(ℤ≥‘(𝑛 + 1))(𝑃 pCnt (!‘(𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘)))))) |
173 | 9, 18, 27, 36, 58, 172 | nn0ind 11472 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (𝑃 ∈ ℙ
→ ∀𝑚 ∈
(ℤ≥‘𝑁)(𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑁 / (𝑃↑𝑘))))) |
174 | 173 | imp 445 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
→ ∀𝑚 ∈
(ℤ≥‘𝑁)(𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑁 / (𝑃↑𝑘)))) |
175 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → (1...𝑚) = (1...𝑀)) |
176 | 175 | sumeq1d 14431 |
. . . . . 6
⊢ (𝑚 = 𝑀 → Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑁 / (𝑃↑𝑘))) = Σ𝑘 ∈ (1...𝑀)(⌊‘(𝑁 / (𝑃↑𝑘)))) |
177 | 176 | eqeq2d 2632 |
. . . . 5
⊢ (𝑚 = 𝑀 → ((𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑁 / (𝑃↑𝑘))) ↔ (𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑀)(⌊‘(𝑁 / (𝑃↑𝑘))))) |
178 | 177 | rspcv 3305 |
. . . 4
⊢ (𝑀 ∈
(ℤ≥‘𝑁) → (∀𝑚 ∈ (ℤ≥‘𝑁)(𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑁 / (𝑃↑𝑘))) → (𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑀)(⌊‘(𝑁 / (𝑃↑𝑘))))) |
179 | 174, 178 | syl5 34 |
. . 3
⊢ (𝑀 ∈
(ℤ≥‘𝑁) → ((𝑁 ∈ ℕ0 ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑀)(⌊‘(𝑁 / (𝑃↑𝑘))))) |
180 | 179 | 3impib 1262 |
. 2
⊢ ((𝑀 ∈
(ℤ≥‘𝑁) ∧ 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑀)(⌊‘(𝑁 / (𝑃↑𝑘)))) |
181 | 180 | 3com12 1269 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
(ℤ≥‘𝑁) ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑀)(⌊‘(𝑁 / (𝑃↑𝑘)))) |