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	⊢ ℙ ∉ Fin

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝑓 ∈ ran FermatNo ↦ inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } , ℝ , < ) ) = ( 𝑓 ∈ ran FermatNo ↦ inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } , ℝ , < ) )
2	1	prmdvdsfmtnof1	⊢ ( 𝑓 ∈ ran FermatNo ↦ inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } , ℝ , < ) ) : ran FermatNo –1-1→ ℙ
3		ax-1	⊢ ( ℙ ∉ Fin → ( ( 𝑓 ∈ ran FermatNo ↦ inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } , ℝ , < ) ) : ran FermatNo –1-1→ ℙ → ℙ ∉ Fin ) )
4		nnel	⊢ ( ¬ ℙ ∉ Fin ↔ ℙ ∈ Fin )
5		fmtnoinf	⊢ ran FermatNo ∉ Fin
6		f1fi	⊢ ( ( ℙ ∈ Fin ∧ ( 𝑓 ∈ ran FermatNo ↦ inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } , ℝ , < ) ) : ran FermatNo –1-1→ ℙ ) → ran FermatNo ∈ Fin )
7		df-nel	⊢ ( ran FermatNo ∉ Fin ↔ ¬ ran FermatNo ∈ Fin )
8		pm2.21	⊢ ( ¬ ran FermatNo ∈ Fin → ( ran FermatNo ∈ Fin → ℙ ∉ Fin ) )
9	7 8	sylbi	⊢ ( ran FermatNo ∉ Fin → ( ran FermatNo ∈ Fin → ℙ ∉ Fin ) )
10	5 6 9	mpsyl	⊢ ( ( ℙ ∈ Fin ∧ ( 𝑓 ∈ ran FermatNo ↦ inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } , ℝ , < ) ) : ran FermatNo –1-1→ ℙ ) → ℙ ∉ Fin )
11	10	ex	⊢ ( ℙ ∈ Fin → ( ( 𝑓 ∈ ran FermatNo ↦ inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } , ℝ , < ) ) : ran FermatNo –1-1→ ℙ → ℙ ∉ Fin ) )
12	4 11	sylbi	⊢ ( ¬ ℙ ∉ Fin → ( ( 𝑓 ∈ ran FermatNo ↦ inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } , ℝ , < ) ) : ran FermatNo –1-1→ ℙ → ℙ ∉ Fin ) )
13	3 12	pm2.61i	⊢ ( ( 𝑓 ∈ ran FermatNo ↦ inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } , ℝ , < ) ) : ran FermatNo –1-1→ ℙ → ℙ ∉ Fin )
14	2 13	ax-mp	⊢ ℙ ∉ Fin