# Metamath Proof Explorer

## Theorem ppi1

Description: The prime-counting function ppi at 1 . (Contributed by Mario Carneiro, 21-Sep-2014)

Ref Expression
Assertion ppi1 ${⊢}\underset{_}{\pi }\left(1\right)=0$

### Proof

Step Hyp Ref Expression
1 1z ${⊢}1\in ℤ$
2 ppival2 ${⊢}1\in ℤ\to \underset{_}{\pi }\left(1\right)=\left|\left(2\dots 1\right)\cap ℙ\right|$
3 1 2 ax-mp ${⊢}\underset{_}{\pi }\left(1\right)=\left|\left(2\dots 1\right)\cap ℙ\right|$
4 1lt2 ${⊢}1<2$
5 2z ${⊢}2\in ℤ$
6 fzn ${⊢}\left(2\in ℤ\wedge 1\in ℤ\right)\to \left(1<2↔\left(2\dots 1\right)=\varnothing \right)$
7 5 1 6 mp2an ${⊢}1<2↔\left(2\dots 1\right)=\varnothing$
8 4 7 mpbi ${⊢}\left(2\dots 1\right)=\varnothing$
9 8 ineq1i ${⊢}\left(2\dots 1\right)\cap ℙ=\varnothing \cap ℙ$
10 0in ${⊢}\varnothing \cap ℙ=\varnothing$
11 9 10 eqtri ${⊢}\left(2\dots 1\right)\cap ℙ=\varnothing$
12 11 fveq2i ${⊢}\left|\left(2\dots 1\right)\cap ℙ\right|=\left|\varnothing \right|$
13 hash0 ${⊢}\left|\varnothing \right|=0$
14 12 13 eqtri ${⊢}\left|\left(2\dots 1\right)\cap ℙ\right|=0$
15 3 14 eqtri ${⊢}\underset{_}{\pi }\left(1\right)=0$