Metamath Proof Explorer

Theorem fmtnoodd

Description: Each Fermat number is odd. (Contributed by AV, 26-Jul-2021)

Ref Expression
Assertion fmtnoodd 
|- ( N e. NN0 -> -. 2 || ( FermatNo ` N ) )

Proof

Step Hyp Ref Expression
1 2nn 
 |-  2 e. NN
2 1 a1i 
 |-  ( N e. NN0 -> 2 e. NN )
3 id 
 |-  ( N e. NN0 -> N e. NN0 )
4 2 3 nnexpcld 
 |-  ( N e. NN0 -> ( 2 ^ N ) e. NN )
5 nnm1nn0 
 |-  ( ( 2 ^ N ) e. NN -> ( ( 2 ^ N ) - 1 ) e. NN0 )
6 4 5 syl 
 |-  ( N e. NN0 -> ( ( 2 ^ N ) - 1 ) e. NN0 )
7 2 6 nnexpcld 
 |-  ( N e. NN0 -> ( 2 ^ ( ( 2 ^ N ) - 1 ) ) e. NN )
8 7 nnzd 
 |-  ( N e. NN0 -> ( 2 ^ ( ( 2 ^ N ) - 1 ) ) e. ZZ )
9 oveq2 
 |-  ( k = ( 2 ^ ( ( 2 ^ N ) - 1 ) ) -> ( 2 x. k ) = ( 2 x. ( 2 ^ ( ( 2 ^ N ) - 1 ) ) ) )
10 9 oveq1d 
 |-  ( k = ( 2 ^ ( ( 2 ^ N ) - 1 ) ) -> ( ( 2 x. k ) + 1 ) = ( ( 2 x. ( 2 ^ ( ( 2 ^ N ) - 1 ) ) ) + 1 ) )
11 fmtno 
 |-  ( N e. NN0 -> ( FermatNo ` N ) = ( ( 2 ^ ( 2 ^ N ) ) + 1 ) )
12 10 11 eqeqan12rd 
 |-  ( ( N e. NN0 /\ k = ( 2 ^ ( ( 2 ^ N ) - 1 ) ) ) -> ( ( ( 2 x. k ) + 1 ) = ( FermatNo ` N ) <-> ( ( 2 x. ( 2 ^ ( ( 2 ^ N ) - 1 ) ) ) + 1 ) = ( ( 2 ^ ( 2 ^ N ) ) + 1 ) ) )
13 2cnd 
 |-  ( N e. NN0 -> 2 e. CC )
14 7 nncnd 
 |-  ( N e. NN0 -> ( 2 ^ ( ( 2 ^ N ) - 1 ) ) e. CC )
15 13 14 mulcomd 
 |-  ( N e. NN0 -> ( 2 x. ( 2 ^ ( ( 2 ^ N ) - 1 ) ) ) = ( ( 2 ^ ( ( 2 ^ N ) - 1 ) ) x. 2 ) )
16 expm1t 
 |-  ( ( 2 e. CC /\ ( 2 ^ N ) e. NN ) -> ( 2 ^ ( 2 ^ N ) ) = ( ( 2 ^ ( ( 2 ^ N ) - 1 ) ) x. 2 ) )
17 13 4 16 syl2anc 
 |-  ( N e. NN0 -> ( 2 ^ ( 2 ^ N ) ) = ( ( 2 ^ ( ( 2 ^ N ) - 1 ) ) x. 2 ) )
18 15 17 eqtr4d 
 |-  ( N e. NN0 -> ( 2 x. ( 2 ^ ( ( 2 ^ N ) - 1 ) ) ) = ( 2 ^ ( 2 ^ N ) ) )
19 18 oveq1d 
 |-  ( N e. NN0 -> ( ( 2 x. ( 2 ^ ( ( 2 ^ N ) - 1 ) ) ) + 1 ) = ( ( 2 ^ ( 2 ^ N ) ) + 1 ) )
20 8 12 19 rspcedvd 
 |-  ( N e. NN0 -> E. k e. ZZ ( ( 2 x. k ) + 1 ) = ( FermatNo ` N ) )
21 fmtnonn 
 |-  ( N e. NN0 -> ( FermatNo ` N ) e. NN )
22 21 nnzd 
 |-  ( N e. NN0 -> ( FermatNo ` N ) e. ZZ )
23 odd2np1 
 |-  ( ( FermatNo ` N ) e. ZZ -> ( -. 2 || ( FermatNo ` N ) <-> E. k e. ZZ ( ( 2 x. k ) + 1 ) = ( FermatNo ` N ) ) )
24 22 23 syl 
 |-  ( N e. NN0 -> ( -. 2 || ( FermatNo ` N ) <-> E. k e. ZZ ( ( 2 x. k ) + 1 ) = ( FermatNo ` N ) ) )
25 20 24 mpbird 
 |-  ( N e. NN0 -> -. 2 || ( FermatNo ` N ) )