Theorem fmtnorec1

Description: The first recurrence relation for Fermat numbers, see Wikipedia "Fermat number", https://en.wikipedia.org/wiki/Fermat_number#Basic_properties , 22-Jul-2021. (Contributed by AV, 22-Jul-2021)

	Ref	Expression
Assertion	fmtnorec1	$$⊢N\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(N+1\right)={\left(\mathrm{FermatNo}\left(N\right)-1\right)}^2+1$$

Proof

Step	Hyp	Ref	Expression
1		peano2nn0	$$⊢N\in {\mathbb{N}}_0\to N+1\in {\mathbb{N}}_0$$
2		fmtno	$$⊢N+1\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(N+1\right)=2^{2^{N+1}}+1$$
3	1 2	syl	$$⊢N\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(N+1\right)=2^{2^{N+1}}+1$$
4		2nn0	$$⊢2\in {\mathbb{N}}_0$$
5		nn0expcl	$$⊢\left(2\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to 2^N\in {\mathbb{N}}_0$$
6	4 5	mpan	$$⊢N\in {\mathbb{N}}_0\to 2^N\in {\mathbb{N}}_0$$
7		nn0expcl	$$⊢\left(2\in {\mathbb{N}}_0\wedge 2^N\in {\mathbb{N}}_0\right)\to 2^{2^N}\in {\mathbb{N}}_0$$
8	7	nn0cnd	$$⊢\left(2\in {\mathbb{N}}_0\wedge 2^N\in {\mathbb{N}}_0\right)\to 2^{2^N}\in ℂ$$
9	4 6 8	sylancr	$$⊢N\in {\mathbb{N}}_0\to 2^{2^N}\in ℂ$$
10		pncan1	$$⊢2^{2^N}\in ℂ\to 2^{2^N}+1-1=2^{2^N}$$
11	9 10	syl	$$⊢N\in {\mathbb{N}}_0\to 2^{2^N}+1-1=2^{2^N}$$
12	11	oveq1d	$$⊢N\in {\mathbb{N}}_0\to {\left(2^{2^N}+1-1\right)}^2={\left(2^{2^N}\right)}^2$$
13		2cnne0	$$⊢\left(2\in ℂ\wedge 2\ne 0\right)$$
14	6	nn0zd	$$⊢N\in {\mathbb{N}}_0\to 2^N\in \mathbb{Z}$$
15		2z	$$⊢2\in \mathbb{Z}$$
16	14 15	jctir	$$⊢N\in {\mathbb{N}}_0\to \left(2^N\in \mathbb{Z}\wedge 2\in \mathbb{Z}\right)$$
17		expmulz	$$⊢\left(\left(2\in ℂ\wedge 2\ne 0\right)\wedge \left(2^N\in \mathbb{Z}\wedge 2\in \mathbb{Z}\right)\right)\to 2^{2^N\cdot 2}={\left(2^{2^N}\right)}^2$$
18	13 16 17	sylancr	$$⊢N\in {\mathbb{N}}_0\to 2^{2^N\cdot 2}={\left(2^{2^N}\right)}^2$$
19		2cn	$$⊢2\in ℂ$$
20		2ne0	$$⊢2\ne 0$$
21		nn0z	$$⊢N\in {\mathbb{N}}_0\to N\in \mathbb{Z}$$
22		expp1z	$$⊢\left(2\in ℂ\wedge 2\ne 0\wedge N\in \mathbb{Z}\right)\to 2^{N+1}=2^N\cdot 2$$
23	19 20 21 22	mp3an12i	$$⊢N\in {\mathbb{N}}_0\to 2^{N+1}=2^N\cdot 2$$
24	23	eqcomd	$$⊢N\in {\mathbb{N}}_0\to 2^N\cdot 2=2^{N+1}$$
25	24	oveq2d	$$⊢N\in {\mathbb{N}}_0\to 2^{2^N\cdot 2}=2^{2^{N+1}}$$
26	12 18 25	3eqtr2rd	$$⊢N\in {\mathbb{N}}_0\to 2^{2^{N+1}}={\left(2^{2^N}+1-1\right)}^2$$
27	26	oveq1d	$$⊢N\in {\mathbb{N}}_0\to 2^{2^{N+1}}+1={\left(2^{2^N}+1-1\right)}^2+1$$
28		fmtno	$$⊢N\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(N\right)=2^{2^N}+1$$
29	28	eqcomd	$$⊢N\in {\mathbb{N}}_0\to 2^{2^N}+1=\mathrm{FermatNo}\left(N\right)$$
30	29	oveq1d	$$⊢N\in {\mathbb{N}}_0\to 2^{2^N}+1-1=\mathrm{FermatNo}\left(N\right)-1$$
31	30	oveq1d	$$⊢N\in {\mathbb{N}}_0\to {\left(2^{2^N}+1-1\right)}^2={\left(\mathrm{FermatNo}\left(N\right)-1\right)}^2$$
32	31	oveq1d	$$⊢N\in {\mathbb{N}}_0\to {\left(2^{2^N}+1-1\right)}^2+1={\left(\mathrm{FermatNo}\left(N\right)-1\right)}^2+1$$
33	3 27 32	3eqtrd	$$⊢N\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(N+1\right)={\left(\mathrm{FermatNo}\left(N\right)-1\right)}^2+1$$