goldpolyfactor - Mathbox for Ender Ting

	Mathbox for Ender Ting		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > goldpolyfactor		Structured version Visualization version GIF version

Theorem goldpolyfactor 47730

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.)

**Hypothesis**
Ref	Expression
goldpolyfactor.1	⊢ 𝐹 ∈ ℂ

**Assertion**
Ref	Expression
goldpolyfactor	⊢ (((((𝐹↑2) − 𝐹) − 1) · (((𝐹↑2) − 𝐹) − 1)) · (𝐹 + 2)) = ((((𝐹↑5) − (5 · (𝐹↑3))) + (5 · 𝐹)) + 2)

**Proof of Theorem goldpolyfactor**
Step	Hyp	Ref	Expression
1		goldpolyfactor.1	. . . . . . . 8 ⊢ 𝐹 ∈ ℂ
2	1	sqcli 14245	. . . . . . 7 ⊢ (𝐹↑2) ∈ ℂ
3	2, 1	subcli 11559	. . . . . 6 ⊢ ((𝐹↑2) − 𝐹) ∈ ℂ
4		ax-1cn 11183	. . . . . 6 ⊢ 1 ∈ ℂ
5	3, 4	subcli 11559	. . . . 5 ⊢ (((𝐹↑2) − 𝐹) − 1) ∈ ℂ
6	5, 3, 4	subdii 11688	. . . 4 ⊢ ((((𝐹↑2) − 𝐹) − 1) · (((𝐹↑2) − 𝐹) − 1)) = (((((𝐹↑2) − 𝐹) − 1) · ((𝐹↑2) − 𝐹)) − ((((𝐹↑2) − 𝐹) − 1) · 1))
7	5, 2, 1	subdii 11688	. . . . . 6 ⊢ ((((𝐹↑2) − 𝐹) − 1) · ((𝐹↑2) − 𝐹)) = (((((𝐹↑2) − 𝐹) − 1) · (𝐹↑2)) − ((((𝐹↑2) − 𝐹) − 1) · 𝐹))
8	3, 4, 2	subdiri 11689	. . . . . . . 8 ⊢ ((((𝐹↑2) − 𝐹) − 1) · (𝐹↑2)) = ((((𝐹↑2) − 𝐹) · (𝐹↑2)) − (1 · (𝐹↑2)))
9	2, 1, 2	subdiri 11689	. . . . . . . . . 10 ⊢ (((𝐹↑2) − 𝐹) · (𝐹↑2)) = (((𝐹↑2) · (𝐹↑2)) − (𝐹 · (𝐹↑2)))
10		2nn0 12546	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℕ₀
11		expadd 14168	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ ℂ ∧ 2 ∈ ℕ₀ ∧ 2 ∈ ℕ₀) → (𝐹↑(2 + 2)) = ((𝐹↑2) · (𝐹↑2)))
12	1, 10, 10, 11	mp3an 1490	. . . . . . . . . . . 12 ⊢ (𝐹↑(2 + 2)) = ((𝐹↑2) · (𝐹↑2))
13		2p2e4 12400	. . . . . . . . . . . . 13 ⊢ (2 + 2) = 4
14	13	oveq2i 7427	. . . . . . . . . . . 12 ⊢ (𝐹↑(2 + 2)) = (𝐹↑4)
15	12, 14	eqtr3i 2787	. . . . . . . . . . 11 ⊢ ((𝐹↑2) · (𝐹↑2)) = (𝐹↑4)
16	1, 2	mulcomi 11242	. . . . . . . . . . . 12 ⊢ (𝐹 · (𝐹↑2)) = ((𝐹↑2) · 𝐹)
17		df-3 12329	. . . . . . . . . . . . . 14 ⊢ 3 = (2 + 1)
18	17	oveq2i 7427	. . . . . . . . . . . . 13 ⊢ (𝐹↑3) = (𝐹↑(2 + 1))
19		expp1 14132	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ℂ ∧ 2 ∈ ℕ₀) → (𝐹↑(2 + 1)) = ((𝐹↑2) · 𝐹))
20	1, 10, 19	mp2an 705	. . . . . . . . . . . . 13 ⊢ (𝐹↑(2 + 1)) = ((𝐹↑2) · 𝐹)
21	18, 20	eqtr2i 2786	. . . . . . . . . . . 12 ⊢ ((𝐹↑2) · 𝐹) = (𝐹↑3)
22	16, 21	eqtri 2785	. . . . . . . . . . 11 ⊢ (𝐹 · (𝐹↑2)) = (𝐹↑3)
23	15, 22	oveq12i 7428	. . . . . . . . . 10 ⊢ (((𝐹↑2) · (𝐹↑2)) − (𝐹 · (𝐹↑2))) = ((𝐹↑4) − (𝐹↑3))
24	9, 23	eqtri 2785	. . . . . . . . 9 ⊢ (((𝐹↑2) − 𝐹) · (𝐹↑2)) = ((𝐹↑4) − (𝐹↑3))
25	2	mullidi 11239	. . . . . . . . 9 ⊢ (1 · (𝐹↑2)) = (𝐹↑2)
26	24, 25	oveq12i 7428	. . . . . . . 8 ⊢ ((((𝐹↑2) − 𝐹) · (𝐹↑2)) − (1 · (𝐹↑2))) = (((𝐹↑4) − (𝐹↑3)) − (𝐹↑2))
27	8, 26	eqtri 2785	. . . . . . 7 ⊢ ((((𝐹↑2) − 𝐹) − 1) · (𝐹↑2)) = (((𝐹↑4) − (𝐹↑3)) − (𝐹↑2))
28	3, 4, 1	subdiri 11689	. . . . . . . 8 ⊢ ((((𝐹↑2) − 𝐹) − 1) · 𝐹) = ((((𝐹↑2) − 𝐹) · 𝐹) − (1 · 𝐹))
29	2, 1, 1	subdiri 11689	. . . . . . . . . 10 ⊢ (((𝐹↑2) − 𝐹) · 𝐹) = (((𝐹↑2) · 𝐹) − (𝐹 · 𝐹))
30	1	sqvali 14244	. . . . . . . . . . . 12 ⊢ (𝐹↑2) = (𝐹 · 𝐹)
31	30	eqcomi 2771	. . . . . . . . . . 11 ⊢ (𝐹 · 𝐹) = (𝐹↑2)
32	21, 31	oveq12i 7428	. . . . . . . . . 10 ⊢ (((𝐹↑2) · 𝐹) − (𝐹 · 𝐹)) = ((𝐹↑3) − (𝐹↑2))
33	29, 32	eqtri 2785	. . . . . . . . 9 ⊢ (((𝐹↑2) − 𝐹) · 𝐹) = ((𝐹↑3) − (𝐹↑2))
34	1	mullidi 11239	. . . . . . . . 9 ⊢ (1 · 𝐹) = 𝐹
35	33, 34	oveq12i 7428	. . . . . . . 8 ⊢ ((((𝐹↑2) − 𝐹) · 𝐹) − (1 · 𝐹)) = (((𝐹↑3) − (𝐹↑2)) − 𝐹)
36	28, 35	eqtri 2785	. . . . . . 7 ⊢ ((((𝐹↑2) − 𝐹) − 1) · 𝐹) = (((𝐹↑3) − (𝐹↑2)) − 𝐹)
37	27, 36	oveq12i 7428	. . . . . 6 ⊢ (((((𝐹↑2) − 𝐹) − 1) · (𝐹↑2)) − ((((𝐹↑2) − 𝐹) − 1) · 𝐹)) = ((((𝐹↑4) − (𝐹↑3)) − (𝐹↑2)) − (((𝐹↑3) − (𝐹↑2)) − 𝐹))
38		4nn0 12548	. . . . . . . . . . 11 ⊢ 4 ∈ ℕ₀
39		expcl 14143	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ ℂ ∧ 4 ∈ ℕ₀) → (𝐹↑4) ∈ ℂ)
40	1, 38, 39	mp2an 705	. . . . . . . . . 10 ⊢ (𝐹↑4) ∈ ℂ
41		3nn0 12547	. . . . . . . . . . 11 ⊢ 3 ∈ ℕ₀
42		expcl 14143	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝐹↑3) ∈ ℂ)
43	1, 41, 42	mp2an 705	. . . . . . . . . 10 ⊢ (𝐹↑3) ∈ ℂ
44	40, 43	subcli 11559	. . . . . . . . 9 ⊢ ((𝐹↑4) − (𝐹↑3)) ∈ ℂ
45	44, 2	subcli 11559	. . . . . . . 8 ⊢ (((𝐹↑4) − (𝐹↑3)) − (𝐹↑2)) ∈ ℂ
46	43, 2	subcli 11559	. . . . . . . 8 ⊢ ((𝐹↑3) − (𝐹↑2)) ∈ ℂ
47		subsub 11513	. . . . . . . 8 ⊢ (((((𝐹↑4) − (𝐹↑3)) − (𝐹↑2)) ∈ ℂ ∧ ((𝐹↑3) − (𝐹↑2)) ∈ ℂ ∧ 𝐹 ∈ ℂ) → ((((𝐹↑4) − (𝐹↑3)) − (𝐹↑2)) − (((𝐹↑3) − (𝐹↑2)) − 𝐹)) = (((((𝐹↑4) − (𝐹↑3)) − (𝐹↑2)) − ((𝐹↑3) − (𝐹↑2))) + 𝐹))
48	45, 46, 1, 47	mp3an 1490	. . . . . . 7 ⊢ ((((𝐹↑4) − (𝐹↑3)) − (𝐹↑2)) − (((𝐹↑3) − (𝐹↑2)) − 𝐹)) = (((((𝐹↑4) − (𝐹↑3)) − (𝐹↑2)) − ((𝐹↑3) − (𝐹↑2))) + 𝐹)
49		nnncan2 11520	. . . . . . . . . 10 ⊢ ((((𝐹↑4) − (𝐹↑3)) ∈ ℂ ∧ (𝐹↑3) ∈ ℂ ∧ (𝐹↑2) ∈ ℂ) → ((((𝐹↑4) − (𝐹↑3)) − (𝐹↑2)) − ((𝐹↑3) − (𝐹↑2))) = (((𝐹↑4) − (𝐹↑3)) − (𝐹↑3)))
50	44, 43, 2, 49	mp3an 1490	. . . . . . . . 9 ⊢ ((((𝐹↑4) − (𝐹↑3)) − (𝐹↑2)) − ((𝐹↑3) − (𝐹↑2))) = (((𝐹↑4) − (𝐹↑3)) − (𝐹↑3))
51		subsub4 11516	. . . . . . . . . . 11 ⊢ (((𝐹↑4) ∈ ℂ ∧ (𝐹↑3) ∈ ℂ ∧ (𝐹↑3) ∈ ℂ) → (((𝐹↑4) − (𝐹↑3)) − (𝐹↑3)) = ((𝐹↑4) − ((𝐹↑3) + (𝐹↑3))))
52	40, 43, 43, 51	mp3an 1490	. . . . . . . . . 10 ⊢ (((𝐹↑4) − (𝐹↑3)) − (𝐹↑3)) = ((𝐹↑4) − ((𝐹↑3) + (𝐹↑3)))
53	43	2timesi 12403	. . . . . . . . . . 11 ⊢ (2 · (𝐹↑3)) = ((𝐹↑3) + (𝐹↑3))
54	53	oveq2i 7427	. . . . . . . . . 10 ⊢ ((𝐹↑4) − (2 · (𝐹↑3))) = ((𝐹↑4) − ((𝐹↑3) + (𝐹↑3)))
55	52, 54	eqtr4i 2788	. . . . . . . . 9 ⊢ (((𝐹↑4) − (𝐹↑3)) − (𝐹↑3)) = ((𝐹↑4) − (2 · (𝐹↑3)))
56	50, 55	eqtri 2785	. . . . . . . 8 ⊢ ((((𝐹↑4) − (𝐹↑3)) − (𝐹↑2)) − ((𝐹↑3) − (𝐹↑2))) = ((𝐹↑4) − (2 · (𝐹↑3)))
57	56	oveq1i 7426	. . . . . . 7 ⊢ (((((𝐹↑4) − (𝐹↑3)) − (𝐹↑2)) − ((𝐹↑3) − (𝐹↑2))) + 𝐹) = (((𝐹↑4) − (2 · (𝐹↑3))) + 𝐹)
58	48, 57	eqtri 2785	. . . . . 6 ⊢ ((((𝐹↑4) − (𝐹↑3)) − (𝐹↑2)) − (((𝐹↑3) − (𝐹↑2)) − 𝐹)) = (((𝐹↑4) − (2 · (𝐹↑3))) + 𝐹)
59	7, 37, 58	3eqtri 2789	. . . . 5 ⊢ ((((𝐹↑2) − 𝐹) − 1) · ((𝐹↑2) − 𝐹)) = (((𝐹↑4) − (2 · (𝐹↑3))) + 𝐹)
60	5	mulridi 11238	. . . . 5 ⊢ ((((𝐹↑2) − 𝐹) − 1) · 1) = (((𝐹↑2) − 𝐹) − 1)
61	59, 60	oveq12i 7428	. . . 4 ⊢ (((((𝐹↑2) − 𝐹) − 1) · ((𝐹↑2) − 𝐹)) − ((((𝐹↑2) − 𝐹) − 1) · 1)) = ((((𝐹↑4) − (2 · (𝐹↑3))) + 𝐹) − (((𝐹↑2) − 𝐹) − 1))
62		2cn 12341	. . . . . . . . 9 ⊢ 2 ∈ ℂ
63	62, 43	mulcli 11241	. . . . . . . 8 ⊢ (2 · (𝐹↑3)) ∈ ℂ
64	40, 63	subcli 11559	. . . . . . 7 ⊢ ((𝐹↑4) − (2 · (𝐹↑3))) ∈ ℂ
65	64, 1	addcli 11240	. . . . . 6 ⊢ (((𝐹↑4) − (2 · (𝐹↑3))) + 𝐹) ∈ ℂ
66		subsub 11513	. . . . . 6 ⊢ (((((𝐹↑4) − (2 · (𝐹↑3))) + 𝐹) ∈ ℂ ∧ ((𝐹↑2) − 𝐹) ∈ ℂ ∧ 1 ∈ ℂ) → ((((𝐹↑4) − (2 · (𝐹↑3))) + 𝐹) − (((𝐹↑2) − 𝐹) − 1)) = (((((𝐹↑4) − (2 · (𝐹↑3))) + 𝐹) − ((𝐹↑2) − 𝐹)) + 1))
67	65, 3, 4, 66	mp3an 1490	. . . . 5 ⊢ ((((𝐹↑4) − (2 · (𝐹↑3))) + 𝐹) − (((𝐹↑2) − 𝐹) − 1)) = (((((𝐹↑4) − (2 · (𝐹↑3))) + 𝐹) − ((𝐹↑2) − 𝐹)) + 1)
68	64	a1i 11	. . . . . . . . 9 ⊢ (⊤ → ((𝐹↑4) − (2 · (𝐹↑3))) ∈ ℂ)
69	1	a1i 11	. . . . . . . . 9 ⊢ (⊤ → 𝐹 ∈ ℂ)
70	2	a1i 11	. . . . . . . . 9 ⊢ (⊤ → (𝐹↑2) ∈ ℂ)
71	68, 69, 70, 69	addsubsub23 11647	. . . . . . . 8 ⊢ (⊤ → ((((𝐹↑4) − (2 · (𝐹↑3))) + 𝐹) − ((𝐹↑2) − 𝐹)) = ((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) + (𝐹 + 𝐹)))
72	71	mptru 1577	. . . . . . 7 ⊢ ((((𝐹↑4) − (2 · (𝐹↑3))) + 𝐹) − ((𝐹↑2) − 𝐹)) = ((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) + (𝐹 + 𝐹))
73	1	2timesi 12403	. . . . . . . 8 ⊢ (2 · 𝐹) = (𝐹 + 𝐹)
74	73	oveq2i 7427	. . . . . . 7 ⊢ ((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) + (2 · 𝐹)) = ((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) + (𝐹 + 𝐹))
75	72, 74	eqtr4i 2788	. . . . . 6 ⊢ ((((𝐹↑4) − (2 · (𝐹↑3))) + 𝐹) − ((𝐹↑2) − 𝐹)) = ((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) + (2 · 𝐹))
76	75	oveq1i 7426	. . . . 5 ⊢ (((((𝐹↑4) − (2 · (𝐹↑3))) + 𝐹) − ((𝐹↑2) − 𝐹)) + 1) = (((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) + (2 · 𝐹)) + 1)
77	67, 76	eqtri 2785	. . . 4 ⊢ ((((𝐹↑4) − (2 · (𝐹↑3))) + 𝐹) − (((𝐹↑2) − 𝐹) − 1)) = (((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) + (2 · 𝐹)) + 1)
78	6, 61, 77	3eqtri 2789	. . 3 ⊢ ((((𝐹↑2) − 𝐹) − 1) · (((𝐹↑2) − 𝐹) − 1)) = (((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) + (2 · 𝐹)) + 1)
79	78	oveq1i 7426	. 2 ⊢ (((((𝐹↑2) − 𝐹) − 1) · (((𝐹↑2) − 𝐹) − 1)) · (𝐹 + 2)) = ((((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) + (2 · 𝐹)) + 1) · (𝐹 + 2))
80	64, 2	subcli 11559	. . . . 5 ⊢ (((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) ∈ ℂ
81	62, 1	mulcli 11241	. . . . 5 ⊢ (2 · 𝐹) ∈ ℂ
82	80, 81	addcli 11240	. . . 4 ⊢ ((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) + (2 · 𝐹)) ∈ ℂ
83	82, 4	addcli 11240	. . 3 ⊢ (((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) + (2 · 𝐹)) + 1) ∈ ℂ
84	83, 1, 62	adddii 11246	. 2 ⊢ ((((((𝐹↑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 11247	. . . . 5 ⊢ ((((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) + (2 · 𝐹)) + 1) · 𝐹) = ((((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) + (2 · 𝐹)) · 𝐹) + (1 · 𝐹))
86	80, 81, 1	adddiri 11247	. . . . . . 7 ⊢ (((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) + (2 · 𝐹)) · 𝐹) = (((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) · 𝐹) + ((2 · 𝐹) · 𝐹))
87	64, 2, 1	subdiri 11689	. . . . . . . . 9 ⊢ ((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) · 𝐹) = ((((𝐹↑4) − (2 · (𝐹↑3))) · 𝐹) − ((𝐹↑2) · 𝐹))
88	40, 63, 1	subdiri 11689	. . . . . . . . . . 11 ⊢ (((𝐹↑4) − (2 · (𝐹↑3))) · 𝐹) = (((𝐹↑4) · 𝐹) − ((2 · (𝐹↑3)) · 𝐹))
89		df-5 12331	. . . . . . . . . . . . . 14 ⊢ 5 = (4 + 1)
90	89	oveq2i 7427	. . . . . . . . . . . . 13 ⊢ (𝐹↑5) = (𝐹↑(4 + 1))
91		expp1 14132	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ ℂ ∧ 4 ∈ ℕ₀) → (𝐹↑(4 + 1)) = ((𝐹↑4) · 𝐹))
92	1, 38, 91	mp2an 705	. . . . . . . . . . . . 13 ⊢ (𝐹↑(4 + 1)) = ((𝐹↑4) · 𝐹)
93	90, 92	eqtr2i 2786	. . . . . . . . . . . 12 ⊢ ((𝐹↑4) · 𝐹) = (𝐹↑5)
94	62, 43, 1	mulassi 11245	. . . . . . . . . . . . 13 ⊢ ((2 · (𝐹↑3)) · 𝐹) = (2 · ((𝐹↑3) · 𝐹))
95		df-4 12330	. . . . . . . . . . . . . . . 16 ⊢ 4 = (3 + 1)
96	95	oveq2i 7427	. . . . . . . . . . . . . . 15 ⊢ (𝐹↑4) = (𝐹↑(3 + 1))
97		expp1 14132	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝐹↑(3 + 1)) = ((𝐹↑3) · 𝐹))
98	1, 41, 97	mp2an 705	. . . . . . . . . . . . . . 15 ⊢ (𝐹↑(3 + 1)) = ((𝐹↑3) · 𝐹)
99	96, 98	eqtri 2785	. . . . . . . . . . . . . 14 ⊢ (𝐹↑4) = ((𝐹↑3) · 𝐹)
100	99	oveq2i 7427	. . . . . . . . . . . . 13 ⊢ (2 · (𝐹↑4)) = (2 · ((𝐹↑3) · 𝐹))
101	94, 100	eqtr4i 2788	. . . . . . . . . . . 12 ⊢ ((2 · (𝐹↑3)) · 𝐹) = (2 · (𝐹↑4))
102	93, 101	oveq12i 7428	. . . . . . . . . . 11 ⊢ (((𝐹↑4) · 𝐹) − ((2 · (𝐹↑3)) · 𝐹)) = ((𝐹↑5) − (2 · (𝐹↑4)))
103	88, 102	eqtri 2785	. . . . . . . . . 10 ⊢ (((𝐹↑4) − (2 · (𝐹↑3))) · 𝐹) = ((𝐹↑5) − (2 · (𝐹↑4)))
104	103, 21	oveq12i 7428	. . . . . . . . 9 ⊢ ((((𝐹↑4) − (2 · (𝐹↑3))) · 𝐹) − ((𝐹↑2) · 𝐹)) = (((𝐹↑5) − (2 · (𝐹↑4))) − (𝐹↑3))
105	87, 104	eqtri 2785	. . . . . . . 8 ⊢ ((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) · 𝐹) = (((𝐹↑5) − (2 · (𝐹↑4))) − (𝐹↑3))
106	62, 1, 1	mulassi 11245	. . . . . . . . 9 ⊢ ((2 · 𝐹) · 𝐹) = (2 · (𝐹 · 𝐹))
107	30	oveq2i 7427	. . . . . . . . 9 ⊢ (2 · (𝐹↑2)) = (2 · (𝐹 · 𝐹))
108	106, 107	eqtr4i 2788	. . . . . . . 8 ⊢ ((2 · 𝐹) · 𝐹) = (2 · (𝐹↑2))
109	105, 108	oveq12i 7428	. . . . . . 7 ⊢ (((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) · 𝐹) + ((2 · 𝐹) · 𝐹)) = ((((𝐹↑5) − (2 · (𝐹↑4))) − (𝐹↑3)) + (2 · (𝐹↑2)))
110	86, 109	eqtri 2785	. . . . . 6 ⊢ (((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) + (2 · 𝐹)) · 𝐹) = ((((𝐹↑5) − (2 · (𝐹↑4))) − (𝐹↑3)) + (2 · (𝐹↑2)))
111	110, 34	oveq12i 7428	. . . . 5 ⊢ ((((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) + (2 · 𝐹)) · 𝐹) + (1 · 𝐹)) = (((((𝐹↑5) − (2 · (𝐹↑4))) − (𝐹↑3)) + (2 · (𝐹↑2))) + 𝐹)
112	85, 111	eqtri 2785	. . . 4 ⊢ ((((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) + (2 · 𝐹)) + 1) · 𝐹) = (((((𝐹↑5) − (2 · (𝐹↑4))) − (𝐹↑3)) + (2 · (𝐹↑2))) + 𝐹)
113	82, 4, 62	adddiri 11247	. . . . 5 ⊢ ((((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) + (2 · 𝐹)) + 1) · 2) = ((((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) + (2 · 𝐹)) · 2) + (1 · 2))
114	80, 81, 62	adddiri 11247	. . . . . . 7 ⊢ (((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) + (2 · 𝐹)) · 2) = (((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) · 2) + ((2 · 𝐹) · 2))
115	64, 2, 62	subdiri 11689	. . . . . . . . 9 ⊢ ((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) · 2) = ((((𝐹↑4) − (2 · (𝐹↑3))) · 2) − ((𝐹↑2) · 2))
116	40, 63, 62	subdiri 11689	. . . . . . . . . . 11 ⊢ (((𝐹↑4) − (2 · (𝐹↑3))) · 2) = (((𝐹↑4) · 2) − ((2 · (𝐹↑3)) · 2))
117	40, 62	mulcomi 11242	. . . . . . . . . . . 12 ⊢ ((𝐹↑4) · 2) = (2 · (𝐹↑4))
118	62, 43, 62	mul32i 11431	. . . . . . . . . . . . 13 ⊢ ((2 · (𝐹↑3)) · 2) = ((2 · 2) · (𝐹↑3))
119		2t2e4 12429	. . . . . . . . . . . . . 14 ⊢ (2 · 2) = 4
120	119	oveq1i 7426	. . . . . . . . . . . . 13 ⊢ ((2 · 2) · (𝐹↑3)) = (4 · (𝐹↑3))
121	118, 120	eqtri 2785	. . . . . . . . . . . 12 ⊢ ((2 · (𝐹↑3)) · 2) = (4 · (𝐹↑3))
122	117, 121	oveq12i 7428	. . . . . . . . . . 11 ⊢ (((𝐹↑4) · 2) − ((2 · (𝐹↑3)) · 2)) = ((2 · (𝐹↑4)) − (4 · (𝐹↑3)))
123	116, 122	eqtri 2785	. . . . . . . . . 10 ⊢ (((𝐹↑4) − (2 · (𝐹↑3))) · 2) = ((2 · (𝐹↑4)) − (4 · (𝐹↑3)))
124	2, 62	mulcomi 11242	. . . . . . . . . 10 ⊢ ((𝐹↑2) · 2) = (2 · (𝐹↑2))
125	123, 124	oveq12i 7428	. . . . . . . . 9 ⊢ ((((𝐹↑4) − (2 · (𝐹↑3))) · 2) − ((𝐹↑2) · 2)) = (((2 · (𝐹↑4)) − (4 · (𝐹↑3))) − (2 · (𝐹↑2)))
126	115, 125	eqtri 2785	. . . . . . . 8 ⊢ ((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) · 2) = (((2 · (𝐹↑4)) − (4 · (𝐹↑3))) − (2 · (𝐹↑2)))
127	62, 1, 62	mul32i 11431	. . . . . . . . 9 ⊢ ((2 · 𝐹) · 2) = ((2 · 2) · 𝐹)
128	119	oveq1i 7426	. . . . . . . . 9 ⊢ ((2 · 2) · 𝐹) = (4 · 𝐹)
129	127, 128	eqtri 2785	. . . . . . . 8 ⊢ ((2 · 𝐹) · 2) = (4 · 𝐹)
130	126, 129	oveq12i 7428	. . . . . . 7 ⊢ (((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) · 2) + ((2 · 𝐹) · 2)) = ((((2 · (𝐹↑4)) − (4 · (𝐹↑3))) − (2 · (𝐹↑2))) + (4 · 𝐹))
131	114, 130	eqtri 2785	. . . . . 6 ⊢ (((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) + (2 · 𝐹)) · 2) = ((((2 · (𝐹↑4)) − (4 · (𝐹↑3))) − (2 · (𝐹↑2))) + (4 · 𝐹))
132	62	mullidi 11239	. . . . . 6 ⊢ (1 · 2) = 2
133	131, 132	oveq12i 7428	. . . . 5 ⊢ ((((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) + (2 · 𝐹)) · 2) + (1 · 2)) = (((((2 · (𝐹↑4)) − (4 · (𝐹↑3))) − (2 · (𝐹↑2))) + (4 · 𝐹)) + 2)
134	113, 133	eqtri 2785	. . . 4 ⊢ ((((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) + (2 · 𝐹)) + 1) · 2) = (((((2 · (𝐹↑4)) − (4 · (𝐹↑3))) − (2 · (𝐹↑2))) + (4 · 𝐹)) + 2)
135	112, 134	oveq12i 7428	. . 3 ⊢ (((((((𝐹↑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 12549	. . . . . . . . 9 ⊢ 5 ∈ ℕ₀
137		expcl 14143	. . . . . . . . 9 ⊢ ((𝐹 ∈ ℂ ∧ 5 ∈ ℕ₀) → (𝐹↑5) ∈ ℂ)
138	1, 136, 137	mp2an 705	. . . . . . . 8 ⊢ (𝐹↑5) ∈ ℂ
139	62, 40	mulcli 11241	. . . . . . . 8 ⊢ (2 · (𝐹↑4)) ∈ ℂ
140	138, 139	subcli 11559	. . . . . . 7 ⊢ ((𝐹↑5) − (2 · (𝐹↑4))) ∈ ℂ
141	140, 43	subcli 11559	. . . . . 6 ⊢ (((𝐹↑5) − (2 · (𝐹↑4))) − (𝐹↑3)) ∈ ℂ
142	62, 2	mulcli 11241	. . . . . 6 ⊢ (2 · (𝐹↑2)) ∈ ℂ
143	141, 142	addcli 11240	. . . . 5 ⊢ ((((𝐹↑5) − (2 · (𝐹↑4))) − (𝐹↑3)) + (2 · (𝐹↑2))) ∈ ℂ
144	143, 1	addcli 11240	. . . 4 ⊢ (((((𝐹↑5) − (2 · (𝐹↑4))) − (𝐹↑3)) + (2 · (𝐹↑2))) + 𝐹) ∈ ℂ
145		4cn 12351	. . . . . . . 8 ⊢ 4 ∈ ℂ
146	145, 43	mulcli 11241	. . . . . . 7 ⊢ (4 · (𝐹↑3)) ∈ ℂ
147	139, 146	subcli 11559	. . . . . 6 ⊢ ((2 · (𝐹↑4)) − (4 · (𝐹↑3))) ∈ ℂ
148	147, 142	subcli 11559	. . . . 5 ⊢ (((2 · (𝐹↑4)) − (4 · (𝐹↑3))) − (2 · (𝐹↑2))) ∈ ℂ
149	145, 1	mulcli 11241	. . . . 5 ⊢ (4 · 𝐹) ∈ ℂ
150	148, 149	addcli 11240	. . . 4 ⊢ ((((2 · (𝐹↑4)) − (4 · (𝐹↑3))) − (2 · (𝐹↑2))) + (4 · 𝐹)) ∈ ℂ
151	144, 150, 62	addassi 11244	. . 3 ⊢ (((((((𝐹↑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 11460	. . . . 5 ⊢ ((((((𝐹↑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 11525	. . . . . . . 8 ⊢ (((((𝐹↑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 1490	. . . . . . 7 ⊢ (((((𝐹↑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 11579	. . . . . . 7 ⊢ ((((𝐹↑5) − (2 · (𝐹↑4))) + (2 · (𝐹↑4))) − ((𝐹↑3) + (4 · (𝐹↑3)))) = ((((𝐹↑5) − (2 · (𝐹↑4))) − (𝐹↑3)) + ((2 · (𝐹↑4)) − (4 · (𝐹↑3))))
156		npcan 11491	. . . . . . . . 9 ⊢ (((𝐹↑5) ∈ ℂ ∧ (2 · (𝐹↑4)) ∈ ℂ) → (((𝐹↑5) − (2 · (𝐹↑4))) + (2 · (𝐹↑4))) = (𝐹↑5))
157	138, 139, 156	mp2an 705	. . . . . . . 8 ⊢ (((𝐹↑5) − (2 · (𝐹↑4))) + (2 · (𝐹↑4))) = (𝐹↑5)
158	145, 4, 89	comraddi 11450	. . . . . . . . . 10 ⊢ 5 = (1 + 4)
159	158	oveq1i 7426	. . . . . . . . 9 ⊢ (5 · (𝐹↑3)) = ((1 + 4) · (𝐹↑3))
160	4, 145, 43	adddiri 11247	. . . . . . . . 9 ⊢ ((1 + 4) · (𝐹↑3)) = ((1 · (𝐹↑3)) + (4 · (𝐹↑3)))
161	43	mullidi 11239	. . . . . . . . . 10 ⊢ (1 · (𝐹↑3)) = (𝐹↑3)
162	161	oveq1i 7426	. . . . . . . . 9 ⊢ ((1 · (𝐹↑3)) + (4 · (𝐹↑3))) = ((𝐹↑3) + (4 · (𝐹↑3)))
163	159, 160, 162	3eqtrri 2790	. . . . . . . 8 ⊢ ((𝐹↑3) + (4 · (𝐹↑3))) = (5 · (𝐹↑3))
164	157, 163	oveq12i 7428	. . . . . . 7 ⊢ ((((𝐹↑5) − (2 · (𝐹↑4))) + (2 · (𝐹↑4))) − ((𝐹↑3) + (4 · (𝐹↑3)))) = ((𝐹↑5) − (5 · (𝐹↑3)))
165	154, 155, 164	3eqtr2i 2791	. . . . . 6 ⊢ (((((𝐹↑5) − (2 · (𝐹↑4))) − (𝐹↑3)) + (2 · (𝐹↑2))) + (((2 · (𝐹↑4)) − (4 · (𝐹↑3))) − (2 · (𝐹↑2)))) = ((𝐹↑5) − (5 · (𝐹↑3)))
166	4, 145, 1	adddiri 11247	. . . . . . 7 ⊢ ((1 + 4) · 𝐹) = ((1 · 𝐹) + (4 · 𝐹))
167	158	oveq1i 7426	. . . . . . 7 ⊢ (5 · 𝐹) = ((1 + 4) · 𝐹)
168	34	eqcomi 2771	. . . . . . . 8 ⊢ 𝐹 = (1 · 𝐹)
169	168	oveq1i 7426	. . . . . . 7 ⊢ (𝐹 + (4 · 𝐹)) = ((1 · 𝐹) + (4 · 𝐹))
170	166, 167, 169	3eqtr4ri 2796	. . . . . 6 ⊢ (𝐹 + (4 · 𝐹)) = (5 · 𝐹)
171	165, 170	oveq12i 7428	. . . . 5 ⊢ ((((((𝐹↑5) − (2 · (𝐹↑4))) − (𝐹↑3)) + (2 · (𝐹↑2))) + (((2 · (𝐹↑4)) − (4 · (𝐹↑3))) − (2 · (𝐹↑2)))) + (𝐹 + (4 · 𝐹))) = (((𝐹↑5) − (5 · (𝐹↑3))) + (5 · 𝐹))
172	152, 171	eqtri 2785	. . . 4 ⊢ ((((((𝐹↑5) − (2 · (𝐹↑4))) − (𝐹↑3)) + (2 · (𝐹↑2))) + 𝐹) + ((((2 · (𝐹↑4)) − (4 · (𝐹↑3))) − (2 · (𝐹↑2))) + (4 · 𝐹))) = (((𝐹↑5) − (5 · (𝐹↑3))) + (5 · 𝐹))
173	172	oveq1i 7426	. . 3 ⊢ (((((((𝐹↑5) − (2 · (𝐹↑4))) − (𝐹↑3)) + (2 · (𝐹↑2))) + 𝐹) + ((((2 · (𝐹↑4)) − (4 · (𝐹↑3))) − (2 · (𝐹↑2))) + (4 · 𝐹))) + 2) = ((((𝐹↑5) − (5 · (𝐹↑3))) + (5 · 𝐹)) + 2)
174	135, 151, 173	3eqtr2i 2791	. 2 ⊢ (((((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) + (2 · 𝐹)) + 1) · 𝐹) + ((((((𝐹↑4) − (2 · (𝐹↑3))) − (𝐹↑2)) + (2 · 𝐹)) + 1) · 2)) = ((((𝐹↑5) − (5 · (𝐹↑3))) + (5 · 𝐹)) + 2)
175	79, 84, 174	3eqtri 2789	1 ⊢ (((((𝐹↑2) − 𝐹) − 1) · (((𝐹↑2) − 𝐹) − 1)) · (𝐹 + 2)) = ((((𝐹↑5) − (5 · (𝐹↑3))) + (5 · 𝐹)) + 2)

Colors of variables: wff setvar class

This proof depends on syntax axioms: = wceq 1570 ⊤wtru 1571 ∈ wcel 2145 (class class class)co 7416 ℂcc 11123 1c1 11126 + caddc 11128 · cmul 11130 − cmin 11466 2c2 12320 3c3 12321 4c4 12322 5c5 12323 ℕ₀cn0 12529 ↑cexp 14125

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7739 ax-cnex 11181 ax-resscn 11182 ax-1cn 11183 ax-icn 11184 ax-addcl 11185 ax-addrcl 11186 ax-mulcl 11187 ax-mulrcl 11188 ax-mulcom 11189 ax-addass 11190 ax-mulass 11191 ax-distr 11192 ax-i2m1 11193 ax-1ne0 11194 ax-1rid 11195 ax-rnegex 11196 ax-rrecex 11197 ax-cnre 11198 ax-pre-lttri 11199 ax-pre-lttrn 11200 ax-pre-ltadd 11201 ax-pre-mulgt0 11202

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4871 df-iun 4956 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-om 7866 df-2nd 7990 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-er 8699 df-en 8956 df-dom 8957 df-sdom 8958 df-pnf 11270 df-mnf 11271 df-xr 11272 df-ltxr 11273 df-le 11274 df-sub 11468 df-neg 11469 df-nn 12259 df-2 12328 df-3 12329 df-4 12330 df-5 12331 df-n0 12530 df-z 12617 df-uz 12889 df-seq 14066 df-exp 14126

This theorem is used by: goldratmolem4 47738

W3C validator