Metamath Proof Explorer

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	$⊢ ℙ \notin Fin$

Proof

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