Metamath Proof Explorer

Theorem fmtnorec1

Description: The first recurrence relation for Fermat numbers, see Wikipedia "Fermat number", https://en.wikipedia.org/wiki/Fermat_number#Basic_properties , 22-Jul-2021. (Contributed by AV, 22-Jul-2021)

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

Proof

Step Hyp Ref Expression
1 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
2 fmtno 
 |-  ( ( N + 1 ) e. NN0 -> ( FermatNo ` ( N + 1 ) ) = ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) + 1 ) )
3 1 2 syl 
 |-  ( N e. NN0 -> ( FermatNo ` ( N + 1 ) ) = ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) + 1 ) )
4 2nn0 
 |-  2 e. NN0
5 nn0expcl 
 |-  ( ( 2 e. NN0 /\ N e. NN0 ) -> ( 2 ^ N ) e. NN0 )
6 4 5 mpan 
 |-  ( N e. NN0 -> ( 2 ^ N ) e. NN0 )
7 nn0expcl 
 |-  ( ( 2 e. NN0 /\ ( 2 ^ N ) e. NN0 ) -> ( 2 ^ ( 2 ^ N ) ) e. NN0 )
8 7 nn0cnd 
 |-  ( ( 2 e. NN0 /\ ( 2 ^ N ) e. NN0 ) -> ( 2 ^ ( 2 ^ N ) ) e. CC )
9 4 6 8 sylancr 
 |-  ( N e. NN0 -> ( 2 ^ ( 2 ^ N ) ) e. CC )
10 pncan1 
 |-  ( ( 2 ^ ( 2 ^ N ) ) e. CC -> ( ( ( 2 ^ ( 2 ^ N ) ) + 1 ) - 1 ) = ( 2 ^ ( 2 ^ N ) ) )
11 9 10 syl 
 |-  ( N e. NN0 -> ( ( ( 2 ^ ( 2 ^ N ) ) + 1 ) - 1 ) = ( 2 ^ ( 2 ^ N ) ) )
12 11 oveq1d 
 |-  ( N e. NN0 -> ( ( ( ( 2 ^ ( 2 ^ N ) ) + 1 ) - 1 ) ^ 2 ) = ( ( 2 ^ ( 2 ^ N ) ) ^ 2 ) )
13 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
14 6 nn0zd 
 |-  ( N e. NN0 -> ( 2 ^ N ) e. ZZ )
15 2z 
 |-  2 e. ZZ
16 14 15 jctir 
 |-  ( N e. NN0 -> ( ( 2 ^ N ) e. ZZ /\ 2 e. ZZ ) )
17 expmulz 
 |-  ( ( ( 2 e. CC /\ 2 =/= 0 ) /\ ( ( 2 ^ N ) e. ZZ /\ 2 e. ZZ ) ) -> ( 2 ^ ( ( 2 ^ N ) x. 2 ) ) = ( ( 2 ^ ( 2 ^ N ) ) ^ 2 ) )
18 13 16 17 sylancr 
 |-  ( N e. NN0 -> ( 2 ^ ( ( 2 ^ N ) x. 2 ) ) = ( ( 2 ^ ( 2 ^ N ) ) ^ 2 ) )
19 2cn 
 |-  2 e. CC
20 2ne0 
 |-  2 =/= 0
21 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
22 expp1z 
 |-  ( ( 2 e. CC /\ 2 =/= 0 /\ N e. ZZ ) -> ( 2 ^ ( N + 1 ) ) = ( ( 2 ^ N ) x. 2 ) )
23 19 20 21 22 mp3an12i 
 |-  ( N e. NN0 -> ( 2 ^ ( N + 1 ) ) = ( ( 2 ^ N ) x. 2 ) )
24 23 eqcomd 
 |-  ( N e. NN0 -> ( ( 2 ^ N ) x. 2 ) = ( 2 ^ ( N + 1 ) ) )
25 24 oveq2d 
 |-  ( N e. NN0 -> ( 2 ^ ( ( 2 ^ N ) x. 2 ) ) = ( 2 ^ ( 2 ^ ( N + 1 ) ) ) )
26 12 18 25 3eqtr2rd 
 |-  ( N e. NN0 -> ( 2 ^ ( 2 ^ ( N + 1 ) ) ) = ( ( ( ( 2 ^ ( 2 ^ N ) ) + 1 ) - 1 ) ^ 2 ) )
27 26 oveq1d 
 |-  ( N e. NN0 -> ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) + 1 ) = ( ( ( ( ( 2 ^ ( 2 ^ N ) ) + 1 ) - 1 ) ^ 2 ) + 1 ) )
28 fmtno 
 |-  ( N e. NN0 -> ( FermatNo ` N ) = ( ( 2 ^ ( 2 ^ N ) ) + 1 ) )
29 28 eqcomd 
 |-  ( N e. NN0 -> ( ( 2 ^ ( 2 ^ N ) ) + 1 ) = ( FermatNo ` N ) )
30 29 oveq1d 
 |-  ( N e. NN0 -> ( ( ( 2 ^ ( 2 ^ N ) ) + 1 ) - 1 ) = ( ( FermatNo ` N ) - 1 ) )
31 30 oveq1d 
 |-  ( N e. NN0 -> ( ( ( ( 2 ^ ( 2 ^ N ) ) + 1 ) - 1 ) ^ 2 ) = ( ( ( FermatNo ` N ) - 1 ) ^ 2 ) )
32 31 oveq1d 
 |-  ( N e. NN0 -> ( ( ( ( ( 2 ^ ( 2 ^ N ) ) + 1 ) - 1 ) ^ 2 ) + 1 ) = ( ( ( ( FermatNo ` N ) - 1 ) ^ 2 ) + 1 ) )
33 3 27 32 3eqtrd 
 |-  ( N e. NN0 -> ( FermatNo ` ( N + 1 ) ) = ( ( ( ( FermatNo ` N ) - 1 ) ^ 2 ) + 1 ) )