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