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 ⊢ 𝐼 = ( 2 ... 𝐴 )
Assertion indprmfz ( ( 𝟭 ‘ 𝐼 ) ‘ ( 𝐼 ∩ ℙ ) ) = ( 𝑘 ∈ 𝐼 ↦ ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 indprmfz.i ⊢ 𝐼 = ( 2 ... 𝐴 )
2 1 ovexi ⊢ 𝐼 ∈ V
3 inss1 ⊢ ( 𝐼 ∩ ℙ ) ⊆ 𝐼
4 indval ⊢ ( ( 𝐼 ∈ V ∧ ( 𝐼 ∩ ℙ ) ⊆ 𝐼 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ ( 𝐼 ∩ ℙ ) ) = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 ∈ ( 𝐼 ∩ ℙ ) , 1 , 0 ) ) )
5 2 3 4 mp2an ⊢ ( ( 𝟭 ‘ 𝐼 ) ‘ ( 𝐼 ∩ ℙ ) ) = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 ∈ ( 𝐼 ∩ ℙ ) , 1 , 0 ) )
6 elin ⊢ ( 𝑘 ∈ ( 𝐼 ∩ ℙ ) ↔ ( 𝑘 ∈ 𝐼 ∧ 𝑘 ∈ ℙ ) )
7 ppivalnnprm ⊢ ( 𝑘 ∈ ℙ → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) = 1 )
8 7 adantl ⊢ ( ( 𝑘 ∈ 𝐼 ∧ 𝑘 ∈ ℙ ) → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) = 1 )
9 8 eqcomd ⊢ ( ( 𝑘 ∈ 𝐼 ∧ 𝑘 ∈ ℙ ) → 1 = ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) )
10 6 9 sylbi ⊢ ( 𝑘 ∈ ( 𝐼 ∩ ℙ ) → 1 = ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) )
11 10 adantl ⊢ ( ( 𝑘 ∈ 𝐼 ∧ 𝑘 ∈ ( 𝐼 ∩ ℙ ) ) → 1 = ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) )
12 elfzuz ⊢ ( 𝑘 ∈ ( 2 ... 𝐴 ) → 𝑘 ∈ ( ℤ≥ ‘ 2 ) )
13 12 1 eleq2s ⊢ ( 𝑘 ∈ 𝐼 → 𝑘 ∈ ( ℤ≥ ‘ 2 ) )
14 6 biimpri ⊢ ( ( 𝑘 ∈ 𝐼 ∧ 𝑘 ∈ ℙ ) → 𝑘 ∈ ( 𝐼 ∩ ℙ ) )
15 14 stoic1a ⊢ ( ( 𝑘 ∈ 𝐼 ∧ ¬ 𝑘 ∈ ( 𝐼 ∩ ℙ ) ) → ¬ 𝑘 ∈ ℙ )
16 df-nel ⊢ ( 𝑘 ∉ ℙ ↔ ¬ 𝑘 ∈ ℙ )
17 15 16 sylibr ⊢ ( ( 𝑘 ∈ 𝐼 ∧ ¬ 𝑘 ∈ ( 𝐼 ∩ ℙ ) ) → 𝑘 ∉ ℙ )
18 ppivalnnnprm ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑘 ∉ ℙ ) → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) = 0 )
19 13 17 18 syl2an2r ⊢ ( ( 𝑘 ∈ 𝐼 ∧ ¬ 𝑘 ∈ ( 𝐼 ∩ ℙ ) ) → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) = 0 )
20 19 eqcomd ⊢ ( ( 𝑘 ∈ 𝐼 ∧ ¬ 𝑘 ∈ ( 𝐼 ∩ ℙ ) ) → 0 = ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) )
21 11 20 ifeqda ⊢ ( 𝑘 ∈ 𝐼 → if ( 𝑘 ∈ ( 𝐼 ∩ ℙ ) , 1 , 0 ) = ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) )
22 21 mpteq2ia ⊢ ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 ∈ ( 𝐼 ∩ ℙ ) , 1 , 0 ) ) = ( 𝑘 ∈ 𝐼 ↦ ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) )
23 5 22 eqtri ⊢ ( ( 𝟭 ‘ 𝐼 ) ‘ ( 𝐼 ∩ ℙ ) ) = ( 𝑘 ∈ 𝐼 ↦ ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) )