Metamath Proof Explorer

Theorem ppivalnn

Description: Value of the prime-counting function pi for positive integers, according to Ján Mináč, see statement in Ribenboim, p. 181. (Contributed by AV, 10-Apr-2026)

Ref Expression
Assertion ppivalnn ( 𝑁 ∈ ℕ → ( π ‘ 𝑁 ) = Σ 𝑘 ∈ ( 2 ... 𝑁 ) ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 elnn1uz2 ⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 = 1 ∨ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) )
2 ppi1sum ⊢ ( π ‘ 1 ) = Σ 𝑘 ∈ ∅ ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) )
3 fveq2 ⊢ ( 𝑁 = 1 → ( π ‘ 𝑁 ) = ( π ‘ 1 ) )
4 oveq2 ⊢ ( 𝑁 = 1 → ( 2 ... 𝑁 ) = ( 2 ... 1 ) )
5 1lt2 ⊢ 1 < 2
6 2z ⊢ 2 ∈ ℤ
7 1z ⊢ 1 ∈ ℤ
8 fzn ⊢ ( ( 2 ∈ ℤ ∧ 1 ∈ ℤ ) → ( 1 < 2 ↔ ( 2 ... 1 ) = ∅ ) )
9 6 7 8 mp2an ⊢ ( 1 < 2 ↔ ( 2 ... 1 ) = ∅ )
10 5 9 mpbi ⊢ ( 2 ... 1 ) = ∅
11 4 10 eqtrdi ⊢ ( 𝑁 = 1 → ( 2 ... 𝑁 ) = ∅ )
12 11 sumeq1d ⊢ ( 𝑁 = 1 → Σ 𝑘 ∈ ( 2 ... 𝑁 ) ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) = Σ 𝑘 ∈ ∅ ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) )
13 2 3 12 3eqtr4a ⊢ ( 𝑁 = 1 → ( π ‘ 𝑁 ) = Σ 𝑘 ∈ ( 2 ... 𝑁 ) ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) )
14 fzfid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ... 𝑁 ) ∈ Fin )
15 inss1 ⊢ ( ( 2 ... 𝑁 ) ∩ ℙ ) ⊆ ( 2 ... 𝑁 )
16 eqid ⊢ ( ( 𝟭 ‘ ( 2 ... 𝑁 ) ) ‘ ( ( 2 ... 𝑁 ) ∩ ℙ ) ) = ( ( 𝟭 ‘ ( 2 ... 𝑁 ) ) ‘ ( ( 2 ... 𝑁 ) ∩ ℙ ) )
17 16 indsumhash ⊢ ( ( ( 2 ... 𝑁 ) ∈ Fin ∧ ( ( 2 ... 𝑁 ) ∩ ℙ ) ⊆ ( 2 ... 𝑁 ) ) → Σ 𝑘 ∈ ( 2 ... 𝑁 ) ( ( ( 𝟭 ‘ ( 2 ... 𝑁 ) ) ‘ ( ( 2 ... 𝑁 ) ∩ ℙ ) ) ‘ 𝑘 ) = ( ♯ ‘ ( ( 2 ... 𝑁 ) ∩ ℙ ) ) )
18 14 15 17 sylancl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → Σ 𝑘 ∈ ( 2 ... 𝑁 ) ( ( ( 𝟭 ‘ ( 2 ... 𝑁 ) ) ‘ ( ( 2 ... 𝑁 ) ∩ ℙ ) ) ‘ 𝑘 ) = ( ♯ ‘ ( ( 2 ... 𝑁 ) ∩ ℙ ) ) )
19 eqid ⊢ ( 2 ... 𝑁 ) = ( 2 ... 𝑁 )
20 19 indprmfz ⊢ ( ( 𝟭 ‘ ( 2 ... 𝑁 ) ) ‘ ( ( 2 ... 𝑁 ) ∩ ℙ ) ) = ( 𝑛 ∈ ( 2 ... 𝑁 ) ↦ ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑛 − 1 ) ) + 1 ) / 𝑛 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑛 − 1 ) ) / 𝑛 ) ) ) ) )
21 fvoveq1 ⊢ ( 𝑛 = 𝑘 → ( ! ‘ ( 𝑛 − 1 ) ) = ( ! ‘ ( 𝑘 − 1 ) ) )
22 21 oveq1d ⊢ ( 𝑛 = 𝑘 → ( ( ! ‘ ( 𝑛 − 1 ) ) + 1 ) = ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) )
23 id ⊢ ( 𝑛 = 𝑘 → 𝑛 = 𝑘 )
24 22 23 oveq12d ⊢ ( 𝑛 = 𝑘 → ( ( ( ! ‘ ( 𝑛 − 1 ) ) + 1 ) / 𝑛 ) = ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) )
25 21 23 oveq12d ⊢ ( 𝑛 = 𝑘 → ( ( ! ‘ ( 𝑛 − 1 ) ) / 𝑛 ) = ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) )
26 25 fveq2d ⊢ ( 𝑛 = 𝑘 → ( ⌊ ‘ ( ( ! ‘ ( 𝑛 − 1 ) ) / 𝑛 ) ) = ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) )
27 24 26 oveq12d ⊢ ( 𝑛 = 𝑘 → ( ( ( ( ! ‘ ( 𝑛 − 1 ) ) + 1 ) / 𝑛 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑛 − 1 ) ) / 𝑛 ) ) ) = ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) )
28 27 fveq2d ⊢ ( 𝑛 = 𝑘 → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑛 − 1 ) ) + 1 ) / 𝑛 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑛 − 1 ) ) / 𝑛 ) ) ) ) = ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) )
29 simpr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑘 ∈ ( 2 ... 𝑁 ) ) → 𝑘 ∈ ( 2 ... 𝑁 ) )
30 fvexd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑘 ∈ ( 2 ... 𝑁 ) ) → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) ∈ V )
31 20 28 29 30 fvmptd3 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑘 ∈ ( 2 ... 𝑁 ) ) → ( ( ( 𝟭 ‘ ( 2 ... 𝑁 ) ) ‘ ( ( 2 ... 𝑁 ) ∩ ℙ ) ) ‘ 𝑘 ) = ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) )
32 31 eqcomd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑘 ∈ ( 2 ... 𝑁 ) ) → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) = ( ( ( 𝟭 ‘ ( 2 ... 𝑁 ) ) ‘ ( ( 2 ... 𝑁 ) ∩ ℙ ) ) ‘ 𝑘 ) )
33 32 sumeq2dv ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → Σ 𝑘 ∈ ( 2 ... 𝑁 ) ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) = Σ 𝑘 ∈ ( 2 ... 𝑁 ) ( ( ( 𝟭 ‘ ( 2 ... 𝑁 ) ) ‘ ( ( 2 ... 𝑁 ) ∩ ℙ ) ) ‘ 𝑘 ) )
34 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℤ )
35 ppival2 ⊢ ( 𝑁 ∈ ℤ → ( π ‘ 𝑁 ) = ( ♯ ‘ ( ( 2 ... 𝑁 ) ∩ ℙ ) ) )
36 34 35 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( π ‘ 𝑁 ) = ( ♯ ‘ ( ( 2 ... 𝑁 ) ∩ ℙ ) ) )
37 18 33 36 3eqtr4rd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( π ‘ 𝑁 ) = Σ 𝑘 ∈ ( 2 ... 𝑁 ) ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) )
38 13 37 jaoi ⊢ ( ( 𝑁 = 1 ∨ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( π ‘ 𝑁 ) = Σ 𝑘 ∈ ( 2 ... 𝑁 ) ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) )
39 1 38 sylbi ⊢ ( 𝑁 ∈ ℕ → ( π ‘ 𝑁 ) = Σ 𝑘 ∈ ( 2 ... 𝑁 ) ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) )