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 ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ℙ ) → ( 𝑃 pCnt ( ! ‘ 𝑁 ) ) = Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) )

Proof

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