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	⊢ ( ⌊ ‘ ( ( ( ( ! ‘ ( 4 − 1 ) ) + 1 ) / 4 ) − ( ⌊ ‘ ( ( ! ‘ ( 4 − 1 ) ) / 4 ) ) ) ) = 0

Proof

Step	Hyp	Ref	Expression
1		4m1e3	⊢ ( 4 − 1 ) = 3
2	1	fveq2i	⊢ ( ! ‘ ( 4 − 1 ) ) = ( ! ‘ 3 )
3		fac3	⊢ ( ! ‘ 3 ) = 6
4	2 3	eqtri	⊢ ( ! ‘ ( 4 − 1 ) ) = 6
5	4	oveq1i	⊢ ( ( ! ‘ ( 4 − 1 ) ) + 1 ) = ( 6 + 1 )
6		6p1e7	⊢ ( 6 + 1 ) = 7
7	5 6	eqtri	⊢ ( ( ! ‘ ( 4 − 1 ) ) + 1 ) = 7
8	7	oveq1i	⊢ ( ( ( ! ‘ ( 4 − 1 ) ) + 1 ) / 4 ) = ( 7 / 4 )
9	4	oveq1i	⊢ ( ( ! ‘ ( 4 − 1 ) ) / 4 ) = ( 6 / 4 )
10	9	fveq2i	⊢ ( ⌊ ‘ ( ( ! ‘ ( 4 − 1 ) ) / 4 ) ) = ( ⌊ ‘ ( 6 / 4 ) )
11		3t2e6	⊢ ( 3 · 2 ) = 6
12		2t2e4	⊢ ( 2 · 2 ) = 4
13	11 12	oveq12i	⊢ ( ( 3 · 2 ) / ( 2 · 2 ) ) = ( 6 / 4 )
14		2ne0	⊢ 2 ≠ 0
15		3cn	⊢ 3 ∈ ℂ
16	15	a1i	⊢ ( 2 ≠ 0 → 3 ∈ ℂ )
17		2cnd	⊢ ( 2 ≠ 0 → 2 ∈ ℂ )
18		id	⊢ ( 2 ≠ 0 → 2 ≠ 0 )
19	16 17 17 18 18	divcan5rd	⊢ ( 2 ≠ 0 → ( ( 3 · 2 ) / ( 2 · 2 ) ) = ( 3 / 2 ) )
20	14 19	ax-mp	⊢ ( ( 3 · 2 ) / ( 2 · 2 ) ) = ( 3 / 2 )
21	13 20	eqtr3i	⊢ ( 6 / 4 ) = ( 3 / 2 )
22	21	fveq2i	⊢ ( ⌊ ‘ ( 6 / 4 ) ) = ( ⌊ ‘ ( 3 / 2 ) )
23		ex-fl	⊢ ( ( ⌊ ‘ ( 3 / 2 ) ) = 1 ∧ ( ⌊ ‘ - ( 3 / 2 ) ) = - 2 )
24	23	simpli	⊢ ( ⌊ ‘ ( 3 / 2 ) ) = 1
25	10 22 24	3eqtri	⊢ ( ⌊ ‘ ( ( ! ‘ ( 4 − 1 ) ) / 4 ) ) = 1
26	8 25	oveq12i	⊢ ( ( ( ( ! ‘ ( 4 − 1 ) ) + 1 ) / 4 ) − ( ⌊ ‘ ( ( ! ‘ ( 4 − 1 ) ) / 4 ) ) ) = ( ( 7 / 4 ) − 1 )
27	26	fveq2i	⊢ ( ⌊ ‘ ( ( ( ( ! ‘ ( 4 − 1 ) ) + 1 ) / 4 ) − ( ⌊ ‘ ( ( ! ‘ ( 4 − 1 ) ) / 4 ) ) ) ) = ( ⌊ ‘ ( ( 7 / 4 ) − 1 ) )
28		4cn	⊢ 4 ∈ ℂ
29		4ne0	⊢ 4 ≠ 0
30	28 29	dividi	⊢ ( 4 / 4 ) = 1
31	30	eqcomi	⊢ 1 = ( 4 / 4 )
32	31	oveq2i	⊢ ( ( 7 / 4 ) − 1 ) = ( ( 7 / 4 ) − ( 4 / 4 ) )
33		7cn	⊢ 7 ∈ ℂ
34	28 29	pm3.2i	⊢ ( 4 ∈ ℂ ∧ 4 ≠ 0 )
35		divsubdir	⊢ ( ( 7 ∈ ℂ ∧ 4 ∈ ℂ ∧ ( 4 ∈ ℂ ∧ 4 ≠ 0 ) ) → ( ( 7 − 4 ) / 4 ) = ( ( 7 / 4 ) − ( 4 / 4 ) ) )
36	33 28 34 35	mp3an	⊢ ( ( 7 − 4 ) / 4 ) = ( ( 7 / 4 ) − ( 4 / 4 ) )
37		4p3e7	⊢ ( 4 + 3 ) = 7
38	37	eqcomi	⊢ 7 = ( 4 + 3 )
39	28 15 38	mvrladdi	⊢ ( 7 − 4 ) = 3
40	39	oveq1i	⊢ ( ( 7 − 4 ) / 4 ) = ( 3 / 4 )
41	36 40	eqtr3i	⊢ ( ( 7 / 4 ) − ( 4 / 4 ) ) = ( 3 / 4 )
42	32 41	eqtri	⊢ ( ( 7 / 4 ) − 1 ) = ( 3 / 4 )
43	42	fveq2i	⊢ ( ⌊ ‘ ( ( 7 / 4 ) − 1 ) ) = ( ⌊ ‘ ( 3 / 4 ) )
44		3lt4	⊢ 3 < 4
45		3nn0	⊢ 3 ∈ ℕ0
46		4nn	⊢ 4 ∈ ℕ
47		divfl0	⊢ ( ( 3 ∈ ℕ0 ∧ 4 ∈ ℕ ) → ( 3 < 4 ↔ ( ⌊ ‘ ( 3 / 4 ) ) = 0 ) )
48	45 46 47	mp2an	⊢ ( 3 < 4 ↔ ( ⌊ ‘ ( 3 / 4 ) ) = 0 )
49	44 48	mpbi	⊢ ( ⌊ ‘ ( 3 / 4 ) ) = 0
50	27 43 49	3eqtri	⊢ ( ⌊ ‘ ( ( ( ( ! ‘ ( 4 − 1 ) ) + 1 ) / 4 ) − ( ⌊ ‘ ( ( ! ‘ ( 4 − 1 ) ) / 4 ) ) ) ) = 0