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	imbitrid	⊢ ( ( ( 𝑛 ∈ ℕ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 ... 𝑀 ) ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) )