ppivalnn

Description: Value of the prime-counting function pi for positive integers, according to Ján Mináč, see statement in Ribenboim, p. 181. (Contributed by AV, 10-Apr-2026)

		Ref	Expression
	Assertion	ppivalnn	$⊢ N \in ℕ \to \underline{π} (N) = \sum_{k = 2}^{N} ⌊(\frac{(k - 1)! + 1}{k}) - ⌊\frac{(k - 1)!}{k}⌋⌋$

Proof

Step	Hyp	Ref	Expression
1		elnn1uz2	$⊢ N \in ℕ \leftrightarrow (N = 1 \lor N \in ℤ_{\geq 2})$
2		ppi1sum	$⊢ \underline{π} (1) = \sum_{k \in \emptyset} ⌊(\frac{(k - 1)! + 1}{k}) - ⌊\frac{(k - 1)!}{k}⌋⌋$
3		fveq2	$⊢ N = 1 \to \underline{π} (N) = \underline{π} (1)$
4		oveq2	$⊢ N = 1 \to (2 \dots N) = (2 \dots 1)$
5		1lt2	$⊢ 1 < 2$
6		2z	$⊢ 2 \in ℤ$
7		1z	$⊢ 1 \in ℤ$
8		fzn	$⊢ (2 \in ℤ \land 1 \in ℤ) \to (1 < 2 \leftrightarrow (2 \dots 1) = \emptyset)$
9	6 7 8	mp2an	$⊢ 1 < 2 \leftrightarrow (2 \dots 1) = \emptyset$
10	5 9	mpbi	$⊢ (2 \dots 1) = \emptyset$
11	4 10	eqtrdi	$⊢ N = 1 \to (2 \dots N) = \emptyset$
12	11	sumeq1d	$⊢ N = 1 \to \sum_{k = 2}^{N} ⌊(\frac{(k - 1)! + 1}{k}) - ⌊\frac{(k - 1)!}{k}⌋⌋ = \sum_{k \in \emptyset} ⌊(\frac{(k - 1)! + 1}{k}) - ⌊\frac{(k - 1)!}{k}⌋⌋$
13	2 3 12	3eqtr4a	$⊢ N = 1 \to \underline{π} (N) = \sum_{k = 2}^{N} ⌊(\frac{(k - 1)! + 1}{k}) - ⌊\frac{(k - 1)!}{k}⌋⌋$
14		fzfid	$⊢ N \in ℤ_{\geq 2} \to (2 \dots N) \in Fin$
15		inss1	$⊢ (2 \dots N) \cap ℙ \subseteq (2 \dots N)$
16		eqid	$⊢ 𝟙_{(2 \dots N)} ((2 \dots N) \cap ℙ) = 𝟙_{(2 \dots N)} ((2 \dots N) \cap ℙ)$
17	16	indsumhash	$⊢ ((2 \dots N) \in Fin \land (2 \dots N) \cap ℙ \subseteq (2 \dots N)) \to \sum_{k = 2}^{N} 𝟙_{(2 \dots N)} ((2 \dots N) \cap ℙ) (k) = \|(2 \dots N) \cap ℙ\|$
18	14 15 17	sylancl	$⊢ N \in ℤ_{\geq 2} \to \sum_{k = 2}^{N} 𝟙_{(2 \dots N)} ((2 \dots N) \cap ℙ) (k) = \|(2 \dots N) \cap ℙ\|$
19		eqid	$⊢ (2 \dots N) = (2 \dots N)$
20	19	indprmfz	$⊢ 𝟙_{(2 \dots N)} ((2 \dots N) \cap ℙ) = (n \in (2 \dots N) ⟼ ⌊(\frac{(n - 1)! + 1}{n}) - ⌊\frac{(n - 1)!}{n}⌋⌋)$
21		fvoveq1	$⊢ n = k \to (n - 1)! = (k - 1)!$
22	21	oveq1d	$⊢ n = k \to (n - 1)! + 1 = (k - 1)! + 1$
23		id	$⊢ n = k \to n = k$
24	22 23	oveq12d	$⊢ n = k \to \frac{(n - 1)! + 1}{n} = \frac{(k - 1)! + 1}{k}$
25	21 23	oveq12d	$⊢ n = k \to \frac{(n - 1)!}{n} = \frac{(k - 1)!}{k}$
26	25	fveq2d	$⊢ n = k \to ⌊\frac{(n - 1)!}{n}⌋ = ⌊\frac{(k - 1)!}{k}⌋$
27	24 26	oveq12d	$⊢ n = k \to (\frac{(n - 1)! + 1}{n}) - ⌊\frac{(n - 1)!}{n}⌋ = (\frac{(k - 1)! + 1}{k}) - ⌊\frac{(k - 1)!}{k}⌋$
28	27	fveq2d	$⊢ n = k \to ⌊(\frac{(n - 1)! + 1}{n}) - ⌊\frac{(n - 1)!}{n}⌋⌋ = ⌊(\frac{(k - 1)! + 1}{k}) - ⌊\frac{(k - 1)!}{k}⌋⌋$
29		simpr	$⊢ (N \in ℤ_{\geq 2} \land k \in (2 \dots N)) \to k \in (2 \dots N)$
30		fvexd	$⊢ (N \in ℤ_{\geq 2} \land k \in (2 \dots N)) \to ⌊(\frac{(k - 1)! + 1}{k}) - ⌊\frac{(k - 1)!}{k}⌋⌋ \in V$
31	20 28 29 30	fvmptd3	$⊢ (N \in ℤ_{\geq 2} \land k \in (2 \dots N)) \to 𝟙_{(2 \dots N)} ((2 \dots N) \cap ℙ) (k) = ⌊(\frac{(k - 1)! + 1}{k}) - ⌊\frac{(k - 1)!}{k}⌋⌋$
32	31	eqcomd	$⊢ (N \in ℤ_{\geq 2} \land k \in (2 \dots N)) \to ⌊(\frac{(k - 1)! + 1}{k}) - ⌊\frac{(k - 1)!}{k}⌋⌋ = 𝟙_{(2 \dots N)} ((2 \dots N) \cap ℙ) (k)$
33	32	sumeq2dv	$⊢ N \in ℤ_{\geq 2} \to \sum_{k = 2}^{N} ⌊(\frac{(k - 1)! + 1}{k}) - ⌊\frac{(k - 1)!}{k}⌋⌋ = \sum_{k = 2}^{N} 𝟙_{(2 \dots N)} ((2 \dots N) \cap ℙ) (k)$
34		eluzelz	$⊢ N \in ℤ_{\geq 2} \to N \in ℤ$
35		ppival2	$⊢ N \in ℤ \to \underline{π} (N) = \|(2 \dots N) \cap ℙ\|$
36	34 35	syl	$⊢ N \in ℤ_{\geq 2} \to \underline{π} (N) = \|(2 \dots N) \cap ℙ\|$
37	18 33 36	3eqtr4rd	$⊢ N \in ℤ_{\geq 2} \to \underline{π} (N) = \sum_{k = 2}^{N} ⌊(\frac{(k - 1)! + 1}{k}) - ⌊\frac{(k - 1)!}{k}⌋⌋$
38	13 37	jaoi	$⊢ (N = 1 \lor N \in ℤ_{\geq 2}) \to \underline{π} (N) = \sum_{k = 2}^{N} ⌊(\frac{(k - 1)! + 1}{k}) - ⌊\frac{(k - 1)!}{k}⌋⌋$
39	1 38	sylbi	$⊢ N \in ℕ \to \underline{π} (N) = \sum_{k = 2}^{N} ⌊(\frac{(k - 1)! + 1}{k}) - ⌊\frac{(k - 1)!}{k}⌋⌋$

Metamath Proof Explorer

Theorem ppivalnn

Proof