Metamath Proof Explorer

Theorem 2pwp1prmfmtno

Description: Every prime number of the form ( ( 2 ^ k ) + 1 ) must be a Fermat number. (Contributed by AV, 7-Aug-2021)

Ref Expression
Assertion 2pwp1prmfmtno 
|- ( ( K e. NN /\ P = ( ( 2 ^ K ) + 1 ) /\ P e. Prime ) -> E. n e. NN0 P = ( FermatNo ` n ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( K e. NN /\ P = ( ( 2 ^ K ) + 1 ) /\ P e. Prime ) -> K e. NN )
2 eleq1 
 |-  ( P = ( ( 2 ^ K ) + 1 ) -> ( P e. Prime <-> ( ( 2 ^ K ) + 1 ) e. Prime ) )
3 2 biimpa 
 |-  ( ( P = ( ( 2 ^ K ) + 1 ) /\ P e. Prime ) -> ( ( 2 ^ K ) + 1 ) e. Prime )
4 3 3adant1 
 |-  ( ( K e. NN /\ P = ( ( 2 ^ K ) + 1 ) /\ P e. Prime ) -> ( ( 2 ^ K ) + 1 ) e. Prime )
5 2pwp1prm 
 |-  ( ( K e. NN /\ ( ( 2 ^ K ) + 1 ) e. Prime ) -> E. n e. NN0 K = ( 2 ^ n ) )
6 1 4 5 syl2anc 
 |-  ( ( K e. NN /\ P = ( ( 2 ^ K ) + 1 ) /\ P e. Prime ) -> E. n e. NN0 K = ( 2 ^ n ) )
7 simpl 
 |-  ( ( P = ( ( 2 ^ K ) + 1 ) /\ K = ( 2 ^ n ) ) -> P = ( ( 2 ^ K ) + 1 ) )
8 oveq2 
 |-  ( K = ( 2 ^ n ) -> ( 2 ^ K ) = ( 2 ^ ( 2 ^ n ) ) )
9 8 oveq1d 
 |-  ( K = ( 2 ^ n ) -> ( ( 2 ^ K ) + 1 ) = ( ( 2 ^ ( 2 ^ n ) ) + 1 ) )
10 9 adantl 
 |-  ( ( P = ( ( 2 ^ K ) + 1 ) /\ K = ( 2 ^ n ) ) -> ( ( 2 ^ K ) + 1 ) = ( ( 2 ^ ( 2 ^ n ) ) + 1 ) )
11 7 10 eqtrd 
 |-  ( ( P = ( ( 2 ^ K ) + 1 ) /\ K = ( 2 ^ n ) ) -> P = ( ( 2 ^ ( 2 ^ n ) ) + 1 ) )
12 fmtno 
 |-  ( n e. NN0 -> ( FermatNo ` n ) = ( ( 2 ^ ( 2 ^ n ) ) + 1 ) )
13 12 eqcomd 
 |-  ( n e. NN0 -> ( ( 2 ^ ( 2 ^ n ) ) + 1 ) = ( FermatNo ` n ) )
14 11 13 sylan9eqr 
 |-  ( ( n e. NN0 /\ ( P = ( ( 2 ^ K ) + 1 ) /\ K = ( 2 ^ n ) ) ) -> P = ( FermatNo ` n ) )
15 14 exp32 
 |-  ( n e. NN0 -> ( P = ( ( 2 ^ K ) + 1 ) -> ( K = ( 2 ^ n ) -> P = ( FermatNo ` n ) ) ) )
16 15 com12 
 |-  ( P = ( ( 2 ^ K ) + 1 ) -> ( n e. NN0 -> ( K = ( 2 ^ n ) -> P = ( FermatNo ` n ) ) ) )
17 16 3ad2ant2 
 |-  ( ( K e. NN /\ P = ( ( 2 ^ K ) + 1 ) /\ P e. Prime ) -> ( n e. NN0 -> ( K = ( 2 ^ n ) -> P = ( FermatNo ` n ) ) ) )
18 17 imp 
 |-  ( ( ( K e. NN /\ P = ( ( 2 ^ K ) + 1 ) /\ P e. Prime ) /\ n e. NN0 ) -> ( K = ( 2 ^ n ) -> P = ( FermatNo ` n ) ) )
19 18 reximdva 
 |-  ( ( K e. NN /\ P = ( ( 2 ^ K ) + 1 ) /\ P e. Prime ) -> ( E. n e. NN0 K = ( 2 ^ n ) -> E. n e. NN0 P = ( FermatNo ` n ) ) )
20 6 19 mpd 
 |-  ( ( K e. NN /\ P = ( ( 2 ^ K ) + 1 ) /\ P e. Prime ) -> E. n e. NN0 P = ( FermatNo ` n ) )