Theorem fmtno5

Description: The 5 th Fermat number. (Contributed by AV, 30-Jul-2021)

	Ref	Expression
Assertion	fmtno5	$$⊢\mathrm{FermatNo}\left(5\right)=4294967297$$

Proof

Step	Hyp	Ref	Expression
1		df-5	$$⊢5=4+1$$
2	1	fveq2i	$$⊢\mathrm{FermatNo}\left(5\right)=\mathrm{FermatNo}\left(4+1\right)$$
3		4nn0	$$⊢4\in {\mathbb{N}}_0$$
4		fmtnorec1	$$⊢4\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(4+1\right)={\left(\mathrm{FermatNo}\left(4\right)-1\right)}^2+1$$
5	3 4	ax-mp	$$⊢\mathrm{FermatNo}\left(4+1\right)={\left(\mathrm{FermatNo}\left(4\right)-1\right)}^2+1$$
6	2 5	eqtri	$$⊢\mathrm{FermatNo}\left(5\right)={\left(\mathrm{FermatNo}\left(4\right)-1\right)}^2+1$$
7		2nn0	$$⊢2\in {\mathbb{N}}_0$$
8	3 7	deccl	$$⊢42\in {\mathbb{N}}_0$$
9		9nn0	$$⊢9\in {\mathbb{N}}_0$$
10	8 9	deccl	$$⊢429\in {\mathbb{N}}_0$$
11	10 3	deccl	$$⊢4294\in {\mathbb{N}}_0$$
12	11 9	deccl	$$⊢42949\in {\mathbb{N}}_0$$
13		6nn0	$$⊢6\in {\mathbb{N}}_0$$
14	12 13	deccl	$$⊢429496\in {\mathbb{N}}_0$$
15		7nn0	$$⊢7\in {\mathbb{N}}_0$$
16	14 15	deccl	$$⊢4294967\in {\mathbb{N}}_0$$
17	16 7	deccl	$$⊢42949672\in {\mathbb{N}}_0$$
18	17 9	deccl	$$⊢429496729\in {\mathbb{N}}_0$$
19		6p1e7	$$⊢6+1=7$$
20		5nn0	$$⊢5\in {\mathbb{N}}_0$$
21	13 20	deccl	$$⊢65\in {\mathbb{N}}_0$$
22	21 20	deccl	$$⊢655\in {\mathbb{N}}_0$$
23		3nn0	$$⊢3\in {\mathbb{N}}_0$$
24	22 23	deccl	$$⊢6553\in {\mathbb{N}}_0$$
25		1nn0	$$⊢1\in {\mathbb{N}}_0$$
26		fmtno4	$$⊢\mathrm{FermatNo}\left(4\right)=65537$$
27		3p1e4	$$⊢3+1=4$$
28		eqid	$$⊢6553=6553$$
29	22 23 27 28	decsuc	$$⊢6553+1=6554$$
30		6cn	$$⊢6\in ℂ$$
31		ax-1cn	$$⊢1\in ℂ$$
32		df-7	$$⊢7=6+1$$
33	30 31 32	mvrraddi	$$⊢7-1=6$$
34	24 15 25 26 29 33	decsubi	$$⊢\mathrm{FermatNo}\left(4\right)-1=65536$$
35	34	oveq1i	$$⊢{\left(\mathrm{FermatNo}\left(4\right)-1\right)}^2={65536}^2$$
36		fmtno5lem4	$$⊢{65536}^2=4294967296$$
37	35 36	eqtri	$$⊢{\left(\mathrm{FermatNo}\left(4\right)-1\right)}^2=4294967296$$
38	18 13 19 37	decsuc	$$⊢{\left(\mathrm{FermatNo}\left(4\right)-1\right)}^2+1=4294967297$$
39	6 38	eqtri	$$⊢\mathrm{FermatNo}\left(5\right)=4294967297$$