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 ( 𝐴 ∈ ℝ → ( ( 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 )