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	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N} \land P \in ℙ) \to P pCnt N! = \sum_{k = 1}^{M} ⌊\frac{N}{P^{k}}⌋$

Proof

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

Metamath Proof Explorer

Theorem pcfac

Proof