Theorem fmtnorec2lem

Description: Lemma for fmtnorec2 (induction step). (Contributed by AV, 29-Jul-2021)

	Ref	Expression
Assertion	fmtnorec2lem	$$⊢y\in {\mathbb{N}}_0\to \left(\mathrm{FermatNo}\left(y+1\right)=\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+2\to \mathrm{FermatNo}\left(y+1+1\right)=\prod _{n=0}^{y+1}\mathrm{FermatNo}\left(n\right)+2\right)$$

Proof

Step	Hyp	Ref	Expression
1		peano2nn0	$$⊢y\in {\mathbb{N}}_0\to y+1\in {\mathbb{N}}_0$$
2		peano2nn0	$$⊢y+1\in {\mathbb{N}}_0\to y+1+1\in {\mathbb{N}}_0$$
3		fmtno	$$⊢y+1+1\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(y+1+1\right)=2^{2^{y+1+1}}+1$$
4	1 2 3	3syl	$$⊢y\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(y+1+1\right)=2^{2^{y+1+1}}+1$$
5		2cnd	$$⊢y\in {\mathbb{N}}_0\to 2\in ℂ$$
6	5 1	expp1d	$$⊢y\in {\mathbb{N}}_0\to 2^{y+1+1}=2^{y+1}\cdot 2$$
7	6	oveq2d	$$⊢y\in {\mathbb{N}}_0\to 2^{2^{y+1+1}}=2^{2^{y+1}\cdot 2}$$
8		2nn0	$$⊢2\in {\mathbb{N}}_0$$
9	8	a1i	$$⊢y\in {\mathbb{N}}_0\to 2\in {\mathbb{N}}_0$$
10	9 1	nn0expcld	$$⊢y\in {\mathbb{N}}_0\to 2^{y+1}\in {\mathbb{N}}_0$$
11	9 10	nn0expcld	$$⊢y\in {\mathbb{N}}_0\to 2^{2^{y+1}}\in {\mathbb{N}}_0$$
12	11	nn0cnd	$$⊢y\in {\mathbb{N}}_0\to 2^{2^{y+1}}\in ℂ$$
13	12	sqvald	$$⊢y\in {\mathbb{N}}_0\to {\left(2^{2^{y+1}}\right)}^2=2^{2^{y+1}}{2}^{2^{y+1}}$$
14	5 9 10	expmuld	$$⊢y\in {\mathbb{N}}_0\to 2^{2^{y+1}\cdot 2}={\left(2^{2^{y+1}}\right)}^2$$
15		fmtnom1nn	$$⊢y+1\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(y+1\right)-1=2^{2^{y+1}}$$
16	1 15	syl	$$⊢y\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(y+1\right)-1=2^{2^{y+1}}$$
17	16 16	oveq12d	$$⊢y\in {\mathbb{N}}_0\to \left(\mathrm{FermatNo}\left(y+1\right)-1\right)\left(\mathrm{FermatNo}\left(y+1\right)-1\right)=2^{2^{y+1}}{2}^{2^{y+1}}$$
18	13 14 17	3eqtr4d	$$⊢y\in {\mathbb{N}}_0\to 2^{2^{y+1}\cdot 2}=\left(\mathrm{FermatNo}\left(y+1\right)-1\right)\left(\mathrm{FermatNo}\left(y+1\right)-1\right)$$
19	7 18	eqtrd	$$⊢y\in {\mathbb{N}}_0\to 2^{2^{y+1+1}}=\left(\mathrm{FermatNo}\left(y+1\right)-1\right)\left(\mathrm{FermatNo}\left(y+1\right)-1\right)$$
20	19	oveq1d	$$⊢y\in {\mathbb{N}}_0\to 2^{2^{y+1+1}}+1=\left(\mathrm{FermatNo}\left(y+1\right)-1\right)\left(\mathrm{FermatNo}\left(y+1\right)-1\right)+1$$
21	4 20	eqtrd	$$⊢y\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(y+1+1\right)=\left(\mathrm{FermatNo}\left(y+1\right)-1\right)\left(\mathrm{FermatNo}\left(y+1\right)-1\right)+1$$
22	21	adantr	$$⊢\left(y\in {\mathbb{N}}_0\wedge \mathrm{FermatNo}\left(y+1\right)=\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+2\right)\to \mathrm{FermatNo}\left(y+1+1\right)=\left(\mathrm{FermatNo}\left(y+1\right)-1\right)\left(\mathrm{FermatNo}\left(y+1\right)-1\right)+1$$
23		oveq1	$$⊢\mathrm{FermatNo}\left(y+1\right)=\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+2\to \mathrm{FermatNo}\left(y+1\right)-1=\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+2-1$$
24	23	oveq1d	$$⊢\mathrm{FermatNo}\left(y+1\right)=\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+2\to \left(\mathrm{FermatNo}\left(y+1\right)-1\right)\left(\mathrm{FermatNo}\left(y+1\right)-1\right)=\left(\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+2-1\right)\left(\mathrm{FermatNo}\left(y+1\right)-1\right)$$
25	24	oveq1d	$$⊢\mathrm{FermatNo}\left(y+1\right)=\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+2\to \left(\mathrm{FermatNo}\left(y+1\right)-1\right)\left(\mathrm{FermatNo}\left(y+1\right)-1\right)+1=\left(\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+2-1\right)\left(\mathrm{FermatNo}\left(y+1\right)-1\right)+1$$
26	25	adantl	$$⊢\left(y\in {\mathbb{N}}_0\wedge \mathrm{FermatNo}\left(y+1\right)=\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+2\right)\to \left(\mathrm{FermatNo}\left(y+1\right)-1\right)\left(\mathrm{FermatNo}\left(y+1\right)-1\right)+1=\left(\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+2-1\right)\left(\mathrm{FermatNo}\left(y+1\right)-1\right)+1$$
27		fzfid	$$⊢y\in {\mathbb{N}}_0\to \left(0\dots y\right)\in \mathrm{Fin}$$
28		elfznn0	$$⊢n\in \left(0\dots y\right)\to n\in {\mathbb{N}}_0$$
29		fmtnonn	$$⊢n\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(n\right)\in \mathbb{N}$$
30	29	nncnd	$$⊢n\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(n\right)\in ℂ$$
31	28 30	syl	$$⊢n\in \left(0\dots y\right)\to \mathrm{FermatNo}\left(n\right)\in ℂ$$
32	31	adantl	$$⊢\left(y\in {\mathbb{N}}_0\wedge n\in \left(0\dots y\right)\right)\to \mathrm{FermatNo}\left(n\right)\in ℂ$$
33	27 32	fprodcl	$$⊢y\in {\mathbb{N}}_0\to \prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\in ℂ$$
34		1cnd	$$⊢y\in {\mathbb{N}}_0\to 1\in ℂ$$
35	33 5 34	addsubassd	$$⊢y\in {\mathbb{N}}_0\to \prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+2-1=\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+2-1$$
36		2m1e1	$$⊢2-1=1$$
37	36	oveq2i	$$⊢\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+2-1=\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+1$$
38	35 37	eqtrdi	$$⊢y\in {\mathbb{N}}_0\to \prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+2-1=\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+1$$
39	38	oveq1d	$$⊢y\in {\mathbb{N}}_0\to \left(\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+2-1\right)\left(\mathrm{FermatNo}\left(y+1\right)-1\right)=\left(\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+1\right)\left(\mathrm{FermatNo}\left(y+1\right)-1\right)$$
40		fmtnonn	$$⊢y+1\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(y+1\right)\in \mathbb{N}$$
41	1 40	syl	$$⊢y\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(y+1\right)\in \mathbb{N}$$
42	41	nncnd	$$⊢y\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(y+1\right)\in ℂ$$
43	42 34	subcld	$$⊢y\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(y+1\right)-1\in ℂ$$
44	33 42	muls1d	$$⊢y\in {\mathbb{N}}_0\to \prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\left(\mathrm{FermatNo}\left(y+1\right)-1\right)=\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\mathrm{FermatNo}\left(y+1\right)-\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)$$
45	43	mullidd	$$⊢y\in {\mathbb{N}}_0\to 1\left(\mathrm{FermatNo}\left(y+1\right)-1\right)=\mathrm{FermatNo}\left(y+1\right)-1$$
46	44 45	oveq12d	$$⊢y\in {\mathbb{N}}_0\to \prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\left(\mathrm{FermatNo}\left(y+1\right)-1\right)+1\left(\mathrm{FermatNo}\left(y+1\right)-1\right)=\left(\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\mathrm{FermatNo}\left(y+1\right)-\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\right)+\mathrm{FermatNo}\left(y+1\right)-1$$
47	33 43 34 46	joinlmuladdmuld	$$⊢y\in {\mathbb{N}}_0\to \left(\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+1\right)\left(\mathrm{FermatNo}\left(y+1\right)-1\right)=\left(\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\mathrm{FermatNo}\left(y+1\right)-\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\right)+\mathrm{FermatNo}\left(y+1\right)-1$$
48	39 47	eqtrd	$$⊢y\in {\mathbb{N}}_0\to \left(\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+2-1\right)\left(\mathrm{FermatNo}\left(y+1\right)-1\right)=\left(\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\mathrm{FermatNo}\left(y+1\right)-\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\right)+\mathrm{FermatNo}\left(y+1\right)-1$$
49	48	adantr	$$⊢\left(y\in {\mathbb{N}}_0\wedge \mathrm{FermatNo}\left(y+1\right)=\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+2\right)\to \left(\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+2-1\right)\left(\mathrm{FermatNo}\left(y+1\right)-1\right)=\left(\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\mathrm{FermatNo}\left(y+1\right)-\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\right)+\mathrm{FermatNo}\left(y+1\right)-1$$
50	49	oveq1d	$$⊢\left(y\in {\mathbb{N}}_0\wedge \mathrm{FermatNo}\left(y+1\right)=\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+2\right)\to \left(\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+2-1\right)\left(\mathrm{FermatNo}\left(y+1\right)-1\right)+1=\left(\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\mathrm{FermatNo}\left(y+1\right)-\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\right)+\left(\mathrm{FermatNo}\left(y+1\right)-1\right)+1$$
51		eqcom	$$⊢\mathrm{FermatNo}\left(y+1\right)=\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+2\leftrightarrow \prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+2=\mathrm{FermatNo}\left(y+1\right)$$
52	42 5 33	subadd2d	$$⊢y\in {\mathbb{N}}_0\to \left(\mathrm{FermatNo}\left(y+1\right)-2=\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\leftrightarrow \prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+2=\mathrm{FermatNo}\left(y+1\right)\right)$$
53	51 52	bitr4id	$$⊢y\in {\mathbb{N}}_0\to \left(\mathrm{FermatNo}\left(y+1\right)=\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+2\leftrightarrow \mathrm{FermatNo}\left(y+1\right)-2=\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\right)$$
54		oveq2	$$⊢\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)=\mathrm{FermatNo}\left(y+1\right)-2\to \prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\mathrm{FermatNo}\left(y+1\right)-\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)=\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\mathrm{FermatNo}\left(y+1\right)-\left(\mathrm{FermatNo}\left(y+1\right)-2\right)$$
55	54	oveq1d	$$⊢\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)=\mathrm{FermatNo}\left(y+1\right)-2\to \left(\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\mathrm{FermatNo}\left(y+1\right)-\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\right)+\mathrm{FermatNo}\left(y+1\right)-1=\left(\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\mathrm{FermatNo}\left(y+1\right)-\left(\mathrm{FermatNo}\left(y+1\right)-2\right)\right)+\mathrm{FermatNo}\left(y+1\right)-1$$
56	55	oveq1d	$$⊢\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)=\mathrm{FermatNo}\left(y+1\right)-2\to \left(\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\mathrm{FermatNo}\left(y+1\right)-\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\right)+\left(\mathrm{FermatNo}\left(y+1\right)-1\right)+1=\left(\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\mathrm{FermatNo}\left(y+1\right)-\left(\mathrm{FermatNo}\left(y+1\right)-2\right)\right)+\left(\mathrm{FermatNo}\left(y+1\right)-1\right)+1$$
57	56	eqcoms	$$⊢\mathrm{FermatNo}\left(y+1\right)-2=\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\to \left(\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\mathrm{FermatNo}\left(y+1\right)-\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\right)+\left(\mathrm{FermatNo}\left(y+1\right)-1\right)+1=\left(\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\mathrm{FermatNo}\left(y+1\right)-\left(\mathrm{FermatNo}\left(y+1\right)-2\right)\right)+\left(\mathrm{FermatNo}\left(y+1\right)-1\right)+1$$
58	33 42	mulcld	$$⊢y\in {\mathbb{N}}_0\to \prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\mathrm{FermatNo}\left(y+1\right)\in ℂ$$
59	42 5	subcld	$$⊢y\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(y+1\right)-2\in ℂ$$
60	58 59	subcld	$$⊢y\in {\mathbb{N}}_0\to \prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\mathrm{FermatNo}\left(y+1\right)-\left(\mathrm{FermatNo}\left(y+1\right)-2\right)\in ℂ$$
61	60 43 34	addassd	$$⊢y\in {\mathbb{N}}_0\to \left(\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\mathrm{FermatNo}\left(y+1\right)-\left(\mathrm{FermatNo}\left(y+1\right)-2\right)\right)+\left(\mathrm{FermatNo}\left(y+1\right)-1\right)+1=\left(\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\mathrm{FermatNo}\left(y+1\right)-\left(\mathrm{FermatNo}\left(y+1\right)-2\right)\right)+\left(\mathrm{FermatNo}\left(y+1\right)-1\right)+1$$
62		elnn0uz	$$⊢y\in {\mathbb{N}}_0\leftrightarrow y\in {\mathbb{Z}}_{\ge 0}$$
63	62	biimpi	$$⊢y\in {\mathbb{N}}_0\to y\in {\mathbb{Z}}_{\ge 0}$$
64		elfznn0	$$⊢n\in \left(0\dots y+1\right)\to n\in {\mathbb{N}}_0$$
65	64 30	syl	$$⊢n\in \left(0\dots y+1\right)\to \mathrm{FermatNo}\left(n\right)\in ℂ$$
66	65	adantl	$$⊢\left(y\in {\mathbb{N}}_0\wedge n\in \left(0\dots y+1\right)\right)\to \mathrm{FermatNo}\left(n\right)\in ℂ$$
67		fveq2	$$⊢n=y+1\to \mathrm{FermatNo}\left(n\right)=\mathrm{FermatNo}\left(y+1\right)$$
68	63 66 67	fprodp1	$$⊢y\in {\mathbb{N}}_0\to \prod _{n=0}^{y+1}\mathrm{FermatNo}\left(n\right)=\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\mathrm{FermatNo}\left(y+1\right)$$
69	68	eqcomd	$$⊢y\in {\mathbb{N}}_0\to \prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\mathrm{FermatNo}\left(y+1\right)=\prod _{n=0}^{y+1}\mathrm{FermatNo}\left(n\right)$$
70	69	oveq1d	$$⊢y\in {\mathbb{N}}_0\to \prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\mathrm{FermatNo}\left(y+1\right)-\left(\mathrm{FermatNo}\left(y+1\right)-2\right)=\prod _{n=0}^{y+1}\mathrm{FermatNo}\left(n\right)-\left(\mathrm{FermatNo}\left(y+1\right)-2\right)$$
71		npcan1	$$⊢\mathrm{FermatNo}\left(y+1\right)\in ℂ\to \mathrm{FermatNo}\left(y+1\right)-1+1=\mathrm{FermatNo}\left(y+1\right)$$
72	42 71	syl	$$⊢y\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(y+1\right)-1+1=\mathrm{FermatNo}\left(y+1\right)$$
73	70 72	oveq12d	$$⊢y\in {\mathbb{N}}_0\to \left(\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\mathrm{FermatNo}\left(y+1\right)-\left(\mathrm{FermatNo}\left(y+1\right)-2\right)\right)+\left(\mathrm{FermatNo}\left(y+1\right)-1\right)+1=\prod _{n=0}^{y+1}\mathrm{FermatNo}\left(n\right)-\left(\mathrm{FermatNo}\left(y+1\right)-2\right)+\mathrm{FermatNo}\left(y+1\right)$$
74		fzfid	$$⊢y\in {\mathbb{N}}_0\to \left(0\dots y+1\right)\in \mathrm{Fin}$$
75	74 66	fprodcl	$$⊢y\in {\mathbb{N}}_0\to \prod _{n=0}^{y+1}\mathrm{FermatNo}\left(n\right)\in ℂ$$
76	75 59 42	subadd23d	$$⊢y\in {\mathbb{N}}_0\to \prod _{n=0}^{y+1}\mathrm{FermatNo}\left(n\right)-\left(\mathrm{FermatNo}\left(y+1\right)-2\right)+\mathrm{FermatNo}\left(y+1\right)=\prod _{n=0}^{y+1}\mathrm{FermatNo}\left(n\right)+\mathrm{FermatNo}\left(y+1\right)-\left(\mathrm{FermatNo}\left(y+1\right)-2\right)$$
77	73 76	eqtrd	$$⊢y\in {\mathbb{N}}_0\to \left(\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\mathrm{FermatNo}\left(y+1\right)-\left(\mathrm{FermatNo}\left(y+1\right)-2\right)\right)+\left(\mathrm{FermatNo}\left(y+1\right)-1\right)+1=\prod _{n=0}^{y+1}\mathrm{FermatNo}\left(n\right)+\mathrm{FermatNo}\left(y+1\right)-\left(\mathrm{FermatNo}\left(y+1\right)-2\right)$$
78	42 5	nncand	$$⊢y\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(y+1\right)-\left(\mathrm{FermatNo}\left(y+1\right)-2\right)=2$$
79	78	oveq2d	$$⊢y\in {\mathbb{N}}_0\to \prod _{n=0}^{y+1}\mathrm{FermatNo}\left(n\right)+\mathrm{FermatNo}\left(y+1\right)-\left(\mathrm{FermatNo}\left(y+1\right)-2\right)=\prod _{n=0}^{y+1}\mathrm{FermatNo}\left(n\right)+2$$
80	61 77 79	3eqtrd	$$⊢y\in {\mathbb{N}}_0\to \left(\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\mathrm{FermatNo}\left(y+1\right)-\left(\mathrm{FermatNo}\left(y+1\right)-2\right)\right)+\left(\mathrm{FermatNo}\left(y+1\right)-1\right)+1=\prod _{n=0}^{y+1}\mathrm{FermatNo}\left(n\right)+2$$
81	57 80	sylan9eqr	$$⊢\left(y\in {\mathbb{N}}_0\wedge \mathrm{FermatNo}\left(y+1\right)-2=\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\right)\to \left(\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\mathrm{FermatNo}\left(y+1\right)-\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\right)+\left(\mathrm{FermatNo}\left(y+1\right)-1\right)+1=\prod _{n=0}^{y+1}\mathrm{FermatNo}\left(n\right)+2$$
82	81	ex	$$⊢y\in {\mathbb{N}}_0\to \left(\mathrm{FermatNo}\left(y+1\right)-2=\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\to \left(\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\mathrm{FermatNo}\left(y+1\right)-\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\right)+\left(\mathrm{FermatNo}\left(y+1\right)-1\right)+1=\prod _{n=0}^{y+1}\mathrm{FermatNo}\left(n\right)+2\right)$$
83	53 82	sylbid	$$⊢y\in {\mathbb{N}}_0\to \left(\mathrm{FermatNo}\left(y+1\right)=\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+2\to \left(\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\mathrm{FermatNo}\left(y+1\right)-\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\right)+\left(\mathrm{FermatNo}\left(y+1\right)-1\right)+1=\prod _{n=0}^{y+1}\mathrm{FermatNo}\left(n\right)+2\right)$$
84	83	imp	$$⊢\left(y\in {\mathbb{N}}_0\wedge \mathrm{FermatNo}\left(y+1\right)=\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+2\right)\to \left(\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\mathrm{FermatNo}\left(y+1\right)-\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)\right)+\left(\mathrm{FermatNo}\left(y+1\right)-1\right)+1=\prod _{n=0}^{y+1}\mathrm{FermatNo}\left(n\right)+2$$
85	50 84	eqtrd	$$⊢\left(y\in {\mathbb{N}}_0\wedge \mathrm{FermatNo}\left(y+1\right)=\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+2\right)\to \left(\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+2-1\right)\left(\mathrm{FermatNo}\left(y+1\right)-1\right)+1=\prod _{n=0}^{y+1}\mathrm{FermatNo}\left(n\right)+2$$
86	22 26 85	3eqtrd	$$⊢\left(y\in {\mathbb{N}}_0\wedge \mathrm{FermatNo}\left(y+1\right)=\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+2\right)\to \mathrm{FermatNo}\left(y+1+1\right)=\prod _{n=0}^{y+1}\mathrm{FermatNo}\left(n\right)+2$$
87	86	ex	$$⊢y\in {\mathbb{N}}_0\to \left(\mathrm{FermatNo}\left(y+1\right)=\prod _{n=0}^y\mathrm{FermatNo}\left(n\right)+2\to \mathrm{FermatNo}\left(y+1+1\right)=\prod _{n=0}^{y+1}\mathrm{FermatNo}\left(n\right)+2\right)$$