Theorem fmtnorec2lem

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

	Ref	Expression
Assertion	fmtnorec2lem	⊢ ( 𝑦 ∈ ℕ0 → ( ( FermatNo ‘ ( 𝑦 + 1 ) ) = ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 2 ) → ( FermatNo ‘ ( ( 𝑦 + 1 ) + 1 ) ) = ( ∏ 𝑛 ∈ ( 0 ... ( 𝑦 + 1 ) ) ( FermatNo ‘ 𝑛 ) + 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		peano2nn0	⊢ ( 𝑦 ∈ ℕ0 → ( 𝑦 + 1 ) ∈ ℕ0 )
2		peano2nn0	⊢ ( ( 𝑦 + 1 ) ∈ ℕ0 → ( ( 𝑦 + 1 ) + 1 ) ∈ ℕ0 )
3		fmtno	⊢ ( ( ( 𝑦 + 1 ) + 1 ) ∈ ℕ0 → ( FermatNo ‘ ( ( 𝑦 + 1 ) + 1 ) ) = ( ( 2 ↑ ( 2 ↑ ( ( 𝑦 + 1 ) + 1 ) ) ) + 1 ) )
4	1 2 3	3syl	⊢ ( 𝑦 ∈ ℕ0 → ( FermatNo ‘ ( ( 𝑦 + 1 ) + 1 ) ) = ( ( 2 ↑ ( 2 ↑ ( ( 𝑦 + 1 ) + 1 ) ) ) + 1 ) )
5		2cnd	⊢ ( 𝑦 ∈ ℕ0 → 2 ∈ ℂ )
6	5 1	expp1d	⊢ ( 𝑦 ∈ ℕ0 → ( 2 ↑ ( ( 𝑦 + 1 ) + 1 ) ) = ( ( 2 ↑ ( 𝑦 + 1 ) ) · 2 ) )
7	6	oveq2d	⊢ ( 𝑦 ∈ ℕ0 → ( 2 ↑ ( 2 ↑ ( ( 𝑦 + 1 ) + 1 ) ) ) = ( 2 ↑ ( ( 2 ↑ ( 𝑦 + 1 ) ) · 2 ) ) )
8		2nn0	⊢ 2 ∈ ℕ0
9	8	a1i	⊢ ( 𝑦 ∈ ℕ0 → 2 ∈ ℕ0 )
10	9 1	nn0expcld	⊢ ( 𝑦 ∈ ℕ0 → ( 2 ↑ ( 𝑦 + 1 ) ) ∈ ℕ0 )
11	9 10	nn0expcld	⊢ ( 𝑦 ∈ ℕ0 → ( 2 ↑ ( 2 ↑ ( 𝑦 + 1 ) ) ) ∈ ℕ0 )
12	11	nn0cnd	⊢ ( 𝑦 ∈ ℕ0 → ( 2 ↑ ( 2 ↑ ( 𝑦 + 1 ) ) ) ∈ ℂ )
13	12	sqvald	⊢ ( 𝑦 ∈ ℕ0 → ( ( 2 ↑ ( 2 ↑ ( 𝑦 + 1 ) ) ) ↑ 2 ) = ( ( 2 ↑ ( 2 ↑ ( 𝑦 + 1 ) ) ) · ( 2 ↑ ( 2 ↑ ( 𝑦 + 1 ) ) ) ) )
14	5 9 10	expmuld	⊢ ( 𝑦 ∈ ℕ0 → ( 2 ↑ ( ( 2 ↑ ( 𝑦 + 1 ) ) · 2 ) ) = ( ( 2 ↑ ( 2 ↑ ( 𝑦 + 1 ) ) ) ↑ 2 ) )
15		fmtnom1nn	⊢ ( ( 𝑦 + 1 ) ∈ ℕ0 → ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) = ( 2 ↑ ( 2 ↑ ( 𝑦 + 1 ) ) ) )
16	1 15	syl	⊢ ( 𝑦 ∈ ℕ0 → ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) = ( 2 ↑ ( 2 ↑ ( 𝑦 + 1 ) ) ) )
17	16 16	oveq12d	⊢ ( 𝑦 ∈ ℕ0 → ( ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) · ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) = ( ( 2 ↑ ( 2 ↑ ( 𝑦 + 1 ) ) ) · ( 2 ↑ ( 2 ↑ ( 𝑦 + 1 ) ) ) ) )
18	13 14 17	3eqtr4d	⊢ ( 𝑦 ∈ ℕ0 → ( 2 ↑ ( ( 2 ↑ ( 𝑦 + 1 ) ) · 2 ) ) = ( ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) · ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) )
19	7 18	eqtrd	⊢ ( 𝑦 ∈ ℕ0 → ( 2 ↑ ( 2 ↑ ( ( 𝑦 + 1 ) + 1 ) ) ) = ( ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) · ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) )
20	19	oveq1d	⊢ ( 𝑦 ∈ ℕ0 → ( ( 2 ↑ ( 2 ↑ ( ( 𝑦 + 1 ) + 1 ) ) ) + 1 ) = ( ( ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) · ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) + 1 ) )
21	4 20	eqtrd	⊢ ( 𝑦 ∈ ℕ0 → ( FermatNo ‘ ( ( 𝑦 + 1 ) + 1 ) ) = ( ( ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) · ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) + 1 ) )
22	21	adantr	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( FermatNo ‘ ( 𝑦 + 1 ) ) = ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 2 ) ) → ( FermatNo ‘ ( ( 𝑦 + 1 ) + 1 ) ) = ( ( ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) · ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) + 1 ) )
23		oveq1	⊢ ( ( FermatNo ‘ ( 𝑦 + 1 ) ) = ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 2 ) → ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) = ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 2 ) − 1 ) )
24	23	oveq1d	⊢ ( ( FermatNo ‘ ( 𝑦 + 1 ) ) = ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 2 ) → ( ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) · ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) = ( ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 2 ) − 1 ) · ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) )
25	24	oveq1d	⊢ ( ( FermatNo ‘ ( 𝑦 + 1 ) ) = ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 2 ) → ( ( ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) · ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) + 1 ) = ( ( ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 2 ) − 1 ) · ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) + 1 ) )
26	25	adantl	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( FermatNo ‘ ( 𝑦 + 1 ) ) = ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 2 ) ) → ( ( ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) · ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) + 1 ) = ( ( ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 2 ) − 1 ) · ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) + 1 ) )
27		fzfid	⊢ ( 𝑦 ∈ ℕ0 → ( 0 ... 𝑦 ) ∈ Fin )
28		elfznn0	⊢ ( 𝑛 ∈ ( 0 ... 𝑦 ) → 𝑛 ∈ ℕ0 )
29		fmtnonn	⊢ ( 𝑛 ∈ ℕ0 → ( FermatNo ‘ 𝑛 ) ∈ ℕ )
30	29	nncnd	⊢ ( 𝑛 ∈ ℕ0 → ( FermatNo ‘ 𝑛 ) ∈ ℂ )
31	28 30	syl	⊢ ( 𝑛 ∈ ( 0 ... 𝑦 ) → ( FermatNo ‘ 𝑛 ) ∈ ℂ )
32	31	adantl	⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑛 ∈ ( 0 ... 𝑦 ) ) → ( FermatNo ‘ 𝑛 ) ∈ ℂ )
33	27 32	fprodcl	⊢ ( 𝑦 ∈ ℕ0 → ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) ∈ ℂ )
34		1cnd	⊢ ( 𝑦 ∈ ℕ0 → 1 ∈ ℂ )
35	33 5 34	addsubassd	⊢ ( 𝑦 ∈ ℕ0 → ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 2 ) − 1 ) = ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + ( 2 − 1 ) ) )
36		2m1e1	⊢ ( 2 − 1 ) = 1
37	36	oveq2i	⊢ ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + ( 2 − 1 ) ) = ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 1 )
38	35 37	eqtrdi	⊢ ( 𝑦 ∈ ℕ0 → ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 2 ) − 1 ) = ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 1 ) )
39	38	oveq1d	⊢ ( 𝑦 ∈ ℕ0 → ( ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 2 ) − 1 ) · ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) = ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 1 ) · ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) )
40		fmtnonn	⊢ ( ( 𝑦 + 1 ) ∈ ℕ0 → ( FermatNo ‘ ( 𝑦 + 1 ) ) ∈ ℕ )
41	1 40	syl	⊢ ( 𝑦 ∈ ℕ0 → ( FermatNo ‘ ( 𝑦 + 1 ) ) ∈ ℕ )
42	41	nncnd	⊢ ( 𝑦 ∈ ℕ0 → ( FermatNo ‘ ( 𝑦 + 1 ) ) ∈ ℂ )
43	42 34	subcld	⊢ ( 𝑦 ∈ ℕ0 → ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ∈ ℂ )
44	33 42	muls1d	⊢ ( 𝑦 ∈ ℕ0 → ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) · ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) = ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) · ( FermatNo ‘ ( 𝑦 + 1 ) ) ) − ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) ) )
45	43	mullidd	⊢ ( 𝑦 ∈ ℕ0 → ( 1 · ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) = ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) )
46	44 45	oveq12d	⊢ ( 𝑦 ∈ ℕ0 → ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) · ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) + ( 1 · ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) ) = ( ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) · ( FermatNo ‘ ( 𝑦 + 1 ) ) ) − ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) ) + ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) )
47	33 43 34 46	joinlmuladdmuld	⊢ ( 𝑦 ∈ ℕ0 → ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 1 ) · ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) = ( ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) · ( FermatNo ‘ ( 𝑦 + 1 ) ) ) − ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) ) + ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) )
48	39 47	eqtrd	⊢ ( 𝑦 ∈ ℕ0 → ( ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 2 ) − 1 ) · ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) = ( ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) · ( FermatNo ‘ ( 𝑦 + 1 ) ) ) − ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) ) + ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) )
49	48	adantr	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( FermatNo ‘ ( 𝑦 + 1 ) ) = ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 2 ) ) → ( ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 2 ) − 1 ) · ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) = ( ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) · ( FermatNo ‘ ( 𝑦 + 1 ) ) ) − ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) ) + ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) )
50	49	oveq1d	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( FermatNo ‘ ( 𝑦 + 1 ) ) = ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 2 ) ) → ( ( ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 2 ) − 1 ) · ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) + 1 ) = ( ( ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) · ( FermatNo ‘ ( 𝑦 + 1 ) ) ) − ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) ) + ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) + 1 ) )
51		eqcom	⊢ ( ( FermatNo ‘ ( 𝑦 + 1 ) ) = ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 2 ) ↔ ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 2 ) = ( FermatNo ‘ ( 𝑦 + 1 ) ) )
52	42 5 33	subadd2d	⊢ ( 𝑦 ∈ ℕ0 → ( ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 2 ) = ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) ↔ ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 2 ) = ( FermatNo ‘ ( 𝑦 + 1 ) ) ) )
53	51 52	bitr4id	⊢ ( 𝑦 ∈ ℕ0 → ( ( FermatNo ‘ ( 𝑦 + 1 ) ) = ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 2 ) ↔ ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 2 ) = ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) ) )
54		oveq2	⊢ ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) = ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 2 ) → ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) · ( FermatNo ‘ ( 𝑦 + 1 ) ) ) − ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) ) = ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) · ( FermatNo ‘ ( 𝑦 + 1 ) ) ) − ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 2 ) ) )
55	54	oveq1d	⊢ ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) = ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 2 ) → ( ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) · ( FermatNo ‘ ( 𝑦 + 1 ) ) ) − ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) ) + ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) = ( ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) · ( FermatNo ‘ ( 𝑦 + 1 ) ) ) − ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 2 ) ) + ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) )
56	55	oveq1d	⊢ ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) = ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 2 ) → ( ( ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) · ( FermatNo ‘ ( 𝑦 + 1 ) ) ) − ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) ) + ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) + 1 ) = ( ( ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) · ( FermatNo ‘ ( 𝑦 + 1 ) ) ) − ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 2 ) ) + ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) + 1 ) )
57	56	eqcoms	⊢ ( ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 2 ) = ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) → ( ( ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) · ( FermatNo ‘ ( 𝑦 + 1 ) ) ) − ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) ) + ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) + 1 ) = ( ( ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) · ( FermatNo ‘ ( 𝑦 + 1 ) ) ) − ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 2 ) ) + ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) + 1 ) )
58	33 42	mulcld	⊢ ( 𝑦 ∈ ℕ0 → ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) · ( FermatNo ‘ ( 𝑦 + 1 ) ) ) ∈ ℂ )
59	42 5	subcld	⊢ ( 𝑦 ∈ ℕ0 → ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 2 ) ∈ ℂ )
60	58 59	subcld	⊢ ( 𝑦 ∈ ℕ0 → ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) · ( FermatNo ‘ ( 𝑦 + 1 ) ) ) − ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 2 ) ) ∈ ℂ )
61	60 43 34	addassd	⊢ ( 𝑦 ∈ ℕ0 → ( ( ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) · ( FermatNo ‘ ( 𝑦 + 1 ) ) ) − ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 2 ) ) + ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) + 1 ) = ( ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) · ( FermatNo ‘ ( 𝑦 + 1 ) ) ) − ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 2 ) ) + ( ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) + 1 ) ) )
62		elnn0uz	⊢ ( 𝑦 ∈ ℕ0 ↔ 𝑦 ∈ ( ℤ≥ ‘ 0 ) )
63	62	biimpi	⊢ ( 𝑦 ∈ ℕ0 → 𝑦 ∈ ( ℤ≥ ‘ 0 ) )
64		elfznn0	⊢ ( 𝑛 ∈ ( 0 ... ( 𝑦 + 1 ) ) → 𝑛 ∈ ℕ0 )
65	64 30	syl	⊢ ( 𝑛 ∈ ( 0 ... ( 𝑦 + 1 ) ) → ( FermatNo ‘ 𝑛 ) ∈ ℂ )
66	65	adantl	⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑛 ∈ ( 0 ... ( 𝑦 + 1 ) ) ) → ( FermatNo ‘ 𝑛 ) ∈ ℂ )
67		fveq2	⊢ ( 𝑛 = ( 𝑦 + 1 ) → ( FermatNo ‘ 𝑛 ) = ( FermatNo ‘ ( 𝑦 + 1 ) ) )
68	63 66 67	fprodp1	⊢ ( 𝑦 ∈ ℕ0 → ∏ 𝑛 ∈ ( 0 ... ( 𝑦 + 1 ) ) ( FermatNo ‘ 𝑛 ) = ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) · ( FermatNo ‘ ( 𝑦 + 1 ) ) ) )
69	68	eqcomd	⊢ ( 𝑦 ∈ ℕ0 → ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) · ( FermatNo ‘ ( 𝑦 + 1 ) ) ) = ∏ 𝑛 ∈ ( 0 ... ( 𝑦 + 1 ) ) ( FermatNo ‘ 𝑛 ) )
70	69	oveq1d	⊢ ( 𝑦 ∈ ℕ0 → ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) · ( FermatNo ‘ ( 𝑦 + 1 ) ) ) − ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 2 ) ) = ( ∏ 𝑛 ∈ ( 0 ... ( 𝑦 + 1 ) ) ( FermatNo ‘ 𝑛 ) − ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 2 ) ) )
71		npcan1	⊢ ( ( FermatNo ‘ ( 𝑦 + 1 ) ) ∈ ℂ → ( ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) + 1 ) = ( FermatNo ‘ ( 𝑦 + 1 ) ) )
72	42 71	syl	⊢ ( 𝑦 ∈ ℕ0 → ( ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) + 1 ) = ( FermatNo ‘ ( 𝑦 + 1 ) ) )
73	70 72	oveq12d	⊢ ( 𝑦 ∈ ℕ0 → ( ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) · ( FermatNo ‘ ( 𝑦 + 1 ) ) ) − ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 2 ) ) + ( ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) + 1 ) ) = ( ( ∏ 𝑛 ∈ ( 0 ... ( 𝑦 + 1 ) ) ( FermatNo ‘ 𝑛 ) − ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 2 ) ) + ( FermatNo ‘ ( 𝑦 + 1 ) ) ) )
74		fzfid	⊢ ( 𝑦 ∈ ℕ0 → ( 0 ... ( 𝑦 + 1 ) ) ∈ Fin )
75	74 66	fprodcl	⊢ ( 𝑦 ∈ ℕ0 → ∏ 𝑛 ∈ ( 0 ... ( 𝑦 + 1 ) ) ( FermatNo ‘ 𝑛 ) ∈ ℂ )
76	75 59 42	subadd23d	⊢ ( 𝑦 ∈ ℕ0 → ( ( ∏ 𝑛 ∈ ( 0 ... ( 𝑦 + 1 ) ) ( FermatNo ‘ 𝑛 ) − ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 2 ) ) + ( FermatNo ‘ ( 𝑦 + 1 ) ) ) = ( ∏ 𝑛 ∈ ( 0 ... ( 𝑦 + 1 ) ) ( FermatNo ‘ 𝑛 ) + ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 2 ) ) ) )
77	73 76	eqtrd	⊢ ( 𝑦 ∈ ℕ0 → ( ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) · ( FermatNo ‘ ( 𝑦 + 1 ) ) ) − ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 2 ) ) + ( ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) + 1 ) ) = ( ∏ 𝑛 ∈ ( 0 ... ( 𝑦 + 1 ) ) ( FermatNo ‘ 𝑛 ) + ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 2 ) ) ) )
78	42 5	nncand	⊢ ( 𝑦 ∈ ℕ0 → ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 2 ) ) = 2 )
79	78	oveq2d	⊢ ( 𝑦 ∈ ℕ0 → ( ∏ 𝑛 ∈ ( 0 ... ( 𝑦 + 1 ) ) ( FermatNo ‘ 𝑛 ) + ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 2 ) ) ) = ( ∏ 𝑛 ∈ ( 0 ... ( 𝑦 + 1 ) ) ( FermatNo ‘ 𝑛 ) + 2 ) )
80	61 77 79	3eqtrd	⊢ ( 𝑦 ∈ ℕ0 → ( ( ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) · ( FermatNo ‘ ( 𝑦 + 1 ) ) ) − ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 2 ) ) + ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) + 1 ) = ( ∏ 𝑛 ∈ ( 0 ... ( 𝑦 + 1 ) ) ( FermatNo ‘ 𝑛 ) + 2 ) )
81	57 80	sylan9eqr	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 2 ) = ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) ) → ( ( ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) · ( FermatNo ‘ ( 𝑦 + 1 ) ) ) − ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) ) + ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) + 1 ) = ( ∏ 𝑛 ∈ ( 0 ... ( 𝑦 + 1 ) ) ( FermatNo ‘ 𝑛 ) + 2 ) )
82	81	ex	⊢ ( 𝑦 ∈ ℕ0 → ( ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 2 ) = ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) → ( ( ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) · ( FermatNo ‘ ( 𝑦 + 1 ) ) ) − ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) ) + ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) + 1 ) = ( ∏ 𝑛 ∈ ( 0 ... ( 𝑦 + 1 ) ) ( FermatNo ‘ 𝑛 ) + 2 ) ) )
83	53 82	sylbid	⊢ ( 𝑦 ∈ ℕ0 → ( ( FermatNo ‘ ( 𝑦 + 1 ) ) = ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 2 ) → ( ( ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) · ( FermatNo ‘ ( 𝑦 + 1 ) ) ) − ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) ) + ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) + 1 ) = ( ∏ 𝑛 ∈ ( 0 ... ( 𝑦 + 1 ) ) ( FermatNo ‘ 𝑛 ) + 2 ) ) )
84	83	imp	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( FermatNo ‘ ( 𝑦 + 1 ) ) = ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 2 ) ) → ( ( ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) · ( FermatNo ‘ ( 𝑦 + 1 ) ) ) − ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) ) + ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) + 1 ) = ( ∏ 𝑛 ∈ ( 0 ... ( 𝑦 + 1 ) ) ( FermatNo ‘ 𝑛 ) + 2 ) )
85	50 84	eqtrd	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( FermatNo ‘ ( 𝑦 + 1 ) ) = ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 2 ) ) → ( ( ( ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 2 ) − 1 ) · ( ( FermatNo ‘ ( 𝑦 + 1 ) ) − 1 ) ) + 1 ) = ( ∏ 𝑛 ∈ ( 0 ... ( 𝑦 + 1 ) ) ( FermatNo ‘ 𝑛 ) + 2 ) )
86	22 26 85	3eqtrd	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( FermatNo ‘ ( 𝑦 + 1 ) ) = ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 2 ) ) → ( FermatNo ‘ ( ( 𝑦 + 1 ) + 1 ) ) = ( ∏ 𝑛 ∈ ( 0 ... ( 𝑦 + 1 ) ) ( FermatNo ‘ 𝑛 ) + 2 ) )
87	86	ex	⊢ ( 𝑦 ∈ ℕ0 → ( ( FermatNo ‘ ( 𝑦 + 1 ) ) = ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 2 ) → ( FermatNo ‘ ( ( 𝑦 + 1 ) + 1 ) ) = ( ∏ 𝑛 ∈ ( 0 ... ( 𝑦 + 1 ) ) ( FermatNo ‘ 𝑛 ) + 2 ) ) )