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	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( FermatNo ‘ 𝑁 ) = ( ( FermatNo ‘ ( 𝑁 − 1 ) ) + ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) · ∏ 𝑛 ∈ ( 0 ... ( 𝑁 − 2 ) ) ( FermatNo ‘ 𝑛 ) ) ) )

Proof

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