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→ ℙ