Metamath Proof Explorer

Theorem prmdvdsfi

Description: The set of prime divisors of a number is a finite set. (Contributed by Mario Carneiro, 7-Apr-2016)

Ref Expression
Assertion prmdvdsfi 
|- ( A e. NN -> { p e. Prime | p || A } e. Fin )

Proof

Step Hyp Ref Expression
1 fzfi 
 |-  ( 1 ... A ) e. Fin
2 prmssnn 
 |-  Prime C_ NN
3 rabss2 
 |-  ( Prime C_ NN -> { p e. Prime | p || A } C_ { p e. NN | p || A } )
4 2 3 ax-mp 
 |-  { p e. Prime | p || A } C_ { p e. NN | p || A }
5 dvdsssfz1 
 |-  ( A e. NN -> { p e. NN | p || A } C_ ( 1 ... A ) )
6 4 5 sstrid 
 |-  ( A e. NN -> { p e. Prime | p || A } C_ ( 1 ... A ) )
7 ssfi 
 |-  ( ( ( 1 ... A ) e. Fin /\ { p e. Prime | p || A } C_ ( 1 ... A ) ) -> { p e. Prime | p || A } e. Fin )
8 1 6 7 sylancr 
 |-  ( A e. NN -> { p e. Prime | p || A } e. Fin )