Metamath Proof Explorer

Theorem dvdsfi

Description: A natural number has finitely many divisors. (Contributed by Jim Kingdon, 9-Oct-2025)

Ref Expression
Assertion dvdsfi 
|- ( N e. NN -> { x e. NN | x || N } e. Fin )

Proof

Step Hyp Ref Expression
1 fzfid 
 |-  ( N e. NN -> ( 1 ... N ) e. Fin )
2 dvdsssfz1 
 |-  ( N e. NN -> { x e. NN | x || N } C_ ( 1 ... N ) )
3 1 2 ssfid 
 |-  ( N e. NN -> { x e. NN | x || N } e. Fin )