Metamath Proof Explorer

Theorem indprm

Description: An indicator function for prime numbers, according to Ján Mináč. (Contributed by AV, 4-Apr-2026)

Ref Expression
Assertion indprm 
|- ( ( _Ind ` ( ZZ>= ` 2 ) ) ` Prime ) = ( k e. ( ZZ>= ` 2 ) |-> ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fvex 
 |-  ( ZZ>= ` 2 ) e. _V
2 prmssuz2 
 |-  Prime C_ ( ZZ>= ` 2 )
3 indval 
 |-  ( ( ( ZZ>= ` 2 ) e. _V /\ Prime C_ ( ZZ>= ` 2 ) ) -> ( ( _Ind ` ( ZZ>= ` 2 ) ) ` Prime ) = ( k e. ( ZZ>= ` 2 ) |-> if ( k e. Prime , 1 , 0 ) ) )
4 1 2 3 mp2an 
 |-  ( ( _Ind ` ( ZZ>= ` 2 ) ) ` Prime ) = ( k e. ( ZZ>= ` 2 ) |-> if ( k e. Prime , 1 , 0 ) )
5 ppivalnnprm 
 |-  ( k e. Prime -> ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) = 1 )
6 5 adantl 
 |-  ( ( k e. ( ZZ>= ` 2 ) /\ k e. Prime ) -> ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) = 1 )
7 6 eqcomd 
 |-  ( ( k e. ( ZZ>= ` 2 ) /\ k e. Prime ) -> 1 = ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) )
8 df-nel 
 |-  ( k e/ Prime <-> -. k e. Prime )
9 ppivalnnnprm 
 |-  ( ( k e. ( ZZ>= ` 2 ) /\ k e/ Prime ) -> ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) = 0 )
10 8 9 sylan2br 
 |-  ( ( k e. ( ZZ>= ` 2 ) /\ -. k e. Prime ) -> ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) = 0 )
11 10 eqcomd 
 |-  ( ( k e. ( ZZ>= ` 2 ) /\ -. k e. Prime ) -> 0 = ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) )
12 7 11 ifeqda 
 |-  ( k e. ( ZZ>= ` 2 ) -> if ( k e. Prime , 1 , 0 ) = ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) )
13 12 mpteq2ia 
 |-  ( k e. ( ZZ>= ` 2 ) |-> if ( k e. Prime , 1 , 0 ) ) = ( k e. ( ZZ>= ` 2 ) |-> ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) )
14 4 13 eqtri 
 |-  ( ( _Ind ` ( ZZ>= ` 2 ) ) ` Prime ) = ( k e. ( ZZ>= ` 2 ) |-> ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) )