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 ⊢ 𝐹 = ( 𝑓 ∈ ran FermatNo ↦ inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } , ℝ , < ) )
Assertion prmdvdsfmtnof1 𝐹 : ran FermatNo –1-1→ ℙ

Proof

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