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 \in ℂ$
	Assertion	goldpolyfactor	$⊢ (F^{2} - F - 1) (F^{2} - F - 1) (F + 2) = (F^{5} - 5 F^{3}) + 5 F + 2$

Proof

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

Metamath Proof Explorer

Theorem goldpolyfactor

Proof