Theorem fmtno4

Description: The 4 th Fermat number, see remark in ApostolNT p. 7. (Contributed by AV, 13-Jun-2021)

	Ref	Expression
Assertion	fmtno4	$$⊢\mathrm{FermatNo}\left(4\right)=65537$$

Proof

Step	Hyp	Ref	Expression
1		4nn0	$$⊢4\in {\mathbb{N}}_0$$
2		fmtno	$$⊢4\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(4\right)=2^{2^4}+1$$
3	1 2	ax-mp	$$⊢\mathrm{FermatNo}\left(4\right)=2^{2^4}+1$$
4		2exp4	$$⊢2^4=16$$
5	4	oveq2i	$$⊢2^{2^4}=2^{16}$$
6	5	oveq1i	$$⊢2^{2^4}+1=2^{16}+1$$
7		2exp16	$$⊢2^{16}=65536$$
8	7	oveq1i	$$⊢2^{16}+1=65536+1$$
9		6nn0	$$⊢6\in {\mathbb{N}}_0$$
10		5nn0	$$⊢5\in {\mathbb{N}}_0$$
11	9 10	deccl	$$⊢65\in {\mathbb{N}}_0$$
12	11 10	deccl	$$⊢655\in {\mathbb{N}}_0$$
13		3nn0	$$⊢3\in {\mathbb{N}}_0$$
14	12 13	deccl	$$⊢6553\in {\mathbb{N}}_0$$
15		6p1e7	$$⊢6+1=7$$
16		eqid	$$⊢65536=65536$$
17	14 9 15 16	decsuc	$$⊢65536+1=65537$$
18	6 8 17	3eqtri	$$⊢2^{2^4}+1=65537$$
19	3 18	eqtri	$$⊢\mathrm{FermatNo}\left(4\right)=65537$$