Metamath Proof Explorer

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 
|- F = ( f e. ran FermatNo |-> inf ( { p e. Prime | p || f } , RR , < ) )
Assertion prmdvdsfmtnof 
|- F : ran FermatNo --> Prime

Proof

Step Hyp Ref Expression
1 prmdvdsfmtnof.1 
 |-  F = ( f e. ran FermatNo |-> inf ( { p e. Prime | p || f } , RR , < ) )
2 fmtnorn 
 |-  ( f e. ran FermatNo <-> E. n e. NN0 ( FermatNo ` n ) = f )
3 ltso 
 |-  < Or RR
4 3 a1i 
 |-  ( ( n e. NN0 /\ ( FermatNo ` n ) = f ) -> < Or RR )
5 fmtnoge3 
 |-  ( n e. NN0 -> ( FermatNo ` n ) e. ( ZZ>= ` 3 ) )
6 5 adantr 
 |-  ( ( n e. NN0 /\ ( FermatNo ` n ) = f ) -> ( FermatNo ` n ) e. ( ZZ>= ` 3 ) )
7 eleq1 
 |-  ( ( FermatNo ` n ) = f -> ( ( FermatNo ` n ) e. ( ZZ>= ` 3 ) <-> f e. ( ZZ>= ` 3 ) ) )
8 7 adantl 
 |-  ( ( n e. NN0 /\ ( FermatNo ` n ) = f ) -> ( ( FermatNo ` n ) e. ( ZZ>= ` 3 ) <-> f e. ( ZZ>= ` 3 ) ) )
9 6 8 mpbid 
 |-  ( ( n e. NN0 /\ ( FermatNo ` n ) = f ) -> f e. ( ZZ>= ` 3 ) )
10 uzuzle23 
 |-  ( f e. ( ZZ>= ` 3 ) -> f e. ( ZZ>= ` 2 ) )
11 9 10 syl 
 |-  ( ( n e. NN0 /\ ( FermatNo ` n ) = f ) -> f e. ( ZZ>= ` 2 ) )
12 eluz2nn 
 |-  ( f e. ( ZZ>= ` 2 ) -> f e. NN )
13 prmdvdsfi 
 |-  ( f e. NN -> { p e. Prime | p || f } e. Fin )
14 11 12 13 3syl 
 |-  ( ( n e. NN0 /\ ( FermatNo ` n ) = f ) -> { p e. Prime | p || f } e. Fin )
15 exprmfct 
 |-  ( f e. ( ZZ>= ` 2 ) -> E. p e. Prime p || f )
16 11 15 syl 
 |-  ( ( n e. NN0 /\ ( FermatNo ` n ) = f ) -> E. p e. Prime p || f )
17 rabn0 
 |-  ( { p e. Prime | p || f } =/= (/) <-> E. p e. Prime p || f )
18 16 17 sylibr 
 |-  ( ( n e. NN0 /\ ( FermatNo ` n ) = f ) -> { p e. Prime | p || f } =/= (/) )
19 ssrab2 
 |-  { p e. Prime | p || f } C_ Prime
20 prmssnn 
 |-  Prime C_ NN
21 nnssre 
 |-  NN C_ RR
22 20 21 sstri 
 |-  Prime C_ RR
23 19 22 sstri 
 |-  { p e. Prime | p || f } C_ RR
24 23 a1i 
 |-  ( ( n e. NN0 /\ ( FermatNo ` n ) = f ) -> { p e. Prime | p || f } C_ RR )
25 fiinfcl 
 |-  ( ( < Or RR /\ ( { p e. Prime | p || f } e. Fin /\ { p e. Prime | p || f } =/= (/) /\ { p e. Prime | p || f } C_ RR ) ) -> inf ( { p e. Prime | p || f } , RR , < ) e. { p e. Prime | p || f } )
26 19 25 sseldi 
 |-  ( ( < Or RR /\ ( { p e. Prime | p || f } e. Fin /\ { p e. Prime | p || f } =/= (/) /\ { p e. Prime | p || f } C_ RR ) ) -> inf ( { p e. Prime | p || f } , RR , < ) e. Prime )
27 4 14 18 24 26 syl13anc 
 |-  ( ( n e. NN0 /\ ( FermatNo ` n ) = f ) -> inf ( { p e. Prime | p || f } , RR , < ) e. Prime )
28 27 rexlimiva 
 |-  ( E. n e. NN0 ( FermatNo ` n ) = f -> inf ( { p e. Prime | p || f } , RR , < ) e. Prime )
29 2 28 sylbi 
 |-  ( f e. ran FermatNo -> inf ( { p e. Prime | p || f } , RR , < ) e. Prime )
30 1 29 fmpti 
 |-  F : ran FermatNo --> Prime