Metamath Proof Explorer

Theorem prminf2

Description: The set of prime numbers is infinite. The proof of this variant of prminf is based on Goldbach's theorem goldbachth (via prmdvdsfmtnof1 and prmdvdsfmtnof1lem2 ), see Wikipedia "Fermat number", 4-Aug-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties . (Contributed by AV, 4-Aug-2021)

Ref Expression
Assertion prminf2 
|- Prime e/ Fin

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( f e. ran FermatNo |-> inf ( { p e. Prime | p || f } , RR , < ) ) = ( f e. ran FermatNo |-> inf ( { p e. Prime | p || f } , RR , < ) )
2 1 prmdvdsfmtnof1 
 |-  ( f e. ran FermatNo |-> inf ( { p e. Prime | p || f } , RR , < ) ) : ran FermatNo -1-1-> Prime
3 ax-1 
 |-  ( Prime e/ Fin -> ( ( f e. ran FermatNo |-> inf ( { p e. Prime | p || f } , RR , < ) ) : ran FermatNo -1-1-> Prime -> Prime e/ Fin ) )
4 nnel 
 |-  ( -. Prime e/ Fin <-> Prime e. Fin )
5 fmtnoinf 
 |-  ran FermatNo e/ Fin
6 f1fi 
 |-  ( ( Prime e. Fin /\ ( f e. ran FermatNo |-> inf ( { p e. Prime | p || f } , RR , < ) ) : ran FermatNo -1-1-> Prime ) -> ran FermatNo e. Fin )
7 df-nel 
 |-  ( ran FermatNo e/ Fin <-> -. ran FermatNo e. Fin )
8 pm2.21 
 |-  ( -. ran FermatNo e. Fin -> ( ran FermatNo e. Fin -> Prime e/ Fin ) )
9 7 8 sylbi 
 |-  ( ran FermatNo e/ Fin -> ( ran FermatNo e. Fin -> Prime e/ Fin ) )
10 5 6 9 mpsyl 
 |-  ( ( Prime e. Fin /\ ( f e. ran FermatNo |-> inf ( { p e. Prime | p || f } , RR , < ) ) : ran FermatNo -1-1-> Prime ) -> Prime e/ Fin )
11 10 ex 
 |-  ( Prime e. Fin -> ( ( f e. ran FermatNo |-> inf ( { p e. Prime | p || f } , RR , < ) ) : ran FermatNo -1-1-> Prime -> Prime e/ Fin ) )
12 4 11 sylbi 
 |-  ( -. Prime e/ Fin -> ( ( f e. ran FermatNo |-> inf ( { p e. Prime | p || f } , RR , < ) ) : ran FermatNo -1-1-> Prime -> Prime e/ Fin ) )
13 3 12 pm2.61i 
 |-  ( ( f e. ran FermatNo |-> inf ( { p e. Prime | p || f } , RR , < ) ) : ran FermatNo -1-1-> Prime -> Prime e/ Fin )
14 2 13 ax-mp 
 |-  Prime e/ Fin