Metamath Proof Explorer

Theorem indprmfz

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

Ref Expression
Hypothesis indprmfz.i 
|- I = ( 2 ... A )
Assertion indprmfz 
|- ( ( _Ind ` I ) ` ( I i^i Prime ) ) = ( k e. I |-> ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) )

Proof

Step Hyp Ref Expression
1 indprmfz.i 
 |-  I = ( 2 ... A )
2 1 ovexi 
 |-  I e. _V
3 inss1 
 |-  ( I i^i Prime ) C_ I
4 indval 
 |-  ( ( I e. _V /\ ( I i^i Prime ) C_ I ) -> ( ( _Ind ` I ) ` ( I i^i Prime ) ) = ( k e. I |-> if ( k e. ( I i^i Prime ) , 1 , 0 ) ) )
5 2 3 4 mp2an 
 |-  ( ( _Ind ` I ) ` ( I i^i Prime ) ) = ( k e. I |-> if ( k e. ( I i^i Prime ) , 1 , 0 ) )
6 elin 
 |-  ( k e. ( I i^i Prime ) <-> ( k e. I /\ k e. Prime ) )
7 ppivalnnprm 
 |-  ( k e. Prime -> ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) = 1 )
8 7 adantl 
 |-  ( ( k e. I /\ k e. Prime ) -> ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) = 1 )
9 8 eqcomd 
 |-  ( ( k e. I /\ k e. Prime ) -> 1 = ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) )
10 6 9 sylbi 
 |-  ( k e. ( I i^i Prime ) -> 1 = ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) )
11 10 adantl 
 |-  ( ( k e. I /\ k e. ( I i^i Prime ) ) -> 1 = ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) )
12 elfzuz 
 |-  ( k e. ( 2 ... A ) -> k e. ( ZZ>= ` 2 ) )
13 12 1 eleq2s 
 |-  ( k e. I -> k e. ( ZZ>= ` 2 ) )
14 6 biimpri 
 |-  ( ( k e. I /\ k e. Prime ) -> k e. ( I i^i Prime ) )
15 14 stoic1a 
 |-  ( ( k e. I /\ -. k e. ( I i^i Prime ) ) -> -. k e. Prime )
16 df-nel 
 |-  ( k e/ Prime <-> -. k e. Prime )
17 15 16 sylibr 
 |-  ( ( k e. I /\ -. k e. ( I i^i Prime ) ) -> k e/ Prime )
18 ppivalnnnprm 
 |-  ( ( k e. ( ZZ>= ` 2 ) /\ k e/ Prime ) -> ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) = 0 )
19 13 17 18 syl2an2r 
 |-  ( ( k e. I /\ -. k e. ( I i^i Prime ) ) -> ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) = 0 )
20 19 eqcomd 
 |-  ( ( k e. I /\ -. k e. ( I i^i Prime ) ) -> 0 = ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) )
21 11 20 ifeqda 
 |-  ( k e. I -> if ( k e. ( I i^i Prime ) , 1 , 0 ) = ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) )
22 21 mpteq2ia 
 |-  ( k e. I |-> if ( k e. ( I i^i Prime ) , 1 , 0 ) ) = ( k e. I |-> ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) )
23 5 22 eqtri 
 |-  ( ( _Ind ` I ) ` ( I i^i Prime ) ) = ( k e. I |-> ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) )