Metamath Proof Explorer

Theorem fmtnorec4

Description: The fourth recurrence relation for Fermat numbers, see Wikipedia "Fermat number", 31-Jul-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties . (Contributed by AV, 31-Jul-2021)

Ref Expression
Assertion fmtnorec4 ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( FermatNo ‘ 𝑁 ) = ( ( ( FermatNo ‘ ( 𝑁 − 1 ) ) ↑ 2 ) − ( 2 · ( ( ( FermatNo ‘ ( 𝑁 − 2 ) ) − 1 ) ↑ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 eluz2nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℕ )
2 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
3 1 2 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 − 1 ) ∈ ℕ0 )
4 fmtno ⊢ ( ( 𝑁 − 1 ) ∈ ℕ0 → ( FermatNo ‘ ( 𝑁 − 1 ) ) = ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) + 1 ) )
5 3 4 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( FermatNo ‘ ( 𝑁 − 1 ) ) = ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) + 1 ) )
6 5 oveq1d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( FermatNo ‘ ( 𝑁 − 1 ) ) ↑ 2 ) = ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) + 1 ) ↑ 2 ) )
7 2nn ⊢ 2 ∈ ℕ
8 7 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ∈ ℕ )
9 2nn0 ⊢ 2 ∈ ℕ0
10 9 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ∈ ℕ0 )
11 10 3 nn0expcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( 𝑁 − 1 ) ) ∈ ℕ0 )
12 8 11 nnexpcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ∈ ℕ )
13 12 nncnd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ∈ ℂ )
14 binom21 ⊢ ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ∈ ℂ → ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) + 1 ) ↑ 2 ) = ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ↑ 2 ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) ) + 1 ) )
15 13 14 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) + 1 ) ↑ 2 ) = ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ↑ 2 ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) ) + 1 ) )
16 2cn ⊢ 2 ∈ ℂ
17 16 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ∈ ℂ )
18 17 10 11 expmuld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( ( 2 ↑ ( 𝑁 − 1 ) ) · 2 ) ) = ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ↑ 2 ) )
19 17 3 expp1d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( ( 𝑁 − 1 ) + 1 ) ) = ( ( 2 ↑ ( 𝑁 − 1 ) ) · 2 ) )
20 1 nncnd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℂ )
21 npcan1 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
22 20 21 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
23 22 oveq2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( ( 𝑁 − 1 ) + 1 ) ) = ( 2 ↑ 𝑁 ) )
24 19 23 eqtr3d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 ↑ ( 𝑁 − 1 ) ) · 2 ) = ( 2 ↑ 𝑁 ) )
25 24 oveq2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( ( 2 ↑ ( 𝑁 − 1 ) ) · 2 ) ) = ( 2 ↑ ( 2 ↑ 𝑁 ) ) )
26 18 25 eqtr3d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ↑ 2 ) = ( 2 ↑ ( 2 ↑ 𝑁 ) ) )
27 26 oveq1d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ↑ 2 ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) ) = ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) ) )
28 27 oveq1d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ↑ 2 ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) ) + 1 ) = ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) ) + 1 ) )
29 6 15 28 3eqtrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( FermatNo ‘ ( 𝑁 − 1 ) ) ↑ 2 ) = ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) ) + 1 ) )
30 uznn0sub ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 − 2 ) ∈ ℕ0 )
31 fmtno ⊢ ( ( 𝑁 − 2 ) ∈ ℕ0 → ( FermatNo ‘ ( 𝑁 − 2 ) ) = ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) )
32 30 31 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( FermatNo ‘ ( 𝑁 − 2 ) ) = ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) )
33 32 oveq1d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( FermatNo ‘ ( 𝑁 − 2 ) ) − 1 ) = ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) − 1 ) )
34 33 oveq1d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( FermatNo ‘ ( 𝑁 − 2 ) ) − 1 ) ↑ 2 ) = ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) − 1 ) ↑ 2 ) )
35 10 30 nn0expcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( 𝑁 − 2 ) ) ∈ ℕ0 )
36 8 35 nnexpcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ∈ ℕ )
37 36 nncnd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ∈ ℂ )
38 peano2cn ⊢ ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ∈ ℂ → ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ∈ ℂ )
39 37 38 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ∈ ℂ )
40 binom2sub1 ⊢ ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ∈ ℂ → ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) − 1 ) ↑ 2 ) = ( ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ↑ 2 ) − ( 2 · ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ) ) + 1 ) )
41 39 40 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) − 1 ) ↑ 2 ) = ( ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ↑ 2 ) − ( 2 · ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ) ) + 1 ) )
42 binom21 ⊢ ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ∈ ℂ → ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ↑ 2 ) = ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 1 ) )
43 37 42 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ↑ 2 ) = ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 1 ) )
44 43 oveq1d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ↑ 2 ) − ( 2 · ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ) ) = ( ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 1 ) − ( 2 · ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ) ) )
45 44 oveq1d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ↑ 2 ) − ( 2 · ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ) ) + 1 ) = ( ( ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 1 ) − ( 2 · ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ) ) + 1 ) )
46 34 41 45 3eqtrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( FermatNo ‘ ( 𝑁 − 2 ) ) − 1 ) ↑ 2 ) = ( ( ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 1 ) − ( 2 · ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ) ) + 1 ) )
47 46 oveq2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · ( ( ( FermatNo ‘ ( 𝑁 − 2 ) ) − 1 ) ↑ 2 ) ) = ( 2 · ( ( ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 1 ) − ( 2 · ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ) ) + 1 ) ) )
48 29 47 oveq12d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( FermatNo ‘ ( 𝑁 − 1 ) ) ↑ 2 ) − ( 2 · ( ( ( FermatNo ‘ ( 𝑁 − 2 ) ) − 1 ) ↑ 2 ) ) ) = ( ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) ) + 1 ) − ( 2 · ( ( ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 1 ) − ( 2 · ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ) ) + 1 ) ) ) )
49 36 10 nnexpcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) ∈ ℕ )
50 49 nncnd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) ∈ ℂ )
51 17 37 mulcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ∈ ℂ )
52 50 51 addcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) ∈ ℂ )
53 peano2cn ⊢ ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) ∈ ℂ → ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 1 ) ∈ ℂ )
54 52 53 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 1 ) ∈ ℂ )
55 17 39 mulcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ) ∈ ℂ )
56 54 55 subcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 1 ) − ( 2 · ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ) ) ∈ ℂ )
57 1cnd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 1 ∈ ℂ )
58 17 56 57 adddid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · ( ( ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 1 ) − ( 2 · ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ) ) + 1 ) ) = ( ( 2 · ( ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 1 ) − ( 2 · ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ) ) ) + ( 2 · 1 ) ) )
59 52 57 addcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 1 ) ∈ ℂ )
60 17 59 55 subdid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · ( ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 1 ) − ( 2 · ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ) ) ) = ( ( 2 · ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 1 ) ) − ( 2 · ( 2 · ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ) ) ) )
61 17 52 57 adddid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 1 ) ) = ( ( 2 · ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) ) + ( 2 · 1 ) ) )
62 17 50 51 adddid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) ) = ( ( 2 · ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) ) + ( 2 · ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) ) )
63 17 10 35 expmuld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( ( 2 ↑ ( 𝑁 − 2 ) ) · 2 ) ) = ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) )
64 17 30 expp1d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( ( 𝑁 − 2 ) + 1 ) ) = ( ( 2 ↑ ( 𝑁 − 2 ) ) · 2 ) )
65 20 17 57 subsubd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 − ( 2 − 1 ) ) = ( ( 𝑁 − 2 ) + 1 ) )
66 65 eqcomd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑁 − 2 ) + 1 ) = ( 𝑁 − ( 2 − 1 ) ) )
67 66 oveq2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( ( 𝑁 − 2 ) + 1 ) ) = ( 2 ↑ ( 𝑁 − ( 2 − 1 ) ) ) )
68 64 67 eqtr3d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 ↑ ( 𝑁 − 2 ) ) · 2 ) = ( 2 ↑ ( 𝑁 − ( 2 − 1 ) ) ) )
69 68 oveq2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( ( 2 ↑ ( 𝑁 − 2 ) ) · 2 ) ) = ( 2 ↑ ( 2 ↑ ( 𝑁 − ( 2 − 1 ) ) ) ) )
70 63 69 eqtr3d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) = ( 2 ↑ ( 2 ↑ ( 𝑁 − ( 2 − 1 ) ) ) ) )
71 70 oveq2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) ) = ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − ( 2 − 1 ) ) ) ) ) )
72 2m1e1 ⊢ ( 2 − 1 ) = 1
73 72 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 − 1 ) = 1 )
74 73 oveq2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 − ( 2 − 1 ) ) = ( 𝑁 − 1 ) )
75 74 oveq2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( 𝑁 − ( 2 − 1 ) ) ) = ( 2 ↑ ( 𝑁 − 1 ) ) )
76 75 oveq2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( 2 ↑ ( 𝑁 − ( 2 − 1 ) ) ) ) = ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) )
77 76 oveq2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − ( 2 − 1 ) ) ) ) ) = ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) )
78 71 77 eqtrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) ) = ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) )
79 17 17 37 mulassd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) = ( 2 · ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) )
80 79 eqcomd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) = ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) )
81 78 80 oveq12d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 · ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) ) + ( 2 · ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) ) = ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) )
82 62 81 eqtrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) ) = ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) )
83 2t1e2 ⊢ ( 2 · 1 ) = 2
84 83 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · 1 ) = 2 )
85 82 84 oveq12d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 · ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) ) + ( 2 · 1 ) ) = ( ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 2 ) )
86 61 85 eqtrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 1 ) ) = ( ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 2 ) )
87 17 37 57 adddid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ) = ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) + ( 2 · 1 ) ) )
88 84 oveq2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) + ( 2 · 1 ) ) = ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) + 2 ) )
89 87 88 eqtrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ) = ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) + 2 ) )
90 89 oveq2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · ( 2 · ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ) ) = ( 2 · ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) + 2 ) ) )
91 17 51 17 adddid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) + 2 ) ) = ( ( 2 · ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + ( 2 · 2 ) ) )
92 2t2e4 ⊢ ( 2 · 2 ) = 4
93 92 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · 2 ) = 4 )
94 80 93 oveq12d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 · ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + ( 2 · 2 ) ) = ( ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) + 4 ) )
95 90 91 94 3eqtrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · ( 2 · ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ) ) = ( ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) + 4 ) )
96 86 95 oveq12d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 · ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 1 ) ) − ( 2 · ( 2 · ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ) ) ) = ( ( ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 2 ) − ( ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) + 4 ) ) )
97 60 96 eqtrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · ( ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 1 ) − ( 2 · ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ) ) ) = ( ( ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 2 ) − ( ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) + 4 ) ) )
98 97 84 oveq12d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 · ( ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 1 ) − ( 2 · ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ) ) ) + ( 2 · 1 ) ) = ( ( ( ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 2 ) − ( ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) + 4 ) ) + 2 ) )
99 58 98 eqtrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · ( ( ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 1 ) − ( 2 · ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ) ) + 1 ) ) = ( ( ( ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 2 ) − ( ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) + 4 ) ) + 2 ) )
100 99 oveq2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) ) + 1 ) − ( 2 · ( ( ( ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ↑ 2 ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 1 ) − ( 2 · ( ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) + 1 ) ) ) + 1 ) ) ) = ( ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) ) + 1 ) − ( ( ( ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 2 ) − ( ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) + 4 ) ) + 2 ) ) )
101 17 13 mulcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) ∈ ℂ )
102 16 16 mulcli ⊢ ( 2 · 2 ) ∈ ℂ
103 102 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · 2 ) ∈ ℂ )
104 103 37 mulcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ∈ ℂ )
105 101 104 addcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) ∈ ℂ )
106 105 17 addcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 2 ) ∈ ℂ )
107 4cn ⊢ 4 ∈ ℂ
108 107 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 4 ∈ ℂ )
109 104 108 addcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) + 4 ) ∈ ℂ )
110 105 17 17 addassd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 2 ) + 2 ) = ( ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + ( 2 + 2 ) ) )
111 2p2e4 ⊢ ( 2 + 2 ) = 4
112 111 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 + 2 ) = 4 )
113 112 oveq2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + ( 2 + 2 ) ) = ( ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 4 ) )
114 101 104 108 addassd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 4 ) = ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) + 4 ) ) )
115 110 113 114 3eqtrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 2 ) + 2 ) = ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) + 4 ) ) )
116 106 17 101 109 115 subaddeqd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 2 ) − ( ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) + 4 ) ) = ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) − 2 ) )
117 116 eqcomd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) − 2 ) = ( ( ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 2 ) − ( ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) + 4 ) ) )
118 106 109 subcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 2 ) − ( ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) + 4 ) ) ∈ ℂ )
119 101 17 118 subadd2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) − 2 ) = ( ( ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 2 ) − ( ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) + 4 ) ) ↔ ( ( ( ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 2 ) − ( ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) + 4 ) ) + 2 ) = ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) ) )
120 117 119 mpbid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 2 ) − ( ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) + 4 ) ) + 2 ) = ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) )
121 120 oveq2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + ( ( ( ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 2 ) − ( ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) + 4 ) ) + 2 ) ) = ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) ) )
122 eluzge2nn0 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℕ0 )
123 10 122 nn0expcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ 𝑁 ) ∈ ℕ0 )
124 8 123 nnexpcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( 2 ↑ 𝑁 ) ) ∈ ℕ )
125 124 nncnd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( 2 ↑ 𝑁 ) ) ∈ ℂ )
126 125 101 addcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) ) ∈ ℂ )
127 118 17 addcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 2 ) − ( ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) + 4 ) ) + 2 ) ∈ ℂ )
128 126 127 125 subadd2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) ) − ( ( ( ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 2 ) − ( ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) + 4 ) ) + 2 ) ) = ( 2 ↑ ( 2 ↑ 𝑁 ) ) ↔ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + ( ( ( ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 2 ) − ( ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) + 4 ) ) + 2 ) ) = ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) ) ) )
129 121 128 mpbird ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) ) − ( ( ( ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 2 ) − ( ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) + 4 ) ) + 2 ) ) = ( 2 ↑ ( 2 ↑ 𝑁 ) ) )
130 129 oveq1d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) ) − ( ( ( ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 2 ) − ( ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) + 4 ) ) + 2 ) ) + 1 ) = ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) )
131 126 57 127 addsubd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) ) + 1 ) − ( ( ( ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 2 ) − ( ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) + 4 ) ) + 2 ) ) = ( ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) ) − ( ( ( ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 2 ) − ( ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) + 4 ) ) + 2 ) ) + 1 ) )
132 fmtno ⊢ ( 𝑁 ∈ ℕ0 → ( FermatNo ‘ 𝑁 ) = ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) )
133 122 132 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( FermatNo ‘ 𝑁 ) = ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) )
134 130 131 133 3eqtr4d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) ) + 1 ) − ( ( ( ( ( 2 · ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) ) + ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) ) + 2 ) − ( ( ( 2 · 2 ) · ( 2 ↑ ( 2 ↑ ( 𝑁 − 2 ) ) ) ) + 4 ) ) + 2 ) ) = ( FermatNo ‘ 𝑁 ) )
135 48 100 134 3eqtrrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( FermatNo ‘ 𝑁 ) = ( ( ( FermatNo ‘ ( 𝑁 − 1 ) ) ↑ 2 ) − ( 2 · ( ( ( FermatNo ‘ ( 𝑁 − 2 ) ) − 1 ) ↑ 2 ) ) ) )