Metamath Proof Explorer

Theorem fmtnoodd

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

Ref Expression
Assertion fmtnoodd ( ๐‘ โˆˆ โ„•0 โ†’ ยฌ 2 โˆฅ ( FermatNo โ€˜ ๐‘ ) )

Proof

Step Hyp Ref Expression
1 2nn โŠข 2 โˆˆ โ„•
2 1 a1i โŠข ( ๐‘ โˆˆ โ„•0 โ†’ 2 โˆˆ โ„• )
3 id โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ๐‘ โˆˆ โ„•0 )
4 2 3 nnexpcld โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( 2 โ†‘ ๐‘ ) โˆˆ โ„• )
5 nnm1nn0 โŠข ( ( 2 โ†‘ ๐‘ ) โˆˆ โ„• โ†’ ( ( 2 โ†‘ ๐‘ ) โˆ’ 1 ) โˆˆ โ„•0 )
6 4 5 syl โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( ( 2 โ†‘ ๐‘ ) โˆ’ 1 ) โˆˆ โ„•0 )
7 2 6 nnexpcld โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( 2 โ†‘ ( ( 2 โ†‘ ๐‘ ) โˆ’ 1 ) ) โˆˆ โ„• )
8 7 nnzd โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( 2 โ†‘ ( ( 2 โ†‘ ๐‘ ) โˆ’ 1 ) ) โˆˆ โ„ค )
9 oveq2 โŠข ( ๐‘˜ = ( 2 โ†‘ ( ( 2 โ†‘ ๐‘ ) โˆ’ 1 ) ) โ†’ ( 2 ยท ๐‘˜ ) = ( 2 ยท ( 2 โ†‘ ( ( 2 โ†‘ ๐‘ ) โˆ’ 1 ) ) ) )
10 9 oveq1d โŠข ( ๐‘˜ = ( 2 โ†‘ ( ( 2 โ†‘ ๐‘ ) โˆ’ 1 ) ) โ†’ ( ( 2 ยท ๐‘˜ ) + 1 ) = ( ( 2 ยท ( 2 โ†‘ ( ( 2 โ†‘ ๐‘ ) โˆ’ 1 ) ) ) + 1 ) )
11 fmtno โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( FermatNo โ€˜ ๐‘ ) = ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) )
12 10 11 eqeqan12rd โŠข ( ( ๐‘ โˆˆ โ„•0 โˆง ๐‘˜ = ( 2 โ†‘ ( ( 2 โ†‘ ๐‘ ) โˆ’ 1 ) ) ) โ†’ ( ( ( 2 ยท ๐‘˜ ) + 1 ) = ( FermatNo โ€˜ ๐‘ ) โ†” ( ( 2 ยท ( 2 โ†‘ ( ( 2 โ†‘ ๐‘ ) โˆ’ 1 ) ) ) + 1 ) = ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) ) )
13 2cnd โŠข ( ๐‘ โˆˆ โ„•0 โ†’ 2 โˆˆ โ„‚ )
14 7 nncnd โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( 2 โ†‘ ( ( 2 โ†‘ ๐‘ ) โˆ’ 1 ) ) โˆˆ โ„‚ )
15 13 14 mulcomd โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( 2 ยท ( 2 โ†‘ ( ( 2 โ†‘ ๐‘ ) โˆ’ 1 ) ) ) = ( ( 2 โ†‘ ( ( 2 โ†‘ ๐‘ ) โˆ’ 1 ) ) ยท 2 ) )
16 expm1t โŠข ( ( 2 โˆˆ โ„‚ โˆง ( 2 โ†‘ ๐‘ ) โˆˆ โ„• ) โ†’ ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) = ( ( 2 โ†‘ ( ( 2 โ†‘ ๐‘ ) โˆ’ 1 ) ) ยท 2 ) )
17 13 4 16 syl2anc โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) = ( ( 2 โ†‘ ( ( 2 โ†‘ ๐‘ ) โˆ’ 1 ) ) ยท 2 ) )
18 15 17 eqtr4d โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( 2 ยท ( 2 โ†‘ ( ( 2 โ†‘ ๐‘ ) โˆ’ 1 ) ) ) = ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) )
19 18 oveq1d โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( ( 2 ยท ( 2 โ†‘ ( ( 2 โ†‘ ๐‘ ) โˆ’ 1 ) ) ) + 1 ) = ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) )
20 8 12 19 rspcedvd โŠข ( ๐‘ โˆˆ โ„•0 โ†’ โˆƒ ๐‘˜ โˆˆ โ„ค ( ( 2 ยท ๐‘˜ ) + 1 ) = ( FermatNo โ€˜ ๐‘ ) )
21 fmtnonn โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( FermatNo โ€˜ ๐‘ ) โˆˆ โ„• )
22 21 nnzd โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( FermatNo โ€˜ ๐‘ ) โˆˆ โ„ค )
23 odd2np1 โŠข ( ( FermatNo โ€˜ ๐‘ ) โˆˆ โ„ค โ†’ ( ยฌ 2 โˆฅ ( FermatNo โ€˜ ๐‘ ) โ†” โˆƒ ๐‘˜ โˆˆ โ„ค ( ( 2 ยท ๐‘˜ ) + 1 ) = ( FermatNo โ€˜ ๐‘ ) ) )
24 22 23 syl โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( ยฌ 2 โˆฅ ( FermatNo โ€˜ ๐‘ ) โ†” โˆƒ ๐‘˜ โˆˆ โ„ค ( ( 2 ยท ๐‘˜ ) + 1 ) = ( FermatNo โ€˜ ๐‘ ) ) )
25 20 24 mpbird โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ยฌ 2 โˆฅ ( FermatNo โ€˜ ๐‘ ) )