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

Proof

Step	Hyp	Ref	Expression
1		prmdvdsfmtnof.1	⊢ 𝐹 = ( 𝑓 ∈ ran FermatNo ↦ inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } , ℝ , < ) )
2		fmtnorn	⊢ ( 𝑓 ∈ ran FermatNo ↔ ∃ 𝑛 ∈ ℕ0 ( FermatNo ‘ 𝑛 ) = 𝑓 )
3		ltso	⊢ < Or ℝ
4	3	a1i	⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( FermatNo ‘ 𝑛 ) = 𝑓 ) → < Or ℝ )
5		fmtnoge3	⊢ ( 𝑛 ∈ ℕ0 → ( FermatNo ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 3 ) )
6	5	adantr	⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( FermatNo ‘ 𝑛 ) = 𝑓 ) → ( FermatNo ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 3 ) )
7		eleq1	⊢ ( ( FermatNo ‘ 𝑛 ) = 𝑓 → ( ( FermatNo ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 3 ) ↔ 𝑓 ∈ ( ℤ≥ ‘ 3 ) ) )
8	7	adantl	⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( FermatNo ‘ 𝑛 ) = 𝑓 ) → ( ( FermatNo ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 3 ) ↔ 𝑓 ∈ ( ℤ≥ ‘ 3 ) ) )
9	6 8	mpbid	⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( FermatNo ‘ 𝑛 ) = 𝑓 ) → 𝑓 ∈ ( ℤ≥ ‘ 3 ) )
10		uzuzle23	⊢ ( 𝑓 ∈ ( ℤ≥ ‘ 3 ) → 𝑓 ∈ ( ℤ≥ ‘ 2 ) )
11	9 10	syl	⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( FermatNo ‘ 𝑛 ) = 𝑓 ) → 𝑓 ∈ ( ℤ≥ ‘ 2 ) )
12		eluz2nn	⊢ ( 𝑓 ∈ ( ℤ≥ ‘ 2 ) → 𝑓 ∈ ℕ )
13		prmdvdsfi	⊢ ( 𝑓 ∈ ℕ → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } ∈ Fin )
14	11 12 13	3syl	⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( FermatNo ‘ 𝑛 ) = 𝑓 ) → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } ∈ Fin )
15		exprmfct	⊢ ( 𝑓 ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑓 )
16	11 15	syl	⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( FermatNo ‘ 𝑛 ) = 𝑓 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑓 )
17		rabn0	⊢ ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } ≠ ∅ ↔ ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑓 )
18	16 17	sylibr	⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( FermatNo ‘ 𝑛 ) = 𝑓 ) → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } ≠ ∅ )
19		ssrab2	⊢ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } ⊆ ℙ
20		prmssnn	⊢ ℙ ⊆ ℕ
21		nnssre	⊢ ℕ ⊆ ℝ
22	20 21	sstri	⊢ ℙ ⊆ ℝ
23	19 22	sstri	⊢ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } ⊆ ℝ
24	23	a1i	⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( FermatNo ‘ 𝑛 ) = 𝑓 ) → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } ⊆ ℝ )
25		fiinfcl	⊢ ( ( < Or ℝ ∧ ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } ∈ Fin ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } ≠ ∅ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } ⊆ ℝ ) ) → inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } , ℝ , < ) ∈ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } )
26	19 25	sseldi	⊢ ( ( < Or ℝ ∧ ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } ∈ Fin ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } ≠ ∅ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } ⊆ ℝ ) ) → inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } , ℝ , < ) ∈ ℙ )
27	4 14 18 24 26	syl13anc	⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( FermatNo ‘ 𝑛 ) = 𝑓 ) → inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } , ℝ , < ) ∈ ℙ )
28	27	rexlimiva	⊢ ( ∃ 𝑛 ∈ ℕ0 ( FermatNo ‘ 𝑛 ) = 𝑓 → inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } , ℝ , < ) ∈ ℙ )
29	2 28	sylbi	⊢ ( 𝑓 ∈ ran FermatNo → inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓 } , ℝ , < ) ∈ ℙ )
30	1 29	fmpti	⊢ 𝐹 : ran FermatNo ⟶ ℙ