Theorem fmtnorec4

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

	Ref	Expression
Assertion	fmtnorec4	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \mathrm{FermatNo}\left(N\right)={\mathrm{FermatNo}\left(N-1\right)}^2-2{\left(\mathrm{FermatNo}\left(N-2\right)-1\right)}^2$$

Proof

Step	Hyp	Ref	Expression
1		eluz2nn	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N\in \mathbb{N}$$
2		nnm1nn0	$$⊢N\in \mathbb{N}\to N-1\in {\mathbb{N}}_0$$
3	1 2	syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N-1\in {\mathbb{N}}_0$$
4		fmtno	$$⊢N-1\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(N-1\right)=2^{2^{N-1}}+1$$
5	3 4	syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \mathrm{FermatNo}\left(N-1\right)=2^{2^{N-1}}+1$$
6	5	oveq1d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\mathrm{FermatNo}\left(N-1\right)}^2={\left(2^{2^{N-1}}+1\right)}^2$$
7		2nn	$$⊢2\in \mathbb{N}$$
8	7	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\in \mathbb{N}$$
9		2nn0	$$⊢2\in {\mathbb{N}}_0$$
10	9	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\in {\mathbb{N}}_0$$
11	10 3	nn0expcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{N-1}\in {\mathbb{N}}_0$$
12	8 11	nnexpcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{2^{N-1}}\in \mathbb{N}$$
13	12	nncnd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{2^{N-1}}\in ℂ$$
14		binom21	$$⊢2^{2^{N-1}}\in ℂ\to {\left(2^{2^{N-1}}+1\right)}^2={\left(2^{2^{N-1}}\right)}^2+22^{2^{N-1}}+1$$
15	13 14	syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\left(2^{2^{N-1}}+1\right)}^2={\left(2^{2^{N-1}}\right)}^2+22^{2^{N-1}}+1$$
16		2cn	$$⊢2\in ℂ$$
17	16	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\in ℂ$$
18	17 10 11	expmuld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{2^{N-1}\cdot 2}={\left(2^{2^{N-1}}\right)}^2$$
19	17 3	expp1d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{N-1+1}=2^{N-1}\cdot 2$$
20	1	nncnd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N\in ℂ$$
21		npcan1	$$⊢N\in ℂ\to N-1+1=N$$
22	20 21	syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N-1+1=N$$
23	22	oveq2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{N-1+1}=2^N$$
24	19 23	eqtr3d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{N-1}\cdot 2=2^N$$
25	24	oveq2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{2^{N-1}\cdot 2}=2^{2^N}$$
26	18 25	eqtr3d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\left(2^{2^{N-1}}\right)}^2=2^{2^N}$$
27	26	oveq1d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\left(2^{2^{N-1}}\right)}^2+22^{2^{N-1}}=2^{2^N}+22^{2^{N-1}}$$
28	27	oveq1d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\left(2^{2^{N-1}}\right)}^2+22^{2^{N-1}}+1=2^{2^N}+22^{2^{N-1}}+1$$
29	6 15 28	3eqtrd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\mathrm{FermatNo}\left(N-1\right)}^2=2^{2^N}+22^{2^{N-1}}+1$$
30		uznn0sub	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N-2\in {\mathbb{N}}_0$$
31		fmtno	$$⊢N-2\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(N-2\right)=2^{2^{N-2}}+1$$
32	30 31	syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \mathrm{FermatNo}\left(N-2\right)=2^{2^{N-2}}+1$$
33	32	oveq1d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \mathrm{FermatNo}\left(N-2\right)-1=2^{2^{N-2}}+1-1$$
34	33	oveq1d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\left(\mathrm{FermatNo}\left(N-2\right)-1\right)}^2={\left(2^{2^{N-2}}+1-1\right)}^2$$
35	10 30	nn0expcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{N-2}\in {\mathbb{N}}_0$$
36	8 35	nnexpcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{2^{N-2}}\in \mathbb{N}$$
37	36	nncnd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{2^{N-2}}\in ℂ$$
38		peano2cn	$$⊢2^{2^{N-2}}\in ℂ\to 2^{2^{N-2}}+1\in ℂ$$
39	37 38	syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{2^{N-2}}+1\in ℂ$$
40		binom2sub1	$$⊢2^{2^{N-2}}+1\in ℂ\to {\left(2^{2^{N-2}}+1-1\right)}^2={\left(2^{2^{N-2}}+1\right)}^2-2\left(2^{2^{N-2}}+1\right)+1$$
41	39 40	syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\left(2^{2^{N-2}}+1-1\right)}^2={\left(2^{2^{N-2}}+1\right)}^2-2\left(2^{2^{N-2}}+1\right)+1$$
42		binom21	$$⊢2^{2^{N-2}}\in ℂ\to {\left(2^{2^{N-2}}+1\right)}^2={\left(2^{2^{N-2}}\right)}^2+22^{2^{N-2}}+1$$
43	37 42	syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\left(2^{2^{N-2}}+1\right)}^2={\left(2^{2^{N-2}}\right)}^2+22^{2^{N-2}}+1$$
44	43	oveq1d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\left(2^{2^{N-2}}+1\right)}^2-2\left(2^{2^{N-2}}+1\right)=\left({\left(2^{2^{N-2}}\right)}^2+22^{2^{N-2}}\right)+1-2\left(2^{2^{N-2}}+1\right)$$
45	44	oveq1d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\left(2^{2^{N-2}}+1\right)}^2-2\left(2^{2^{N-2}}+1\right)+1=\left({\left(2^{2^{N-2}}\right)}^2+22^{2^{N-2}}+1\right)-2\left(2^{2^{N-2}}+1\right)+1$$
46	34 41 45	3eqtrd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\left(\mathrm{FermatNo}\left(N-2\right)-1\right)}^2=\left({\left(2^{2^{N-2}}\right)}^2+22^{2^{N-2}}+1\right)-2\left(2^{2^{N-2}}+1\right)+1$$
47	46	oveq2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2{\left(\mathrm{FermatNo}\left(N-2\right)-1\right)}^2=2\left(\left({\left(2^{2^{N-2}}\right)}^2+22^{2^{N-2}}+1\right)-2\left(2^{2^{N-2}}+1\right)+1\right)$$
48	29 47	oveq12d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\mathrm{FermatNo}\left(N-1\right)}^2-2{\left(\mathrm{FermatNo}\left(N-2\right)-1\right)}^2=\left(2^{2^N}+22^{2^{N-1}}\right)+1-2\left(\left({\left(2^{2^{N-2}}\right)}^2+22^{2^{N-2}}+1\right)-2\left(2^{2^{N-2}}+1\right)+1\right)$$
49	36 10	nnexpcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\left(2^{2^{N-2}}\right)}^2\in \mathbb{N}$$
50	49	nncnd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\left(2^{2^{N-2}}\right)}^2\in ℂ$$
51	17 37	mulcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 22^{2^{N-2}}\in ℂ$$
52	50 51	addcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\left(2^{2^{N-2}}\right)}^2+22^{2^{N-2}}\in ℂ$$
53		peano2cn	$$⊢{\left(2^{2^{N-2}}\right)}^2+22^{2^{N-2}}\in ℂ\to {\left(2^{2^{N-2}}\right)}^2+22^{2^{N-2}}+1\in ℂ$$
54	52 53	syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\left(2^{2^{N-2}}\right)}^2+22^{2^{N-2}}+1\in ℂ$$
55	17 39	mulcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\left(2^{2^{N-2}}+1\right)\in ℂ$$
56	54 55	subcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left({\left(2^{2^{N-2}}\right)}^2+22^{2^{N-2}}\right)+1-2\left(2^{2^{N-2}}+1\right)\in ℂ$$
57		1cnd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 1\in ℂ$$
58	17 56 57	adddid	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\left(\left({\left(2^{2^{N-2}}\right)}^2+22^{2^{N-2}}+1\right)-2\left(2^{2^{N-2}}+1\right)+1\right)=2\left(\left({\left(2^{2^{N-2}}\right)}^2+22^{2^{N-2}}\right)+1-2\left(2^{2^{N-2}}+1\right)\right)+2\cdot 1$$
59	52 57	addcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\left(2^{2^{N-2}}\right)}^2+22^{2^{N-2}}+1\in ℂ$$
60	17 59 55	subdid	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\left(\left({\left(2^{2^{N-2}}\right)}^2+22^{2^{N-2}}\right)+1-2\left(2^{2^{N-2}}+1\right)\right)=2\left({\left(2^{2^{N-2}}\right)}^2+22^{2^{N-2}}+1\right)-22\left(2^{2^{N-2}}+1\right)$$
61	17 52 57	adddid	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\left({\left(2^{2^{N-2}}\right)}^2+22^{2^{N-2}}+1\right)=2\left({\left(2^{2^{N-2}}\right)}^2+22^{2^{N-2}}\right)+2\cdot 1$$
62	17 50 51	adddid	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\left({\left(2^{2^{N-2}}\right)}^2+22^{2^{N-2}}\right)=2{\left(2^{2^{N-2}}\right)}^2+222^{2^{N-2}}$$
63	17 10 35	expmuld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{2^{N-2}\cdot 2}={\left(2^{2^{N-2}}\right)}^2$$
64	17 30	expp1d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{N-2+1}=2^{N-2}\cdot 2$$
65	20 17 57	subsubd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N-\left(2-1\right)=N-2+1$$
66	65	eqcomd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N-2+1=N-\left(2-1\right)$$
67	66	oveq2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{N-2+1}=2^{N-\left(2-1\right)}$$
68	64 67	eqtr3d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{N-2}\cdot 2=2^{N-\left(2-1\right)}$$
69	68	oveq2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{2^{N-2}\cdot 2}=2^{2^{N-\left(2-1\right)}}$$
70	63 69	eqtr3d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\left(2^{2^{N-2}}\right)}^2=2^{2^{N-\left(2-1\right)}}$$
71	70	oveq2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2{\left(2^{2^{N-2}}\right)}^2=22^{2^{N-\left(2-1\right)}}$$
72		2m1e1	$$⊢2-1=1$$
73	72	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2-1=1$$
74	73	oveq2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N-\left(2-1\right)=N-1$$
75	74	oveq2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{N-\left(2-1\right)}=2^{N-1}$$
76	75	oveq2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{2^{N-\left(2-1\right)}}=2^{2^{N-1}}$$
77	76	oveq2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 22^{2^{N-\left(2-1\right)}}=22^{2^{N-1}}$$
78	71 77	eqtrd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2{\left(2^{2^{N-2}}\right)}^2=22^{2^{N-1}}$$
79	17 17 37	mulassd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\cdot 22^{2^{N-2}}=222^{2^{N-2}}$$
80	79	eqcomd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 222^{2^{N-2}}=2\cdot 22^{2^{N-2}}$$
81	78 80	oveq12d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2{\left(2^{2^{N-2}}\right)}^2+222^{2^{N-2}}=22^{2^{N-1}}+2\cdot 22^{2^{N-2}}$$
82	62 81	eqtrd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\left({\left(2^{2^{N-2}}\right)}^2+22^{2^{N-2}}\right)=22^{2^{N-1}}+2\cdot 22^{2^{N-2}}$$
83		2t1e2	$$⊢2\cdot 1=2$$
84	83	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\cdot 1=2$$
85	82 84	oveq12d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\left({\left(2^{2^{N-2}}\right)}^2+22^{2^{N-2}}\right)+2\cdot 1=22^{2^{N-1}}+2\cdot 22^{2^{N-2}}+2$$
86	61 85	eqtrd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\left({\left(2^{2^{N-2}}\right)}^2+22^{2^{N-2}}+1\right)=22^{2^{N-1}}+2\cdot 22^{2^{N-2}}+2$$
87	17 37 57	adddid	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\left(2^{2^{N-2}}+1\right)=22^{2^{N-2}}+2\cdot 1$$
88	84	oveq2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 22^{2^{N-2}}+2\cdot 1=22^{2^{N-2}}+2$$
89	87 88	eqtrd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\left(2^{2^{N-2}}+1\right)=22^{2^{N-2}}+2$$
90	89	oveq2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 22\left(2^{2^{N-2}}+1\right)=2\left(22^{2^{N-2}}+2\right)$$
91	17 51 17	adddid	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\left(22^{2^{N-2}}+2\right)=222^{2^{N-2}}+2\cdot 2$$
92		2t2e4	$$⊢2\cdot 2=4$$
93	92	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\cdot 2=4$$
94	80 93	oveq12d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 222^{2^{N-2}}+2\cdot 2=2\cdot 22^{2^{N-2}}+4$$
95	90 91 94	3eqtrd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 22\left(2^{2^{N-2}}+1\right)=2\cdot 22^{2^{N-2}}+4$$
96	86 95	oveq12d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\left({\left(2^{2^{N-2}}\right)}^2+22^{2^{N-2}}+1\right)-22\left(2^{2^{N-2}}+1\right)=\left(22^{2^{N-1}}+2\cdot 22^{2^{N-2}}\right)+2-\left(2\cdot 22^{2^{N-2}}+4\right)$$
97	60 96	eqtrd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\left(\left({\left(2^{2^{N-2}}\right)}^2+22^{2^{N-2}}\right)+1-2\left(2^{2^{N-2}}+1\right)\right)=\left(22^{2^{N-1}}+2\cdot 22^{2^{N-2}}\right)+2-\left(2\cdot 22^{2^{N-2}}+4\right)$$
98	97 84	oveq12d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\left(\left({\left(2^{2^{N-2}}\right)}^2+22^{2^{N-2}}\right)+1-2\left(2^{2^{N-2}}+1\right)\right)+2\cdot 1=\left(22^{2^{N-1}}+2\cdot 22^{2^{N-2}}+2\right)-\left(2\cdot 22^{2^{N-2}}+4\right)+2$$
99	58 98	eqtrd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\left(\left({\left(2^{2^{N-2}}\right)}^2+22^{2^{N-2}}+1\right)-2\left(2^{2^{N-2}}+1\right)+1\right)=\left(22^{2^{N-1}}+2\cdot 22^{2^{N-2}}+2\right)-\left(2\cdot 22^{2^{N-2}}+4\right)+2$$
100	99	oveq2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(2^{2^N}+22^{2^{N-1}}\right)+1-2\left(\left({\left(2^{2^{N-2}}\right)}^2+22^{2^{N-2}}+1\right)-2\left(2^{2^{N-2}}+1\right)+1\right)=\left(2^{2^N}+22^{2^{N-1}}\right)+1-\left(\left(22^{2^{N-1}}+2\cdot 22^{2^{N-2}}+2\right)-\left(2\cdot 22^{2^{N-2}}+4\right)+2\right)$$
101	17 13	mulcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 22^{2^{N-1}}\in ℂ$$
102	16 16	mulcli	$$⊢2\cdot 2\in ℂ$$
103	102	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\cdot 2\in ℂ$$
104	103 37	mulcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\cdot 22^{2^{N-2}}\in ℂ$$
105	101 104	addcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 22^{2^{N-1}}+2\cdot 22^{2^{N-2}}\in ℂ$$
106	105 17	addcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 22^{2^{N-1}}+2\cdot 22^{2^{N-2}}+2\in ℂ$$
107		4cn	$$⊢4\in ℂ$$
108	107	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 4\in ℂ$$
109	104 108	addcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\cdot 22^{2^{N-2}}+4\in ℂ$$
110	105 17 17	addassd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(22^{2^{N-1}}+2\cdot 22^{2^{N-2}}\right)+2+2=22^{2^{N-1}}+2\cdot 22^{2^{N-2}}+2+2$$
111		2p2e4	$$⊢2+2=4$$
112	111	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2+2=4$$
113	112	oveq2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 22^{2^{N-1}}+2\cdot 22^{2^{N-2}}+2+2=22^{2^{N-1}}+2\cdot 22^{2^{N-2}}+4$$
114	101 104 108	addassd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 22^{2^{N-1}}+2\cdot 22^{2^{N-2}}+4=22^{2^{N-1}}+2\cdot 22^{2^{N-2}}+4$$
115	110 113 114	3eqtrd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(22^{2^{N-1}}+2\cdot 22^{2^{N-2}}\right)+2+2=22^{2^{N-1}}+2\cdot 22^{2^{N-2}}+4$$
116	106 17 101 109 115	subaddeqd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(22^{2^{N-1}}+2\cdot 22^{2^{N-2}}\right)+2-\left(2\cdot 22^{2^{N-2}}+4\right)=22^{2^{N-1}}-2$$
117	116	eqcomd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 22^{2^{N-1}}-2=\left(22^{2^{N-1}}+2\cdot 22^{2^{N-2}}\right)+2-\left(2\cdot 22^{2^{N-2}}+4\right)$$
118	106 109	subcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(22^{2^{N-1}}+2\cdot 22^{2^{N-2}}\right)+2-\left(2\cdot 22^{2^{N-2}}+4\right)\in ℂ$$
119	101 17 118	subadd2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(22^{2^{N-1}}-2=\left(22^{2^{N-1}}+2\cdot 22^{2^{N-2}}\right)+2-\left(2\cdot 22^{2^{N-2}}+4\right)\leftrightarrow \left(22^{2^{N-1}}+2\cdot 22^{2^{N-2}}+2\right)-\left(2\cdot 22^{2^{N-2}}+4\right)+2=22^{2^{N-1}}\right)$$
120	117 119	mpbid	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(22^{2^{N-1}}+2\cdot 22^{2^{N-2}}+2\right)-\left(2\cdot 22^{2^{N-2}}+4\right)+2=22^{2^{N-1}}$$
121	120	oveq2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{2^N}+\left(\left(22^{2^{N-1}}+2\cdot 22^{2^{N-2}}\right)+2-\left(2\cdot 22^{2^{N-2}}+4\right)\right)+2=2^{2^N}+22^{2^{N-1}}$$
122		eluzge2nn0	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N\in {\mathbb{N}}_0$$
123	10 122	nn0expcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^N\in {\mathbb{N}}_0$$
124	8 123	nnexpcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{2^N}\in \mathbb{N}$$
125	124	nncnd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{2^N}\in ℂ$$
126	125 101	addcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{2^N}+22^{2^{N-1}}\in ℂ$$
127	118 17	addcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(22^{2^{N-1}}+2\cdot 22^{2^{N-2}}+2\right)-\left(2\cdot 22^{2^{N-2}}+4\right)+2\in ℂ$$
128	126 127 125	subadd2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(2^{2^N}+22^{2^{N-1}}-\left(\left(22^{2^{N-1}}+2\cdot 22^{2^{N-2}}+2\right)-\left(2\cdot 22^{2^{N-2}}+4\right)+2\right)=2^{2^N}\leftrightarrow 2^{2^N}+\left(\left(22^{2^{N-1}}+2\cdot 22^{2^{N-2}}\right)+2-\left(2\cdot 22^{2^{N-2}}+4\right)\right)+2=2^{2^N}+22^{2^{N-1}}\right)$$
129	121 128	mpbird	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{2^N}+22^{2^{N-1}}-\left(\left(22^{2^{N-1}}+2\cdot 22^{2^{N-2}}+2\right)-\left(2\cdot 22^{2^{N-2}}+4\right)+2\right)=2^{2^N}$$
130	129	oveq1d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(2^{2^N}+22^{2^{N-1}}\right)-\left(\left(22^{2^{N-1}}+2\cdot 22^{2^{N-2}}+2\right)-\left(2\cdot 22^{2^{N-2}}+4\right)+2\right)+1=2^{2^N}+1$$
131	126 57 127	addsubd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(2^{2^N}+22^{2^{N-1}}\right)+1-\left(\left(22^{2^{N-1}}+2\cdot 22^{2^{N-2}}+2\right)-\left(2\cdot 22^{2^{N-2}}+4\right)+2\right)=\left(2^{2^N}+22^{2^{N-1}}\right)-\left(\left(22^{2^{N-1}}+2\cdot 22^{2^{N-2}}+2\right)-\left(2\cdot 22^{2^{N-2}}+4\right)+2\right)+1$$
132		fmtno	$$⊢N\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(N\right)=2^{2^N}+1$$
133	122 132	syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \mathrm{FermatNo}\left(N\right)=2^{2^N}+1$$
134	130 131 133	3eqtr4d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(2^{2^N}+22^{2^{N-1}}\right)+1-\left(\left(22^{2^{N-1}}+2\cdot 22^{2^{N-2}}+2\right)-\left(2\cdot 22^{2^{N-2}}+4\right)+2\right)=\mathrm{FermatNo}\left(N\right)$$
135	48 100 134	3eqtrrd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \mathrm{FermatNo}\left(N\right)={\mathrm{FermatNo}\left(N-1\right)}^2-2{\left(\mathrm{FermatNo}\left(N-2\right)-1\right)}^2$$