This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ppi1

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

Ref Expression
Assertion ppi1 ( π ‘ 1 ) = 0

Proof

Step Hyp Ref Expression
1 1z ⊢ 1 ∈ ℤ
2 ppival2 ⊢ ( 1 ∈ ℤ → ( π ‘ 1 ) = ( ♯ ‘ ( ( 2 ... 1 ) ∩ ℙ ) ) )
3 1 2 ax-mp ⊢ ( π ‘ 1 ) = ( ♯ ‘ ( ( 2 ... 1 ) ∩ ℙ ) )
4 1lt2 ⊢ 1 < 2
5 2z ⊢ 2 ∈ ℤ
6 fzn ⊢ ( ( 2 ∈ ℤ ∧ 1 ∈ ℤ ) → ( 1 < 2 ↔ ( 2 ... 1 ) = ∅ ) )
7 5 1 6 mp2an ⊢ ( 1 < 2 ↔ ( 2 ... 1 ) = ∅ )
8 4 7 mpbi ⊢ ( 2 ... 1 ) = ∅
9 8 ineq1i ⊢ ( ( 2 ... 1 ) ∩ ℙ ) = ( ∅ ∩ ℙ )
10 0in ⊢ ( ∅ ∩ ℙ ) = ∅
11 9 10 eqtri ⊢ ( ( 2 ... 1 ) ∩ ℙ ) = ∅
12 11 fveq2i ⊢ ( ♯ ‘ ( ( 2 ... 1 ) ∩ ℙ ) ) = ( ♯ ‘ ∅ )
13 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
14 12 13 eqtri ⊢ ( ♯ ‘ ( ( 2 ... 1 ) ∩ ℙ ) ) = 0
15 3 14 eqtri ⊢ ( π ‘ 1 ) = 0