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 
|- ( N e. NN -> ( ppi ` N ) = sum_ k e. ( 2 ... N ) ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) )

Proof

Step Hyp Ref Expression
1 elnn1uz2 
 |-  ( N e. NN <-> ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) )
2 ppi1sum 
 |-  ( ppi ` 1 ) = sum_ k e. (/) ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) )
3 fveq2 
 |-  ( N = 1 -> ( ppi ` N ) = ( ppi ` 1 ) )
4 oveq2 
 |-  ( N = 1 -> ( 2 ... N ) = ( 2 ... 1 ) )
5 1lt2 
 |-  1 < 2
6 2z 
 |-  2 e. ZZ
7 1z 
 |-  1 e. ZZ
8 fzn 
 |-  ( ( 2 e. ZZ /\ 1 e. ZZ ) -> ( 1 < 2 <-> ( 2 ... 1 ) = (/) ) )
9 6 7 8 mp2an 
 |-  ( 1 < 2 <-> ( 2 ... 1 ) = (/) )
10 5 9 mpbi 
 |-  ( 2 ... 1 ) = (/)
11 4 10 eqtrdi 
 |-  ( N = 1 -> ( 2 ... N ) = (/) )
12 11 sumeq1d 
 |-  ( N = 1 -> sum_ k e. ( 2 ... N ) ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) = sum_ k e. (/) ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) )
13 2 3 12 3eqtr4a 
 |-  ( N = 1 -> ( ppi ` N ) = sum_ k e. ( 2 ... N ) ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) )
14 fzfid 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 ... N ) e. Fin )
15 inss1 
 |-  ( ( 2 ... N ) i^i Prime ) C_ ( 2 ... N )
16 eqid 
 |-  ( ( _Ind ` ( 2 ... N ) ) ` ( ( 2 ... N ) i^i Prime ) ) = ( ( _Ind ` ( 2 ... N ) ) ` ( ( 2 ... N ) i^i Prime ) )
17 16 indsumhash 
 |-  ( ( ( 2 ... N ) e. Fin /\ ( ( 2 ... N ) i^i Prime ) C_ ( 2 ... N ) ) -> sum_ k e. ( 2 ... N ) ( ( ( _Ind ` ( 2 ... N ) ) ` ( ( 2 ... N ) i^i Prime ) ) ` k ) = ( # ` ( ( 2 ... N ) i^i Prime ) ) )
18 14 15 17 sylancl 
 |-  ( N e. ( ZZ>= ` 2 ) -> sum_ k e. ( 2 ... N ) ( ( ( _Ind ` ( 2 ... N ) ) ` ( ( 2 ... N ) i^i Prime ) ) ` k ) = ( # ` ( ( 2 ... N ) i^i Prime ) ) )
19 eqid 
 |-  ( 2 ... N ) = ( 2 ... N )
20 19 indprmfz 
 |-  ( ( _Ind ` ( 2 ... N ) ) ` ( ( 2 ... N ) i^i Prime ) ) = ( n e. ( 2 ... N ) |-> ( |_ ` ( ( ( ( ! ` ( n - 1 ) ) + 1 ) / n ) - ( |_ ` ( ( ! ` ( n - 1 ) ) / n ) ) ) ) )
21 fvoveq1 
 |-  ( n = k -> ( ! ` ( n - 1 ) ) = ( ! ` ( k - 1 ) ) )
22 21 oveq1d 
 |-  ( n = k -> ( ( ! ` ( n - 1 ) ) + 1 ) = ( ( ! ` ( k - 1 ) ) + 1 ) )
23 id 
 |-  ( n = k -> n = k )
24 22 23 oveq12d 
 |-  ( n = k -> ( ( ( ! ` ( n - 1 ) ) + 1 ) / n ) = ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) )
25 21 23 oveq12d 
 |-  ( n = k -> ( ( ! ` ( n - 1 ) ) / n ) = ( ( ! ` ( k - 1 ) ) / k ) )
26 25 fveq2d 
 |-  ( n = k -> ( |_ ` ( ( ! ` ( n - 1 ) ) / n ) ) = ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) )
27 24 26 oveq12d 
 |-  ( n = k -> ( ( ( ( ! ` ( n - 1 ) ) + 1 ) / n ) - ( |_ ` ( ( ! ` ( n - 1 ) ) / n ) ) ) = ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) )
28 27 fveq2d 
 |-  ( n = k -> ( |_ ` ( ( ( ( ! ` ( n - 1 ) ) + 1 ) / n ) - ( |_ ` ( ( ! ` ( n - 1 ) ) / n ) ) ) ) = ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) )
29 simpr 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ k e. ( 2 ... N ) ) -> k e. ( 2 ... N ) )
30 fvexd 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ k e. ( 2 ... N ) ) -> ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) e. _V )
31 20 28 29 30 fvmptd3 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ k e. ( 2 ... N ) ) -> ( ( ( _Ind ` ( 2 ... N ) ) ` ( ( 2 ... N ) i^i Prime ) ) ` k ) = ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) )
32 31 eqcomd 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ k e. ( 2 ... N ) ) -> ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) = ( ( ( _Ind ` ( 2 ... N ) ) ` ( ( 2 ... N ) i^i Prime ) ) ` k ) )
33 32 sumeq2dv 
 |-  ( N e. ( ZZ>= ` 2 ) -> sum_ k e. ( 2 ... N ) ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) = sum_ k e. ( 2 ... N ) ( ( ( _Ind ` ( 2 ... N ) ) ` ( ( 2 ... N ) i^i Prime ) ) ` k ) )
34 eluzelz 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. ZZ )
35 ppival2 
 |-  ( N e. ZZ -> ( ppi ` N ) = ( # ` ( ( 2 ... N ) i^i Prime ) ) )
36 34 35 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ppi ` N ) = ( # ` ( ( 2 ... N ) i^i Prime ) ) )
37 18 33 36 3eqtr4rd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ppi ` N ) = sum_ k e. ( 2 ... N ) ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) )
38 13 37 jaoi 
 |-  ( ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) -> ( ppi ` N ) = sum_ k e. ( 2 ... N ) ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) )
39 1 38 sylbi 
 |-  ( N e. NN -> ( ppi ` N ) = sum_ k e. ( 2 ... N ) ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) )