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	⊢ ( 𝐴 ∈ ℕ → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		fzfi	⊢ ( 1 ... 𝐴 ) ∈ Fin
2		prmssnn	⊢ ℙ ⊆ ℕ
3		rabss2	⊢ ( ℙ ⊆ ℕ → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ⊆ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } )
4	2 3	ax-mp	⊢ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ⊆ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 }
5		dvdsssfz1	⊢ ( 𝐴 ∈ ℕ → { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ⊆ ( 1 ... 𝐴 ) )
6	4 5	sstrid	⊢ ( 𝐴 ∈ ℕ → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ⊆ ( 1 ... 𝐴 ) )
7		ssfi	⊢ ( ( ( 1 ... 𝐴 ) ∈ Fin ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ⊆ ( 1 ... 𝐴 ) ) → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ Fin )
8	1 6 7	sylancr	⊢ ( 𝐴 ∈ ℕ → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ Fin )