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 ⊢ 𝟙 I ⁡ I ∩ ℙ = k ∈ I ⟼ k − 1 ! + 1 k − k − 1 ! k

Proof

Step Hyp Ref Expression
1 indprmfz.i ⊢ I = 2 … A
2 1 ovexi ⊢ I ∈ V
3 inss1 ⊢ I ∩ ℙ ⊆ I
4 indval ⊢ I ∈ V ∧ I ∩ ℙ ⊆ I → 𝟙 I ⁡ I ∩ ℙ = k ∈ I ⟼ if k ∈ I ∩ ℙ 1 0
5 2 3 4 mp2an ⊢ 𝟙 I ⁡ I ∩ ℙ = k ∈ I ⟼ if k ∈ I ∩ ℙ 1 0
6 elin ⊢ k ∈ I ∩ ℙ ↔ k ∈ I ∧ k ∈ ℙ
7 ppivalnnprm ⊢ k ∈ ℙ → k − 1 ! + 1 k − k − 1 ! k = 1
8 7 adantl ⊢ k ∈ I ∧ k ∈ ℙ → k − 1 ! + 1 k − k − 1 ! k = 1
9 8 eqcomd ⊢ k ∈ I ∧ k ∈ ℙ → 1 = k − 1 ! + 1 k − k − 1 ! k
10 6 9 sylbi ⊢ k ∈ I ∩ ℙ → 1 = k − 1 ! + 1 k − k − 1 ! k
11 10 adantl ⊢ k ∈ I ∧ k ∈ I ∩ ℙ → 1 = k − 1 ! + 1 k − k − 1 ! k
12 elfzuz ⊢ k ∈ 2 … A → k ∈ ℤ ≥ 2
13 12 1 eleq2s ⊢ k ∈ I → k ∈ ℤ ≥ 2
14 6 biimpri ⊢ k ∈ I ∧ k ∈ ℙ → k ∈ I ∩ ℙ
15 14 stoic1a ⊢ k ∈ I ∧ ¬ k ∈ I ∩ ℙ → ¬ k ∈ ℙ
16 df-nel ⊢ k ∉ ℙ ↔ ¬ k ∈ ℙ
17 15 16 sylibr ⊢ k ∈ I ∧ ¬ k ∈ I ∩ ℙ → k ∉ ℙ
18 ppivalnnnprm ⊢ k ∈ ℤ ≥ 2 ∧ k ∉ ℙ → k − 1 ! + 1 k − k − 1 ! k = 0
19 13 17 18 syl2an2r ⊢ k ∈ I ∧ ¬ k ∈ I ∩ ℙ → k − 1 ! + 1 k − k − 1 ! k = 0
20 19 eqcomd ⊢ k ∈ I ∧ ¬ k ∈ I ∩ ℙ → 0 = k − 1 ! + 1 k − k − 1 ! k
21 11 20 ifeqda ⊢ k ∈ I → if k ∈ I ∩ ℙ 1 0 = k − 1 ! + 1 k − k − 1 ! k
22 21 mpteq2ia ⊢ k ∈ I ⟼ if k ∈ I ∩ ℙ 1 0 = k ∈ I ⟼ k − 1 ! + 1 k − k − 1 ! k
23 5 22 eqtri ⊢ 𝟙 I ⁡ I ∩ ℙ = k ∈ I ⟼ k − 1 ! + 1 k − k − 1 ! k