ppivalnnnprm

Description: Value of a term of the prime-counting function pi for positive integers, according to Ján Miná&ccaron, for a non-prime number greater than 1. (Contributed by AV, 8-Apr-2026)

		Ref	Expression
	Assertion	ppivalnnnprm	$⊢ (N \in ℤ_{\geq 2} \land N \notin ℙ) \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0$

Proof

Step	Hyp	Ref	Expression
1		uzp1	$⊢ N \in ℤ_{\geq 2} \to (N = 2 \lor N \in ℤ_{\geq (2 + 1)})$
2		neleq1	$⊢ N = 2 \to (N \notin ℙ \leftrightarrow 2 \notin ℙ)$
3		2prm	$⊢ 2 \in ℙ$
4		pm2.24nel	$⊢ 2 \in ℙ \to (2 \notin ℙ \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0)$
5	3 4	ax-mp	$⊢ 2 \notin ℙ \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0$
6	2 5	biimtrdi	$⊢ N = 2 \to (N \notin ℙ \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0)$
7		uzp1	$⊢ N \in ℤ_{\geq 3} \to (N = 3 \lor N \in ℤ_{\geq (3 + 1)})$
8		neleq1	$⊢ N = 3 \to (N \notin ℙ \leftrightarrow 3 \notin ℙ)$
9		3prm	$⊢ 3 \in ℙ$
10		pm2.24nel	$⊢ 3 \in ℙ \to (3 \notin ℙ \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0)$
11	9 10	ax-mp	$⊢ 3 \notin ℙ \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0$
12	8 11	biimtrdi	$⊢ N = 3 \to (N \notin ℙ \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0)$
13		uzp1	$⊢ N \in ℤ_{\geq 4} \to (N = 4 \lor N \in ℤ_{\geq (4 + 1)})$
14		fvoveq1	$⊢ N = 4 \to (N - 1)! = (4 - 1)!$
15	14	oveq1d	$⊢ N = 4 \to (N - 1)! + 1 = (4 - 1)! + 1$
16		id	$⊢ N = 4 \to N = 4$
17	15 16	oveq12d	$⊢ N = 4 \to \frac{(N - 1)! + 1}{N} = \frac{(4 - 1)! + 1}{4}$
18	14 16	oveq12d	$⊢ N = 4 \to \frac{(N - 1)!}{N} = \frac{(4 - 1)!}{4}$
19	18	fveq2d	$⊢ N = 4 \to ⌊\frac{(N - 1)!}{N}⌋ = ⌊\frac{(4 - 1)!}{4}⌋$
20	17 19	oveq12d	$⊢ N = 4 \to (\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋ = (\frac{(4 - 1)! + 1}{4}) - ⌊\frac{(4 - 1)!}{4}⌋$
21	20	fveq2d	$⊢ N = 4 \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = ⌊(\frac{(4 - 1)! + 1}{4}) - ⌊\frac{(4 - 1)!}{4}⌋⌋$
22		ppivalnn4	$⊢ ⌊(\frac{(4 - 1)! + 1}{4}) - ⌊\frac{(4 - 1)!}{4}⌋⌋ = 0$
23	21 22	eqtrdi	$⊢ N = 4 \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0$
24	23	a1d	$⊢ N = 4 \to (N \notin ℙ \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0)$
25		uzp1	$⊢ N \in ℤ_{\geq 5} \to (N = 5 \lor N \in ℤ_{\geq (5 + 1)})$
26		neleq1	$⊢ N = 5 \to (N \notin ℙ \leftrightarrow 5 \notin ℙ)$
27		5prm	$⊢ 5 \in ℙ$
28		pm2.24nel	$⊢ 5 \in ℙ \to (5 \notin ℙ \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0)$
29	27 28	ax-mp	$⊢ 5 \notin ℙ \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0$
30	26 29	biimtrdi	$⊢ N = 5 \to (N \notin ℙ \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0)$
31		ppivalnnnprmge6	$⊢ (N \in ℤ_{\geq 6} \land N \notin ℙ) \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0$
32	31	ex	$⊢ N \in ℤ_{\geq 6} \to (N \notin ℙ \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0)$
33		5p1e6	$⊢ 5 + 1 = 6$
34	33	fveq2i	$⊢ ℤ_{\geq (5 + 1)} = ℤ_{\geq 6}$
35	32 34	eleq2s	$⊢ N \in ℤ_{\geq (5 + 1)} \to (N \notin ℙ \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0)$
36	30 35	jaoi	$⊢ (N = 5 \lor N \in ℤ_{\geq (5 + 1)}) \to (N \notin ℙ \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0)$
37	25 36	syl	$⊢ N \in ℤ_{\geq 5} \to (N \notin ℙ \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0)$
38		4p1e5	$⊢ 4 + 1 = 5$
39	38	fveq2i	$⊢ ℤ_{\geq (4 + 1)} = ℤ_{\geq 5}$
40	37 39	eleq2s	$⊢ N \in ℤ_{\geq (4 + 1)} \to (N \notin ℙ \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0)$
41	24 40	jaoi	$⊢ (N = 4 \lor N \in ℤ_{\geq (4 + 1)}) \to (N \notin ℙ \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0)$
42	13 41	syl	$⊢ N \in ℤ_{\geq 4} \to (N \notin ℙ \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0)$
43		3p1e4	$⊢ 3 + 1 = 4$
44	43	fveq2i	$⊢ ℤ_{\geq (3 + 1)} = ℤ_{\geq 4}$
45	42 44	eleq2s	$⊢ N \in ℤ_{\geq (3 + 1)} \to (N \notin ℙ \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0)$
46	12 45	jaoi	$⊢ (N = 3 \lor N \in ℤ_{\geq (3 + 1)}) \to (N \notin ℙ \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0)$
47	7 46	syl	$⊢ N \in ℤ_{\geq 3} \to (N \notin ℙ \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0)$
48		2p1e3	$⊢ 2 + 1 = 3$
49	48	fveq2i	$⊢ ℤ_{\geq (2 + 1)} = ℤ_{\geq 3}$
50	47 49	eleq2s	$⊢ N \in ℤ_{\geq (2 + 1)} \to (N \notin ℙ \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0)$
51	6 50	jaoi	$⊢ (N = 2 \lor N \in ℤ_{\geq (2 + 1)}) \to (N \notin ℙ \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0)$
52	1 51	syl	$⊢ N \in ℤ_{\geq 2} \to (N \notin ℙ \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0)$
53	52	imp	$⊢ (N \in ℤ_{\geq 2} \land N \notin ℙ) \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0$

Metamath Proof Explorer

Theorem ppivalnnnprm

Proof