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	⊢ ( 𝐴 ∈ ℝ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		ppisval	⊢ ( 𝐴 ∈ ℝ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) )
2		fzfi	⊢ ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin
3		inss1	⊢ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ⊆ ( 2 ... ( ⌊ ‘ 𝐴 ) )
4		ssfi	⊢ ( ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin ∧ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ⊆ ( 2 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ∈ Fin )
5	2 3 4	mp2an	⊢ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ∈ Fin
6	1 5	eqeltrdi	⊢ ( 𝐴 ∈ ℝ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∈ Fin )