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\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(N\right)-1=2^{2^N}$$

Proof

Step	Hyp	Ref	Expression
1		fmtno	$$⊢N\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(N\right)=2^{2^N}+1$$
2	1	oveq1d	$$⊢N\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(N\right)-1=2^{2^N}+1-1$$
3		2nn0	$$⊢2\in {\mathbb{N}}_0$$
4	3	a1i	$$⊢N\in {\mathbb{N}}_0\to 2\in {\mathbb{N}}_0$$
5		id	$$⊢N\in {\mathbb{N}}_0\to N\in {\mathbb{N}}_0$$
6	4 5	nn0expcld	$$⊢N\in {\mathbb{N}}_0\to 2^N\in {\mathbb{N}}_0$$
7	4 6	nn0expcld	$$⊢N\in {\mathbb{N}}_0\to 2^{2^N}\in {\mathbb{N}}_0$$
8	7	nn0cnd	$$⊢N\in {\mathbb{N}}_0\to 2^{2^N}\in ℂ$$
9		pncan1	$$⊢2^{2^N}\in ℂ\to 2^{2^N}+1-1=2^{2^N}$$
10	8 9	syl	$$⊢N\in {\mathbb{N}}_0\to 2^{2^N}+1-1=2^{2^N}$$
11	2 10	eqtrd	$$⊢N\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(N\right)-1=2^{2^N}$$