prmdvdsfmtnof1

Description: The mapping of a Fermat number to its smallest prime factor is a one-to-one function. (Contributed by AV, 4-Aug-2021)

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

Proof

Step	Hyp	Ref	Expression
1		prmdvdsfmtnof.1	$⊢ F = (f \in ran FermatNo ⟼ sup (\{p \in ℙ \| p ∥ f\} ℝ <))$
2	1	prmdvdsfmtnof	$⊢ F : ran FermatNo ⟶ ℙ$
3		breq2	$⊢ f = g \to (p ∥ f \leftrightarrow p ∥ g)$
4	3	rabbidv	$⊢ f = g \to \{p \in ℙ \| p ∥ f\} = \{p \in ℙ \| p ∥ g\}$
5	4	infeq1d	$⊢ f = g \to sup (\{p \in ℙ \| p ∥ f\} ℝ <) = sup (\{p \in ℙ \| p ∥ g\} ℝ <)$
6		id	$⊢ g \in ran FermatNo \to g \in ran FermatNo$
7		ltso	$⊢ < Or ℝ$
8	7	a1i	$⊢ g \in ran FermatNo \to < Or ℝ$
9	8	infexd	$⊢ g \in ran FermatNo \to sup (\{p \in ℙ \| p ∥ g\} ℝ <) \in V$
10	1 5 6 9	fvmptd3	$⊢ g \in ran FermatNo \to F (g) = sup (\{p \in ℙ \| p ∥ g\} ℝ <)$
11		breq2	$⊢ f = h \to (p ∥ f \leftrightarrow p ∥ h)$
12	11	rabbidv	$⊢ f = h \to \{p \in ℙ \| p ∥ f\} = \{p \in ℙ \| p ∥ h\}$
13	12	infeq1d	$⊢ f = h \to sup (\{p \in ℙ \| p ∥ f\} ℝ <) = sup (\{p \in ℙ \| p ∥ h\} ℝ <)$
14		id	$⊢ h \in ran FermatNo \to h \in ran FermatNo$
15	7	a1i	$⊢ h \in ran FermatNo \to < Or ℝ$
16	15	infexd	$⊢ h \in ran FermatNo \to sup (\{p \in ℙ \| p ∥ h\} ℝ <) \in V$
17	1 13 14 16	fvmptd3	$⊢ h \in ran FermatNo \to F (h) = sup (\{p \in ℙ \| p ∥ h\} ℝ <)$
18	10 17	eqeqan12d	$⊢ (g \in ran FermatNo \land h \in ran FermatNo) \to (F (g) = F (h) \leftrightarrow sup (\{p \in ℙ \| p ∥ g\} ℝ <) = sup (\{p \in ℙ \| p ∥ h\} ℝ <))$
19		fmtnorn	$⊢ g \in ran FermatNo \leftrightarrow \exists n \in ℕ_{0} FermatNo (n) = g$
20		fmtnoge3	$⊢ n \in ℕ_{0} \to FermatNo (n) \in ℤ_{\geq 3}$
21		uzuzle23	$⊢ FermatNo (n) \in ℤ_{\geq 3} \to FermatNo (n) \in ℤ_{\geq 2}$
22	20 21	syl	$⊢ n \in ℕ_{0} \to FermatNo (n) \in ℤ_{\geq 2}$
23	22	adantr	$⊢ (n \in ℕ_{0} \land FermatNo (n) = g) \to FermatNo (n) \in ℤ_{\geq 2}$
24		eleq1	$⊢ FermatNo (n) = g \to (FermatNo (n) \in ℤ_{\geq 2} \leftrightarrow g \in ℤ_{\geq 2})$
25	24	adantl	$⊢ (n \in ℕ_{0} \land FermatNo (n) = g) \to (FermatNo (n) \in ℤ_{\geq 2} \leftrightarrow g \in ℤ_{\geq 2})$
26	23 25	mpbid	$⊢ (n \in ℕ_{0} \land FermatNo (n) = g) \to g \in ℤ_{\geq 2}$
27	26	rexlimiva	$⊢ \exists n \in ℕ_{0} FermatNo (n) = g \to g \in ℤ_{\geq 2}$
28	19 27	sylbi	$⊢ g \in ran FermatNo \to g \in ℤ_{\geq 2}$
29		fmtnorn	$⊢ h \in ran FermatNo \leftrightarrow \exists n \in ℕ_{0} FermatNo (n) = h$
30	22	adantr	$⊢ (n \in ℕ_{0} \land FermatNo (n) = h) \to FermatNo (n) \in ℤ_{\geq 2}$
31		eleq1	$⊢ FermatNo (n) = h \to (FermatNo (n) \in ℤ_{\geq 2} \leftrightarrow h \in ℤ_{\geq 2})$
32	31	adantl	$⊢ (n \in ℕ_{0} \land FermatNo (n) = h) \to (FermatNo (n) \in ℤ_{\geq 2} \leftrightarrow h \in ℤ_{\geq 2})$
33	30 32	mpbid	$⊢ (n \in ℕ_{0} \land FermatNo (n) = h) \to h \in ℤ_{\geq 2}$
34	33	rexlimiva	$⊢ \exists n \in ℕ_{0} FermatNo (n) = h \to h \in ℤ_{\geq 2}$
35	29 34	sylbi	$⊢ h \in ran FermatNo \to h \in ℤ_{\geq 2}$
36		eqid	$⊢ sup (\{p \in ℙ \| p ∥ g\} ℝ <) = sup (\{p \in ℙ \| p ∥ g\} ℝ <)$
37		eqid	$⊢ sup (\{p \in ℙ \| p ∥ h\} ℝ <) = sup (\{p \in ℙ \| p ∥ h\} ℝ <)$
38	36 37	prmdvdsfmtnof1lem1	$⊢ (g \in ℤ_{\geq 2} \land h \in ℤ_{\geq 2}) \to (sup (\{p \in ℙ \| p ∥ g\} ℝ <) = sup (\{p \in ℙ \| p ∥ h\} ℝ <) \to (sup (\{p \in ℙ \| p ∥ g\} ℝ <) \in ℙ \land sup (\{p \in ℙ \| p ∥ g\} ℝ <) ∥ g \land sup (\{p \in ℙ \| p ∥ g\} ℝ <) ∥ h))$
39	28 35 38	syl2an	$⊢ (g \in ran FermatNo \land h \in ran FermatNo) \to (sup (\{p \in ℙ \| p ∥ g\} ℝ <) = sup (\{p \in ℙ \| p ∥ h\} ℝ <) \to (sup (\{p \in ℙ \| p ∥ g\} ℝ <) \in ℙ \land sup (\{p \in ℙ \| p ∥ g\} ℝ <) ∥ g \land sup (\{p \in ℙ \| p ∥ g\} ℝ <) ∥ h))$
40		prmdvdsfmtnof1lem2	$⊢ (g \in ran FermatNo \land h \in ran FermatNo) \to ((sup (\{p \in ℙ \| p ∥ g\} ℝ <) \in ℙ \land sup (\{p \in ℙ \| p ∥ g\} ℝ <) ∥ g \land sup (\{p \in ℙ \| p ∥ g\} ℝ <) ∥ h) \to g = h)$
41	39 40	syld	$⊢ (g \in ran FermatNo \land h \in ran FermatNo) \to (sup (\{p \in ℙ \| p ∥ g\} ℝ <) = sup (\{p \in ℙ \| p ∥ h\} ℝ <) \to g = h)$
42	18 41	sylbid	$⊢ (g \in ran FermatNo \land h \in ran FermatNo) \to (F (g) = F (h) \to g = h)$
43	42	rgen2	$⊢ \forall g \in ran FermatNo \forall h \in ran FermatNo (F (g) = F (h) \to g = h)$
44		dff13	$⊢ F : ran FermatNo \underset{1-1}{⟶} ℙ \leftrightarrow (F : ran FermatNo ⟶ ℙ \land \forall g \in ran FermatNo \forall h \in ran FermatNo (F (g) = F (h) \to g = h))$
45	2 43 44	mpbir2an	$⊢ F : ran FermatNo \underset{1-1}{⟶} ℙ$

Metamath Proof Explorer

Theorem prmdvdsfmtnof1

Proof