Theorem fmtnoodd

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

	Ref	Expression
Assertion	fmtnoodd	$$⊢N\in {\mathbb{N}}_0\to \neg 2\parallel \mathrm{FermatNo}\left(N\right)$$

Proof

Step	Hyp	Ref	Expression
1		2nn	$$⊢2\in \mathbb{N}$$
2	1	a1i	$$⊢N\in {\mathbb{N}}_0\to 2\in \mathbb{N}$$
3		id	$$⊢N\in {\mathbb{N}}_0\to N\in {\mathbb{N}}_0$$
4	2 3	nnexpcld	$$⊢N\in {\mathbb{N}}_0\to 2^N\in \mathbb{N}$$
5		nnm1nn0	$$⊢2^N\in \mathbb{N}\to 2^N-1\in {\mathbb{N}}_0$$
6	4 5	syl	$$⊢N\in {\mathbb{N}}_0\to 2^N-1\in {\mathbb{N}}_0$$
7	2 6	nnexpcld	$$⊢N\in {\mathbb{N}}_0\to 2^{2^N-1}\in \mathbb{N}$$
8	7	nnzd	$$⊢N\in {\mathbb{N}}_0\to 2^{2^N-1}\in \mathbb{Z}$$
9		oveq2	$$⊢k=2^{2^N-1}\to 2k=22^{2^N-1}$$
10	9	oveq1d	$$⊢k=2^{2^N-1}\to 2k+1=22^{2^N-1}+1$$
11		fmtno	$$⊢N\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(N\right)=2^{2^N}+1$$
12	10 11	eqeqan12rd	$$⊢\left(N\in {\mathbb{N}}_0\wedge k=2^{2^N-1}\right)\to \left(2k+1=\mathrm{FermatNo}\left(N\right)\leftrightarrow 22^{2^N-1}+1=2^{2^N}+1\right)$$
13		2cnd	$$⊢N\in {\mathbb{N}}_0\to 2\in ℂ$$
14	7	nncnd	$$⊢N\in {\mathbb{N}}_0\to 2^{2^N-1}\in ℂ$$
15	13 14	mulcomd	$$⊢N\in {\mathbb{N}}_0\to 22^{2^N-1}=2^{2^N-1}\cdot 2$$
16		expm1t	$$⊢\left(2\in ℂ\wedge 2^N\in \mathbb{N}\right)\to 2^{2^N}=2^{2^N-1}\cdot 2$$
17	13 4 16	syl2anc	$$⊢N\in {\mathbb{N}}_0\to 2^{2^N}=2^{2^N-1}\cdot 2$$
18	15 17	eqtr4d	$$⊢N\in {\mathbb{N}}_0\to 22^{2^N-1}=2^{2^N}$$
19	18	oveq1d	$$⊢N\in {\mathbb{N}}_0\to 22^{2^N-1}+1=2^{2^N}+1$$
20	8 12 19	rspcedvd	$$⊢N\in {\mathbb{N}}_0\to \exists k\in \mathbb{Z}2k+1=\mathrm{FermatNo}\left(N\right)$$
21		fmtnonn	$$⊢N\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(N\right)\in \mathbb{N}$$
22	21	nnzd	$$⊢N\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(N\right)\in \mathbb{Z}$$
23		odd2np1	$$⊢\mathrm{FermatNo}\left(N\right)\in \mathbb{Z}\to \left(\neg 2\parallel \mathrm{FermatNo}\left(N\right)\leftrightarrow \exists k\in \mathbb{Z}2k+1=\mathrm{FermatNo}\left(N\right)\right)$$
24	22 23	syl	$$⊢N\in {\mathbb{N}}_0\to \left(\neg 2\parallel \mathrm{FermatNo}\left(N\right)\leftrightarrow \exists k\in \mathbb{Z}2k+1=\mathrm{FermatNo}\left(N\right)\right)$$
25	20 24	mpbird	$$⊢N\in {\mathbb{N}}_0\to \neg 2\parallel \mathrm{FermatNo}\left(N\right)$$