Theorem dvdsfi

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

	Ref	Expression
Assertion	dvdsfi	⊢ ( 𝑁 ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		fzfid	⊢ ( 𝑁 ∈ ℕ → ( 1 ... 𝑁 ) ∈ Fin )
2		dvdsssfz1	⊢ ( 𝑁 ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ⊆ ( 1 ... 𝑁 ) )
3	1 2	ssfid	⊢ ( 𝑁 ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∈ Fin )