Theorem fmtno3

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

	Ref	Expression
Assertion	fmtno3	$$⊢\mathrm{FermatNo}\left(3\right)=257$$

Proof

Step	Hyp	Ref	Expression
1		3nn0	$$⊢3\in {\mathbb{N}}_0$$
2		fmtno	$$⊢3\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(3\right)=2^{2^3}+1$$
3	1 2	ax-mp	$$⊢\mathrm{FermatNo}\left(3\right)=2^{2^3}+1$$
4		cu2	$$⊢2^3=8$$
5	4	oveq2i	$$⊢2^{2^3}=2^8$$
6	5	oveq1i	$$⊢2^{2^3}+1=2^8+1$$
7		2exp8	$$⊢2^8=256$$
8	7	oveq1i	$$⊢2^8+1=256+1$$
9		2nn0	$$⊢2\in {\mathbb{N}}_0$$
10		5nn0	$$⊢5\in {\mathbb{N}}_0$$
11	9 10	deccl	$$⊢25\in {\mathbb{N}}_0$$
12		6nn0	$$⊢6\in {\mathbb{N}}_0$$
13		6p1e7	$$⊢6+1=7$$
14		eqid	$$⊢256=256$$
15	11 12 13 14	decsuc	$$⊢256+1=257$$
16	6 8 15	3eqtri	$$⊢2^{2^3}+1=257$$
17	3 16	eqtri	$$⊢\mathrm{FermatNo}\left(3\right)=257$$