| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑥 = 0 →
(ℤ≥‘𝑥) =
(ℤ≥‘0)) | 
| 2 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑥 = 0 → (!‘𝑥) =
(!‘0)) | 
| 3 | 2 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑥 = 0 → (𝑃 pCnt (!‘𝑥)) = (𝑃 pCnt (!‘0))) | 
| 4 |  | fvoveq1 7455 | . . . . . . . . . 10
⊢ (𝑥 = 0 →
(⌊‘(𝑥 / (𝑃↑𝑘))) = (⌊‘(0 / (𝑃↑𝑘)))) | 
| 5 | 4 | sumeq2sdv 15740 | . . . . . . . . 9
⊢ (𝑥 = 0 → Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) = Σ𝑘 ∈ (1...𝑚)(⌊‘(0 / (𝑃↑𝑘)))) | 
| 6 | 3, 5 | eqeq12d 2752 | . . . . . . . 8
⊢ (𝑥 = 0 → ((𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) ↔ (𝑃 pCnt (!‘0)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(0 / (𝑃↑𝑘))))) | 
| 7 | 1, 6 | raleqbidv 3345 | . . . . . . 7
⊢ (𝑥 = 0 → (∀𝑚 ∈
(ℤ≥‘𝑥)(𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) ↔ ∀𝑚 ∈
(ℤ≥‘0)(𝑃 pCnt (!‘0)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(0 / (𝑃↑𝑘))))) | 
| 8 | 7 | imbi2d 340 | . . . . . 6
⊢ (𝑥 = 0 → ((𝑃 ∈ ℙ → ∀𝑚 ∈
(ℤ≥‘𝑥)(𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘)))) ↔ (𝑃 ∈ ℙ → ∀𝑚 ∈
(ℤ≥‘0)(𝑃 pCnt (!‘0)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(0 / (𝑃↑𝑘)))))) | 
| 9 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑥 = 𝑛 → (ℤ≥‘𝑥) =
(ℤ≥‘𝑛)) | 
| 10 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑥 = 𝑛 → (!‘𝑥) = (!‘𝑛)) | 
| 11 | 10 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑥 = 𝑛 → (𝑃 pCnt (!‘𝑥)) = (𝑃 pCnt (!‘𝑛))) | 
| 12 |  | fvoveq1 7455 | . . . . . . . . . 10
⊢ (𝑥 = 𝑛 → (⌊‘(𝑥 / (𝑃↑𝑘))) = (⌊‘(𝑛 / (𝑃↑𝑘)))) | 
| 13 | 12 | sumeq2sdv 15740 | . . . . . . . . 9
⊢ (𝑥 = 𝑛 → Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘)))) | 
| 14 | 11, 13 | eqeq12d 2752 | . . . . . . . 8
⊢ (𝑥 = 𝑛 → ((𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) ↔ (𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))))) | 
| 15 | 9, 14 | raleqbidv 3345 | . . . . . . 7
⊢ (𝑥 = 𝑛 → (∀𝑚 ∈ (ℤ≥‘𝑥)(𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) ↔ ∀𝑚 ∈ (ℤ≥‘𝑛)(𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))))) | 
| 16 | 15 | imbi2d 340 | . . . . . 6
⊢ (𝑥 = 𝑛 → ((𝑃 ∈ ℙ → ∀𝑚 ∈
(ℤ≥‘𝑥)(𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘)))) ↔ (𝑃 ∈ ℙ → ∀𝑚 ∈
(ℤ≥‘𝑛)(𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘)))))) | 
| 17 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑥 = (𝑛 + 1) →
(ℤ≥‘𝑥) = (ℤ≥‘(𝑛 + 1))) | 
| 18 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑥 = (𝑛 + 1) → (!‘𝑥) = (!‘(𝑛 + 1))) | 
| 19 | 18 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑥 = (𝑛 + 1) → (𝑃 pCnt (!‘𝑥)) = (𝑃 pCnt (!‘(𝑛 + 1)))) | 
| 20 |  | fvoveq1 7455 | . . . . . . . . . 10
⊢ (𝑥 = (𝑛 + 1) → (⌊‘(𝑥 / (𝑃↑𝑘))) = (⌊‘((𝑛 + 1) / (𝑃↑𝑘)))) | 
| 21 | 20 | sumeq2sdv 15740 | . . . . . . . . 9
⊢ (𝑥 = (𝑛 + 1) → Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘)))) | 
| 22 | 19, 21 | eqeq12d 2752 | . . . . . . . 8
⊢ (𝑥 = (𝑛 + 1) → ((𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) ↔ (𝑃 pCnt (!‘(𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))))) | 
| 23 | 17, 22 | raleqbidv 3345 | . . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → (∀𝑚 ∈ (ℤ≥‘𝑥)(𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) ↔ ∀𝑚 ∈ (ℤ≥‘(𝑛 + 1))(𝑃 pCnt (!‘(𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))))) | 
| 24 | 23 | imbi2d 340 | . . . . . 6
⊢ (𝑥 = (𝑛 + 1) → ((𝑃 ∈ ℙ → ∀𝑚 ∈
(ℤ≥‘𝑥)(𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘)))) ↔ (𝑃 ∈ ℙ → ∀𝑚 ∈
(ℤ≥‘(𝑛 + 1))(𝑃 pCnt (!‘(𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘)))))) | 
| 25 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑥 = 𝑁 → (ℤ≥‘𝑥) =
(ℤ≥‘𝑁)) | 
| 26 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑥 = 𝑁 → (!‘𝑥) = (!‘𝑁)) | 
| 27 | 26 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑥 = 𝑁 → (𝑃 pCnt (!‘𝑥)) = (𝑃 pCnt (!‘𝑁))) | 
| 28 |  | fvoveq1 7455 | . . . . . . . . . 10
⊢ (𝑥 = 𝑁 → (⌊‘(𝑥 / (𝑃↑𝑘))) = (⌊‘(𝑁 / (𝑃↑𝑘)))) | 
| 29 | 28 | sumeq2sdv 15740 | . . . . . . . . 9
⊢ (𝑥 = 𝑁 → Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑁 / (𝑃↑𝑘)))) | 
| 30 | 27, 29 | eqeq12d 2752 | . . . . . . . 8
⊢ (𝑥 = 𝑁 → ((𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) ↔ (𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑁 / (𝑃↑𝑘))))) | 
| 31 | 25, 30 | raleqbidv 3345 | . . . . . . 7
⊢ (𝑥 = 𝑁 → (∀𝑚 ∈ (ℤ≥‘𝑥)(𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘))) ↔ ∀𝑚 ∈ (ℤ≥‘𝑁)(𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑁 / (𝑃↑𝑘))))) | 
| 32 | 31 | imbi2d 340 | . . . . . 6
⊢ (𝑥 = 𝑁 → ((𝑃 ∈ ℙ → ∀𝑚 ∈
(ℤ≥‘𝑥)(𝑃 pCnt (!‘𝑥)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑥 / (𝑃↑𝑘)))) ↔ (𝑃 ∈ ℙ → ∀𝑚 ∈
(ℤ≥‘𝑁)(𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑁 / (𝑃↑𝑘)))))) | 
| 33 |  | fzfid 14015 | . . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝑚 ∈
(ℤ≥‘0)) → (1...𝑚) ∈ Fin) | 
| 34 |  | sumz 15759 | . . . . . . . . . 10
⊢
(((1...𝑚) ⊆
(ℤ≥‘1) ∨ (1...𝑚) ∈ Fin) → Σ𝑘 ∈ (1...𝑚)0 = 0) | 
| 35 | 34 | olcs 876 | . . . . . . . . 9
⊢
((1...𝑚) ∈ Fin
→ Σ𝑘 ∈
(1...𝑚)0 =
0) | 
| 36 | 33, 35 | syl 17 | . . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑚 ∈
(ℤ≥‘0)) → Σ𝑘 ∈ (1...𝑚)0 = 0) | 
| 37 |  | 0nn0 12543 | . . . . . . . . . 10
⊢ 0 ∈
ℕ0 | 
| 38 |  | elfznn 13594 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1...𝑚) → 𝑘 ∈ ℕ) | 
| 39 | 38 | nnnn0d 12589 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...𝑚) → 𝑘 ∈ ℕ0) | 
| 40 |  | nn0uz 12921 | . . . . . . . . . . . 12
⊢
ℕ0 = (ℤ≥‘0) | 
| 41 | 39, 40 | eleqtrdi 2850 | . . . . . . . . . . 11
⊢ (𝑘 ∈ (1...𝑚) → 𝑘 ∈
(ℤ≥‘0)) | 
| 42 | 41 | adantl 481 | . . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝑚 ∈
(ℤ≥‘0)) ∧ 𝑘 ∈ (1...𝑚)) → 𝑘 ∈
(ℤ≥‘0)) | 
| 43 |  | simpll 766 | . . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝑚 ∈
(ℤ≥‘0)) ∧ 𝑘 ∈ (1...𝑚)) → 𝑃 ∈ ℙ) | 
| 44 |  | pcfaclem 16937 | . . . . . . . . . 10
⊢ ((0
∈ ℕ0 ∧ 𝑘 ∈ (ℤ≥‘0)
∧ 𝑃 ∈ ℙ)
→ (⌊‘(0 / (𝑃↑𝑘))) = 0) | 
| 45 | 37, 42, 43, 44 | mp3an2i 1467 | . . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝑚 ∈
(ℤ≥‘0)) ∧ 𝑘 ∈ (1...𝑚)) → (⌊‘(0 / (𝑃↑𝑘))) = 0) | 
| 46 | 45 | sumeq2dv 15739 | . . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑚 ∈
(ℤ≥‘0)) → Σ𝑘 ∈ (1...𝑚)(⌊‘(0 / (𝑃↑𝑘))) = Σ𝑘 ∈ (1...𝑚)0) | 
| 47 |  | fac0 14316 | . . . . . . . . . . 11
⊢
(!‘0) = 1 | 
| 48 | 47 | oveq2i 7443 | . . . . . . . . . 10
⊢ (𝑃 pCnt (!‘0)) = (𝑃 pCnt 1) | 
| 49 |  | pc1 16894 | . . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → (𝑃 pCnt 1) = 0) | 
| 50 | 48, 49 | eqtrid 2788 | . . . . . . . . 9
⊢ (𝑃 ∈ ℙ → (𝑃 pCnt (!‘0)) =
0) | 
| 51 | 50 | adantr 480 | . . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑚 ∈
(ℤ≥‘0)) → (𝑃 pCnt (!‘0)) = 0) | 
| 52 | 36, 46, 51 | 3eqtr4rd 2787 | . . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑚 ∈
(ℤ≥‘0)) → (𝑃 pCnt (!‘0)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(0 / (𝑃↑𝑘)))) | 
| 53 | 52 | ralrimiva 3145 | . . . . . 6
⊢ (𝑃 ∈ ℙ →
∀𝑚 ∈
(ℤ≥‘0)(𝑃 pCnt (!‘0)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(0 / (𝑃↑𝑘)))) | 
| 54 |  | nn0z 12640 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℤ) | 
| 55 | 54 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
→ 𝑛 ∈
ℤ) | 
| 56 |  | uzid 12894 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
(ℤ≥‘𝑛)) | 
| 57 |  | peano2uz 12944 | . . . . . . . . . . 11
⊢ (𝑛 ∈
(ℤ≥‘𝑛) → (𝑛 + 1) ∈
(ℤ≥‘𝑛)) | 
| 58 | 55, 56, 57 | 3syl 18 | . . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
→ (𝑛 + 1) ∈
(ℤ≥‘𝑛)) | 
| 59 |  | uzss 12902 | . . . . . . . . . 10
⊢ ((𝑛 + 1) ∈
(ℤ≥‘𝑛) → (ℤ≥‘(𝑛 + 1)) ⊆
(ℤ≥‘𝑛)) | 
| 60 |  | ssralv 4051 | . . . . . . . . . 10
⊢
((ℤ≥‘(𝑛 + 1)) ⊆
(ℤ≥‘𝑛) → (∀𝑚 ∈ (ℤ≥‘𝑛)(𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) → ∀𝑚 ∈ (ℤ≥‘(𝑛 + 1))(𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))))) | 
| 61 | 58, 59, 60 | 3syl 18 | . . . . . . . . 9
⊢ ((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
→ (∀𝑚 ∈
(ℤ≥‘𝑛)(𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) → ∀𝑚 ∈ (ℤ≥‘(𝑛 + 1))(𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))))) | 
| 62 |  | oveq1 7439 | . . . . . . . . . . 11
⊢ ((𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) → ((𝑃 pCnt (!‘𝑛)) + (𝑃 pCnt (𝑛 + 1))) = (Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) + (𝑃 pCnt (𝑛 + 1)))) | 
| 63 |  | simpll 766 | . . . . . . . . . . . . . . 15
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → 𝑛 ∈ ℕ0) | 
| 64 |  | facp1 14318 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ0
→ (!‘(𝑛 + 1)) =
((!‘𝑛) ·
(𝑛 + 1))) | 
| 65 | 63, 64 | syl 17 | . . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (!‘(𝑛 + 1)) = ((!‘𝑛) · (𝑛 + 1))) | 
| 66 | 65 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃 pCnt (!‘(𝑛 + 1))) = (𝑃 pCnt ((!‘𝑛) · (𝑛 + 1)))) | 
| 67 |  | simplr 768 | . . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → 𝑃 ∈ ℙ) | 
| 68 |  | faccl 14323 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ0
→ (!‘𝑛) ∈
ℕ) | 
| 69 |  | nnz 12636 | . . . . . . . . . . . . . . . 16
⊢
((!‘𝑛) ∈
ℕ → (!‘𝑛)
∈ ℤ) | 
| 70 |  | nnne0 12301 | . . . . . . . . . . . . . . . 16
⊢
((!‘𝑛) ∈
ℕ → (!‘𝑛)
≠ 0) | 
| 71 | 69, 70 | jca 511 | . . . . . . . . . . . . . . 15
⊢
((!‘𝑛) ∈
ℕ → ((!‘𝑛)
∈ ℤ ∧ (!‘𝑛) ≠ 0)) | 
| 72 | 63, 68, 71 | 3syl 18 | . . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((!‘𝑛) ∈ ℤ ∧ (!‘𝑛) ≠ 0)) | 
| 73 |  | nn0p1nn 12567 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ0
→ (𝑛 + 1) ∈
ℕ) | 
| 74 |  | nnz 12636 | . . . . . . . . . . . . . . . 16
⊢ ((𝑛 + 1) ∈ ℕ →
(𝑛 + 1) ∈
ℤ) | 
| 75 |  | nnne0 12301 | . . . . . . . . . . . . . . . 16
⊢ ((𝑛 + 1) ∈ ℕ →
(𝑛 + 1) ≠
0) | 
| 76 | 74, 75 | jca 511 | . . . . . . . . . . . . . . 15
⊢ ((𝑛 + 1) ∈ ℕ →
((𝑛 + 1) ∈ ℤ
∧ (𝑛 + 1) ≠
0)) | 
| 77 | 63, 73, 76 | 3syl 18 | . . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((𝑛 + 1) ∈ ℤ ∧ (𝑛 + 1) ≠ 0)) | 
| 78 |  | pcmul 16890 | . . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧
((!‘𝑛) ∈ ℤ
∧ (!‘𝑛) ≠ 0)
∧ ((𝑛 + 1) ∈
ℤ ∧ (𝑛 + 1) ≠
0)) → (𝑃 pCnt
((!‘𝑛) ·
(𝑛 + 1))) = ((𝑃 pCnt (!‘𝑛)) + (𝑃 pCnt (𝑛 + 1)))) | 
| 79 | 67, 72, 77, 78 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃 pCnt ((!‘𝑛) · (𝑛 + 1))) = ((𝑃 pCnt (!‘𝑛)) + (𝑃 pCnt (𝑛 + 1)))) | 
| 80 | 66, 79 | eqtr2d 2777 | . . . . . . . . . . . 12
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((𝑃 pCnt (!‘𝑛)) + (𝑃 pCnt (𝑛 + 1))) = (𝑃 pCnt (!‘(𝑛 + 1)))) | 
| 81 | 63 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → 𝑛 ∈ ℕ0) | 
| 82 | 81 | nn0zd 12641 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → 𝑛 ∈ ℤ) | 
| 83 |  | prmnn 16712 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) | 
| 84 | 83 | ad2antlr 727 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → 𝑃 ∈ ℕ) | 
| 85 |  | nnexpcl 14116 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑃↑𝑘) ∈
ℕ) | 
| 86 | 84, 39, 85 | syl2an 596 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → (𝑃↑𝑘) ∈ ℕ) | 
| 87 |  | fldivp1 16936 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℤ ∧ (𝑃↑𝑘) ∈ ℕ) →
((⌊‘((𝑛 + 1) /
(𝑃↑𝑘))) − (⌊‘(𝑛 / (𝑃↑𝑘)))) = if((𝑃↑𝑘) ∥ (𝑛 + 1), 1, 0)) | 
| 88 | 82, 86, 87 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → ((⌊‘((𝑛 + 1) / (𝑃↑𝑘))) − (⌊‘(𝑛 / (𝑃↑𝑘)))) = if((𝑃↑𝑘) ∥ (𝑛 + 1), 1, 0)) | 
| 89 |  | elfzuz 13561 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ (1...𝑚) → 𝑘 ∈
(ℤ≥‘1)) | 
| 90 | 63, 73 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑛 + 1) ∈ ℕ) | 
| 91 | 67, 90 | pccld 16889 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃 pCnt (𝑛 + 1)) ∈
ℕ0) | 
| 92 | 91 | nn0zd 12641 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃 pCnt (𝑛 + 1)) ∈ ℤ) | 
| 93 |  | elfz5 13557 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈
(ℤ≥‘1) ∧ (𝑃 pCnt (𝑛 + 1)) ∈ ℤ) → (𝑘 ∈ (1...(𝑃 pCnt (𝑛 + 1))) ↔ 𝑘 ≤ (𝑃 pCnt (𝑛 + 1)))) | 
| 94 | 89, 92, 93 | syl2anr 597 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → (𝑘 ∈ (1...(𝑃 pCnt (𝑛 + 1))) ↔ 𝑘 ≤ (𝑃 pCnt (𝑛 + 1)))) | 
| 95 |  | simpllr 775 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → 𝑃 ∈ ℙ) | 
| 96 | 81, 73 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → (𝑛 + 1) ∈ ℕ) | 
| 97 | 96 | nnzd 12642 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → (𝑛 + 1) ∈ ℤ) | 
| 98 | 39 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → 𝑘 ∈ ℕ0) | 
| 99 |  | pcdvdsb 16908 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ ℙ ∧ (𝑛 + 1) ∈ ℤ ∧ 𝑘 ∈ ℕ0)
→ (𝑘 ≤ (𝑃 pCnt (𝑛 + 1)) ↔ (𝑃↑𝑘) ∥ (𝑛 + 1))) | 
| 100 | 95, 97, 98, 99 | syl3anc 1372 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → (𝑘 ≤ (𝑃 pCnt (𝑛 + 1)) ↔ (𝑃↑𝑘) ∥ (𝑛 + 1))) | 
| 101 | 94, 100 | bitr2d 280 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → ((𝑃↑𝑘) ∥ (𝑛 + 1) ↔ 𝑘 ∈ (1...(𝑃 pCnt (𝑛 + 1))))) | 
| 102 | 101 | ifbid 4548 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → if((𝑃↑𝑘) ∥ (𝑛 + 1), 1, 0) = if(𝑘 ∈ (1...(𝑃 pCnt (𝑛 + 1))), 1, 0)) | 
| 103 | 88, 102 | eqtrd 2776 | . . . . . . . . . . . . . . 15
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → ((⌊‘((𝑛 + 1) / (𝑃↑𝑘))) − (⌊‘(𝑛 / (𝑃↑𝑘)))) = if(𝑘 ∈ (1...(𝑃 pCnt (𝑛 + 1))), 1, 0)) | 
| 104 | 103 | sumeq2dv 15739 | . . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → Σ𝑘 ∈ (1...𝑚)((⌊‘((𝑛 + 1) / (𝑃↑𝑘))) − (⌊‘(𝑛 / (𝑃↑𝑘)))) = Σ𝑘 ∈ (1...𝑚)if(𝑘 ∈ (1...(𝑃 pCnt (𝑛 + 1))), 1, 0)) | 
| 105 |  | fzfid 14015 | . . . . . . . . . . . . . . 15
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (1...𝑚) ∈ Fin) | 
| 106 | 63 | nn0red 12590 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → 𝑛 ∈ ℝ) | 
| 107 |  | peano2re 11435 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℝ → (𝑛 + 1) ∈
ℝ) | 
| 108 | 106, 107 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑛 + 1) ∈ ℝ) | 
| 109 | 108 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → (𝑛 + 1) ∈ ℝ) | 
| 110 | 109, 86 | nndivred 12321 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → ((𝑛 + 1) / (𝑃↑𝑘)) ∈ ℝ) | 
| 111 | 110 | flcld 13839 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → (⌊‘((𝑛 + 1) / (𝑃↑𝑘))) ∈ ℤ) | 
| 112 | 111 | zcnd 12725 | . . . . . . . . . . . . . . 15
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → (⌊‘((𝑛 + 1) / (𝑃↑𝑘))) ∈ ℂ) | 
| 113 | 106 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → 𝑛 ∈ ℝ) | 
| 114 | 113, 86 | nndivred 12321 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → (𝑛 / (𝑃↑𝑘)) ∈ ℝ) | 
| 115 | 114 | flcld 13839 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → (⌊‘(𝑛 / (𝑃↑𝑘))) ∈ ℤ) | 
| 116 | 115 | zcnd 12725 | . . . . . . . . . . . . . . 15
⊢ ((((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) ∧ 𝑘 ∈ (1...𝑚)) → (⌊‘(𝑛 / (𝑃↑𝑘))) ∈ ℂ) | 
| 117 | 105, 112,
116 | fsumsub 15825 | . . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → Σ𝑘 ∈ (1...𝑚)((⌊‘((𝑛 + 1) / (𝑃↑𝑘))) − (⌊‘(𝑛 / (𝑃↑𝑘)))) = (Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))) − Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))))) | 
| 118 |  | fzfi 14014 | . . . . . . . . . . . . . . . 16
⊢
(1...𝑚) ∈
Fin | 
| 119 | 91 | nn0red 12590 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃 pCnt (𝑛 + 1)) ∈ ℝ) | 
| 120 |  | eluzelz 12889 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 ∈
(ℤ≥‘(𝑛 + 1)) → 𝑚 ∈ ℤ) | 
| 121 | 120 | adantl 481 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → 𝑚 ∈ ℤ) | 
| 122 | 121 | zred 12724 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → 𝑚 ∈ ℝ) | 
| 123 |  | prmuz2 16734 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) | 
| 124 | 123 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → 𝑃 ∈
(ℤ≥‘2)) | 
| 125 | 90 | nnnn0d 12589 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑛 + 1) ∈
ℕ0) | 
| 126 |  | bernneq3 14271 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑛 + 1) ∈ ℕ0) →
(𝑛 + 1) < (𝑃↑(𝑛 + 1))) | 
| 127 | 124, 125,
126 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑛 + 1) < (𝑃↑(𝑛 + 1))) | 
| 128 | 119, 108 | letrid 11414 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((𝑃 pCnt (𝑛 + 1)) ≤ (𝑛 + 1) ∨ (𝑛 + 1) ≤ (𝑃 pCnt (𝑛 + 1)))) | 
| 129 | 128 | ord 864 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (¬ (𝑃 pCnt (𝑛 + 1)) ≤ (𝑛 + 1) → (𝑛 + 1) ≤ (𝑃 pCnt (𝑛 + 1)))) | 
| 130 | 90 | nnzd 12642 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑛 + 1) ∈ ℤ) | 
| 131 |  | pcdvdsb 16908 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃 ∈ ℙ ∧ (𝑛 + 1) ∈ ℤ ∧
(𝑛 + 1) ∈
ℕ0) → ((𝑛 + 1) ≤ (𝑃 pCnt (𝑛 + 1)) ↔ (𝑃↑(𝑛 + 1)) ∥ (𝑛 + 1))) | 
| 132 | 67, 130, 125, 131 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((𝑛 + 1) ≤ (𝑃 pCnt (𝑛 + 1)) ↔ (𝑃↑(𝑛 + 1)) ∥ (𝑛 + 1))) | 
| 133 | 84, 125 | nnexpcld 14285 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃↑(𝑛 + 1)) ∈ ℕ) | 
| 134 | 133 | nnzd 12642 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃↑(𝑛 + 1)) ∈ ℤ) | 
| 135 |  | dvdsle 16348 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑃↑(𝑛 + 1)) ∈ ℤ ∧ (𝑛 + 1) ∈ ℕ) →
((𝑃↑(𝑛 + 1)) ∥ (𝑛 + 1) → (𝑃↑(𝑛 + 1)) ≤ (𝑛 + 1))) | 
| 136 | 134, 90, 135 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((𝑃↑(𝑛 + 1)) ∥ (𝑛 + 1) → (𝑃↑(𝑛 + 1)) ≤ (𝑛 + 1))) | 
| 137 | 133 | nnred 12282 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃↑(𝑛 + 1)) ∈ ℝ) | 
| 138 | 137, 108 | lenltd 11408 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((𝑃↑(𝑛 + 1)) ≤ (𝑛 + 1) ↔ ¬ (𝑛 + 1) < (𝑃↑(𝑛 + 1)))) | 
| 139 | 136, 138 | sylibd 239 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((𝑃↑(𝑛 + 1)) ∥ (𝑛 + 1) → ¬ (𝑛 + 1) < (𝑃↑(𝑛 + 1)))) | 
| 140 | 132, 139 | sylbid 240 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((𝑛 + 1) ≤ (𝑃 pCnt (𝑛 + 1)) → ¬ (𝑛 + 1) < (𝑃↑(𝑛 + 1)))) | 
| 141 | 129, 140 | syld 47 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (¬ (𝑃 pCnt (𝑛 + 1)) ≤ (𝑛 + 1) → ¬ (𝑛 + 1) < (𝑃↑(𝑛 + 1)))) | 
| 142 | 127, 141 | mt4d 117 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃 pCnt (𝑛 + 1)) ≤ (𝑛 + 1)) | 
| 143 |  | eluzle 12892 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈
(ℤ≥‘(𝑛 + 1)) → (𝑛 + 1) ≤ 𝑚) | 
| 144 | 143 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑛 + 1) ≤ 𝑚) | 
| 145 | 119, 108,
122, 142, 144 | letrd 11419 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃 pCnt (𝑛 + 1)) ≤ 𝑚) | 
| 146 |  | eluz 12893 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 pCnt (𝑛 + 1)) ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑚 ∈
(ℤ≥‘(𝑃 pCnt (𝑛 + 1))) ↔ (𝑃 pCnt (𝑛 + 1)) ≤ 𝑚)) | 
| 147 | 92, 121, 146 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑚 ∈ (ℤ≥‘(𝑃 pCnt (𝑛 + 1))) ↔ (𝑃 pCnt (𝑛 + 1)) ≤ 𝑚)) | 
| 148 | 145, 147 | mpbird 257 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → 𝑚 ∈ (ℤ≥‘(𝑃 pCnt (𝑛 + 1)))) | 
| 149 |  | fzss2 13605 | . . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈
(ℤ≥‘(𝑃 pCnt (𝑛 + 1))) → (1...(𝑃 pCnt (𝑛 + 1))) ⊆ (1...𝑚)) | 
| 150 | 148, 149 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (1...(𝑃 pCnt (𝑛 + 1))) ⊆ (1...𝑚)) | 
| 151 |  | sumhash 16935 | . . . . . . . . . . . . . . . 16
⊢
(((1...𝑚) ∈ Fin
∧ (1...(𝑃 pCnt (𝑛 + 1))) ⊆ (1...𝑚)) → Σ𝑘 ∈ (1...𝑚)if(𝑘 ∈ (1...(𝑃 pCnt (𝑛 + 1))), 1, 0) = (♯‘(1...(𝑃 pCnt (𝑛 + 1))))) | 
| 152 | 118, 150,
151 | sylancr 587 | . . . . . . . . . . . . . . 15
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → Σ𝑘 ∈ (1...𝑚)if(𝑘 ∈ (1...(𝑃 pCnt (𝑛 + 1))), 1, 0) = (♯‘(1...(𝑃 pCnt (𝑛 + 1))))) | 
| 153 |  | hashfz1 14386 | . . . . . . . . . . . . . . . 16
⊢ ((𝑃 pCnt (𝑛 + 1)) ∈ ℕ0 →
(♯‘(1...(𝑃 pCnt
(𝑛 + 1)))) = (𝑃 pCnt (𝑛 + 1))) | 
| 154 | 91, 153 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (♯‘(1...(𝑃 pCnt (𝑛 + 1)))) = (𝑃 pCnt (𝑛 + 1))) | 
| 155 | 152, 154 | eqtrd 2776 | . . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → Σ𝑘 ∈ (1...𝑚)if(𝑘 ∈ (1...(𝑃 pCnt (𝑛 + 1))), 1, 0) = (𝑃 pCnt (𝑛 + 1))) | 
| 156 | 104, 117,
155 | 3eqtr3d 2784 | . . . . . . . . . . . . 13
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))) − Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘)))) = (𝑃 pCnt (𝑛 + 1))) | 
| 157 | 105, 112 | fsumcl 15770 | . . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))) ∈ ℂ) | 
| 158 | 105, 116 | fsumcl 15770 | . . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) ∈ ℂ) | 
| 159 | 119 | recnd 11290 | . . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑃 pCnt (𝑛 + 1)) ∈ ℂ) | 
| 160 | 157, 158,
159 | subaddd 11639 | . . . . . . . . . . . . 13
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))) − Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘)))) = (𝑃 pCnt (𝑛 + 1)) ↔ (Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) + (𝑃 pCnt (𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))))) | 
| 161 | 156, 160 | mpbid 232 | . . . . . . . . . . . 12
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) + (𝑃 pCnt (𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘)))) | 
| 162 | 80, 161 | eqeq12d 2752 | . . . . . . . . . . 11
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → (((𝑃 pCnt (!‘𝑛)) + (𝑃 pCnt (𝑛 + 1))) = (Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) + (𝑃 pCnt (𝑛 + 1))) ↔ (𝑃 pCnt (!‘(𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))))) | 
| 163 | 62, 162 | imbitrid 244 | . . . . . . . . . 10
⊢ (((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
∧ 𝑚 ∈
(ℤ≥‘(𝑛 + 1))) → ((𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) → (𝑃 pCnt (!‘(𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))))) | 
| 164 | 163 | ralimdva 3166 | . . . . . . . . 9
⊢ ((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
→ (∀𝑚 ∈
(ℤ≥‘(𝑛 + 1))(𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) → ∀𝑚 ∈ (ℤ≥‘(𝑛 + 1))(𝑃 pCnt (!‘(𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))))) | 
| 165 | 61, 164 | syld 47 | . . . . . . . 8
⊢ ((𝑛 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
→ (∀𝑚 ∈
(ℤ≥‘𝑛)(𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) → ∀𝑚 ∈ (ℤ≥‘(𝑛 + 1))(𝑃 pCnt (!‘(𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘))))) | 
| 166 | 165 | ex 412 | . . . . . . 7
⊢ (𝑛 ∈ ℕ0
→ (𝑃 ∈ ℙ
→ (∀𝑚 ∈
(ℤ≥‘𝑛)(𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘))) → ∀𝑚 ∈ (ℤ≥‘(𝑛 + 1))(𝑃 pCnt (!‘(𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘)))))) | 
| 167 | 166 | a2d 29 | . . . . . 6
⊢ (𝑛 ∈ ℕ0
→ ((𝑃 ∈ ℙ
→ ∀𝑚 ∈
(ℤ≥‘𝑛)(𝑃 pCnt (!‘𝑛)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑛 / (𝑃↑𝑘)))) → (𝑃 ∈ ℙ → ∀𝑚 ∈
(ℤ≥‘(𝑛 + 1))(𝑃 pCnt (!‘(𝑛 + 1))) = Σ𝑘 ∈ (1...𝑚)(⌊‘((𝑛 + 1) / (𝑃↑𝑘)))))) | 
| 168 | 8, 16, 24, 32, 53, 167 | nn0ind 12715 | . . . . 5
⊢ (𝑁 ∈ ℕ0
→ (𝑃 ∈ ℙ
→ ∀𝑚 ∈
(ℤ≥‘𝑁)(𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑁 / (𝑃↑𝑘))))) | 
| 169 | 168 | imp 406 | . . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑃 ∈ ℙ)
→ ∀𝑚 ∈
(ℤ≥‘𝑁)(𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑁 / (𝑃↑𝑘)))) | 
| 170 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑚 = 𝑀 → (1...𝑚) = (1...𝑀)) | 
| 171 | 170 | sumeq1d 15737 | . . . . . 6
⊢ (𝑚 = 𝑀 → Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑁 / (𝑃↑𝑘))) = Σ𝑘 ∈ (1...𝑀)(⌊‘(𝑁 / (𝑃↑𝑘)))) | 
| 172 | 171 | eqeq2d 2747 | . . . . 5
⊢ (𝑚 = 𝑀 → ((𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑁 / (𝑃↑𝑘))) ↔ (𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑀)(⌊‘(𝑁 / (𝑃↑𝑘))))) | 
| 173 | 172 | rspcv 3617 | . . . 4
⊢ (𝑀 ∈
(ℤ≥‘𝑁) → (∀𝑚 ∈ (ℤ≥‘𝑁)(𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑚)(⌊‘(𝑁 / (𝑃↑𝑘))) → (𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑀)(⌊‘(𝑁 / (𝑃↑𝑘))))) | 
| 174 | 169, 173 | syl5 34 | . . 3
⊢ (𝑀 ∈
(ℤ≥‘𝑁) → ((𝑁 ∈ ℕ0 ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑀)(⌊‘(𝑁 / (𝑃↑𝑘))))) | 
| 175 | 174 | 3impib 1116 | . 2
⊢ ((𝑀 ∈
(ℤ≥‘𝑁) ∧ 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑀)(⌊‘(𝑁 / (𝑃↑𝑘)))) | 
| 176 | 175 | 3com12 1123 | 1
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
(ℤ≥‘𝑁) ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑀)(⌊‘(𝑁 / (𝑃↑𝑘)))) |