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 ... 𝑀 ) ( ⌊ β€˜ ( 𝑁 / ( 𝑃 ↑ π‘˜ ) ) ) )