Metamath Proof Explorer

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 mulid2d ⊢ ( 𝑦 ∈ ℕ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 ) ) )