ppivalnnnprmge6

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

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

Proof

Step	Hyp	Ref	Expression
1		nprmdvdsfacm1	$⊢ (N \in ℤ_{\geq 6} \land N \notin ℙ) \to N ∥ (N - 1)!$
2		eluzelz	$⊢ N \in ℤ_{\geq 6} \to N \in ℤ$
3		6nn	$⊢ 6 \in ℕ$
4		elnnuz	$⊢ 6 \in ℕ \leftrightarrow 6 \in ℤ_{\geq 1}$
5	3 4	mpbi	$⊢ 6 \in ℤ_{\geq 1}$
6		uzss	$⊢ 6 \in ℤ_{\geq 1} \to ℤ_{\geq 6} \subseteq ℤ_{\geq 1}$
7	5 6	ax-mp	$⊢ ℤ_{\geq 6} \subseteq ℤ_{\geq 1}$
8	7	sseli	$⊢ N \in ℤ_{\geq 6} \to N \in ℤ_{\geq 1}$
9		elnnuz	$⊢ N \in ℕ \leftrightarrow N \in ℤ_{\geq 1}$
10	8 9	sylibr	$⊢ N \in ℤ_{\geq 6} \to N \in ℕ$
11		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
12	10 11	syl	$⊢ N \in ℤ_{\geq 6} \to N - 1 \in ℕ_{0}$
13	12	faccld	$⊢ N \in ℤ_{\geq 6} \to (N - 1)! \in ℕ$
14	13	nnzd	$⊢ N \in ℤ_{\geq 6} \to (N - 1)! \in ℤ$
15		divides	$⊢ (N \in ℤ \land (N - 1)! \in ℤ) \to (N ∥ (N - 1)! \leftrightarrow \exists m \in ℤ m \cdot N = (N - 1)!)$
16	2 14 15	syl2anc	$⊢ N \in ℤ_{\geq 6} \to (N ∥ (N - 1)! \leftrightarrow \exists m \in ℤ m \cdot N = (N - 1)!)$
17		oveq1	$⊢ (N - 1)! = m \cdot N \to (N - 1)! + 1 = m \cdot N + 1$
18	17	oveq1d	$⊢ (N - 1)! = m \cdot N \to \frac{(N - 1)! + 1}{N} = \frac{m \cdot N + 1}{N}$
19		fvoveq1	$⊢ (N - 1)! = m \cdot N \to ⌊\frac{(N - 1)!}{N}⌋ = ⌊\frac{m \cdot N}{N}⌋$
20	18 19	oveq12d	$⊢ (N - 1)! = m \cdot N \to (\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋ = (\frac{m \cdot N + 1}{N}) - ⌊\frac{m \cdot N}{N}⌋$
21	20	fveq2d	$⊢ (N - 1)! = m \cdot N \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = ⌊(\frac{m \cdot N + 1}{N}) - ⌊\frac{m \cdot N}{N}⌋⌋$
22	21	eqcoms	$⊢ m \cdot N = (N - 1)! \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = ⌊(\frac{m \cdot N + 1}{N}) - ⌊\frac{m \cdot N}{N}⌋⌋$
23		zcn	$⊢ m \in ℤ \to m \in ℂ$
24	23	adantl	$⊢ (N \in ℤ_{\geq 6} \land m \in ℤ) \to m \in ℂ$
25		eluzelcn	$⊢ N \in ℤ_{\geq 6} \to N \in ℂ$
26	25	adantr	$⊢ (N \in ℤ_{\geq 6} \land m \in ℤ) \to N \in ℂ$
27		1cnd	$⊢ (N \in ℤ_{\geq 6} \land m \in ℤ) \to 1 \in ℂ$
28	10	nnne0d	$⊢ N \in ℤ_{\geq 6} \to N \neq 0$
29	28	adantr	$⊢ (N \in ℤ_{\geq 6} \land m \in ℤ) \to N \neq 0$
30	24 26 27 29	muldivdid	$⊢ (N \in ℤ_{\geq 6} \land m \in ℤ) \to \frac{m \cdot N + 1}{N} = m + (\frac{1}{N})$
31	24 26 29	divcan4d	$⊢ (N \in ℤ_{\geq 6} \land m \in ℤ) \to \frac{m \cdot N}{N} = m$
32	31	fveq2d	$⊢ (N \in ℤ_{\geq 6} \land m \in ℤ) \to ⌊\frac{m \cdot N}{N}⌋ = ⌊m⌋$
33		flid	$⊢ m \in ℤ \to ⌊m⌋ = m$
34	33	adantl	$⊢ (N \in ℤ_{\geq 6} \land m \in ℤ) \to ⌊m⌋ = m$
35	32 34	eqtrd	$⊢ (N \in ℤ_{\geq 6} \land m \in ℤ) \to ⌊\frac{m \cdot N}{N}⌋ = m$
36	30 35	oveq12d	$⊢ (N \in ℤ_{\geq 6} \land m \in ℤ) \to (\frac{m \cdot N + 1}{N}) - ⌊\frac{m \cdot N}{N}⌋ = m + (\frac{1}{N}) - m$
37	36	fveq2d	$⊢ (N \in ℤ_{\geq 6} \land m \in ℤ) \to ⌊(\frac{m \cdot N + 1}{N}) - ⌊\frac{m \cdot N}{N}⌋⌋ = ⌊m + (\frac{1}{N}) - m⌋$
38	25 28	reccld	$⊢ N \in ℤ_{\geq 6} \to \frac{1}{N} \in ℂ$
39	38	adantr	$⊢ (N \in ℤ_{\geq 6} \land m \in ℤ) \to \frac{1}{N} \in ℂ$
40	24 39	pncan2d	$⊢ (N \in ℤ_{\geq 6} \land m \in ℤ) \to m + (\frac{1}{N}) - m = \frac{1}{N}$
41	40	fveq2d	$⊢ (N \in ℤ_{\geq 6} \land m \in ℤ) \to ⌊m + (\frac{1}{N}) - m⌋ = ⌊\frac{1}{N}⌋$
42		2z	$⊢ 2 \in ℤ$
43	3	nnzi	$⊢ 6 \in ℤ$
44		2re	$⊢ 2 \in ℝ$
45		6re	$⊢ 6 \in ℝ$
46		2lt6	$⊢ 2 < 6$
47	44 45 46	ltleii	$⊢ 2 \leq 6$
48		eluz2	$⊢ 6 \in ℤ_{\geq 2} \leftrightarrow (2 \in ℤ \land 6 \in ℤ \land 2 \leq 6)$
49	42 43 47 48	mpbir3an	$⊢ 6 \in ℤ_{\geq 2}$
50		uzss	$⊢ 6 \in ℤ_{\geq 2} \to ℤ_{\geq 6} \subseteq ℤ_{\geq 2}$
51	49 50	ax-mp	$⊢ ℤ_{\geq 6} \subseteq ℤ_{\geq 2}$
52	51	sseli	$⊢ N \in ℤ_{\geq 6} \to N \in ℤ_{\geq 2}$
53		nnge2recfl0	$⊢ N \in ℤ_{\geq 2} \to ⌊\frac{1}{N}⌋ = 0$
54	52 53	syl	$⊢ N \in ℤ_{\geq 6} \to ⌊\frac{1}{N}⌋ = 0$
55	54	adantr	$⊢ (N \in ℤ_{\geq 6} \land m \in ℤ) \to ⌊\frac{1}{N}⌋ = 0$
56	37 41 55	3eqtrd	$⊢ (N \in ℤ_{\geq 6} \land m \in ℤ) \to ⌊(\frac{m \cdot N + 1}{N}) - ⌊\frac{m \cdot N}{N}⌋⌋ = 0$
57	22 56	sylan9eqr	$⊢ ((N \in ℤ_{\geq 6} \land m \in ℤ) \land m \cdot N = (N - 1)!) \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0$
58	57	ex	$⊢ (N \in ℤ_{\geq 6} \land m \in ℤ) \to (m \cdot N = (N - 1)! \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0)$
59	58	rexlimdva	$⊢ N \in ℤ_{\geq 6} \to (\exists m \in ℤ m \cdot N = (N - 1)! \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0)$
60	16 59	sylbid	$⊢ N \in ℤ_{\geq 6} \to (N ∥ (N - 1)! \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0)$
61	60	adantr	$⊢ (N \in ℤ_{\geq 6} \land N \notin ℙ) \to (N ∥ (N - 1)! \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0)$
62	1 61	mpd	$⊢ (N \in ℤ_{\geq 6} \land N \notin ℙ) \to ⌊(\frac{(N - 1)! + 1}{N}) - ⌊\frac{(N - 1)!}{N}⌋⌋ = 0$

Metamath Proof Explorer

Theorem ppivalnnnprmge6

Proof