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 ( ๐‘ โˆˆ โ„•0 โ†’ ( FermatNo โ€˜ ( ๐‘ + 1 ) ) = ( ( ( ( FermatNo โ€˜ ๐‘ ) โˆ’ 1 ) โ†‘ 2 ) + 1 ) )

Proof

Step Hyp Ref Expression
1 peano2nn0 โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( ๐‘ + 1 ) โˆˆ โ„•0 )
2 fmtno โŠข ( ( ๐‘ + 1 ) โˆˆ โ„•0 โ†’ ( FermatNo โ€˜ ( ๐‘ + 1 ) ) = ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ + 1 ) ) ) + 1 ) )
3 1 2 syl โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( FermatNo โ€˜ ( ๐‘ + 1 ) ) = ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ + 1 ) ) ) + 1 ) )
4 2nn0 โŠข 2 โˆˆ โ„•0
5 nn0expcl โŠข ( ( 2 โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 ) โ†’ ( 2 โ†‘ ๐‘ ) โˆˆ โ„•0 )
6 4 5 mpan โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( 2 โ†‘ ๐‘ ) โˆˆ โ„•0 )
7 nn0expcl โŠข ( ( 2 โˆˆ โ„•0 โˆง ( 2 โ†‘ ๐‘ ) โˆˆ โ„•0 ) โ†’ ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โˆˆ โ„•0 )
8 7 nn0cnd โŠข ( ( 2 โˆˆ โ„•0 โˆง ( 2 โ†‘ ๐‘ ) โˆˆ โ„•0 ) โ†’ ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โˆˆ โ„‚ )
9 4 6 8 sylancr โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โˆˆ โ„‚ )
10 pncan1 โŠข ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โˆˆ โ„‚ โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) โˆ’ 1 ) = ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) )
11 9 10 syl โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) โˆ’ 1 ) = ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) )
12 11 oveq1d โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) โˆ’ 1 ) โ†‘ 2 ) = ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โ†‘ 2 ) )
13 2cnne0 โŠข ( 2 โˆˆ โ„‚ โˆง 2 โ‰  0 )
14 6 nn0zd โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( 2 โ†‘ ๐‘ ) โˆˆ โ„ค )
15 2z โŠข 2 โˆˆ โ„ค
16 14 15 jctir โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( ( 2 โ†‘ ๐‘ ) โˆˆ โ„ค โˆง 2 โˆˆ โ„ค ) )
17 expmulz โŠข ( ( ( 2 โˆˆ โ„‚ โˆง 2 โ‰  0 ) โˆง ( ( 2 โ†‘ ๐‘ ) โˆˆ โ„ค โˆง 2 โˆˆ โ„ค ) ) โ†’ ( 2 โ†‘ ( ( 2 โ†‘ ๐‘ ) ยท 2 ) ) = ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โ†‘ 2 ) )
18 13 16 17 sylancr โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( 2 โ†‘ ( ( 2 โ†‘ ๐‘ ) ยท 2 ) ) = ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โ†‘ 2 ) )
19 2cn โŠข 2 โˆˆ โ„‚
20 2ne0 โŠข 2 โ‰  0
21 nn0z โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ๐‘ โˆˆ โ„ค )
22 expp1z โŠข ( ( 2 โˆˆ โ„‚ โˆง 2 โ‰  0 โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( 2 โ†‘ ( ๐‘ + 1 ) ) = ( ( 2 โ†‘ ๐‘ ) ยท 2 ) )
23 19 20 21 22 mp3an12i โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( 2 โ†‘ ( ๐‘ + 1 ) ) = ( ( 2 โ†‘ ๐‘ ) ยท 2 ) )
24 23 eqcomd โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( ( 2 โ†‘ ๐‘ ) ยท 2 ) = ( 2 โ†‘ ( ๐‘ + 1 ) ) )
25 24 oveq2d โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( 2 โ†‘ ( ( 2 โ†‘ ๐‘ ) ยท 2 ) ) = ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ + 1 ) ) ) )
26 12 18 25 3eqtr2rd โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ + 1 ) ) ) = ( ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) โˆ’ 1 ) โ†‘ 2 ) )
27 26 oveq1d โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ + 1 ) ) ) + 1 ) = ( ( ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) โˆ’ 1 ) โ†‘ 2 ) + 1 ) )
28 fmtno โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( FermatNo โ€˜ ๐‘ ) = ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) )
29 28 eqcomd โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) = ( FermatNo โ€˜ ๐‘ ) )
30 29 oveq1d โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) โˆ’ 1 ) = ( ( FermatNo โ€˜ ๐‘ ) โˆ’ 1 ) )
31 30 oveq1d โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) โˆ’ 1 ) โ†‘ 2 ) = ( ( ( FermatNo โ€˜ ๐‘ ) โˆ’ 1 ) โ†‘ 2 ) )
32 31 oveq1d โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( ( ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) โˆ’ 1 ) โ†‘ 2 ) + 1 ) = ( ( ( ( FermatNo โ€˜ ๐‘ ) โˆ’ 1 ) โ†‘ 2 ) + 1 ) )
33 3 27 32 3eqtrd โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( FermatNo โ€˜ ( ๐‘ + 1 ) ) = ( ( ( ( FermatNo โ€˜ ๐‘ ) โˆ’ 1 ) โ†‘ 2 ) + 1 ) )