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\in \mathbb{N}\to \left\{p\in \mathbb{P}|p\parallel A\right\}\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		fzfi	$$⊢\left(1\dots A\right)\in \mathrm{Fin}$$
2		prmssnn	$$⊢\mathbb{P}\subseteq \mathbb{N}$$
3		rabss2	$$⊢\mathbb{P}\subseteq \mathbb{N}\to \left\{p\in \mathbb{P}|p\parallel A\right\}\subseteq \left\{p\in \mathbb{N}|p\parallel A\right\}$$
4	2 3	ax-mp	$$⊢\left\{p\in \mathbb{P}|p\parallel A\right\}\subseteq \left\{p\in \mathbb{N}|p\parallel A\right\}$$
5		dvdsssfz1	$$⊢A\in \mathbb{N}\to \left\{p\in \mathbb{N}|p\parallel A\right\}\subseteq \left(1\dots A\right)$$
6	4 5	sstrid	$$⊢A\in \mathbb{N}\to \left\{p\in \mathbb{P}|p\parallel A\right\}\subseteq \left(1\dots A\right)$$
7		ssfi	$$⊢\left(\left(1\dots A\right)\in \mathrm{Fin}\wedge \left\{p\in \mathbb{P}|p\parallel A\right\}\subseteq \left(1\dots A\right)\right)\to \left\{p\in \mathbb{P}|p\parallel A\right\}\in \mathrm{Fin}$$
8	1 6 7	sylancr	$$⊢A\in \mathbb{N}\to \left\{p\in \mathbb{P}|p\parallel A\right\}\in \mathrm{Fin}$$