Theorem ppifi

Description: The set of primes less than A is a finite set. (Contributed by Mario Carneiro, 15-Sep-2014)

	Ref	Expression
Assertion	ppifi	$$⊢A\in ℝ\to \left[0,A\right]\cap \mathbb{P}\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		ppisval	$$⊢A\in ℝ\to \left[0,A\right]\cap \mathbb{P}=\left(2\dots ⌊A⌋\right)\cap \mathbb{P}$$
2		fzfi	$$⊢\left(2\dots ⌊A⌋\right)\in \mathrm{Fin}$$
3		inss1	$$⊢\left(2\dots ⌊A⌋\right)\cap \mathbb{P}\subseteq \left(2\dots ⌊A⌋\right)$$
4		ssfi	$$⊢\left(\left(2\dots ⌊A⌋\right)\in \mathrm{Fin}\wedge \left(2\dots ⌊A⌋\right)\cap \mathbb{P}\subseteq \left(2\dots ⌊A⌋\right)\right)\to \left(2\dots ⌊A⌋\right)\cap \mathbb{P}\in \mathrm{Fin}$$
5	2 3 4	mp2an	$$⊢\left(2\dots ⌊A⌋\right)\cap \mathbb{P}\in \mathrm{Fin}$$
6	1 5	eqeltrdi	$$⊢A\in ℝ\to \left[0,A\right]\cap \mathbb{P}\in \mathrm{Fin}$$