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 ) |
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 ) |