Metamath Proof Explorer

Theorem ppi1sum

Description: Value of the prime-counting function pi for 1, according to Ján Mináč. (Contributed by AV, 4-Apr-2026)

Ref Expression
Assertion ppi1sum ⊢ π _ ⁡ 1 = ∑ k ∈ ∅ k − 1 ! + 1 k − k − 1 ! k

Proof

Step Hyp Ref Expression
1 ppi1 ⊢ π _ ⁡ 1 = 0
2 sum0 ⊢ ∑ k ∈ ∅ k − 1 ! + 1 k − k − 1 ! k = 0
3 1 2 eqtr4i ⊢ π _ ⁡ 1 = ∑ k ∈ ∅ k − 1 ! + 1 k − k − 1 ! k