Metamath Proof Explorer

Theorem 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 ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∉ ℙ ) → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 )

Proof

Step Hyp Ref Expression
1 uzp1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 = 2 ∨ 𝑁 ∈ ( ℤ≥ ‘ ( 2 + 1 ) ) ) )
2 neleq1 ⊢ ( 𝑁 = 2 → ( 𝑁 ∉ ℙ ↔ 2 ∉ ℙ ) )
3 2prm ⊢ 2 ∈ ℙ
4 pm2.24nel ⊢ ( 2 ∈ ℙ → ( 2 ∉ ℙ → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 ) )
5 3 4 ax-mp ⊢ ( 2 ∉ ℙ → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 )
6 2 5 biimtrdi ⊢ ( 𝑁 = 2 → ( 𝑁 ∉ ℙ → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 ) )
7 uzp1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 = 3 ∨ 𝑁 ∈ ( ℤ≥ ‘ ( 3 + 1 ) ) ) )
8 neleq1 ⊢ ( 𝑁 = 3 → ( 𝑁 ∉ ℙ ↔ 3 ∉ ℙ ) )
9 3prm ⊢ 3 ∈ ℙ
10 pm2.24nel ⊢ ( 3 ∈ ℙ → ( 3 ∉ ℙ → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 ) )
11 9 10 ax-mp ⊢ ( 3 ∉ ℙ → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 )
12 8 11 biimtrdi ⊢ ( 𝑁 = 3 → ( 𝑁 ∉ ℙ → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 ) )
13 uzp1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( 𝑁 = 4 ∨ 𝑁 ∈ ( ℤ≥ ‘ ( 4 + 1 ) ) ) )
14 fvoveq1 ⊢ ( 𝑁 = 4 → ( ! ‘ ( 𝑁 − 1 ) ) = ( ! ‘ ( 4 − 1 ) ) )
15 14 oveq1d ⊢ ( 𝑁 = 4 → ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) = ( ( ! ‘ ( 4 − 1 ) ) + 1 ) )
16 id ⊢ ( 𝑁 = 4 → 𝑁 = 4 )
17 15 16 oveq12d ⊢ ( 𝑁 = 4 → ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) = ( ( ( ! ‘ ( 4 − 1 ) ) + 1 ) / 4 ) )
18 14 16 oveq12d ⊢ ( 𝑁 = 4 → ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) = ( ( ! ‘ ( 4 − 1 ) ) / 4 ) )
19 18 fveq2d ⊢ ( 𝑁 = 4 → ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) = ( ⌊ ‘ ( ( ! ‘ ( 4 − 1 ) ) / 4 ) ) )
20 17 19 oveq12d ⊢ ( 𝑁 = 4 → ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) = ( ( ( ( ! ‘ ( 4 − 1 ) ) + 1 ) / 4 ) − ( ⌊ ‘ ( ( ! ‘ ( 4 − 1 ) ) / 4 ) ) ) )
21 20 fveq2d ⊢ ( 𝑁 = 4 → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = ( ⌊ ‘ ( ( ( ( ! ‘ ( 4 − 1 ) ) + 1 ) / 4 ) − ( ⌊ ‘ ( ( ! ‘ ( 4 − 1 ) ) / 4 ) ) ) ) )
22 ppivalnn4 ⊢ ( ⌊ ‘ ( ( ( ( ! ‘ ( 4 − 1 ) ) + 1 ) / 4 ) − ( ⌊ ‘ ( ( ! ‘ ( 4 − 1 ) ) / 4 ) ) ) ) = 0
23 21 22 eqtrdi ⊢ ( 𝑁 = 4 → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 )
24 23 a1d ⊢ ( 𝑁 = 4 → ( 𝑁 ∉ ℙ → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 ) )
25 uzp1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) → ( 𝑁 = 5 ∨ 𝑁 ∈ ( ℤ≥ ‘ ( 5 + 1 ) ) ) )
26 neleq1 ⊢ ( 𝑁 = 5 → ( 𝑁 ∉ ℙ ↔ 5 ∉ ℙ ) )
27 5prm ⊢ 5 ∈ ℙ
28 pm2.24nel ⊢ ( 5 ∈ ℙ → ( 5 ∉ ℙ → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 ) )
29 27 28 ax-mp ⊢ ( 5 ∉ ℙ → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 )
30 26 29 biimtrdi ⊢ ( 𝑁 = 5 → ( 𝑁 ∉ ℙ → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 ) )
31 ppivalnnnprmge6 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝑁 ∉ ℙ ) → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 )
32 31 ex ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) → ( 𝑁 ∉ ℙ → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 ) )
33 5p1e6 ⊢ ( 5 + 1 ) = 6
34 33 fveq2i ⊢ ( ℤ≥ ‘ ( 5 + 1 ) ) = ( ℤ≥ ‘ 6 )
35 32 34 eleq2s ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 5 + 1 ) ) → ( 𝑁 ∉ ℙ → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 ) )
36 30 35 jaoi ⊢ ( ( 𝑁 = 5 ∨ 𝑁 ∈ ( ℤ≥ ‘ ( 5 + 1 ) ) ) → ( 𝑁 ∉ ℙ → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 ) )
37 25 36 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) → ( 𝑁 ∉ ℙ → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 ) )
38 4p1e5 ⊢ ( 4 + 1 ) = 5
39 38 fveq2i ⊢ ( ℤ≥ ‘ ( 4 + 1 ) ) = ( ℤ≥ ‘ 5 )
40 37 39 eleq2s ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 4 + 1 ) ) → ( 𝑁 ∉ ℙ → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 ) )
41 24 40 jaoi ⊢ ( ( 𝑁 = 4 ∨ 𝑁 ∈ ( ℤ≥ ‘ ( 4 + 1 ) ) ) → ( 𝑁 ∉ ℙ → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 ) )
42 13 41 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( 𝑁 ∉ ℙ → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 ) )
43 3p1e4 ⊢ ( 3 + 1 ) = 4
44 43 fveq2i ⊢ ( ℤ≥ ‘ ( 3 + 1 ) ) = ( ℤ≥ ‘ 4 )
45 42 44 eleq2s ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 3 + 1 ) ) → ( 𝑁 ∉ ℙ → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 ) )
46 12 45 jaoi ⊢ ( ( 𝑁 = 3 ∨ 𝑁 ∈ ( ℤ≥ ‘ ( 3 + 1 ) ) ) → ( 𝑁 ∉ ℙ → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 ) )
47 7 46 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 ∉ ℙ → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 ) )
48 2p1e3 ⊢ ( 2 + 1 ) = 3
49 48 fveq2i ⊢ ( ℤ≥ ‘ ( 2 + 1 ) ) = ( ℤ≥ ‘ 3 )
50 47 49 eleq2s ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 + 1 ) ) → ( 𝑁 ∉ ℙ → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 ) )
51 6 50 jaoi ⊢ ( ( 𝑁 = 2 ∨ 𝑁 ∈ ( ℤ≥ ‘ ( 2 + 1 ) ) ) → ( 𝑁 ∉ ℙ → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 ) )
52 1 51 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 ∉ ℙ → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 ) )
53 52 imp ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∉ ℙ ) → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) / 𝑁 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑁 − 1 ) ) / 𝑁 ) ) ) ) = 0 )