Theorem fmtnorec3

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

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

Proof

Step	Hyp	Ref	Expression
1		fzfid	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(0\dots N-2\right)\in \mathrm{Fin}$$
2		elfznn0	$$⊢n\in \left(0\dots N-2\right)\to n\in {\mathbb{N}}_0$$
3		fmtnonn	$$⊢n\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(n\right)\in \mathbb{N}$$
4	2 3	syl	$$⊢n\in \left(0\dots N-2\right)\to \mathrm{FermatNo}\left(n\right)\in \mathbb{N}$$
5	4	nncnd	$$⊢n\in \left(0\dots N-2\right)\to \mathrm{FermatNo}\left(n\right)\in ℂ$$
6	5	adantl	$$⊢\left(N\in {\mathbb{Z}}_{\ge 2}\wedge n\in \left(0\dots N-2\right)\right)\to \mathrm{FermatNo}\left(n\right)\in ℂ$$
7	1 6	fprodcl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \prod _{n=0}^{N-2}\mathrm{FermatNo}\left(n\right)\in ℂ$$
8		2cn	$$⊢2\in ℂ$$
9	8	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\in ℂ$$
10		uznn0sub	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N-2\in {\mathbb{N}}_0$$
11		fmtnorec2	$$⊢N-2\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(N-2+1\right)=\prod _{n=0}^{N-2}\mathrm{FermatNo}\left(n\right)+2$$
12	10 11	syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \mathrm{FermatNo}\left(N-2+1\right)=\prod _{n=0}^{N-2}\mathrm{FermatNo}\left(n\right)+2$$
13	12	eqcomd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \prod _{n=0}^{N-2}\mathrm{FermatNo}\left(n\right)+2=\mathrm{FermatNo}\left(N-2+1\right)$$
14	7 9 13	mvlraddd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \prod _{n=0}^{N-2}\mathrm{FermatNo}\left(n\right)=\mathrm{FermatNo}\left(N-2+1\right)-2$$
15	14	oveq2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{2^{N-1}}\prod _{n=0}^{N-2}\mathrm{FermatNo}\left(n\right)=2^{2^{N-1}}\left(\mathrm{FermatNo}\left(N-2+1\right)-2\right)$$
16	15	oveq2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \mathrm{FermatNo}\left(N-1\right)+2^{2^{N-1}}\prod _{n=0}^{N-2}\mathrm{FermatNo}\left(n\right)=\mathrm{FermatNo}\left(N-1\right)+2^{2^{N-1}}\left(\mathrm{FermatNo}\left(N-2+1\right)-2\right)$$
17		2nn0	$$⊢2\in {\mathbb{N}}_0$$
18	17	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\in {\mathbb{N}}_0$$
19		eluz2nn	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N\in \mathbb{N}$$
20		nnm1nn0	$$⊢N\in \mathbb{N}\to N-1\in {\mathbb{N}}_0$$
21	19 20	syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N-1\in {\mathbb{N}}_0$$
22	18 21	nn0expcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{N-1}\in {\mathbb{N}}_0$$
23	18 22	nn0expcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{2^{N-1}}\in {\mathbb{N}}_0$$
24	23	nn0cnd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{2^{N-1}}\in ℂ$$
25		peano2nn0	$$⊢N-2\in {\mathbb{N}}_0\to N-2+1\in {\mathbb{N}}_0$$
26	10 25	syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N-2+1\in {\mathbb{N}}_0$$
27		fmtnonn	$$⊢N-2+1\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(N-2+1\right)\in \mathbb{N}$$
28	26 27	syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \mathrm{FermatNo}\left(N-2+1\right)\in \mathbb{N}$$
29	28	nncnd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \mathrm{FermatNo}\left(N-2+1\right)\in ℂ$$
30	24 29 9	subdid	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{2^{N-1}}\left(\mathrm{FermatNo}\left(N-2+1\right)-2\right)=2^{2^{N-1}}\mathrm{FermatNo}\left(N-2+1\right)-2^{2^{N-1}}\cdot 2$$
31		eluzelcn	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N\in ℂ$$
32		ax-1cn	$$⊢1\in ℂ$$
33	32	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 1\in ℂ$$
34		subsub	$$⊢\left(N\in ℂ\wedge 2\in ℂ\wedge 1\in ℂ\right)\to N-\left(2-1\right)=N-2+1$$
35	34	eqcomd	$$⊢\left(N\in ℂ\wedge 2\in ℂ\wedge 1\in ℂ\right)\to N-2+1=N-\left(2-1\right)$$
36	31 9 33 35	syl3anc	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N-2+1=N-\left(2-1\right)$$
37		2m1e1	$$⊢2-1=1$$
38	37	oveq2i	$$⊢N-\left(2-1\right)=N-1$$
39	36 38	eqtrdi	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N-2+1=N-1$$
40	39	fveq2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \mathrm{FermatNo}\left(N-2+1\right)=\mathrm{FermatNo}\left(N-1\right)$$
41	40	oveq2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{2^{N-1}}\mathrm{FermatNo}\left(N-2+1\right)=2^{2^{N-1}}\mathrm{FermatNo}\left(N-1\right)$$
42	41	oveq1d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{2^{N-1}}\mathrm{FermatNo}\left(N-2+1\right)-2^{2^{N-1}}\cdot 2=2^{2^{N-1}}\mathrm{FermatNo}\left(N-1\right)-2^{2^{N-1}}\cdot 2$$
43	30 42	eqtrd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{2^{N-1}}\left(\mathrm{FermatNo}\left(N-2+1\right)-2\right)=2^{2^{N-1}}\mathrm{FermatNo}\left(N-1\right)-2^{2^{N-1}}\cdot 2$$
44	43	oveq2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \mathrm{FermatNo}\left(N-1\right)+2^{2^{N-1}}\left(\mathrm{FermatNo}\left(N-2+1\right)-2\right)=\mathrm{FermatNo}\left(N-1\right)+2^{2^{N-1}}\mathrm{FermatNo}\left(N-1\right)-2^{2^{N-1}}\cdot 2$$
45		fmtnonn	$$⊢N-1\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(N-1\right)\in \mathbb{N}$$
46	21 45	syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \mathrm{FermatNo}\left(N-1\right)\in \mathbb{N}$$
47	46	nncnd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \mathrm{FermatNo}\left(N-1\right)\in ℂ$$
48	47	mulid2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 1\mathrm{FermatNo}\left(N-1\right)=\mathrm{FermatNo}\left(N-1\right)$$
49	48	eqcomd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \mathrm{FermatNo}\left(N-1\right)=1\mathrm{FermatNo}\left(N-1\right)$$
50	49	oveq1d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \mathrm{FermatNo}\left(N-1\right)+2^{2^{N-1}}\mathrm{FermatNo}\left(N-1\right)=1\mathrm{FermatNo}\left(N-1\right)+2^{2^{N-1}}\mathrm{FermatNo}\left(N-1\right)$$
51	33 24 47	adddird	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(1+2^{2^{N-1}}\right)\mathrm{FermatNo}\left(N-1\right)=1\mathrm{FermatNo}\left(N-1\right)+2^{2^{N-1}}\mathrm{FermatNo}\left(N-1\right)$$
52	33 24	addcomd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 1+2^{2^{N-1}}=2^{2^{N-1}}+1$$
53		fmtno	$$⊢N-1\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(N-1\right)=2^{2^{N-1}}+1$$
54	21 53	syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \mathrm{FermatNo}\left(N-1\right)=2^{2^{N-1}}+1$$
55	52 54	eqtr4d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 1+2^{2^{N-1}}=\mathrm{FermatNo}\left(N-1\right)$$
56	55	oveq1d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(1+2^{2^{N-1}}\right)\mathrm{FermatNo}\left(N-1\right)=\mathrm{FermatNo}\left(N-1\right)\mathrm{FermatNo}\left(N-1\right)$$
57	47	sqvald	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\mathrm{FermatNo}\left(N-1\right)}^2=\mathrm{FermatNo}\left(N-1\right)\mathrm{FermatNo}\left(N-1\right)$$
58	56 57	eqtr4d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(1+2^{2^{N-1}}\right)\mathrm{FermatNo}\left(N-1\right)={\mathrm{FermatNo}\left(N-1\right)}^2$$
59	50 51 58	3eqtr2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \mathrm{FermatNo}\left(N-1\right)+2^{2^{N-1}}\mathrm{FermatNo}\left(N-1\right)={\mathrm{FermatNo}\left(N-1\right)}^2$$
60	59	oveq1d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \mathrm{FermatNo}\left(N-1\right)+2^{2^{N-1}}\mathrm{FermatNo}\left(N-1\right)-2^{2^{N-1}}\cdot 2={\mathrm{FermatNo}\left(N-1\right)}^2-2^{2^{N-1}}\cdot 2$$
61	24 47	mulcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{2^{N-1}}\mathrm{FermatNo}\left(N-1\right)\in ℂ$$
62	24 9	mulcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2^{2^{N-1}}\cdot 2\in ℂ$$
63	47 61 62	addsubassd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \mathrm{FermatNo}\left(N-1\right)+2^{2^{N-1}}\mathrm{FermatNo}\left(N-1\right)-2^{2^{N-1}}\cdot 2=\mathrm{FermatNo}\left(N-1\right)+2^{2^{N-1}}\mathrm{FermatNo}\left(N-1\right)-2^{2^{N-1}}\cdot 2$$
64		npcan1	$$⊢N\in ℂ\to N-1+1=N$$
65	31 64	syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N-1+1=N$$
66	65	eqcomd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N=N-1+1$$
67	66	fveq2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \mathrm{FermatNo}\left(N\right)=\mathrm{FermatNo}\left(N-1+1\right)$$
68		fmtnorec1	$$⊢N-1\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(N-1+1\right)={\left(\mathrm{FermatNo}\left(N-1\right)-1\right)}^2+1$$
69	21 68	syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \mathrm{FermatNo}\left(N-1+1\right)={\left(\mathrm{FermatNo}\left(N-1\right)-1\right)}^2+1$$
70		binom2sub1	$$⊢\mathrm{FermatNo}\left(N-1\right)\in ℂ\to {\left(\mathrm{FermatNo}\left(N-1\right)-1\right)}^2={\mathrm{FermatNo}\left(N-1\right)}^2-2\mathrm{FermatNo}\left(N-1\right)+1$$
71	47 70	syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\left(\mathrm{FermatNo}\left(N-1\right)-1\right)}^2={\mathrm{FermatNo}\left(N-1\right)}^2-2\mathrm{FermatNo}\left(N-1\right)+1$$
72	71	oveq1d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\left(\mathrm{FermatNo}\left(N-1\right)-1\right)}^2+1=\left({\mathrm{FermatNo}\left(N-1\right)}^2-2\mathrm{FermatNo}\left(N-1\right)\right)+1+1$$
73	46	nnsqcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\mathrm{FermatNo}\left(N-1\right)}^2\in \mathbb{N}$$
74	73	nncnd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\mathrm{FermatNo}\left(N-1\right)}^2\in ℂ$$
75	9 47	mulcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\mathrm{FermatNo}\left(N-1\right)\in ℂ$$
76	74 75	subcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\mathrm{FermatNo}\left(N-1\right)}^2-2\mathrm{FermatNo}\left(N-1\right)\in ℂ$$
77	76 33 33	addassd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left({\mathrm{FermatNo}\left(N-1\right)}^2-2\mathrm{FermatNo}\left(N-1\right)\right)+1+1=\left({\mathrm{FermatNo}\left(N-1\right)}^2-2\mathrm{FermatNo}\left(N-1\right)\right)+1+1$$
78	32	2timesi	$$⊢2\cdot 1=1+1$$
79	78	eqcomi	$$⊢1+1=2\cdot 1$$
80	79	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 1+1=2\cdot 1$$
81	80	oveq2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left({\mathrm{FermatNo}\left(N-1\right)}^2-2\mathrm{FermatNo}\left(N-1\right)\right)+1+1={\mathrm{FermatNo}\left(N-1\right)}^2-2\mathrm{FermatNo}\left(N-1\right)+2\cdot 1$$
82	77 81	eqtrd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left({\mathrm{FermatNo}\left(N-1\right)}^2-2\mathrm{FermatNo}\left(N-1\right)\right)+1+1={\mathrm{FermatNo}\left(N-1\right)}^2-2\mathrm{FermatNo}\left(N-1\right)+2\cdot 1$$
83	8 32	mulcli	$$⊢2\cdot 1\in ℂ$$
84	83	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\cdot 1\in ℂ$$
85	74 75 84	subadd23d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\mathrm{FermatNo}\left(N-1\right)}^2-2\mathrm{FermatNo}\left(N-1\right)+2\cdot 1={\mathrm{FermatNo}\left(N-1\right)}^2+2\cdot 1-2\mathrm{FermatNo}\left(N-1\right)$$
86	9 33 47	subdid	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\left(1-\mathrm{FermatNo}\left(N-1\right)\right)=2\cdot 1-2\mathrm{FermatNo}\left(N-1\right)$$
87	86	eqcomd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\cdot 1-2\mathrm{FermatNo}\left(N-1\right)=2\left(1-\mathrm{FermatNo}\left(N-1\right)\right)$$
88	87	oveq2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\mathrm{FermatNo}\left(N-1\right)}^2+2\cdot 1-2\mathrm{FermatNo}\left(N-1\right)={\mathrm{FermatNo}\left(N-1\right)}^2+2\left(1-\mathrm{FermatNo}\left(N-1\right)\right)$$
89	33 47	subcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 1-\mathrm{FermatNo}\left(N-1\right)\in ℂ$$
90	9 89	mulneg2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\left(-\left(1-\mathrm{FermatNo}\left(N-1\right)\right)\right)=-2\left(1-\mathrm{FermatNo}\left(N-1\right)\right)$$
91	33 47	negsubdi2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to -\left(1-\mathrm{FermatNo}\left(N-1\right)\right)=\mathrm{FermatNo}\left(N-1\right)-1$$
92		fmtnom1nn	$$⊢N-1\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(N-1\right)-1=2^{2^{N-1}}$$
93	21 92	syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \mathrm{FermatNo}\left(N-1\right)-1=2^{2^{N-1}}$$
94	91 93	eqtrd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to -\left(1-\mathrm{FermatNo}\left(N-1\right)\right)=2^{2^{N-1}}$$
95	94	oveq2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\left(-\left(1-\mathrm{FermatNo}\left(N-1\right)\right)\right)=22^{2^{N-1}}$$
96	90 95	eqtr3d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to -2\left(1-\mathrm{FermatNo}\left(N-1\right)\right)=22^{2^{N-1}}$$
97	96	oveq2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\mathrm{FermatNo}\left(N-1\right)}^2-\left(-2\left(1-\mathrm{FermatNo}\left(N-1\right)\right)\right)={\mathrm{FermatNo}\left(N-1\right)}^2-22^{2^{N-1}}$$
98	9 89	mulcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\left(1-\mathrm{FermatNo}\left(N-1\right)\right)\in ℂ$$
99	74 98	subnegd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\mathrm{FermatNo}\left(N-1\right)}^2-\left(-2\left(1-\mathrm{FermatNo}\left(N-1\right)\right)\right)={\mathrm{FermatNo}\left(N-1\right)}^2+2\left(1-\mathrm{FermatNo}\left(N-1\right)\right)$$
100	9 24	mulcomd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 22^{2^{N-1}}=2^{2^{N-1}}\cdot 2$$
101	100	oveq2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\mathrm{FermatNo}\left(N-1\right)}^2-22^{2^{N-1}}={\mathrm{FermatNo}\left(N-1\right)}^2-2^{2^{N-1}}\cdot 2$$
102	97 99 101	3eqtr3d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\mathrm{FermatNo}\left(N-1\right)}^2+2\left(1-\mathrm{FermatNo}\left(N-1\right)\right)={\mathrm{FermatNo}\left(N-1\right)}^2-2^{2^{N-1}}\cdot 2$$
103	85 88 102	3eqtrd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\mathrm{FermatNo}\left(N-1\right)}^2-2\mathrm{FermatNo}\left(N-1\right)+2\cdot 1={\mathrm{FermatNo}\left(N-1\right)}^2-2^{2^{N-1}}\cdot 2$$
104	72 82 103	3eqtrd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\left(\mathrm{FermatNo}\left(N-1\right)-1\right)}^2+1={\mathrm{FermatNo}\left(N-1\right)}^2-2^{2^{N-1}}\cdot 2$$
105	67 69 104	3eqtrrd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to {\mathrm{FermatNo}\left(N-1\right)}^2-2^{2^{N-1}}\cdot 2=\mathrm{FermatNo}\left(N\right)$$
106	60 63 105	3eqtr3d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \mathrm{FermatNo}\left(N-1\right)+2^{2^{N-1}}\mathrm{FermatNo}\left(N-1\right)-2^{2^{N-1}}\cdot 2=\mathrm{FermatNo}\left(N\right)$$
107	16 44 106	3eqtrrd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \mathrm{FermatNo}\left(N\right)=\mathrm{FermatNo}\left(N-1\right)+2^{2^{N-1}}\prod _{n=0}^{N-2}\mathrm{FermatNo}\left(n\right)$$