ppival2

Description: Value of the prime-counting function pi. (Contributed by Mario Carneiro, 18-Sep-2014)

		Ref	Expression
	Assertion	ppival2	$⊢ A \in ℤ \to \underline{π} (A) = \|(2 \dots A) \cap ℙ\|$

Step	Hyp	Ref	Expression
1		zre	$⊢ A \in ℤ \to A \in ℝ$
2		ppival	$⊢ A \in ℝ \to \underline{π} (A) = \|[0, A] \cap ℙ\|$
3	1 2	syl	$⊢ A \in ℤ \to \underline{π} (A) = \|[0, A] \cap ℙ\|$
4		ppisval	$⊢ A \in ℝ \to [0, A] \cap ℙ = (2 \dots ⌊A⌋) \cap ℙ$
5	1 4	syl	$⊢ A \in ℤ \to [0, A] \cap ℙ = (2 \dots ⌊A⌋) \cap ℙ$
6		flid	$⊢ A \in ℤ \to ⌊A⌋ = A$
7	6	oveq2d	$⊢ A \in ℤ \to (2 \dots ⌊A⌋) = (2 \dots A)$
8	7	ineq1d	$⊢ A \in ℤ \to (2 \dots ⌊A⌋) \cap ℙ = (2 \dots A) \cap ℙ$
9	5 8	eqtrd	$⊢ A \in ℤ \to [0, A] \cap ℙ = (2 \dots A) \cap ℙ$
10	9	fveq2d	$⊢ A \in ℤ \to \|[0, A] \cap ℙ\| = \|(2 \dots A) \cap ℙ\|$
11	3 10	eqtrd	$⊢ A \in ℤ \to \underline{π} (A) = \|(2 \dots A) \cap ℙ\|$

Metamath Proof Explorer