Theorem prminf2

Description: The set of prime numbers is infinite. The proof of this variant of prminf is based on Goldbach's theorem goldbachth (via prmdvdsfmtnof1 and prmdvdsfmtnof1lem2 ), see Wikipedia "Fermat number", 4-Aug-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties . (Contributed by AV, 4-Aug-2021)

	Ref	Expression
Assertion	prminf2	$$⊢\mathbb{P}\notin \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left(f\in \mathrm{ran}\mathrm{FermatNo}⟼inf\left(\left\{p\in \mathbb{P}|p\parallel f\right\},ℝ,<\right)\right)=\left(f\in \mathrm{ran}\mathrm{FermatNo}⟼inf\left(\left\{p\in \mathbb{P}|p\parallel f\right\},ℝ,<\right)\right)$$
2	1	prmdvdsfmtnof1	$$⊢\left(f\in \mathrm{ran}\mathrm{FermatNo}⟼inf\left(\left\{p\in \mathbb{P}|p\parallel f\right\},ℝ,<\right)\right):\mathrm{ran}\mathrm{FermatNo}\underset{1-1}{⟶}\mathbb{P}$$
3		ax-1	$$⊢\mathbb{P}\notin \mathrm{Fin}\to \left(\left(f\in \mathrm{ran}\mathrm{FermatNo}⟼inf\left(\left\{p\in \mathbb{P}|p\parallel f\right\},ℝ,<\right)\right):\mathrm{ran}\mathrm{FermatNo}\underset{1-1}{⟶}\mathbb{P}\to \mathbb{P}\notin \mathrm{Fin}\right)$$
4		nnel	$$⊢\neg \mathbb{P}\notin \mathrm{Fin}\leftrightarrow \mathbb{P}\in \mathrm{Fin}$$
5		fmtnoinf	$$⊢\mathrm{ran}\mathrm{FermatNo}\notin \mathrm{Fin}$$
6		f1fi	$$⊢\left(\mathbb{P}\in \mathrm{Fin}\wedge \left(f\in \mathrm{ran}\mathrm{FermatNo}⟼inf\left(\left\{p\in \mathbb{P}|p\parallel f\right\},ℝ,<\right)\right):\mathrm{ran}\mathrm{FermatNo}\underset{1-1}{⟶}\mathbb{P}\right)\to \mathrm{ran}\mathrm{FermatNo}\in \mathrm{Fin}$$
7		df-nel	$$⊢\mathrm{ran}\mathrm{FermatNo}\notin \mathrm{Fin}\leftrightarrow \neg \mathrm{ran}\mathrm{FermatNo}\in \mathrm{Fin}$$
8		pm2.21	$$⊢\neg \mathrm{ran}\mathrm{FermatNo}\in \mathrm{Fin}\to \left(\mathrm{ran}\mathrm{FermatNo}\in \mathrm{Fin}\to \mathbb{P}\notin \mathrm{Fin}\right)$$
9	7 8	sylbi	$$⊢\mathrm{ran}\mathrm{FermatNo}\notin \mathrm{Fin}\to \left(\mathrm{ran}\mathrm{FermatNo}\in \mathrm{Fin}\to \mathbb{P}\notin \mathrm{Fin}\right)$$
10	5 6 9	mpsyl	$$⊢\left(\mathbb{P}\in \mathrm{Fin}\wedge \left(f\in \mathrm{ran}\mathrm{FermatNo}⟼inf\left(\left\{p\in \mathbb{P}|p\parallel f\right\},ℝ,<\right)\right):\mathrm{ran}\mathrm{FermatNo}\underset{1-1}{⟶}\mathbb{P}\right)\to \mathbb{P}\notin \mathrm{Fin}$$
11	10	ex	$$⊢\mathbb{P}\in \mathrm{Fin}\to \left(\left(f\in \mathrm{ran}\mathrm{FermatNo}⟼inf\left(\left\{p\in \mathbb{P}|p\parallel f\right\},ℝ,<\right)\right):\mathrm{ran}\mathrm{FermatNo}\underset{1-1}{⟶}\mathbb{P}\to \mathbb{P}\notin \mathrm{Fin}\right)$$
12	4 11	sylbi	$$⊢\neg \mathbb{P}\notin \mathrm{Fin}\to \left(\left(f\in \mathrm{ran}\mathrm{FermatNo}⟼inf\left(\left\{p\in \mathbb{P}|p\parallel f\right\},ℝ,<\right)\right):\mathrm{ran}\mathrm{FermatNo}\underset{1-1}{⟶}\mathbb{P}\to \mathbb{P}\notin \mathrm{Fin}\right)$$
13	3 12	pm2.61i	$$⊢\left(f\in \mathrm{ran}\mathrm{FermatNo}⟼inf\left(\left\{p\in \mathbb{P}|p\parallel f\right\},ℝ,<\right)\right):\mathrm{ran}\mathrm{FermatNo}\underset{1-1}{⟶}\mathbb{P}\to \mathbb{P}\notin \mathrm{Fin}$$
14	2 13	ax-mp	$$⊢\mathbb{P}\notin \mathrm{Fin}$$