Metamath Proof Explorer

Theorem goldpolyfactor

Description: Factorization of a polynomial which has golden ratio among its roots, done by term-by-term-by-term multiplying and summing a few shorter polynomials. (Contributed by Ender Ting, 24-Jul-2026)

Ref Expression
Hypothesis goldpolyfactor.1 ⊢ 𝐹 ∈ ℂ
Assertion goldpolyfactor ( ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) · ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) ) · ( 𝐹 + 2 ) ) = ( ( ( ( 𝐹 ↑ 5 ) − ( 5 · ( 𝐹 ↑ 3 ) ) ) + ( 5 · 𝐹 ) ) + 2 )

Proof

Step Hyp Ref Expression
1 goldpolyfactor.1 ⊢ 𝐹 ∈ ℂ
2 1 sqcli ⊢ ( 𝐹 ↑ 2 ) ∈ ℂ
3 2 1 subcli ⊢ ( ( 𝐹 ↑ 2 ) − 𝐹 ) ∈ ℂ
4 ax-1cn ⊢ 1 ∈ ℂ
5 3 4 subcli ⊢ ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) ∈ ℂ
6 5 3 4 subdii ⊢ ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) · ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) ) = ( ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) · ( ( 𝐹 ↑ 2 ) − 𝐹 ) ) − ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) · 1 ) )
7 5 2 1 subdii ⊢ ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) · ( ( 𝐹 ↑ 2 ) − 𝐹 ) ) = ( ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) · ( 𝐹 ↑ 2 ) ) − ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) · 𝐹 ) )
8 3 4 2 subdiri ⊢ ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) · ( 𝐹 ↑ 2 ) ) = ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) · ( 𝐹 ↑ 2 ) ) − ( 1 · ( 𝐹 ↑ 2 ) ) )
9 2 1 2 subdiri ⊢ ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) · ( 𝐹 ↑ 2 ) ) = ( ( ( 𝐹 ↑ 2 ) · ( 𝐹 ↑ 2 ) ) − ( 𝐹 · ( 𝐹 ↑ 2 ) ) )
10 2nn0 ⊢ 2 ∈ ℕ0
11 expadd ⊢ ( ( 𝐹 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) → ( 𝐹 ↑ ( 2 + 2 ) ) = ( ( 𝐹 ↑ 2 ) · ( 𝐹 ↑ 2 ) ) )
12 1 10 10 11 mp3an ⊢ ( 𝐹 ↑ ( 2 + 2 ) ) = ( ( 𝐹 ↑ 2 ) · ( 𝐹 ↑ 2 ) )
13 2p2e4 ⊢ ( 2 + 2 ) = 4
14 13 oveq2i ⊢ ( 𝐹 ↑ ( 2 + 2 ) ) = ( 𝐹 ↑ 4 )
15 12 14 eqtr3i ⊢ ( ( 𝐹 ↑ 2 ) · ( 𝐹 ↑ 2 ) ) = ( 𝐹 ↑ 4 )
16 1 2 mulcomi ⊢ ( 𝐹 · ( 𝐹 ↑ 2 ) ) = ( ( 𝐹 ↑ 2 ) · 𝐹 )
17 df-3 ⊢ 3 = ( 2 + 1 )
18 17 oveq2i ⊢ ( 𝐹 ↑ 3 ) = ( 𝐹 ↑ ( 2 + 1 ) )
19 expp1 ⊢ ( ( 𝐹 ∈ ℂ ∧ 2 ∈ ℕ0 ) → ( 𝐹 ↑ ( 2 + 1 ) ) = ( ( 𝐹 ↑ 2 ) · 𝐹 ) )
20 1 10 19 mp2an ⊢ ( 𝐹 ↑ ( 2 + 1 ) ) = ( ( 𝐹 ↑ 2 ) · 𝐹 )
21 18 20 eqtr2i ⊢ ( ( 𝐹 ↑ 2 ) · 𝐹 ) = ( 𝐹 ↑ 3 )
22 16 21 eqtri ⊢ ( 𝐹 · ( 𝐹 ↑ 2 ) ) = ( 𝐹 ↑ 3 )
23 15 22 oveq12i ⊢ ( ( ( 𝐹 ↑ 2 ) · ( 𝐹 ↑ 2 ) ) − ( 𝐹 · ( 𝐹 ↑ 2 ) ) ) = ( ( 𝐹 ↑ 4 ) − ( 𝐹 ↑ 3 ) )
24 9 23 eqtri ⊢ ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) · ( 𝐹 ↑ 2 ) ) = ( ( 𝐹 ↑ 4 ) − ( 𝐹 ↑ 3 ) )
25 2 mullidi ⊢ ( 1 · ( 𝐹 ↑ 2 ) ) = ( 𝐹 ↑ 2 )
26 24 25 oveq12i ⊢ ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) · ( 𝐹 ↑ 2 ) ) − ( 1 · ( 𝐹 ↑ 2 ) ) ) = ( ( ( 𝐹 ↑ 4 ) − ( 𝐹 ↑ 3 ) ) − ( 𝐹 ↑ 2 ) )
27 8 26 eqtri ⊢ ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) · ( 𝐹 ↑ 2 ) ) = ( ( ( 𝐹 ↑ 4 ) − ( 𝐹 ↑ 3 ) ) − ( 𝐹 ↑ 2 ) )
28 3 4 1 subdiri ⊢ ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) · 𝐹 ) = ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) · 𝐹 ) − ( 1 · 𝐹 ) )
29 2 1 1 subdiri ⊢ ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) · 𝐹 ) = ( ( ( 𝐹 ↑ 2 ) · 𝐹 ) − ( 𝐹 · 𝐹 ) )
30 1 sqvali ⊢ ( 𝐹 ↑ 2 ) = ( 𝐹 · 𝐹 )
31 30 eqcomi ⊢ ( 𝐹 · 𝐹 ) = ( 𝐹 ↑ 2 )
32 21 31 oveq12i ⊢ ( ( ( 𝐹 ↑ 2 ) · 𝐹 ) − ( 𝐹 · 𝐹 ) ) = ( ( 𝐹 ↑ 3 ) − ( 𝐹 ↑ 2 ) )
33 29 32 eqtri ⊢ ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) · 𝐹 ) = ( ( 𝐹 ↑ 3 ) − ( 𝐹 ↑ 2 ) )
34 1 mullidi ⊢ ( 1 · 𝐹 ) = 𝐹
35 33 34 oveq12i ⊢ ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) · 𝐹 ) − ( 1 · 𝐹 ) ) = ( ( ( 𝐹 ↑ 3 ) − ( 𝐹 ↑ 2 ) ) − 𝐹 )
36 28 35 eqtri ⊢ ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) · 𝐹 ) = ( ( ( 𝐹 ↑ 3 ) − ( 𝐹 ↑ 2 ) ) − 𝐹 )
37 27 36 oveq12i ⊢ ( ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) · ( 𝐹 ↑ 2 ) ) − ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) · 𝐹 ) ) = ( ( ( ( 𝐹 ↑ 4 ) − ( 𝐹 ↑ 3 ) ) − ( 𝐹 ↑ 2 ) ) − ( ( ( 𝐹 ↑ 3 ) − ( 𝐹 ↑ 2 ) ) − 𝐹 ) )
38 4nn0 ⊢ 4 ∈ ℕ0
39 expcl ⊢ ( ( 𝐹 ∈ ℂ ∧ 4 ∈ ℕ0 ) → ( 𝐹 ↑ 4 ) ∈ ℂ )
40 1 38 39 mp2an ⊢ ( 𝐹 ↑ 4 ) ∈ ℂ
41 3nn0 ⊢ 3 ∈ ℕ0
42 expcl ⊢ ( ( 𝐹 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝐹 ↑ 3 ) ∈ ℂ )
43 1 41 42 mp2an ⊢ ( 𝐹 ↑ 3 ) ∈ ℂ
44 40 43 subcli ⊢ ( ( 𝐹 ↑ 4 ) − ( 𝐹 ↑ 3 ) ) ∈ ℂ
45 44 2 subcli ⊢ ( ( ( 𝐹 ↑ 4 ) − ( 𝐹 ↑ 3 ) ) − ( 𝐹 ↑ 2 ) ) ∈ ℂ
46 43 2 subcli ⊢ ( ( 𝐹 ↑ 3 ) − ( 𝐹 ↑ 2 ) ) ∈ ℂ
47 subsub ⊢ ( ( ( ( ( 𝐹 ↑ 4 ) − ( 𝐹 ↑ 3 ) ) − ( 𝐹 ↑ 2 ) ) ∈ ℂ ∧ ( ( 𝐹 ↑ 3 ) − ( 𝐹 ↑ 2 ) ) ∈ ℂ ∧ 𝐹 ∈ ℂ ) → ( ( ( ( 𝐹 ↑ 4 ) − ( 𝐹 ↑ 3 ) ) − ( 𝐹 ↑ 2 ) ) − ( ( ( 𝐹 ↑ 3 ) − ( 𝐹 ↑ 2 ) ) − 𝐹 ) ) = ( ( ( ( ( 𝐹 ↑ 4 ) − ( 𝐹 ↑ 3 ) ) − ( 𝐹 ↑ 2 ) ) − ( ( 𝐹 ↑ 3 ) − ( 𝐹 ↑ 2 ) ) ) + 𝐹 ) )
48 45 46 1 47 mp3an ⊢ ( ( ( ( 𝐹 ↑ 4 ) − ( 𝐹 ↑ 3 ) ) − ( 𝐹 ↑ 2 ) ) − ( ( ( 𝐹 ↑ 3 ) − ( 𝐹 ↑ 2 ) ) − 𝐹 ) ) = ( ( ( ( ( 𝐹 ↑ 4 ) − ( 𝐹 ↑ 3 ) ) − ( 𝐹 ↑ 2 ) ) − ( ( 𝐹 ↑ 3 ) − ( 𝐹 ↑ 2 ) ) ) + 𝐹 )
49 nnncan2 ⊢ ( ( ( ( 𝐹 ↑ 4 ) − ( 𝐹 ↑ 3 ) ) ∈ ℂ ∧ ( 𝐹 ↑ 3 ) ∈ ℂ ∧ ( 𝐹 ↑ 2 ) ∈ ℂ ) → ( ( ( ( 𝐹 ↑ 4 ) − ( 𝐹 ↑ 3 ) ) − ( 𝐹 ↑ 2 ) ) − ( ( 𝐹 ↑ 3 ) − ( 𝐹 ↑ 2 ) ) ) = ( ( ( 𝐹 ↑ 4 ) − ( 𝐹 ↑ 3 ) ) − ( 𝐹 ↑ 3 ) ) )
50 44 43 2 49 mp3an ⊢ ( ( ( ( 𝐹 ↑ 4 ) − ( 𝐹 ↑ 3 ) ) − ( 𝐹 ↑ 2 ) ) − ( ( 𝐹 ↑ 3 ) − ( 𝐹 ↑ 2 ) ) ) = ( ( ( 𝐹 ↑ 4 ) − ( 𝐹 ↑ 3 ) ) − ( 𝐹 ↑ 3 ) )
51 subsub4 ⊢ ( ( ( 𝐹 ↑ 4 ) ∈ ℂ ∧ ( 𝐹 ↑ 3 ) ∈ ℂ ∧ ( 𝐹 ↑ 3 ) ∈ ℂ ) → ( ( ( 𝐹 ↑ 4 ) − ( 𝐹 ↑ 3 ) ) − ( 𝐹 ↑ 3 ) ) = ( ( 𝐹 ↑ 4 ) − ( ( 𝐹 ↑ 3 ) + ( 𝐹 ↑ 3 ) ) ) )
52 40 43 43 51 mp3an ⊢ ( ( ( 𝐹 ↑ 4 ) − ( 𝐹 ↑ 3 ) ) − ( 𝐹 ↑ 3 ) ) = ( ( 𝐹 ↑ 4 ) − ( ( 𝐹 ↑ 3 ) + ( 𝐹 ↑ 3 ) ) )
53 43 2timesi ⊢ ( 2 · ( 𝐹 ↑ 3 ) ) = ( ( 𝐹 ↑ 3 ) + ( 𝐹 ↑ 3 ) )
54 53 oveq2i ⊢ ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) = ( ( 𝐹 ↑ 4 ) − ( ( 𝐹 ↑ 3 ) + ( 𝐹 ↑ 3 ) ) )
55 52 54 eqtr4i ⊢ ( ( ( 𝐹 ↑ 4 ) − ( 𝐹 ↑ 3 ) ) − ( 𝐹 ↑ 3 ) ) = ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) )
56 50 55 eqtri ⊢ ( ( ( ( 𝐹 ↑ 4 ) − ( 𝐹 ↑ 3 ) ) − ( 𝐹 ↑ 2 ) ) − ( ( 𝐹 ↑ 3 ) − ( 𝐹 ↑ 2 ) ) ) = ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) )
57 56 oveq1i ⊢ ( ( ( ( ( 𝐹 ↑ 4 ) − ( 𝐹 ↑ 3 ) ) − ( 𝐹 ↑ 2 ) ) − ( ( 𝐹 ↑ 3 ) − ( 𝐹 ↑ 2 ) ) ) + 𝐹 ) = ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) + 𝐹 )
58 48 57 eqtri ⊢ ( ( ( ( 𝐹 ↑ 4 ) − ( 𝐹 ↑ 3 ) ) − ( 𝐹 ↑ 2 ) ) − ( ( ( 𝐹 ↑ 3 ) − ( 𝐹 ↑ 2 ) ) − 𝐹 ) ) = ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) + 𝐹 )
59 7 37 58 3eqtri ⊢ ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) · ( ( 𝐹 ↑ 2 ) − 𝐹 ) ) = ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) + 𝐹 )
60 5 mulridi ⊢ ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) · 1 ) = ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 )
61 59 60 oveq12i ⊢ ( ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) · ( ( 𝐹 ↑ 2 ) − 𝐹 ) ) − ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) · 1 ) ) = ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) + 𝐹 ) − ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) )
62 2cn ⊢ 2 ∈ ℂ
63 62 43 mulcli ⊢ ( 2 · ( 𝐹 ↑ 3 ) ) ∈ ℂ
64 40 63 subcli ⊢ ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) ∈ ℂ
65 64 1 addcli ⊢ ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) + 𝐹 ) ∈ ℂ
66 subsub ⊢ ( ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) + 𝐹 ) ∈ ℂ ∧ ( ( 𝐹 ↑ 2 ) − 𝐹 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) + 𝐹 ) − ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) ) = ( ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) + 𝐹 ) − ( ( 𝐹 ↑ 2 ) − 𝐹 ) ) + 1 ) )
67 65 3 4 66 mp3an ⊢ ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) + 𝐹 ) − ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) ) = ( ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) + 𝐹 ) − ( ( 𝐹 ↑ 2 ) − 𝐹 ) ) + 1 )
68 64 a1i ⊢ ( ⊤ → ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) ∈ ℂ )
69 1 a1i ⊢ ( ⊤ → 𝐹 ∈ ℂ )
70 2 a1i ⊢ ( ⊤ → ( 𝐹 ↑ 2 ) ∈ ℂ )
71 68 69 70 69 addsubsub23 ⊢ ( ⊤ → ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) + 𝐹 ) − ( ( 𝐹 ↑ 2 ) − 𝐹 ) ) = ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) + ( 𝐹 + 𝐹 ) ) )
72 71 mptru ⊢ ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) + 𝐹 ) − ( ( 𝐹 ↑ 2 ) − 𝐹 ) ) = ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) + ( 𝐹 + 𝐹 ) )
73 1 2timesi ⊢ ( 2 · 𝐹 ) = ( 𝐹 + 𝐹 )
74 73 oveq2i ⊢ ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) + ( 2 · 𝐹 ) ) = ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) + ( 𝐹 + 𝐹 ) )
75 72 74 eqtr4i ⊢ ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) + 𝐹 ) − ( ( 𝐹 ↑ 2 ) − 𝐹 ) ) = ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) + ( 2 · 𝐹 ) )
76 75 oveq1i ⊢ ( ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) + 𝐹 ) − ( ( 𝐹 ↑ 2 ) − 𝐹 ) ) + 1 ) = ( ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) + ( 2 · 𝐹 ) ) + 1 )
77 67 76 eqtri ⊢ ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) + 𝐹 ) − ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) ) = ( ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) + ( 2 · 𝐹 ) ) + 1 )
78 6 61 77 3eqtri ⊢ ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) · ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) ) = ( ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) + ( 2 · 𝐹 ) ) + 1 )
79 78 oveq1i ⊢ ( ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) · ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) ) · ( 𝐹 + 2 ) ) = ( ( ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) + ( 2 · 𝐹 ) ) + 1 ) · ( 𝐹 + 2 ) )
80 64 2 subcli ⊢ ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) ∈ ℂ
81 62 1 mulcli ⊢ ( 2 · 𝐹 ) ∈ ℂ
82 80 81 addcli ⊢ ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) + ( 2 · 𝐹 ) ) ∈ ℂ
83 82 4 addcli ⊢ ( ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) + ( 2 · 𝐹 ) ) + 1 ) ∈ ℂ
84 83 1 62 adddii ⊢ ( ( ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) + ( 2 · 𝐹 ) ) + 1 ) · ( 𝐹 + 2 ) ) = ( ( ( ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) + ( 2 · 𝐹 ) ) + 1 ) · 𝐹 ) + ( ( ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) + ( 2 · 𝐹 ) ) + 1 ) · 2 ) )
85 82 4 1 adddiri ⊢ ( ( ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) + ( 2 · 𝐹 ) ) + 1 ) · 𝐹 ) = ( ( ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) + ( 2 · 𝐹 ) ) · 𝐹 ) + ( 1 · 𝐹 ) )
86 80 81 1 adddiri ⊢ ( ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) + ( 2 · 𝐹 ) ) · 𝐹 ) = ( ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) · 𝐹 ) + ( ( 2 · 𝐹 ) · 𝐹 ) )
87 64 2 1 subdiri ⊢ ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) · 𝐹 ) = ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) · 𝐹 ) − ( ( 𝐹 ↑ 2 ) · 𝐹 ) )
88 40 63 1 subdiri ⊢ ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) · 𝐹 ) = ( ( ( 𝐹 ↑ 4 ) · 𝐹 ) − ( ( 2 · ( 𝐹 ↑ 3 ) ) · 𝐹 ) )
89 df-5 ⊢ 5 = ( 4 + 1 )
90 89 oveq2i ⊢ ( 𝐹 ↑ 5 ) = ( 𝐹 ↑ ( 4 + 1 ) )
91 expp1 ⊢ ( ( 𝐹 ∈ ℂ ∧ 4 ∈ ℕ0 ) → ( 𝐹 ↑ ( 4 + 1 ) ) = ( ( 𝐹 ↑ 4 ) · 𝐹 ) )
92 1 38 91 mp2an ⊢ ( 𝐹 ↑ ( 4 + 1 ) ) = ( ( 𝐹 ↑ 4 ) · 𝐹 )
93 90 92 eqtr2i ⊢ ( ( 𝐹 ↑ 4 ) · 𝐹 ) = ( 𝐹 ↑ 5 )
94 62 43 1 mulassi ⊢ ( ( 2 · ( 𝐹 ↑ 3 ) ) · 𝐹 ) = ( 2 · ( ( 𝐹 ↑ 3 ) · 𝐹 ) )
95 df-4 ⊢ 4 = ( 3 + 1 )
96 95 oveq2i ⊢ ( 𝐹 ↑ 4 ) = ( 𝐹 ↑ ( 3 + 1 ) )
97 expp1 ⊢ ( ( 𝐹 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝐹 ↑ ( 3 + 1 ) ) = ( ( 𝐹 ↑ 3 ) · 𝐹 ) )
98 1 41 97 mp2an ⊢ ( 𝐹 ↑ ( 3 + 1 ) ) = ( ( 𝐹 ↑ 3 ) · 𝐹 )
99 96 98 eqtri ⊢ ( 𝐹 ↑ 4 ) = ( ( 𝐹 ↑ 3 ) · 𝐹 )
100 99 oveq2i ⊢ ( 2 · ( 𝐹 ↑ 4 ) ) = ( 2 · ( ( 𝐹 ↑ 3 ) · 𝐹 ) )
101 94 100 eqtr4i ⊢ ( ( 2 · ( 𝐹 ↑ 3 ) ) · 𝐹 ) = ( 2 · ( 𝐹 ↑ 4 ) )
102 93 101 oveq12i ⊢ ( ( ( 𝐹 ↑ 4 ) · 𝐹 ) − ( ( 2 · ( 𝐹 ↑ 3 ) ) · 𝐹 ) ) = ( ( 𝐹 ↑ 5 ) − ( 2 · ( 𝐹 ↑ 4 ) ) )
103 88 102 eqtri ⊢ ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) · 𝐹 ) = ( ( 𝐹 ↑ 5 ) − ( 2 · ( 𝐹 ↑ 4 ) ) )
104 103 21 oveq12i ⊢ ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) · 𝐹 ) − ( ( 𝐹 ↑ 2 ) · 𝐹 ) ) = ( ( ( 𝐹 ↑ 5 ) − ( 2 · ( 𝐹 ↑ 4 ) ) ) − ( 𝐹 ↑ 3 ) )
105 87 104 eqtri ⊢ ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) · 𝐹 ) = ( ( ( 𝐹 ↑ 5 ) − ( 2 · ( 𝐹 ↑ 4 ) ) ) − ( 𝐹 ↑ 3 ) )
106 62 1 1 mulassi ⊢ ( ( 2 · 𝐹 ) · 𝐹 ) = ( 2 · ( 𝐹 · 𝐹 ) )
107 30 oveq2i ⊢ ( 2 · ( 𝐹 ↑ 2 ) ) = ( 2 · ( 𝐹 · 𝐹 ) )
108 106 107 eqtr4i ⊢ ( ( 2 · 𝐹 ) · 𝐹 ) = ( 2 · ( 𝐹 ↑ 2 ) )
109 105 108 oveq12i ⊢ ( ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) · 𝐹 ) + ( ( 2 · 𝐹 ) · 𝐹 ) ) = ( ( ( ( 𝐹 ↑ 5 ) − ( 2 · ( 𝐹 ↑ 4 ) ) ) − ( 𝐹 ↑ 3 ) ) + ( 2 · ( 𝐹 ↑ 2 ) ) )
110 86 109 eqtri ⊢ ( ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) + ( 2 · 𝐹 ) ) · 𝐹 ) = ( ( ( ( 𝐹 ↑ 5 ) − ( 2 · ( 𝐹 ↑ 4 ) ) ) − ( 𝐹 ↑ 3 ) ) + ( 2 · ( 𝐹 ↑ 2 ) ) )
111 110 34 oveq12i ⊢ ( ( ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) + ( 2 · 𝐹 ) ) · 𝐹 ) + ( 1 · 𝐹 ) ) = ( ( ( ( ( 𝐹 ↑ 5 ) − ( 2 · ( 𝐹 ↑ 4 ) ) ) − ( 𝐹 ↑ 3 ) ) + ( 2 · ( 𝐹 ↑ 2 ) ) ) + 𝐹 )
112 85 111 eqtri ⊢ ( ( ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) + ( 2 · 𝐹 ) ) + 1 ) · 𝐹 ) = ( ( ( ( ( 𝐹 ↑ 5 ) − ( 2 · ( 𝐹 ↑ 4 ) ) ) − ( 𝐹 ↑ 3 ) ) + ( 2 · ( 𝐹 ↑ 2 ) ) ) + 𝐹 )
113 82 4 62 adddiri ⊢ ( ( ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) + ( 2 · 𝐹 ) ) + 1 ) · 2 ) = ( ( ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) + ( 2 · 𝐹 ) ) · 2 ) + ( 1 · 2 ) )
114 80 81 62 adddiri ⊢ ( ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) + ( 2 · 𝐹 ) ) · 2 ) = ( ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) · 2 ) + ( ( 2 · 𝐹 ) · 2 ) )
115 64 2 62 subdiri ⊢ ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) · 2 ) = ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) · 2 ) − ( ( 𝐹 ↑ 2 ) · 2 ) )
116 40 63 62 subdiri ⊢ ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) · 2 ) = ( ( ( 𝐹 ↑ 4 ) · 2 ) − ( ( 2 · ( 𝐹 ↑ 3 ) ) · 2 ) )
117 40 62 mulcomi ⊢ ( ( 𝐹 ↑ 4 ) · 2 ) = ( 2 · ( 𝐹 ↑ 4 ) )
118 62 43 62 mul32i ⊢ ( ( 2 · ( 𝐹 ↑ 3 ) ) · 2 ) = ( ( 2 · 2 ) · ( 𝐹 ↑ 3 ) )
119 2t2e4 ⊢ ( 2 · 2 ) = 4
120 119 oveq1i ⊢ ( ( 2 · 2 ) · ( 𝐹 ↑ 3 ) ) = ( 4 · ( 𝐹 ↑ 3 ) )
121 118 120 eqtri ⊢ ( ( 2 · ( 𝐹 ↑ 3 ) ) · 2 ) = ( 4 · ( 𝐹 ↑ 3 ) )
122 117 121 oveq12i ⊢ ( ( ( 𝐹 ↑ 4 ) · 2 ) − ( ( 2 · ( 𝐹 ↑ 3 ) ) · 2 ) ) = ( ( 2 · ( 𝐹 ↑ 4 ) ) − ( 4 · ( 𝐹 ↑ 3 ) ) )
123 116 122 eqtri ⊢ ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) · 2 ) = ( ( 2 · ( 𝐹 ↑ 4 ) ) − ( 4 · ( 𝐹 ↑ 3 ) ) )
124 2 62 mulcomi ⊢ ( ( 𝐹 ↑ 2 ) · 2 ) = ( 2 · ( 𝐹 ↑ 2 ) )
125 123 124 oveq12i ⊢ ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) · 2 ) − ( ( 𝐹 ↑ 2 ) · 2 ) ) = ( ( ( 2 · ( 𝐹 ↑ 4 ) ) − ( 4 · ( 𝐹 ↑ 3 ) ) ) − ( 2 · ( 𝐹 ↑ 2 ) ) )
126 115 125 eqtri ⊢ ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) · 2 ) = ( ( ( 2 · ( 𝐹 ↑ 4 ) ) − ( 4 · ( 𝐹 ↑ 3 ) ) ) − ( 2 · ( 𝐹 ↑ 2 ) ) )
127 62 1 62 mul32i ⊢ ( ( 2 · 𝐹 ) · 2 ) = ( ( 2 · 2 ) · 𝐹 )
128 119 oveq1i ⊢ ( ( 2 · 2 ) · 𝐹 ) = ( 4 · 𝐹 )
129 127 128 eqtri ⊢ ( ( 2 · 𝐹 ) · 2 ) = ( 4 · 𝐹 )
130 126 129 oveq12i ⊢ ( ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) · 2 ) + ( ( 2 · 𝐹 ) · 2 ) ) = ( ( ( ( 2 · ( 𝐹 ↑ 4 ) ) − ( 4 · ( 𝐹 ↑ 3 ) ) ) − ( 2 · ( 𝐹 ↑ 2 ) ) ) + ( 4 · 𝐹 ) )
131 114 130 eqtri ⊢ ( ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) + ( 2 · 𝐹 ) ) · 2 ) = ( ( ( ( 2 · ( 𝐹 ↑ 4 ) ) − ( 4 · ( 𝐹 ↑ 3 ) ) ) − ( 2 · ( 𝐹 ↑ 2 ) ) ) + ( 4 · 𝐹 ) )
132 62 mullidi ⊢ ( 1 · 2 ) = 2
133 131 132 oveq12i ⊢ ( ( ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) + ( 2 · 𝐹 ) ) · 2 ) + ( 1 · 2 ) ) = ( ( ( ( ( 2 · ( 𝐹 ↑ 4 ) ) − ( 4 · ( 𝐹 ↑ 3 ) ) ) − ( 2 · ( 𝐹 ↑ 2 ) ) ) + ( 4 · 𝐹 ) ) + 2 )
134 113 133 eqtri ⊢ ( ( ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) + ( 2 · 𝐹 ) ) + 1 ) · 2 ) = ( ( ( ( ( 2 · ( 𝐹 ↑ 4 ) ) − ( 4 · ( 𝐹 ↑ 3 ) ) ) − ( 2 · ( 𝐹 ↑ 2 ) ) ) + ( 4 · 𝐹 ) ) + 2 )
135 112 134 oveq12i ⊢ ( ( ( ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) + ( 2 · 𝐹 ) ) + 1 ) · 𝐹 ) + ( ( ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) + ( 2 · 𝐹 ) ) + 1 ) · 2 ) ) = ( ( ( ( ( ( 𝐹 ↑ 5 ) − ( 2 · ( 𝐹 ↑ 4 ) ) ) − ( 𝐹 ↑ 3 ) ) + ( 2 · ( 𝐹 ↑ 2 ) ) ) + 𝐹 ) + ( ( ( ( ( 2 · ( 𝐹 ↑ 4 ) ) − ( 4 · ( 𝐹 ↑ 3 ) ) ) − ( 2 · ( 𝐹 ↑ 2 ) ) ) + ( 4 · 𝐹 ) ) + 2 ) )
136 5nn0 ⊢ 5 ∈ ℕ0
137 expcl ⊢ ( ( 𝐹 ∈ ℂ ∧ 5 ∈ ℕ0 ) → ( 𝐹 ↑ 5 ) ∈ ℂ )
138 1 136 137 mp2an ⊢ ( 𝐹 ↑ 5 ) ∈ ℂ
139 62 40 mulcli ⊢ ( 2 · ( 𝐹 ↑ 4 ) ) ∈ ℂ
140 138 139 subcli ⊢ ( ( 𝐹 ↑ 5 ) − ( 2 · ( 𝐹 ↑ 4 ) ) ) ∈ ℂ
141 140 43 subcli ⊢ ( ( ( 𝐹 ↑ 5 ) − ( 2 · ( 𝐹 ↑ 4 ) ) ) − ( 𝐹 ↑ 3 ) ) ∈ ℂ
142 62 2 mulcli ⊢ ( 2 · ( 𝐹 ↑ 2 ) ) ∈ ℂ
143 141 142 addcli ⊢ ( ( ( ( 𝐹 ↑ 5 ) − ( 2 · ( 𝐹 ↑ 4 ) ) ) − ( 𝐹 ↑ 3 ) ) + ( 2 · ( 𝐹 ↑ 2 ) ) ) ∈ ℂ
144 143 1 addcli ⊢ ( ( ( ( ( 𝐹 ↑ 5 ) − ( 2 · ( 𝐹 ↑ 4 ) ) ) − ( 𝐹 ↑ 3 ) ) + ( 2 · ( 𝐹 ↑ 2 ) ) ) + 𝐹 ) ∈ ℂ
145 4cn ⊢ 4 ∈ ℂ
146 145 43 mulcli ⊢ ( 4 · ( 𝐹 ↑ 3 ) ) ∈ ℂ
147 139 146 subcli ⊢ ( ( 2 · ( 𝐹 ↑ 4 ) ) − ( 4 · ( 𝐹 ↑ 3 ) ) ) ∈ ℂ
148 147 142 subcli ⊢ ( ( ( 2 · ( 𝐹 ↑ 4 ) ) − ( 4 · ( 𝐹 ↑ 3 ) ) ) − ( 2 · ( 𝐹 ↑ 2 ) ) ) ∈ ℂ
149 145 1 mulcli ⊢ ( 4 · 𝐹 ) ∈ ℂ
150 148 149 addcli ⊢ ( ( ( ( 2 · ( 𝐹 ↑ 4 ) ) − ( 4 · ( 𝐹 ↑ 3 ) ) ) − ( 2 · ( 𝐹 ↑ 2 ) ) ) + ( 4 · 𝐹 ) ) ∈ ℂ
151 144 150 62 addassi ⊢ ( ( ( ( ( ( ( 𝐹 ↑ 5 ) − ( 2 · ( 𝐹 ↑ 4 ) ) ) − ( 𝐹 ↑ 3 ) ) + ( 2 · ( 𝐹 ↑ 2 ) ) ) + 𝐹 ) + ( ( ( ( 2 · ( 𝐹 ↑ 4 ) ) − ( 4 · ( 𝐹 ↑ 3 ) ) ) − ( 2 · ( 𝐹 ↑ 2 ) ) ) + ( 4 · 𝐹 ) ) ) + 2 ) = ( ( ( ( ( ( 𝐹 ↑ 5 ) − ( 2 · ( 𝐹 ↑ 4 ) ) ) − ( 𝐹 ↑ 3 ) ) + ( 2 · ( 𝐹 ↑ 2 ) ) ) + 𝐹 ) + ( ( ( ( ( 2 · ( 𝐹 ↑ 4 ) ) − ( 4 · ( 𝐹 ↑ 3 ) ) ) − ( 2 · ( 𝐹 ↑ 2 ) ) ) + ( 4 · 𝐹 ) ) + 2 ) )
152 143 1 148 149 add4i ⊢ ( ( ( ( ( ( 𝐹 ↑ 5 ) − ( 2 · ( 𝐹 ↑ 4 ) ) ) − ( 𝐹 ↑ 3 ) ) + ( 2 · ( 𝐹 ↑ 2 ) ) ) + 𝐹 ) + ( ( ( ( 2 · ( 𝐹 ↑ 4 ) ) − ( 4 · ( 𝐹 ↑ 3 ) ) ) − ( 2 · ( 𝐹 ↑ 2 ) ) ) + ( 4 · 𝐹 ) ) ) = ( ( ( ( ( ( 𝐹 ↑ 5 ) − ( 2 · ( 𝐹 ↑ 4 ) ) ) − ( 𝐹 ↑ 3 ) ) + ( 2 · ( 𝐹 ↑ 2 ) ) ) + ( ( ( 2 · ( 𝐹 ↑ 4 ) ) − ( 4 · ( 𝐹 ↑ 3 ) ) ) − ( 2 · ( 𝐹 ↑ 2 ) ) ) ) + ( 𝐹 + ( 4 · 𝐹 ) ) )
153 ppncan ⊢ ( ( ( ( ( 𝐹 ↑ 5 ) − ( 2 · ( 𝐹 ↑ 4 ) ) ) − ( 𝐹 ↑ 3 ) ) ∈ ℂ ∧ ( 2 · ( 𝐹 ↑ 2 ) ) ∈ ℂ ∧ ( ( 2 · ( 𝐹 ↑ 4 ) ) − ( 4 · ( 𝐹 ↑ 3 ) ) ) ∈ ℂ ) → ( ( ( ( ( 𝐹 ↑ 5 ) − ( 2 · ( 𝐹 ↑ 4 ) ) ) − ( 𝐹 ↑ 3 ) ) + ( 2 · ( 𝐹 ↑ 2 ) ) ) + ( ( ( 2 · ( 𝐹 ↑ 4 ) ) − ( 4 · ( 𝐹 ↑ 3 ) ) ) − ( 2 · ( 𝐹 ↑ 2 ) ) ) ) = ( ( ( ( 𝐹 ↑ 5 ) − ( 2 · ( 𝐹 ↑ 4 ) ) ) − ( 𝐹 ↑ 3 ) ) + ( ( 2 · ( 𝐹 ↑ 4 ) ) − ( 4 · ( 𝐹 ↑ 3 ) ) ) ) )
154 141 142 147 153 mp3an ⊢ ( ( ( ( ( 𝐹 ↑ 5 ) − ( 2 · ( 𝐹 ↑ 4 ) ) ) − ( 𝐹 ↑ 3 ) ) + ( 2 · ( 𝐹 ↑ 2 ) ) ) + ( ( ( 2 · ( 𝐹 ↑ 4 ) ) − ( 4 · ( 𝐹 ↑ 3 ) ) ) − ( 2 · ( 𝐹 ↑ 2 ) ) ) ) = ( ( ( ( 𝐹 ↑ 5 ) − ( 2 · ( 𝐹 ↑ 4 ) ) ) − ( 𝐹 ↑ 3 ) ) + ( ( 2 · ( 𝐹 ↑ 4 ) ) − ( 4 · ( 𝐹 ↑ 3 ) ) ) )
155 140 139 43 146 addsub4i ⊢ ( ( ( ( 𝐹 ↑ 5 ) − ( 2 · ( 𝐹 ↑ 4 ) ) ) + ( 2 · ( 𝐹 ↑ 4 ) ) ) − ( ( 𝐹 ↑ 3 ) + ( 4 · ( 𝐹 ↑ 3 ) ) ) ) = ( ( ( ( 𝐹 ↑ 5 ) − ( 2 · ( 𝐹 ↑ 4 ) ) ) − ( 𝐹 ↑ 3 ) ) + ( ( 2 · ( 𝐹 ↑ 4 ) ) − ( 4 · ( 𝐹 ↑ 3 ) ) ) )
156 npcan ⊢ ( ( ( 𝐹 ↑ 5 ) ∈ ℂ ∧ ( 2 · ( 𝐹 ↑ 4 ) ) ∈ ℂ ) → ( ( ( 𝐹 ↑ 5 ) − ( 2 · ( 𝐹 ↑ 4 ) ) ) + ( 2 · ( 𝐹 ↑ 4 ) ) ) = ( 𝐹 ↑ 5 ) )
157 138 139 156 mp2an ⊢ ( ( ( 𝐹 ↑ 5 ) − ( 2 · ( 𝐹 ↑ 4 ) ) ) + ( 2 · ( 𝐹 ↑ 4 ) ) ) = ( 𝐹 ↑ 5 )
158 145 4 89 comraddi ⊢ 5 = ( 1 + 4 )
159 158 oveq1i ⊢ ( 5 · ( 𝐹 ↑ 3 ) ) = ( ( 1 + 4 ) · ( 𝐹 ↑ 3 ) )
160 4 145 43 adddiri ⊢ ( ( 1 + 4 ) · ( 𝐹 ↑ 3 ) ) = ( ( 1 · ( 𝐹 ↑ 3 ) ) + ( 4 · ( 𝐹 ↑ 3 ) ) )
161 43 mullidi ⊢ ( 1 · ( 𝐹 ↑ 3 ) ) = ( 𝐹 ↑ 3 )
162 161 oveq1i ⊢ ( ( 1 · ( 𝐹 ↑ 3 ) ) + ( 4 · ( 𝐹 ↑ 3 ) ) ) = ( ( 𝐹 ↑ 3 ) + ( 4 · ( 𝐹 ↑ 3 ) ) )
163 159 160 162 3eqtrri ⊢ ( ( 𝐹 ↑ 3 ) + ( 4 · ( 𝐹 ↑ 3 ) ) ) = ( 5 · ( 𝐹 ↑ 3 ) )
164 157 163 oveq12i ⊢ ( ( ( ( 𝐹 ↑ 5 ) − ( 2 · ( 𝐹 ↑ 4 ) ) ) + ( 2 · ( 𝐹 ↑ 4 ) ) ) − ( ( 𝐹 ↑ 3 ) + ( 4 · ( 𝐹 ↑ 3 ) ) ) ) = ( ( 𝐹 ↑ 5 ) − ( 5 · ( 𝐹 ↑ 3 ) ) )
165 154 155 164 3eqtr2i ⊢ ( ( ( ( ( 𝐹 ↑ 5 ) − ( 2 · ( 𝐹 ↑ 4 ) ) ) − ( 𝐹 ↑ 3 ) ) + ( 2 · ( 𝐹 ↑ 2 ) ) ) + ( ( ( 2 · ( 𝐹 ↑ 4 ) ) − ( 4 · ( 𝐹 ↑ 3 ) ) ) − ( 2 · ( 𝐹 ↑ 2 ) ) ) ) = ( ( 𝐹 ↑ 5 ) − ( 5 · ( 𝐹 ↑ 3 ) ) )
166 4 145 1 adddiri ⊢ ( ( 1 + 4 ) · 𝐹 ) = ( ( 1 · 𝐹 ) + ( 4 · 𝐹 ) )
167 158 oveq1i ⊢ ( 5 · 𝐹 ) = ( ( 1 + 4 ) · 𝐹 )
168 34 eqcomi ⊢ 𝐹 = ( 1 · 𝐹 )
169 168 oveq1i ⊢ ( 𝐹 + ( 4 · 𝐹 ) ) = ( ( 1 · 𝐹 ) + ( 4 · 𝐹 ) )
170 166 167 169 3eqtr4ri ⊢ ( 𝐹 + ( 4 · 𝐹 ) ) = ( 5 · 𝐹 )
171 165 170 oveq12i ⊢ ( ( ( ( ( ( 𝐹 ↑ 5 ) − ( 2 · ( 𝐹 ↑ 4 ) ) ) − ( 𝐹 ↑ 3 ) ) + ( 2 · ( 𝐹 ↑ 2 ) ) ) + ( ( ( 2 · ( 𝐹 ↑ 4 ) ) − ( 4 · ( 𝐹 ↑ 3 ) ) ) − ( 2 · ( 𝐹 ↑ 2 ) ) ) ) + ( 𝐹 + ( 4 · 𝐹 ) ) ) = ( ( ( 𝐹 ↑ 5 ) − ( 5 · ( 𝐹 ↑ 3 ) ) ) + ( 5 · 𝐹 ) )
172 152 171 eqtri ⊢ ( ( ( ( ( ( 𝐹 ↑ 5 ) − ( 2 · ( 𝐹 ↑ 4 ) ) ) − ( 𝐹 ↑ 3 ) ) + ( 2 · ( 𝐹 ↑ 2 ) ) ) + 𝐹 ) + ( ( ( ( 2 · ( 𝐹 ↑ 4 ) ) − ( 4 · ( 𝐹 ↑ 3 ) ) ) − ( 2 · ( 𝐹 ↑ 2 ) ) ) + ( 4 · 𝐹 ) ) ) = ( ( ( 𝐹 ↑ 5 ) − ( 5 · ( 𝐹 ↑ 3 ) ) ) + ( 5 · 𝐹 ) )
173 172 oveq1i ⊢ ( ( ( ( ( ( ( 𝐹 ↑ 5 ) − ( 2 · ( 𝐹 ↑ 4 ) ) ) − ( 𝐹 ↑ 3 ) ) + ( 2 · ( 𝐹 ↑ 2 ) ) ) + 𝐹 ) + ( ( ( ( 2 · ( 𝐹 ↑ 4 ) ) − ( 4 · ( 𝐹 ↑ 3 ) ) ) − ( 2 · ( 𝐹 ↑ 2 ) ) ) + ( 4 · 𝐹 ) ) ) + 2 ) = ( ( ( ( 𝐹 ↑ 5 ) − ( 5 · ( 𝐹 ↑ 3 ) ) ) + ( 5 · 𝐹 ) ) + 2 )
174 135 151 173 3eqtr2i ⊢ ( ( ( ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) + ( 2 · 𝐹 ) ) + 1 ) · 𝐹 ) + ( ( ( ( ( ( 𝐹 ↑ 4 ) − ( 2 · ( 𝐹 ↑ 3 ) ) ) − ( 𝐹 ↑ 2 ) ) + ( 2 · 𝐹 ) ) + 1 ) · 2 ) ) = ( ( ( ( 𝐹 ↑ 5 ) − ( 5 · ( 𝐹 ↑ 3 ) ) ) + ( 5 · 𝐹 ) ) + 2 )
175 79 84 174 3eqtri ⊢ ( ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) · ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) ) · ( 𝐹 + 2 ) ) = ( ( ( ( 𝐹 ↑ 5 ) − ( 5 · ( 𝐹 ↑ 3 ) ) ) + ( 5 · 𝐹 ) ) + 2 )