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

Proof

Step Hyp Ref Expression
1 fvex ⊢ ℤ ≥ 2 ∈ V
2 prmssuz2 ⊢ ℙ ⊆ ℤ ≥ 2
3 indval ⊢ ℤ ≥ 2 ∈ V ∧ ℙ ⊆ ℤ ≥ 2 → 𝟙 ℤ ≥ 2 ⁡ ℙ = k ∈ ℤ ≥ 2 ⟼ if k ∈ ℙ 1 0
4 1 2 3 mp2an ⊢ 𝟙 ℤ ≥ 2 ⁡ ℙ = k ∈ ℤ ≥ 2 ⟼ if k ∈ ℙ 1 0
5 ppivalnnprm ⊢ k ∈ ℙ → k − 1 ! + 1 k − k − 1 ! k = 1
6 5 adantl ⊢ k ∈ ℤ ≥ 2 ∧ k ∈ ℙ → k − 1 ! + 1 k − k − 1 ! k = 1
7 6 eqcomd ⊢ k ∈ ℤ ≥ 2 ∧ k ∈ ℙ → 1 = k − 1 ! + 1 k − k − 1 ! k
8 df-nel ⊢ k ∉ ℙ ↔ ¬ k ∈ ℙ
9 ppivalnnnprm ⊢ k ∈ ℤ ≥ 2 ∧ k ∉ ℙ → k − 1 ! + 1 k − k − 1 ! k = 0
10 8 9 sylan2br ⊢ k ∈ ℤ ≥ 2 ∧ ¬ k ∈ ℙ → k − 1 ! + 1 k − k − 1 ! k = 0
11 10 eqcomd ⊢ k ∈ ℤ ≥ 2 ∧ ¬ k ∈ ℙ → 0 = k − 1 ! + 1 k − k − 1 ! k
12 7 11 ifeqda ⊢ k ∈ ℤ ≥ 2 → if k ∈ ℙ 1 0 = k − 1 ! + 1 k − k − 1 ! k
13 12 mpteq2ia ⊢ k ∈ ℤ ≥ 2 ⟼ if k ∈ ℙ 1 0 = k ∈ ℤ ≥ 2 ⟼ k − 1 ! + 1 k − k − 1 ! k
14 4 13 eqtri ⊢ 𝟙 ℤ ≥ 2 ⁡ ℙ = k ∈ ℤ ≥ 2 ⟼ k − 1 ! + 1 k − k − 1 ! k