Theorem ppivalnn4

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

	Ref	Expression
Assertion	ppivalnn4	$$⊢⌊\left(\frac{\left(4-1\right)!+1}{4}\right)-⌊\frac{\left(4-1\right)!}{4}⌋⌋=0$$

Proof

Step	Hyp	Ref	Expression
1		4m1e3	$$⊢4-1=3$$
2	1	fveq2i	$$⊢\left(4-1\right)!=3!$$
3		fac3	$$⊢3!=6$$
4	2 3	eqtri	$$⊢\left(4-1\right)!=6$$
5	4	oveq1i	$$⊢\left(4-1\right)!+1=6+1$$
6		6p1e7	$$⊢6+1=7$$
7	5 6	eqtri	$$⊢\left(4-1\right)!+1=7$$
8	7	oveq1i	$$⊢\frac{\left(4-1\right)!+1}{4}=\frac{7}{4}$$
9	4	oveq1i	$$⊢\frac{\left(4-1\right)!}{4}=\frac{6}{4}$$
10	9	fveq2i	$$⊢⌊\frac{\left(4-1\right)!}{4}⌋=⌊\frac{6}{4}⌋$$
11		3t2e6	$$⊢3\cdot 2=6$$
12		2t2e4	$$⊢2\cdot 2=4$$
13	11 12	oveq12i	$$⊢\frac{3\cdot 2}{2\cdot 2}=\frac{6}{4}$$
14		2ne0	$$⊢2\ne 0$$
15		3cn	$$⊢3\in ℂ$$
16	15	a1i	$$⊢2\ne 0\to 3\in ℂ$$
17		2cnd	$$⊢2\ne 0\to 2\in ℂ$$
18		id	$$⊢2\ne 0\to 2\ne 0$$
19	16 17 17 18 18	divcan5rd	$$⊢2\ne 0\to \frac{3\cdot 2}{2\cdot 2}=\frac{3}{2}$$
20	14 19	ax-mp	$$⊢\frac{3\cdot 2}{2\cdot 2}=\frac{3}{2}$$
21	13 20	eqtr3i	$$⊢\frac{6}{4}=\frac{3}{2}$$
22	21	fveq2i	$$⊢⌊\frac{6}{4}⌋=⌊\frac{3}{2}⌋$$
23		ex-fl	$$⊢\left(⌊\frac{3}{2}⌋=1\wedge ⌊-\frac{3}{2}⌋=-2\right)$$
24	23	simpli	$$⊢⌊\frac{3}{2}⌋=1$$
25	10 22 24	3eqtri	$$⊢⌊\frac{\left(4-1\right)!}{4}⌋=1$$
26	8 25	oveq12i	$$⊢\left(\frac{\left(4-1\right)!+1}{4}\right)-⌊\frac{\left(4-1\right)!}{4}⌋=\left(\frac{7}{4}\right)-1$$
27	26	fveq2i	$$⊢⌊\left(\frac{\left(4-1\right)!+1}{4}\right)-⌊\frac{\left(4-1\right)!}{4}⌋⌋=⌊\left(\frac{7}{4}\right)-1⌋$$
28		4cn	$$⊢4\in ℂ$$
29		4ne0	$$⊢4\ne 0$$
30	28 29	dividi	$$⊢\frac{4}{4}=1$$
31	30	eqcomi	$$⊢1=\frac{4}{4}$$
32	31	oveq2i	$$⊢\left(\frac{7}{4}\right)-1=\left(\frac{7}{4}\right)-\left(\frac{4}{4}\right)$$
33		7cn	$$⊢7\in ℂ$$
34	28 29	pm3.2i	$$⊢\left(4\in ℂ\wedge 4\ne 0\right)$$
35		divsubdir	$$⊢\left(7\in ℂ\wedge 4\in ℂ\wedge \left(4\in ℂ\wedge 4\ne 0\right)\right)\to \frac{7-4}{4}=\left(\frac{7}{4}\right)-\left(\frac{4}{4}\right)$$
36	33 28 34 35	mp3an	$$⊢\frac{7-4}{4}=\left(\frac{7}{4}\right)-\left(\frac{4}{4}\right)$$
37		4p3e7	$$⊢4+3=7$$
38	37	eqcomi	$$⊢7=4+3$$
39	28 15 38	mvrladdi	$$⊢7-4=3$$
40	39	oveq1i	$$⊢\frac{7-4}{4}=\frac{3}{4}$$
41	36 40	eqtr3i	$$⊢\left(\frac{7}{4}\right)-\left(\frac{4}{4}\right)=\frac{3}{4}$$
42	32 41	eqtri	$$⊢\left(\frac{7}{4}\right)-1=\frac{3}{4}$$
43	42	fveq2i	$$⊢⌊\left(\frac{7}{4}\right)-1⌋=⌊\frac{3}{4}⌋$$
44		3lt4	$$⊢3<4$$
45		3nn0	$$⊢3\in {\mathbb{N}}_0$$
46		4nn	$$⊢4\in \mathbb{N}$$
47		divfl0	$$⊢\left(3\in {\mathbb{N}}_0\wedge 4\in \mathbb{N}\right)\to \left(3<4\leftrightarrow ⌊\frac{3}{4}⌋=0\right)$$
48	45 46 47	mp2an	$$⊢3<4\leftrightarrow ⌊\frac{3}{4}⌋=0$$
49	44 48	mpbi	$$⊢⌊\frac{3}{4}⌋=0$$
50	27 43 49	3eqtri	$$⊢⌊\left(\frac{\left(4-1\right)!+1}{4}\right)-⌊\frac{\left(4-1\right)!}{4}⌋⌋=0$$