Metamath Proof Explorer

Theorem pcbc

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

Ref Expression
Assertion pcbc ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( 𝑃 pCnt ( 𝑁 C 𝐾 ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) − ( ( ⌊ ‘ ( ( 𝑁 − 𝐾 ) / ( 𝑃 ↑ 𝑘 ) ) ) + ( ⌊ ‘ ( 𝐾 / ( 𝑃 ↑ 𝑘 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 simp3 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → 𝑃 ∈ ℙ )
2 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
3 2 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → 𝑁 ∈ ℕ0 )
4 3 faccld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( ! ‘ 𝑁 ) ∈ ℕ )
5 4 nnzd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( ! ‘ 𝑁 ) ∈ ℤ )
6 4 nnne0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( ! ‘ 𝑁 ) ≠ 0 )
7 fznn0sub ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 − 𝐾 ) ∈ ℕ0 )
8 7 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( 𝑁 − 𝐾 ) ∈ ℕ0 )
9 8 faccld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( ! ‘ ( 𝑁 − 𝐾 ) ) ∈ ℕ )
10 elfznn0 ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ℕ0 )
11 10 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → 𝐾 ∈ ℕ0 )
12 11 faccld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( ! ‘ 𝐾 ) ∈ ℕ )
13 9 12 nnmulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ∈ ℕ )
14 pcdiv ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( ! ‘ 𝑁 ) ∈ ℤ ∧ ( ! ‘ 𝑁 ) ≠ 0 ) ∧ ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ∈ ℕ ) → ( 𝑃 pCnt ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) ) = ( ( 𝑃 pCnt ( ! ‘ 𝑁 ) ) − ( 𝑃 pCnt ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) ) )
15 1 5 6 13 14 syl121anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( 𝑃 pCnt ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) ) = ( ( 𝑃 pCnt ( ! ‘ 𝑁 ) ) − ( 𝑃 pCnt ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) ) )
16 bcval2 ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝐾 ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) )
17 16 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( 𝑁 C 𝐾 ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) )
18 17 oveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( 𝑃 pCnt ( 𝑁 C 𝐾 ) ) = ( 𝑃 pCnt ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) ) )
19 fzfid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( 1 ... 𝑁 ) ∈ Fin )
20 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
21 20 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → 𝑁 ∈ ℝ )
22 21 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑁 ∈ ℝ )
23 simpl3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑃 ∈ ℙ )
24 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
25 23 24 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑃 ∈ ℕ )
26 elfznn ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℕ )
27 26 nnnn0d ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
28 27 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
29 25 28 nnexpcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑃 ↑ 𝑘 ) ∈ ℕ )
30 22 29 nndivred ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ∈ ℝ )
31 30 flcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) ∈ ℤ )
32 31 zcnd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) ∈ ℂ )
33 11 nn0red ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → 𝐾 ∈ ℝ )
34 21 33 resubcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( 𝑁 − 𝐾 ) ∈ ℝ )
35 34 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑁 − 𝐾 ) ∈ ℝ )
36 35 29 nndivred ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑁 − 𝐾 ) / ( 𝑃 ↑ 𝑘 ) ) ∈ ℝ )
37 36 flcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ⌊ ‘ ( ( 𝑁 − 𝐾 ) / ( 𝑃 ↑ 𝑘 ) ) ) ∈ ℤ )
38 37 zcnd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ⌊ ‘ ( ( 𝑁 − 𝐾 ) / ( 𝑃 ↑ 𝑘 ) ) ) ∈ ℂ )
39 33 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝐾 ∈ ℝ )
40 39 29 nndivred ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝐾 / ( 𝑃 ↑ 𝑘 ) ) ∈ ℝ )
41 40 flcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ⌊ ‘ ( 𝐾 / ( 𝑃 ↑ 𝑘 ) ) ) ∈ ℤ )
42 41 zcnd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ⌊ ‘ ( 𝐾 / ( 𝑃 ↑ 𝑘 ) ) ) ∈ ℂ )
43 38 42 addcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( ⌊ ‘ ( ( 𝑁 − 𝐾 ) / ( 𝑃 ↑ 𝑘 ) ) ) + ( ⌊ ‘ ( 𝐾 / ( 𝑃 ↑ 𝑘 ) ) ) ) ∈ ℂ )
44 19 32 43 fsumsub ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) − ( ( ⌊ ‘ ( ( 𝑁 − 𝐾 ) / ( 𝑃 ↑ 𝑘 ) ) ) + ( ⌊ ‘ ( 𝐾 / ( 𝑃 ↑ 𝑘 ) ) ) ) ) = ( Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) − Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( ⌊ ‘ ( ( 𝑁 − 𝐾 ) / ( 𝑃 ↑ 𝑘 ) ) ) + ( ⌊ ‘ ( 𝐾 / ( 𝑃 ↑ 𝑘 ) ) ) ) ) )
45 3 nn0zd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → 𝑁 ∈ ℤ )
46 uzid ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) )
47 45 46 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) )
48 pcfac ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( 𝑃 pCnt ( ! ‘ 𝑁 ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) )
49 3 47 1 48 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( 𝑃 pCnt ( ! ‘ 𝑁 ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) )
50 11 nn0ge0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → 0 ≤ 𝐾 )
51 21 33 subge02d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( 0 ≤ 𝐾 ↔ ( 𝑁 − 𝐾 ) ≤ 𝑁 ) )
52 50 51 mpbid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( 𝑁 − 𝐾 ) ≤ 𝑁 )
53 11 nn0zd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → 𝐾 ∈ ℤ )
54 45 53 zsubcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( 𝑁 − 𝐾 ) ∈ ℤ )
55 eluz ⊢ ( ( ( 𝑁 − 𝐾 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 𝐾 ) ) ↔ ( 𝑁 − 𝐾 ) ≤ 𝑁 ) )
56 54 45 55 syl2anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 𝐾 ) ) ↔ ( 𝑁 − 𝐾 ) ≤ 𝑁 ) )
57 52 56 mpbird ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 𝐾 ) ) )
58 pcfac ⊢ ( ( ( 𝑁 − 𝐾 ) ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 𝐾 ) ) ∧ 𝑃 ∈ ℙ ) → ( 𝑃 pCnt ( ! ‘ ( 𝑁 − 𝐾 ) ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ⌊ ‘ ( ( 𝑁 − 𝐾 ) / ( 𝑃 ↑ 𝑘 ) ) ) )
59 8 57 1 58 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( 𝑃 pCnt ( ! ‘ ( 𝑁 − 𝐾 ) ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ⌊ ‘ ( ( 𝑁 − 𝐾 ) / ( 𝑃 ↑ 𝑘 ) ) ) )
60 elfzuz3 ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
61 60 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
62 pcfac ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝑃 ∈ ℙ ) → ( 𝑃 pCnt ( ! ‘ 𝐾 ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ⌊ ‘ ( 𝐾 / ( 𝑃 ↑ 𝑘 ) ) ) )
63 11 61 1 62 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( 𝑃 pCnt ( ! ‘ 𝐾 ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ⌊ ‘ ( 𝐾 / ( 𝑃 ↑ 𝑘 ) ) ) )
64 59 63 oveq12d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( ( 𝑃 pCnt ( ! ‘ ( 𝑁 − 𝐾 ) ) ) + ( 𝑃 pCnt ( ! ‘ 𝐾 ) ) ) = ( Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ⌊ ‘ ( ( 𝑁 − 𝐾 ) / ( 𝑃 ↑ 𝑘 ) ) ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ⌊ ‘ ( 𝐾 / ( 𝑃 ↑ 𝑘 ) ) ) ) )
65 9 nnzd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( ! ‘ ( 𝑁 − 𝐾 ) ) ∈ ℤ )
66 9 nnne0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( ! ‘ ( 𝑁 − 𝐾 ) ) ≠ 0 )
67 12 nnzd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( ! ‘ 𝐾 ) ∈ ℤ )
68 12 nnne0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( ! ‘ 𝐾 ) ≠ 0 )
69 pcmul ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( ! ‘ ( 𝑁 − 𝐾 ) ) ∈ ℤ ∧ ( ! ‘ ( 𝑁 − 𝐾 ) ) ≠ 0 ) ∧ ( ( ! ‘ 𝐾 ) ∈ ℤ ∧ ( ! ‘ 𝐾 ) ≠ 0 ) ) → ( 𝑃 pCnt ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) = ( ( 𝑃 pCnt ( ! ‘ ( 𝑁 − 𝐾 ) ) ) + ( 𝑃 pCnt ( ! ‘ 𝐾 ) ) ) )
70 1 65 66 67 68 69 syl122anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( 𝑃 pCnt ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) = ( ( 𝑃 pCnt ( ! ‘ ( 𝑁 − 𝐾 ) ) ) + ( 𝑃 pCnt ( ! ‘ 𝐾 ) ) ) )
71 19 38 42 fsumadd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( ⌊ ‘ ( ( 𝑁 − 𝐾 ) / ( 𝑃 ↑ 𝑘 ) ) ) + ( ⌊ ‘ ( 𝐾 / ( 𝑃 ↑ 𝑘 ) ) ) ) = ( Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ⌊ ‘ ( ( 𝑁 − 𝐾 ) / ( 𝑃 ↑ 𝑘 ) ) ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ⌊ ‘ ( 𝐾 / ( 𝑃 ↑ 𝑘 ) ) ) ) )
72 64 70 71 3eqtr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( 𝑃 pCnt ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( ⌊ ‘ ( ( 𝑁 − 𝐾 ) / ( 𝑃 ↑ 𝑘 ) ) ) + ( ⌊ ‘ ( 𝐾 / ( 𝑃 ↑ 𝑘 ) ) ) ) )
73 49 72 oveq12d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( ( 𝑃 pCnt ( ! ‘ 𝑁 ) ) − ( 𝑃 pCnt ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) ) = ( Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) − Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( ⌊ ‘ ( ( 𝑁 − 𝐾 ) / ( 𝑃 ↑ 𝑘 ) ) ) + ( ⌊ ‘ ( 𝐾 / ( 𝑃 ↑ 𝑘 ) ) ) ) ) )
74 44 73 eqtr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) − ( ( ⌊ ‘ ( ( 𝑁 − 𝐾 ) / ( 𝑃 ↑ 𝑘 ) ) ) + ( ⌊ ‘ ( 𝐾 / ( 𝑃 ↑ 𝑘 ) ) ) ) ) = ( ( 𝑃 pCnt ( ! ‘ 𝑁 ) ) − ( 𝑃 pCnt ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) ) )
75 15 18 74 3eqtr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( 𝑃 pCnt ( 𝑁 C 𝐾 ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) − ( ( ⌊ ‘ ( ( 𝑁 − 𝐾 ) / ( 𝑃 ↑ 𝑘 ) ) ) + ( ⌊ ‘ ( 𝐾 / ( 𝑃 ↑ 𝑘 ) ) ) ) ) )