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 ) ) ‘ ℙ ) = ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ↦ ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fvex	⊢ ( ℤ≥ ‘ 2 ) ∈ V
2		prmssuz2	⊢ ℙ ⊆ ( ℤ≥ ‘ 2 )
3		indval	⊢ ( ( ( ℤ≥ ‘ 2 ) ∈ V ∧ ℙ ⊆ ( ℤ≥ ‘ 2 ) ) → ( ( 𝟭 ‘ ( ℤ≥ ‘ 2 ) ) ‘ ℙ ) = ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ↦ if ( 𝑘 ∈ ℙ , 1 , 0 ) ) )
4	1 2 3	mp2an	⊢ ( ( 𝟭 ‘ ( ℤ≥ ‘ 2 ) ) ‘ ℙ ) = ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ↦ if ( 𝑘 ∈ ℙ , 1 , 0 ) )
5		ppivalnnprm	⊢ ( 𝑘 ∈ ℙ → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) = 1 )
6	5	adantl	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑘 ∈ ℙ ) → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) = 1 )
7	6	eqcomd	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑘 ∈ ℙ ) → 1 = ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) )
8		df-nel	⊢ ( 𝑘 ∉ ℙ ↔ ¬ 𝑘 ∈ ℙ )
9		ppivalnnnprm	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑘 ∉ ℙ ) → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) = 0 )
10	8 9	sylan2br	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ ¬ 𝑘 ∈ ℙ ) → ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) = 0 )
11	10	eqcomd	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ ¬ 𝑘 ∈ ℙ ) → 0 = ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) )
12	7 11	ifeqda	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) → if ( 𝑘 ∈ ℙ , 1 , 0 ) = ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) )
13	12	mpteq2ia	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ↦ if ( 𝑘 ∈ ℙ , 1 , 0 ) ) = ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ↦ ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) )
14	4 13	eqtri	⊢ ( ( 𝟭 ‘ ( ℤ≥ ‘ 2 ) ) ‘ ℙ ) = ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ↦ ( ⌊ ‘ ( ( ( ( ! ‘ ( 𝑘 − 1 ) ) + 1 ) / 𝑘 ) − ( ⌊ ‘ ( ( ! ‘ ( 𝑘 − 1 ) ) / 𝑘 ) ) ) ) )