prmdvdsfmtnof

Description: The mapping of a Fermat number to its smallest prime factor is a function. (Contributed by AV, 4-Aug-2021) (Proof shortened by II, 16-Feb-2023)

		Ref	Expression
	Hypothesis	prmdvdsfmtnof.1	$⊢ F = (f \in ran FermatNo ⟼ inf (\{p \in ℙ \| p ∥ f\} ℝ <))$
	Assertion	prmdvdsfmtnof	$⊢ F : ran FermatNo ⟶ ℙ$

Proof

Step	Hyp	Ref	Expression
1		prmdvdsfmtnof.1	$⊢ F = (f \in ran FermatNo ⟼ inf (\{p \in ℙ \| p ∥ f\} ℝ <))$
2		fmtnorn	$⊢ f \in ran FermatNo \leftrightarrow \exists n \in ℕ_{0} FermatNo (n) = f$
3		ltso	$⊢ < Or ℝ$
4	3	a1i	$⊢ (n \in ℕ_{0} \land FermatNo (n) = f) \to < Or ℝ$
5		fmtnoge3	$⊢ n \in ℕ_{0} \to FermatNo (n) \in ℤ_{\geq 3}$
6	5	adantr	$⊢ (n \in ℕ_{0} \land FermatNo (n) = f) \to FermatNo (n) \in ℤ_{\geq 3}$
7		eleq1	$⊢ FermatNo (n) = f \to (FermatNo (n) \in ℤ_{\geq 3} \leftrightarrow f \in ℤ_{\geq 3})$
8	7	adantl	$⊢ (n \in ℕ_{0} \land FermatNo (n) = f) \to (FermatNo (n) \in ℤ_{\geq 3} \leftrightarrow f \in ℤ_{\geq 3})$
9	6 8	mpbid	$⊢ (n \in ℕ_{0} \land FermatNo (n) = f) \to f \in ℤ_{\geq 3}$
10		uzuzle23	$⊢ f \in ℤ_{\geq 3} \to f \in ℤ_{\geq 2}$
11	9 10	syl	$⊢ (n \in ℕ_{0} \land FermatNo (n) = f) \to f \in ℤ_{\geq 2}$
12		eluz2nn	$⊢ f \in ℤ_{\geq 2} \to f \in ℕ$
13		prmdvdsfi	$⊢ f \in ℕ \to \{p \in ℙ \| p ∥ f\} \in Fin$
14	11 12 13	3syl	$⊢ (n \in ℕ_{0} \land FermatNo (n) = f) \to \{p \in ℙ \| p ∥ f\} \in Fin$
15		exprmfct	$⊢ f \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ f$
16	11 15	syl	$⊢ (n \in ℕ_{0} \land FermatNo (n) = f) \to \exists p \in ℙ p ∥ f$
17		rabn0	$⊢ \{p \in ℙ \| p ∥ f\} \neq \emptyset \leftrightarrow \exists p \in ℙ p ∥ f$
18	16 17	sylibr	$⊢ (n \in ℕ_{0} \land FermatNo (n) = f) \to \{p \in ℙ \| p ∥ f\} \neq \emptyset$
19		ssrab2	$⊢ \{p \in ℙ \| p ∥ f\} \subseteq ℙ$
20		prmssnn	$⊢ ℙ \subseteq ℕ$
21		nnssre	$⊢ ℕ \subseteq ℝ$
22	20 21	sstri	$⊢ ℙ \subseteq ℝ$
23	19 22	sstri	$⊢ \{p \in ℙ \| p ∥ f\} \subseteq ℝ$
24	23	a1i	$⊢ (n \in ℕ_{0} \land FermatNo (n) = f) \to \{p \in ℙ \| p ∥ f\} \subseteq ℝ$
25		fiinfcl	$⊢ (< Or ℝ \land (\{p \in ℙ \| p ∥ f\} \in Fin \land \{p \in ℙ \| p ∥ f\} \neq \emptyset \land \{p \in ℙ \| p ∥ f\} \subseteq ℝ)) \to inf (\{p \in ℙ \| p ∥ f\} ℝ <) \in \{p \in ℙ \| p ∥ f\}$
26	19 25	sselid	$⊢ (< Or ℝ \land (\{p \in ℙ \| p ∥ f\} \in Fin \land \{p \in ℙ \| p ∥ f\} \neq \emptyset \land \{p \in ℙ \| p ∥ f\} \subseteq ℝ)) \to inf (\{p \in ℙ \| p ∥ f\} ℝ <) \in ℙ$
27	4 14 18 24 26	syl13anc	$⊢ (n \in ℕ_{0} \land FermatNo (n) = f) \to inf (\{p \in ℙ \| p ∥ f\} ℝ <) \in ℙ$
28	27	rexlimiva	$⊢ \exists n \in ℕ_{0} FermatNo (n) = f \to inf (\{p \in ℙ \| p ∥ f\} ℝ <) \in ℙ$
29	2 28	sylbi	$⊢ f \in ran FermatNo \to inf (\{p \in ℙ \| p ∥ f\} ℝ <) \in ℙ$
30	1 29	fmpti	$⊢ F : ran FermatNo ⟶ ℙ$

Metamath Proof Explorer

Theorem prmdvdsfmtnof

Proof