Metamath Proof Explorer

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 ‘ 𝑛 ) ) ) )