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

Metamath Proof Explorer

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 [0, A] \cap ℙ \in Fin$

Step	Hyp	Ref	Expression
1		ppisval	$⊢ A \in ℝ \to [0, A] \cap ℙ = (2 \dots ⌊A⌋) \cap ℙ$
2		fzfi	$⊢ (2 \dots ⌊A⌋) \in Fin$
3		inss1	$⊢ (2 \dots ⌊A⌋) \cap ℙ \subseteq (2 \dots ⌊A⌋)$
4		ssfi	$⊢ ((2 \dots ⌊A⌋) \in Fin \land (2 \dots ⌊A⌋) \cap ℙ \subseteq (2 \dots ⌊A⌋)) \to (2 \dots ⌊A⌋) \cap ℙ \in Fin$
5	2 3 4	mp2an	$⊢ (2 \dots ⌊A⌋) \cap ℙ \in Fin$
6	1 5	eqeltrdi	$⊢ A \in ℝ \to [0, A] \cap ℙ \in Fin$