Metamath Proof Explorer

Theorem pcfac

Description: Calculate the prime count of a factorial. (Contributed by Mario Carneiro, 11-Mar-2014) (Revised by Mario Carneiro, 21-May-2014)

Ref Expression
Assertion pcfac ${⊢}\left({N}\in {ℕ}_{0}\wedge {M}\in {ℤ}_{\ge {N}}\wedge {P}\in ℙ\right)\to {P}\mathrm{pCnt}{N}!=\sum _{{k}=1}^{{M}}⌊\frac{{N}}{{{P}}^{{k}}}⌋$

Proof

Step Hyp Ref Expression
1 fveq2 ${⊢}{x}=0\to {ℤ}_{\ge {x}}={ℤ}_{\ge 0}$
2 fveq2 ${⊢}{x}=0\to {x}!=0!$
3 2 oveq2d ${⊢}{x}=0\to {P}\mathrm{pCnt}{x}!={P}\mathrm{pCnt}0!$
4 fvoveq1 ${⊢}{x}=0\to ⌊\frac{{x}}{{{P}}^{{k}}}⌋=⌊\frac{0}{{{P}}^{{k}}}⌋$
5 4 sumeq2sdv ${⊢}{x}=0\to \sum _{{k}=1}^{{m}}⌊\frac{{x}}{{{P}}^{{k}}}⌋=\sum _{{k}=1}^{{m}}⌊\frac{0}{{{P}}^{{k}}}⌋$
6 3 5 eqeq12d ${⊢}{x}=0\to \left({P}\mathrm{pCnt}{x}!=\sum _{{k}=1}^{{m}}⌊\frac{{x}}{{{P}}^{{k}}}⌋↔{P}\mathrm{pCnt}0!=\sum _{{k}=1}^{{m}}⌊\frac{0}{{{P}}^{{k}}}⌋\right)$
7 1 6 raleqbidv ${⊢}{x}=0\to \left(\forall {m}\in {ℤ}_{\ge {x}}\phantom{\rule{.4em}{0ex}}{P}\mathrm{pCnt}{x}!=\sum _{{k}=1}^{{m}}⌊\frac{{x}}{{{P}}^{{k}}}⌋↔\forall {m}\in {ℤ}_{\ge 0}\phantom{\rule{.4em}{0ex}}{P}\mathrm{pCnt}0!=\sum _{{k}=1}^{{m}}⌊\frac{0}{{{P}}^{{k}}}⌋\right)$
8 7 imbi2d ${⊢}{x}=0\to \left(\left({P}\in ℙ\to \forall {m}\in {ℤ}_{\ge {x}}\phantom{\rule{.4em}{0ex}}{P}\mathrm{pCnt}{x}!=\sum _{{k}=1}^{{m}}⌊\frac{{x}}{{{P}}^{{k}}}⌋\right)↔\left({P}\in ℙ\to \forall {m}\in {ℤ}_{\ge 0}\phantom{\rule{.4em}{0ex}}{P}\mathrm{pCnt}0!=\sum _{{k}=1}^{{m}}⌊\frac{0}{{{P}}^{{k}}}⌋\right)\right)$
9 fveq2 ${⊢}{x}={n}\to {ℤ}_{\ge {x}}={ℤ}_{\ge {n}}$
10 fveq2 ${⊢}{x}={n}\to {x}!={n}!$
11 10 oveq2d ${⊢}{x}={n}\to {P}\mathrm{pCnt}{x}!={P}\mathrm{pCnt}{n}!$
12 fvoveq1 ${⊢}{x}={n}\to ⌊\frac{{x}}{{{P}}^{{k}}}⌋=⌊\frac{{n}}{{{P}}^{{k}}}⌋$
13 12 sumeq2sdv ${⊢}{x}={n}\to \sum _{{k}=1}^{{m}}⌊\frac{{x}}{{{P}}^{{k}}}⌋=\sum _{{k}=1}^{{m}}⌊\frac{{n}}{{{P}}^{{k}}}⌋$
14 11 13 eqeq12d ${⊢}{x}={n}\to \left({P}\mathrm{pCnt}{x}!=\sum _{{k}=1}^{{m}}⌊\frac{{x}}{{{P}}^{{k}}}⌋↔{P}\mathrm{pCnt}{n}!=\sum _{{k}=1}^{{m}}⌊\frac{{n}}{{{P}}^{{k}}}⌋\right)$
15 9 14 raleqbidv ${⊢}{x}={n}\to \left(\forall {m}\in {ℤ}_{\ge {x}}\phantom{\rule{.4em}{0ex}}{P}\mathrm{pCnt}{x}!=\sum _{{k}=1}^{{m}}⌊\frac{{x}}{{{P}}^{{k}}}⌋↔\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{P}\mathrm{pCnt}{n}!=\sum _{{k}=1}^{{m}}⌊\frac{{n}}{{{P}}^{{k}}}⌋\right)$
16 15 imbi2d ${⊢}{x}={n}\to \left(\left({P}\in ℙ\to \forall {m}\in {ℤ}_{\ge {x}}\phantom{\rule{.4em}{0ex}}{P}\mathrm{pCnt}{x}!=\sum _{{k}=1}^{{m}}⌊\frac{{x}}{{{P}}^{{k}}}⌋\right)↔\left({P}\in ℙ\to \forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{P}\mathrm{pCnt}{n}!=\sum _{{k}=1}^{{m}}⌊\frac{{n}}{{{P}}^{{k}}}⌋\right)\right)$
17 fveq2 ${⊢}{x}={n}+1\to {ℤ}_{\ge {x}}={ℤ}_{\ge \left({n}+1\right)}$
18 fveq2 ${⊢}{x}={n}+1\to {x}!=\left({n}+1\right)!$
19 18 oveq2d ${⊢}{x}={n}+1\to {P}\mathrm{pCnt}{x}!={P}\mathrm{pCnt}\left({n}+1\right)!$
20 fvoveq1 ${⊢}{x}={n}+1\to ⌊\frac{{x}}{{{P}}^{{k}}}⌋=⌊\frac{{n}+1}{{{P}}^{{k}}}⌋$
21 20 sumeq2sdv ${⊢}{x}={n}+1\to \sum _{{k}=1}^{{m}}⌊\frac{{x}}{{{P}}^{{k}}}⌋=\sum _{{k}=1}^{{m}}⌊\frac{{n}+1}{{{P}}^{{k}}}⌋$
22 19 21 eqeq12d ${⊢}{x}={n}+1\to \left({P}\mathrm{pCnt}{x}!=\sum _{{k}=1}^{{m}}⌊\frac{{x}}{{{P}}^{{k}}}⌋↔{P}\mathrm{pCnt}\left({n}+1\right)!=\sum _{{k}=1}^{{m}}⌊\frac{{n}+1}{{{P}}^{{k}}}⌋\right)$
23 17 22 raleqbidv ${⊢}{x}={n}+1\to \left(\forall {m}\in {ℤ}_{\ge {x}}\phantom{\rule{.4em}{0ex}}{P}\mathrm{pCnt}{x}!=\sum _{{k}=1}^{{m}}⌊\frac{{x}}{{{P}}^{{k}}}⌋↔\forall {m}\in {ℤ}_{\ge \left({n}+1\right)}\phantom{\rule{.4em}{0ex}}{P}\mathrm{pCnt}\left({n}+1\right)!=\sum _{{k}=1}^{{m}}⌊\frac{{n}+1}{{{P}}^{{k}}}⌋\right)$
24 23 imbi2d ${⊢}{x}={n}+1\to \left(\left({P}\in ℙ\to \forall {m}\in {ℤ}_{\ge {x}}\phantom{\rule{.4em}{0ex}}{P}\mathrm{pCnt}{x}!=\sum _{{k}=1}^{{m}}⌊\frac{{x}}{{{P}}^{{k}}}⌋\right)↔\left({P}\in ℙ\to \forall {m}\in {ℤ}_{\ge \left({n}+1\right)}\phantom{\rule{.4em}{0ex}}{P}\mathrm{pCnt}\left({n}+1\right)!=\sum _{{k}=1}^{{m}}⌊\frac{{n}+1}{{{P}}^{{k}}}⌋\right)\right)$
25 fveq2 ${⊢}{x}={N}\to {ℤ}_{\ge {x}}={ℤ}_{\ge {N}}$
26 fveq2 ${⊢}{x}={N}\to {x}!={N}!$
27 26 oveq2d ${⊢}{x}={N}\to {P}\mathrm{pCnt}{x}!={P}\mathrm{pCnt}{N}!$
28 fvoveq1 ${⊢}{x}={N}\to ⌊\frac{{x}}{{{P}}^{{k}}}⌋=⌊\frac{{N}}{{{P}}^{{k}}}⌋$
29 28 sumeq2sdv ${⊢}{x}={N}\to \sum _{{k}=1}^{{m}}⌊\frac{{x}}{{{P}}^{{k}}}⌋=\sum _{{k}=1}^{{m}}⌊\frac{{N}}{{{P}}^{{k}}}⌋$
30 27 29 eqeq12d ${⊢}{x}={N}\to \left({P}\mathrm{pCnt}{x}!=\sum _{{k}=1}^{{m}}⌊\frac{{x}}{{{P}}^{{k}}}⌋↔{P}\mathrm{pCnt}{N}!=\sum _{{k}=1}^{{m}}⌊\frac{{N}}{{{P}}^{{k}}}⌋\right)$
31 25 30 raleqbidv ${⊢}{x}={N}\to \left(\forall {m}\in {ℤ}_{\ge {x}}\phantom{\rule{.4em}{0ex}}{P}\mathrm{pCnt}{x}!=\sum _{{k}=1}^{{m}}⌊\frac{{x}}{{{P}}^{{k}}}⌋↔\forall {m}\in {ℤ}_{\ge {N}}\phantom{\rule{.4em}{0ex}}{P}\mathrm{pCnt}{N}!=\sum _{{k}=1}^{{m}}⌊\frac{{N}}{{{P}}^{{k}}}⌋\right)$
32 31 imbi2d ${⊢}{x}={N}\to \left(\left({P}\in ℙ\to \forall {m}\in {ℤ}_{\ge {x}}\phantom{\rule{.4em}{0ex}}{P}\mathrm{pCnt}{x}!=\sum _{{k}=1}^{{m}}⌊\frac{{x}}{{{P}}^{{k}}}⌋\right)↔\left({P}\in ℙ\to \forall {m}\in {ℤ}_{\ge {N}}\phantom{\rule{.4em}{0ex}}{P}\mathrm{pCnt}{N}!=\sum _{{k}=1}^{{m}}⌊\frac{{N}}{{{P}}^{{k}}}⌋\right)\right)$
33 fzfid ${⊢}\left({P}\in ℙ\wedge {m}\in {ℤ}_{\ge 0}\right)\to \left(1\dots {m}\right)\in \mathrm{Fin}$
34 sumz ${⊢}\left(\left(1\dots {m}\right)\subseteq {ℤ}_{\ge 1}\vee \left(1\dots {m}\right)\in \mathrm{Fin}\right)\to \sum _{{k}=1}^{{m}}0=0$
35 34 olcs ${⊢}\left(1\dots {m}\right)\in \mathrm{Fin}\to \sum _{{k}=1}^{{m}}0=0$
36 33 35 syl ${⊢}\left({P}\in ℙ\wedge {m}\in {ℤ}_{\ge 0}\right)\to \sum _{{k}=1}^{{m}}0=0$
37 0nn0 ${⊢}0\in {ℕ}_{0}$
38 elfznn ${⊢}{k}\in \left(1\dots {m}\right)\to {k}\in ℕ$
39 38 nnnn0d ${⊢}{k}\in \left(1\dots {m}\right)\to {k}\in {ℕ}_{0}$
40 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
41 39 40 syl6eleq ${⊢}{k}\in \left(1\dots {m}\right)\to {k}\in {ℤ}_{\ge 0}$
42 41 adantl ${⊢}\left(\left({P}\in ℙ\wedge {m}\in {ℤ}_{\ge 0}\right)\wedge {k}\in \left(1\dots {m}\right)\right)\to {k}\in {ℤ}_{\ge 0}$
43 simpll ${⊢}\left(\left({P}\in ℙ\wedge {m}\in {ℤ}_{\ge 0}\right)\wedge {k}\in \left(1\dots {m}\right)\right)\to {P}\in ℙ$
44 pcfaclem ${⊢}\left(0\in {ℕ}_{0}\wedge {k}\in {ℤ}_{\ge 0}\wedge {P}\in ℙ\right)\to ⌊\frac{0}{{{P}}^{{k}}}⌋=0$
45 37 42 43 44 mp3an2i ${⊢}\left(\left({P}\in ℙ\wedge {m}\in {ℤ}_{\ge 0}\right)\wedge {k}\in \left(1\dots {m}\right)\right)\to ⌊\frac{0}{{{P}}^{{k}}}⌋=0$
46 45 sumeq2dv ${⊢}\left({P}\in ℙ\wedge {m}\in {ℤ}_{\ge 0}\right)\to \sum _{{k}=1}^{{m}}⌊\frac{0}{{{P}}^{{k}}}⌋=\sum _{{k}=1}^{{m}}0$
47 fac0 ${⊢}0!=1$
48 47 oveq2i ${⊢}{P}\mathrm{pCnt}0!={P}\mathrm{pCnt}1$
49 pc1 ${⊢}{P}\in ℙ\to {P}\mathrm{pCnt}1=0$
50 48 49 syl5eq ${⊢}{P}\in ℙ\to {P}\mathrm{pCnt}0!=0$
51 50 adantr ${⊢}\left({P}\in ℙ\wedge {m}\in {ℤ}_{\ge 0}\right)\to {P}\mathrm{pCnt}0!=0$
52 36 46 51 3eqtr4rd ${⊢}\left({P}\in ℙ\wedge {m}\in {ℤ}_{\ge 0}\right)\to {P}\mathrm{pCnt}0!=\sum _{{k}=1}^{{m}}⌊\frac{0}{{{P}}^{{k}}}⌋$
53 52 ralrimiva ${⊢}{P}\in ℙ\to \forall {m}\in {ℤ}_{\ge 0}\phantom{\rule{.4em}{0ex}}{P}\mathrm{pCnt}0!=\sum _{{k}=1}^{{m}}⌊\frac{0}{{{P}}^{{k}}}⌋$
54 nn0z ${⊢}{n}\in {ℕ}_{0}\to {n}\in ℤ$
55 54 adantr ${⊢}\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\to {n}\in ℤ$
56 uzid ${⊢}{n}\in ℤ\to {n}\in {ℤ}_{\ge {n}}$
57 peano2uz ${⊢}{n}\in {ℤ}_{\ge {n}}\to {n}+1\in {ℤ}_{\ge {n}}$
58 55 56 57 3syl ${⊢}\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\to {n}+1\in {ℤ}_{\ge {n}}$
59 uzss ${⊢}{n}+1\in {ℤ}_{\ge {n}}\to {ℤ}_{\ge \left({n}+1\right)}\subseteq {ℤ}_{\ge {n}}$
60 ssralv ${⊢}{ℤ}_{\ge \left({n}+1\right)}\subseteq {ℤ}_{\ge {n}}\to \left(\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{P}\mathrm{pCnt}{n}!=\sum _{{k}=1}^{{m}}⌊\frac{{n}}{{{P}}^{{k}}}⌋\to \forall {m}\in {ℤ}_{\ge \left({n}+1\right)}\phantom{\rule{.4em}{0ex}}{P}\mathrm{pCnt}{n}!=\sum _{{k}=1}^{{m}}⌊\frac{{n}}{{{P}}^{{k}}}⌋\right)$
61 58 59 60 3syl ${⊢}\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\to \left(\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{P}\mathrm{pCnt}{n}!=\sum _{{k}=1}^{{m}}⌊\frac{{n}}{{{P}}^{{k}}}⌋\to \forall {m}\in {ℤ}_{\ge \left({n}+1\right)}\phantom{\rule{.4em}{0ex}}{P}\mathrm{pCnt}{n}!=\sum _{{k}=1}^{{m}}⌊\frac{{n}}{{{P}}^{{k}}}⌋\right)$
62 oveq1 ${⊢}{P}\mathrm{pCnt}{n}!=\sum _{{k}=1}^{{m}}⌊\frac{{n}}{{{P}}^{{k}}}⌋\to \left({P}\mathrm{pCnt}{n}!\right)+\left({P}\mathrm{pCnt}\left({n}+1\right)\right)=\sum _{{k}=1}^{{m}}⌊\frac{{n}}{{{P}}^{{k}}}⌋+\left({P}\mathrm{pCnt}\left({n}+1\right)\right)$
63 simpll ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to {n}\in {ℕ}_{0}$
64 facp1 ${⊢}{n}\in {ℕ}_{0}\to \left({n}+1\right)!={n}!\left({n}+1\right)$
65 63 64 syl ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to \left({n}+1\right)!={n}!\left({n}+1\right)$
66 65 oveq2d ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to {P}\mathrm{pCnt}\left({n}+1\right)!={P}\mathrm{pCnt}{n}!\left({n}+1\right)$
67 simplr ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to {P}\in ℙ$
68 faccl ${⊢}{n}\in {ℕ}_{0}\to {n}!\in ℕ$
69 nnz ${⊢}{n}!\in ℕ\to {n}!\in ℤ$
70 nnne0 ${⊢}{n}!\in ℕ\to {n}!\ne 0$
71 69 70 jca ${⊢}{n}!\in ℕ\to \left({n}!\in ℤ\wedge {n}!\ne 0\right)$
72 63 68 71 3syl ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to \left({n}!\in ℤ\wedge {n}!\ne 0\right)$
73 nn0p1nn ${⊢}{n}\in {ℕ}_{0}\to {n}+1\in ℕ$
74 nnz ${⊢}{n}+1\in ℕ\to {n}+1\in ℤ$
75 nnne0 ${⊢}{n}+1\in ℕ\to {n}+1\ne 0$
76 74 75 jca ${⊢}{n}+1\in ℕ\to \left({n}+1\in ℤ\wedge {n}+1\ne 0\right)$
77 63 73 76 3syl ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to \left({n}+1\in ℤ\wedge {n}+1\ne 0\right)$
78 pcmul ${⊢}\left({P}\in ℙ\wedge \left({n}!\in ℤ\wedge {n}!\ne 0\right)\wedge \left({n}+1\in ℤ\wedge {n}+1\ne 0\right)\right)\to {P}\mathrm{pCnt}{n}!\left({n}+1\right)=\left({P}\mathrm{pCnt}{n}!\right)+\left({P}\mathrm{pCnt}\left({n}+1\right)\right)$
79 67 72 77 78 syl3anc ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to {P}\mathrm{pCnt}{n}!\left({n}+1\right)=\left({P}\mathrm{pCnt}{n}!\right)+\left({P}\mathrm{pCnt}\left({n}+1\right)\right)$
80 66 79 eqtr2d ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to \left({P}\mathrm{pCnt}{n}!\right)+\left({P}\mathrm{pCnt}\left({n}+1\right)\right)={P}\mathrm{pCnt}\left({n}+1\right)!$
81 63 adantr ${⊢}\left(\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\wedge {k}\in \left(1\dots {m}\right)\right)\to {n}\in {ℕ}_{0}$
82 81 nn0zd ${⊢}\left(\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\wedge {k}\in \left(1\dots {m}\right)\right)\to {n}\in ℤ$
83 prmnn ${⊢}{P}\in ℙ\to {P}\in ℕ$
84 83 ad2antlr ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to {P}\in ℕ$
85 nnexpcl ${⊢}\left({P}\in ℕ\wedge {k}\in {ℕ}_{0}\right)\to {{P}}^{{k}}\in ℕ$
86 84 39 85 syl2an ${⊢}\left(\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\wedge {k}\in \left(1\dots {m}\right)\right)\to {{P}}^{{k}}\in ℕ$
87 fldivp1 ${⊢}\left({n}\in ℤ\wedge {{P}}^{{k}}\in ℕ\right)\to ⌊\frac{{n}+1}{{{P}}^{{k}}}⌋-⌊\frac{{n}}{{{P}}^{{k}}}⌋=if\left({{P}}^{{k}}\parallel \left({n}+1\right),1,0\right)$
88 82 86 87 syl2anc ${⊢}\left(\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\wedge {k}\in \left(1\dots {m}\right)\right)\to ⌊\frac{{n}+1}{{{P}}^{{k}}}⌋-⌊\frac{{n}}{{{P}}^{{k}}}⌋=if\left({{P}}^{{k}}\parallel \left({n}+1\right),1,0\right)$
89 elfzuz ${⊢}{k}\in \left(1\dots {m}\right)\to {k}\in {ℤ}_{\ge 1}$
90 63 73 syl ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to {n}+1\in ℕ$
91 67 90 pccld ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to {P}\mathrm{pCnt}\left({n}+1\right)\in {ℕ}_{0}$
92 91 nn0zd ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to {P}\mathrm{pCnt}\left({n}+1\right)\in ℤ$
93 elfz5 ${⊢}\left({k}\in {ℤ}_{\ge 1}\wedge {P}\mathrm{pCnt}\left({n}+1\right)\in ℤ\right)\to \left({k}\in \left(1\dots {P}\mathrm{pCnt}\left({n}+1\right)\right)↔{k}\le {P}\mathrm{pCnt}\left({n}+1\right)\right)$
94 89 92 93 syl2anr ${⊢}\left(\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\wedge {k}\in \left(1\dots {m}\right)\right)\to \left({k}\in \left(1\dots {P}\mathrm{pCnt}\left({n}+1\right)\right)↔{k}\le {P}\mathrm{pCnt}\left({n}+1\right)\right)$
95 simpllr ${⊢}\left(\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\wedge {k}\in \left(1\dots {m}\right)\right)\to {P}\in ℙ$
96 81 73 syl ${⊢}\left(\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\wedge {k}\in \left(1\dots {m}\right)\right)\to {n}+1\in ℕ$
97 96 nnzd ${⊢}\left(\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\wedge {k}\in \left(1\dots {m}\right)\right)\to {n}+1\in ℤ$
98 39 adantl ${⊢}\left(\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\wedge {k}\in \left(1\dots {m}\right)\right)\to {k}\in {ℕ}_{0}$
99 pcdvdsb ${⊢}\left({P}\in ℙ\wedge {n}+1\in ℤ\wedge {k}\in {ℕ}_{0}\right)\to \left({k}\le {P}\mathrm{pCnt}\left({n}+1\right)↔{{P}}^{{k}}\parallel \left({n}+1\right)\right)$
100 95 97 98 99 syl3anc ${⊢}\left(\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\wedge {k}\in \left(1\dots {m}\right)\right)\to \left({k}\le {P}\mathrm{pCnt}\left({n}+1\right)↔{{P}}^{{k}}\parallel \left({n}+1\right)\right)$
101 94 100 bitr2d ${⊢}\left(\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\wedge {k}\in \left(1\dots {m}\right)\right)\to \left({{P}}^{{k}}\parallel \left({n}+1\right)↔{k}\in \left(1\dots {P}\mathrm{pCnt}\left({n}+1\right)\right)\right)$
102 101 ifbid ${⊢}\left(\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\wedge {k}\in \left(1\dots {m}\right)\right)\to if\left({{P}}^{{k}}\parallel \left({n}+1\right),1,0\right)=if\left({k}\in \left(1\dots {P}\mathrm{pCnt}\left({n}+1\right)\right),1,0\right)$
103 88 102 eqtrd ${⊢}\left(\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\wedge {k}\in \left(1\dots {m}\right)\right)\to ⌊\frac{{n}+1}{{{P}}^{{k}}}⌋-⌊\frac{{n}}{{{P}}^{{k}}}⌋=if\left({k}\in \left(1\dots {P}\mathrm{pCnt}\left({n}+1\right)\right),1,0\right)$
104 103 sumeq2dv ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to \sum _{{k}=1}^{{m}}\left(⌊\frac{{n}+1}{{{P}}^{{k}}}⌋-⌊\frac{{n}}{{{P}}^{{k}}}⌋\right)=\sum _{{k}=1}^{{m}}if\left({k}\in \left(1\dots {P}\mathrm{pCnt}\left({n}+1\right)\right),1,0\right)$
105 fzfid ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to \left(1\dots {m}\right)\in \mathrm{Fin}$
106 63 nn0red ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to {n}\in ℝ$
107 peano2re ${⊢}{n}\in ℝ\to {n}+1\in ℝ$
108 106 107 syl ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to {n}+1\in ℝ$
109 108 adantr ${⊢}\left(\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\wedge {k}\in \left(1\dots {m}\right)\right)\to {n}+1\in ℝ$
110 109 86 nndivred ${⊢}\left(\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\wedge {k}\in \left(1\dots {m}\right)\right)\to \frac{{n}+1}{{{P}}^{{k}}}\in ℝ$
111 110 flcld ${⊢}\left(\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\wedge {k}\in \left(1\dots {m}\right)\right)\to ⌊\frac{{n}+1}{{{P}}^{{k}}}⌋\in ℤ$
112 111 zcnd ${⊢}\left(\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\wedge {k}\in \left(1\dots {m}\right)\right)\to ⌊\frac{{n}+1}{{{P}}^{{k}}}⌋\in ℂ$
113 106 adantr ${⊢}\left(\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\wedge {k}\in \left(1\dots {m}\right)\right)\to {n}\in ℝ$
114 113 86 nndivred ${⊢}\left(\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\wedge {k}\in \left(1\dots {m}\right)\right)\to \frac{{n}}{{{P}}^{{k}}}\in ℝ$
115 114 flcld ${⊢}\left(\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\wedge {k}\in \left(1\dots {m}\right)\right)\to ⌊\frac{{n}}{{{P}}^{{k}}}⌋\in ℤ$
116 115 zcnd ${⊢}\left(\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\wedge {k}\in \left(1\dots {m}\right)\right)\to ⌊\frac{{n}}{{{P}}^{{k}}}⌋\in ℂ$
117 105 112 116 fsumsub ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to \sum _{{k}=1}^{{m}}\left(⌊\frac{{n}+1}{{{P}}^{{k}}}⌋-⌊\frac{{n}}{{{P}}^{{k}}}⌋\right)=\sum _{{k}=1}^{{m}}⌊\frac{{n}+1}{{{P}}^{{k}}}⌋-\sum _{{k}=1}^{{m}}⌊\frac{{n}}{{{P}}^{{k}}}⌋$
118 fzfi ${⊢}\left(1\dots {m}\right)\in \mathrm{Fin}$
119 91 nn0red ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to {P}\mathrm{pCnt}\left({n}+1\right)\in ℝ$
120 eluzelz ${⊢}{m}\in {ℤ}_{\ge \left({n}+1\right)}\to {m}\in ℤ$
121 120 adantl ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to {m}\in ℤ$
122 121 zred ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to {m}\in ℝ$
123 prmuz2 ${⊢}{P}\in ℙ\to {P}\in {ℤ}_{\ge 2}$
124 123 ad2antlr ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to {P}\in {ℤ}_{\ge 2}$
125 90 nnnn0d ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to {n}+1\in {ℕ}_{0}$
126 bernneq3 ${⊢}\left({P}\in {ℤ}_{\ge 2}\wedge {n}+1\in {ℕ}_{0}\right)\to {n}+1<{{P}}^{{n}+1}$
127 124 125 126 syl2anc ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to {n}+1<{{P}}^{{n}+1}$
128 119 108 letrid ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to \left({P}\mathrm{pCnt}\left({n}+1\right)\le {n}+1\vee {n}+1\le {P}\mathrm{pCnt}\left({n}+1\right)\right)$
129 128 ord ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to \left(¬{P}\mathrm{pCnt}\left({n}+1\right)\le {n}+1\to {n}+1\le {P}\mathrm{pCnt}\left({n}+1\right)\right)$
130 90 nnzd ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to {n}+1\in ℤ$
131 pcdvdsb ${⊢}\left({P}\in ℙ\wedge {n}+1\in ℤ\wedge {n}+1\in {ℕ}_{0}\right)\to \left({n}+1\le {P}\mathrm{pCnt}\left({n}+1\right)↔{{P}}^{{n}+1}\parallel \left({n}+1\right)\right)$
132 67 130 125 131 syl3anc ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to \left({n}+1\le {P}\mathrm{pCnt}\left({n}+1\right)↔{{P}}^{{n}+1}\parallel \left({n}+1\right)\right)$
133 84 125 nnexpcld ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to {{P}}^{{n}+1}\in ℕ$
134 133 nnzd ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to {{P}}^{{n}+1}\in ℤ$
135 dvdsle ${⊢}\left({{P}}^{{n}+1}\in ℤ\wedge {n}+1\in ℕ\right)\to \left({{P}}^{{n}+1}\parallel \left({n}+1\right)\to {{P}}^{{n}+1}\le {n}+1\right)$
136 134 90 135 syl2anc ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to \left({{P}}^{{n}+1}\parallel \left({n}+1\right)\to {{P}}^{{n}+1}\le {n}+1\right)$
137 133 nnred ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to {{P}}^{{n}+1}\in ℝ$
138 137 108 lenltd ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to \left({{P}}^{{n}+1}\le {n}+1↔¬{n}+1<{{P}}^{{n}+1}\right)$
139 136 138 sylibd ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to \left({{P}}^{{n}+1}\parallel \left({n}+1\right)\to ¬{n}+1<{{P}}^{{n}+1}\right)$
140 132 139 sylbid ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to \left({n}+1\le {P}\mathrm{pCnt}\left({n}+1\right)\to ¬{n}+1<{{P}}^{{n}+1}\right)$
141 129 140 syld ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to \left(¬{P}\mathrm{pCnt}\left({n}+1\right)\le {n}+1\to ¬{n}+1<{{P}}^{{n}+1}\right)$
142 127 141 mt4d ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to {P}\mathrm{pCnt}\left({n}+1\right)\le {n}+1$
143 eluzle ${⊢}{m}\in {ℤ}_{\ge \left({n}+1\right)}\to {n}+1\le {m}$
144 143 adantl ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to {n}+1\le {m}$
145 119 108 122 142 144 letrd ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to {P}\mathrm{pCnt}\left({n}+1\right)\le {m}$
146 eluz ${⊢}\left({P}\mathrm{pCnt}\left({n}+1\right)\in ℤ\wedge {m}\in ℤ\right)\to \left({m}\in {ℤ}_{\ge \left({P}\mathrm{pCnt}\left({n}+1\right)\right)}↔{P}\mathrm{pCnt}\left({n}+1\right)\le {m}\right)$
147 92 121 146 syl2anc ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to \left({m}\in {ℤ}_{\ge \left({P}\mathrm{pCnt}\left({n}+1\right)\right)}↔{P}\mathrm{pCnt}\left({n}+1\right)\le {m}\right)$
148 145 147 mpbird ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to {m}\in {ℤ}_{\ge \left({P}\mathrm{pCnt}\left({n}+1\right)\right)}$
149 fzss2 ${⊢}{m}\in {ℤ}_{\ge \left({P}\mathrm{pCnt}\left({n}+1\right)\right)}\to \left(1\dots {P}\mathrm{pCnt}\left({n}+1\right)\right)\subseteq \left(1\dots {m}\right)$
150 148 149 syl ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to \left(1\dots {P}\mathrm{pCnt}\left({n}+1\right)\right)\subseteq \left(1\dots {m}\right)$
151 sumhash ${⊢}\left(\left(1\dots {m}\right)\in \mathrm{Fin}\wedge \left(1\dots {P}\mathrm{pCnt}\left({n}+1\right)\right)\subseteq \left(1\dots {m}\right)\right)\to \sum _{{k}=1}^{{m}}if\left({k}\in \left(1\dots {P}\mathrm{pCnt}\left({n}+1\right)\right),1,0\right)=\left|\left(1\dots {P}\mathrm{pCnt}\left({n}+1\right)\right)\right|$
152 118 150 151 sylancr ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to \sum _{{k}=1}^{{m}}if\left({k}\in \left(1\dots {P}\mathrm{pCnt}\left({n}+1\right)\right),1,0\right)=\left|\left(1\dots {P}\mathrm{pCnt}\left({n}+1\right)\right)\right|$
153 hashfz1 ${⊢}{P}\mathrm{pCnt}\left({n}+1\right)\in {ℕ}_{0}\to \left|\left(1\dots {P}\mathrm{pCnt}\left({n}+1\right)\right)\right|={P}\mathrm{pCnt}\left({n}+1\right)$
154 91 153 syl ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to \left|\left(1\dots {P}\mathrm{pCnt}\left({n}+1\right)\right)\right|={P}\mathrm{pCnt}\left({n}+1\right)$
155 152 154 eqtrd ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to \sum _{{k}=1}^{{m}}if\left({k}\in \left(1\dots {P}\mathrm{pCnt}\left({n}+1\right)\right),1,0\right)={P}\mathrm{pCnt}\left({n}+1\right)$
156 104 117 155 3eqtr3d ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to \sum _{{k}=1}^{{m}}⌊\frac{{n}+1}{{{P}}^{{k}}}⌋-\sum _{{k}=1}^{{m}}⌊\frac{{n}}{{{P}}^{{k}}}⌋={P}\mathrm{pCnt}\left({n}+1\right)$
157 105 112 fsumcl ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to \sum _{{k}=1}^{{m}}⌊\frac{{n}+1}{{{P}}^{{k}}}⌋\in ℂ$
158 105 116 fsumcl ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to \sum _{{k}=1}^{{m}}⌊\frac{{n}}{{{P}}^{{k}}}⌋\in ℂ$
159 119 recnd ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to {P}\mathrm{pCnt}\left({n}+1\right)\in ℂ$
160 157 158 159 subaddd ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to \left(\sum _{{k}=1}^{{m}}⌊\frac{{n}+1}{{{P}}^{{k}}}⌋-\sum _{{k}=1}^{{m}}⌊\frac{{n}}{{{P}}^{{k}}}⌋={P}\mathrm{pCnt}\left({n}+1\right)↔\sum _{{k}=1}^{{m}}⌊\frac{{n}}{{{P}}^{{k}}}⌋+\left({P}\mathrm{pCnt}\left({n}+1\right)\right)=\sum _{{k}=1}^{{m}}⌊\frac{{n}+1}{{{P}}^{{k}}}⌋\right)$
161 156 160 mpbid ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to \sum _{{k}=1}^{{m}}⌊\frac{{n}}{{{P}}^{{k}}}⌋+\left({P}\mathrm{pCnt}\left({n}+1\right)\right)=\sum _{{k}=1}^{{m}}⌊\frac{{n}+1}{{{P}}^{{k}}}⌋$
162 80 161 eqeq12d ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to \left(\left({P}\mathrm{pCnt}{n}!\right)+\left({P}\mathrm{pCnt}\left({n}+1\right)\right)=\sum _{{k}=1}^{{m}}⌊\frac{{n}}{{{P}}^{{k}}}⌋+\left({P}\mathrm{pCnt}\left({n}+1\right)\right)↔{P}\mathrm{pCnt}\left({n}+1\right)!=\sum _{{k}=1}^{{m}}⌊\frac{{n}+1}{{{P}}^{{k}}}⌋\right)$
163 62 162 syl5ib ${⊢}\left(\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\wedge {m}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to \left({P}\mathrm{pCnt}{n}!=\sum _{{k}=1}^{{m}}⌊\frac{{n}}{{{P}}^{{k}}}⌋\to {P}\mathrm{pCnt}\left({n}+1\right)!=\sum _{{k}=1}^{{m}}⌊\frac{{n}+1}{{{P}}^{{k}}}⌋\right)$
164 163 ralimdva ${⊢}\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\to \left(\forall {m}\in {ℤ}_{\ge \left({n}+1\right)}\phantom{\rule{.4em}{0ex}}{P}\mathrm{pCnt}{n}!=\sum _{{k}=1}^{{m}}⌊\frac{{n}}{{{P}}^{{k}}}⌋\to \forall {m}\in {ℤ}_{\ge \left({n}+1\right)}\phantom{\rule{.4em}{0ex}}{P}\mathrm{pCnt}\left({n}+1\right)!=\sum _{{k}=1}^{{m}}⌊\frac{{n}+1}{{{P}}^{{k}}}⌋\right)$
165 61 164 syld ${⊢}\left({n}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\to \left(\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{P}\mathrm{pCnt}{n}!=\sum _{{k}=1}^{{m}}⌊\frac{{n}}{{{P}}^{{k}}}⌋\to \forall {m}\in {ℤ}_{\ge \left({n}+1\right)}\phantom{\rule{.4em}{0ex}}{P}\mathrm{pCnt}\left({n}+1\right)!=\sum _{{k}=1}^{{m}}⌊\frac{{n}+1}{{{P}}^{{k}}}⌋\right)$
166 165 ex ${⊢}{n}\in {ℕ}_{0}\to \left({P}\in ℙ\to \left(\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{P}\mathrm{pCnt}{n}!=\sum _{{k}=1}^{{m}}⌊\frac{{n}}{{{P}}^{{k}}}⌋\to \forall {m}\in {ℤ}_{\ge \left({n}+1\right)}\phantom{\rule{.4em}{0ex}}{P}\mathrm{pCnt}\left({n}+1\right)!=\sum _{{k}=1}^{{m}}⌊\frac{{n}+1}{{{P}}^{{k}}}⌋\right)\right)$
167 166 a2d ${⊢}{n}\in {ℕ}_{0}\to \left(\left({P}\in ℙ\to \forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{P}\mathrm{pCnt}{n}!=\sum _{{k}=1}^{{m}}⌊\frac{{n}}{{{P}}^{{k}}}⌋\right)\to \left({P}\in ℙ\to \forall {m}\in {ℤ}_{\ge \left({n}+1\right)}\phantom{\rule{.4em}{0ex}}{P}\mathrm{pCnt}\left({n}+1\right)!=\sum _{{k}=1}^{{m}}⌊\frac{{n}+1}{{{P}}^{{k}}}⌋\right)\right)$
168 8 16 24 32 53 167 nn0ind ${⊢}{N}\in {ℕ}_{0}\to \left({P}\in ℙ\to \forall {m}\in {ℤ}_{\ge {N}}\phantom{\rule{.4em}{0ex}}{P}\mathrm{pCnt}{N}!=\sum _{{k}=1}^{{m}}⌊\frac{{N}}{{{P}}^{{k}}}⌋\right)$
169 168 imp ${⊢}\left({N}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\to \forall {m}\in {ℤ}_{\ge {N}}\phantom{\rule{.4em}{0ex}}{P}\mathrm{pCnt}{N}!=\sum _{{k}=1}^{{m}}⌊\frac{{N}}{{{P}}^{{k}}}⌋$
170 oveq2 ${⊢}{m}={M}\to \left(1\dots {m}\right)=\left(1\dots {M}\right)$
171 170 sumeq1d ${⊢}{m}={M}\to \sum _{{k}=1}^{{m}}⌊\frac{{N}}{{{P}}^{{k}}}⌋=\sum _{{k}=1}^{{M}}⌊\frac{{N}}{{{P}}^{{k}}}⌋$
172 171 eqeq2d ${⊢}{m}={M}\to \left({P}\mathrm{pCnt}{N}!=\sum _{{k}=1}^{{m}}⌊\frac{{N}}{{{P}}^{{k}}}⌋↔{P}\mathrm{pCnt}{N}!=\sum _{{k}=1}^{{M}}⌊\frac{{N}}{{{P}}^{{k}}}⌋\right)$
173 172 rspcv ${⊢}{M}\in {ℤ}_{\ge {N}}\to \left(\forall {m}\in {ℤ}_{\ge {N}}\phantom{\rule{.4em}{0ex}}{P}\mathrm{pCnt}{N}!=\sum _{{k}=1}^{{m}}⌊\frac{{N}}{{{P}}^{{k}}}⌋\to {P}\mathrm{pCnt}{N}!=\sum _{{k}=1}^{{M}}⌊\frac{{N}}{{{P}}^{{k}}}⌋\right)$
174 169 173 syl5 ${⊢}{M}\in {ℤ}_{\ge {N}}\to \left(\left({N}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\to {P}\mathrm{pCnt}{N}!=\sum _{{k}=1}^{{M}}⌊\frac{{N}}{{{P}}^{{k}}}⌋\right)$
175 174 3impib ${⊢}\left({M}\in {ℤ}_{\ge {N}}\wedge {N}\in {ℕ}_{0}\wedge {P}\in ℙ\right)\to {P}\mathrm{pCnt}{N}!=\sum _{{k}=1}^{{M}}⌊\frac{{N}}{{{P}}^{{k}}}⌋$
176 175 3com12 ${⊢}\left({N}\in {ℕ}_{0}\wedge {M}\in {ℤ}_{\ge {N}}\wedge {P}\in ℙ\right)\to {P}\mathrm{pCnt}{N}!=\sum _{{k}=1}^{{M}}⌊\frac{{N}}{{{P}}^{{k}}}⌋$