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 
|- F e. CC
Assertion goldpolyfactor 
|- ( ( ( ( ( F ^ 2 ) - F ) - 1 ) x. ( ( ( F ^ 2 ) - F ) - 1 ) ) x. ( F + 2 ) ) = ( ( ( ( F ^ 5 ) - ( 5 x. ( F ^ 3 ) ) ) + ( 5 x. F ) ) + 2 )

Proof

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