ppivalnnprm

Description: Value of a term of the prime-counting function pi for positive integers, according to Ján Mináč, for a prime number. (Contributed by AV, 10-Apr-2026)

		Ref	Expression
	Assertion	ppivalnnprm	$⊢ P \in ℙ \to ⌊(\frac{(P - 1)! + 1}{P}) - ⌊\frac{(P - 1)!}{P}⌋⌋ = 1$

Proof

Step	Hyp	Ref	Expression
1		wilth	$⊢ P \in ℙ \leftrightarrow (P \in ℤ_{\geq 2} \land P ∥ ((P - 1)! + 1))$
2		eluzelz	$⊢ P \in ℤ_{\geq 2} \to P \in ℤ$
3		eluz2nn	$⊢ P \in ℤ_{\geq 2} \to P \in ℕ$
4		nnm1nn0	$⊢ P \in ℕ \to P - 1 \in ℕ_{0}$
5	3 4	syl	$⊢ P \in ℤ_{\geq 2} \to P - 1 \in ℕ_{0}$
6	5	faccld	$⊢ P \in ℤ_{\geq 2} \to (P - 1)! \in ℕ$
7	6	nnzd	$⊢ P \in ℤ_{\geq 2} \to (P - 1)! \in ℤ$
8	7	peano2zd	$⊢ P \in ℤ_{\geq 2} \to (P - 1)! + 1 \in ℤ$
9		divides	$⊢ (P \in ℤ \land (P - 1)! + 1 \in ℤ) \to (P ∥ ((P - 1)! + 1) \leftrightarrow \exists m \in ℤ m P = (P - 1)! + 1)$
10	2 8 9	syl2anc	$⊢ P \in ℤ_{\geq 2} \to (P ∥ ((P - 1)! + 1) \leftrightarrow \exists m \in ℤ m P = (P - 1)! + 1)$
11		oveq1	$⊢ (P - 1)! + 1 = m P \to \frac{(P - 1)! + 1}{P} = \frac{m P}{P}$
12	11	eqcoms	$⊢ m P = (P - 1)! + 1 \to \frac{(P - 1)! + 1}{P} = \frac{m P}{P}$
13		zcn	$⊢ m \in ℤ \to m \in ℂ$
14	13	adantl	$⊢ (P \in ℤ_{\geq 2} \land m \in ℤ) \to m \in ℂ$
15		eluzelcn	$⊢ P \in ℤ_{\geq 2} \to P \in ℂ$
16	15	adantr	$⊢ (P \in ℤ_{\geq 2} \land m \in ℤ) \to P \in ℂ$
17		eluz2n0	$⊢ P \in ℤ_{\geq 2} \to P \neq 0$
18	17	adantr	$⊢ (P \in ℤ_{\geq 2} \land m \in ℤ) \to P \neq 0$
19	14 16 18	divcan4d	$⊢ (P \in ℤ_{\geq 2} \land m \in ℤ) \to \frac{m P}{P} = m$
20	12 19	sylan9eqr	$⊢ ((P \in ℤ_{\geq 2} \land m \in ℤ) \land m P = (P - 1)! + 1) \to \frac{(P - 1)! + 1}{P} = m$
21	6	nncnd	$⊢ P \in ℤ_{\geq 2} \to (P - 1)! \in ℂ$
22		pncan1	$⊢ (P - 1)! \in ℂ \to (P - 1)! + 1 - 1 = (P - 1)!$
23	21 22	syl	$⊢ P \in ℤ_{\geq 2} \to (P - 1)! + 1 - 1 = (P - 1)!$
24	23	eqcomd	$⊢ P \in ℤ_{\geq 2} \to (P - 1)! = (P - 1)! + 1 - 1$
25	24	adantr	$⊢ (P \in ℤ_{\geq 2} \land m \in ℤ) \to (P - 1)! = (P - 1)! + 1 - 1$
26		oveq1	$⊢ (P - 1)! + 1 = m P \to (P - 1)! + 1 - 1 = m P - 1$
27	26	eqcoms	$⊢ m P = (P - 1)! + 1 \to (P - 1)! + 1 - 1 = m P - 1$
28	25 27	sylan9eq	$⊢ ((P \in ℤ_{\geq 2} \land m \in ℤ) \land m P = (P - 1)! + 1) \to (P - 1)! = m P - 1$
29	28	oveq1d	$⊢ ((P \in ℤ_{\geq 2} \land m \in ℤ) \land m P = (P - 1)! + 1) \to \frac{(P - 1)!}{P} = \frac{m P - 1}{P}$
30		simpr	$⊢ (P \in ℤ_{\geq 2} \land m \in ℤ) \to m \in ℤ$
31	2	adantr	$⊢ (P \in ℤ_{\geq 2} \land m \in ℤ) \to P \in ℤ$
32	30 31	zmulcld	$⊢ (P \in ℤ_{\geq 2} \land m \in ℤ) \to m P \in ℤ$
33	32	zcnd	$⊢ (P \in ℤ_{\geq 2} \land m \in ℤ) \to m P \in ℂ$
34		1cnd	$⊢ (P \in ℤ_{\geq 2} \land m \in ℤ) \to 1 \in ℂ$
35	33 34 16 18	divsubdird	$⊢ (P \in ℤ_{\geq 2} \land m \in ℤ) \to \frac{m P - 1}{P} = (\frac{m P}{P}) - (\frac{1}{P})$
36	19	oveq1d	$⊢ (P \in ℤ_{\geq 2} \land m \in ℤ) \to (\frac{m P}{P}) - (\frac{1}{P}) = m - (\frac{1}{P})$
37	35 36	eqtrd	$⊢ (P \in ℤ_{\geq 2} \land m \in ℤ) \to \frac{m P - 1}{P} = m - (\frac{1}{P})$
38	37	adantr	$⊢ ((P \in ℤ_{\geq 2} \land m \in ℤ) \land m P = (P - 1)! + 1) \to \frac{m P - 1}{P} = m - (\frac{1}{P})$
39	29 38	eqtrd	$⊢ ((P \in ℤ_{\geq 2} \land m \in ℤ) \land m P = (P - 1)! + 1) \to \frac{(P - 1)!}{P} = m - (\frac{1}{P})$
40	39	fveq2d	$⊢ ((P \in ℤ_{\geq 2} \land m \in ℤ) \land m P = (P - 1)! + 1) \to ⌊\frac{(P - 1)!}{P}⌋ = ⌊m - (\frac{1}{P})⌋$
41	3	anim1ci	$⊢ (P \in ℤ_{\geq 2} \land m \in ℤ) \to (m \in ℤ \land P \in ℕ)$
42		flmrecm1	$⊢ (m \in ℤ \land P \in ℕ) \to ⌊m - (\frac{1}{P})⌋ = m - 1$
43	41 42	syl	$⊢ (P \in ℤ_{\geq 2} \land m \in ℤ) \to ⌊m - (\frac{1}{P})⌋ = m - 1$
44	43	adantr	$⊢ ((P \in ℤ_{\geq 2} \land m \in ℤ) \land m P = (P - 1)! + 1) \to ⌊m - (\frac{1}{P})⌋ = m - 1$
45	40 44	eqtrd	$⊢ ((P \in ℤ_{\geq 2} \land m \in ℤ) \land m P = (P - 1)! + 1) \to ⌊\frac{(P - 1)!}{P}⌋ = m - 1$
46	20 45	oveq12d	$⊢ ((P \in ℤ_{\geq 2} \land m \in ℤ) \land m P = (P - 1)! + 1) \to (\frac{(P - 1)! + 1}{P}) - ⌊\frac{(P - 1)!}{P}⌋ = m - (m - 1)$
47	46	fveq2d	$⊢ ((P \in ℤ_{\geq 2} \land m \in ℤ) \land m P = (P - 1)! + 1) \to ⌊(\frac{(P - 1)! + 1}{P}) - ⌊\frac{(P - 1)!}{P}⌋⌋ = ⌊m - (m - 1)⌋$
48		1cnd	$⊢ m \in ℤ \to 1 \in ℂ$
49	13 48	nncand	$⊢ m \in ℤ \to m - (m - 1) = 1$
50	49	fveq2d	$⊢ m \in ℤ \to ⌊m - (m - 1)⌋ = ⌊1⌋$
51		1z	$⊢ 1 \in ℤ$
52		flid	$⊢ 1 \in ℤ \to ⌊1⌋ = 1$
53	51 52	mp1i	$⊢ m \in ℤ \to ⌊1⌋ = 1$
54	50 53	eqtrd	$⊢ m \in ℤ \to ⌊m - (m - 1)⌋ = 1$
55	54	adantl	$⊢ (P \in ℤ_{\geq 2} \land m \in ℤ) \to ⌊m - (m - 1)⌋ = 1$
56	55	adantr	$⊢ ((P \in ℤ_{\geq 2} \land m \in ℤ) \land m P = (P - 1)! + 1) \to ⌊m - (m - 1)⌋ = 1$
57	47 56	eqtrd	$⊢ ((P \in ℤ_{\geq 2} \land m \in ℤ) \land m P = (P - 1)! + 1) \to ⌊(\frac{(P - 1)! + 1}{P}) - ⌊\frac{(P - 1)!}{P}⌋⌋ = 1$
58	57	ex	$⊢ (P \in ℤ_{\geq 2} \land m \in ℤ) \to (m P = (P - 1)! + 1 \to ⌊(\frac{(P - 1)! + 1}{P}) - ⌊\frac{(P - 1)!}{P}⌋⌋ = 1)$
59	58	rexlimdva	$⊢ P \in ℤ_{\geq 2} \to (\exists m \in ℤ m P = (P - 1)! + 1 \to ⌊(\frac{(P - 1)! + 1}{P}) - ⌊\frac{(P - 1)!}{P}⌋⌋ = 1)$
60	10 59	sylbid	$⊢ P \in ℤ_{\geq 2} \to (P ∥ ((P - 1)! + 1) \to ⌊(\frac{(P - 1)! + 1}{P}) - ⌊\frac{(P - 1)!}{P}⌋⌋ = 1)$
61	60	imp	$⊢ (P \in ℤ_{\geq 2} \land P ∥ ((P - 1)! + 1)) \to ⌊(\frac{(P - 1)! + 1}{P}) - ⌊\frac{(P - 1)!}{P}⌋⌋ = 1$
62	1 61	sylbi	$⊢ P \in ℙ \to ⌊(\frac{(P - 1)! + 1}{P}) - ⌊\frac{(P - 1)!}{P}⌋⌋ = 1$

Metamath Proof Explorer

Theorem ppivalnnprm

Proof