Metamath Proof Explorer

Theorem 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 ∈ ran ⁡ FermatNo ⟼ inf p ∈ ℙ | p ∥ f ℝ <
Assertion prmdvdsfmtnof1 ⊢ F : ran ⁡ FermatNo ⟶ 1-1 ℙ

Proof

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