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 
|- ( ppi ` 1 ) = sum_ k e. (/) ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) )

Proof

Step Hyp Ref Expression
1 ppi1 
 |-  ( ppi ` 1 ) = 0
2 sum0 
 |-  sum_ k e. (/) ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) ) = 0
3 1 2 eqtr4i 
 |-  ( ppi ` 1 ) = sum_ k e. (/) ( |_ ` ( ( ( ( ! ` ( k - 1 ) ) + 1 ) / k ) - ( |_ ` ( ( ! ` ( k - 1 ) ) / k ) ) ) )