Metamath Proof Explorer

Theorem fmtnom1nn

Description: A Fermat number minus one is a power of a power of two. (Contributed by AV, 29-Jul-2021)

Ref Expression
Assertion fmtnom1nn 
|- ( N e. NN0 -> ( ( FermatNo ` N ) - 1 ) = ( 2 ^ ( 2 ^ N ) ) )

Proof

Step Hyp Ref Expression
1 fmtno 
 |-  ( N e. NN0 -> ( FermatNo ` N ) = ( ( 2 ^ ( 2 ^ N ) ) + 1 ) )
2 1 oveq1d 
 |-  ( N e. NN0 -> ( ( FermatNo ` N ) - 1 ) = ( ( ( 2 ^ ( 2 ^ N ) ) + 1 ) - 1 ) )
3 2nn0 
 |-  2 e. NN0
4 3 a1i 
 |-  ( N e. NN0 -> 2 e. NN0 )
5 id 
 |-  ( N e. NN0 -> N e. NN0 )
6 4 5 nn0expcld 
 |-  ( N e. NN0 -> ( 2 ^ N ) e. NN0 )
7 4 6 nn0expcld 
 |-  ( N e. NN0 -> ( 2 ^ ( 2 ^ N ) ) e. NN0 )
8 7 nn0cnd 
 |-  ( N e. NN0 -> ( 2 ^ ( 2 ^ N ) ) e. CC )
9 pncan1 
 |-  ( ( 2 ^ ( 2 ^ N ) ) e. CC -> ( ( ( 2 ^ ( 2 ^ N ) ) + 1 ) - 1 ) = ( 2 ^ ( 2 ^ N ) ) )
10 8 9 syl 
 |-  ( N e. NN0 -> ( ( ( 2 ^ ( 2 ^ N ) ) + 1 ) - 1 ) = ( 2 ^ ( 2 ^ N ) ) )
11 2 10 eqtrd 
 |-  ( N e. NN0 -> ( ( FermatNo ` N ) - 1 ) = ( 2 ^ ( 2 ^ N ) ) )