binom4 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > binom4		GIF version

Theorem binom4 15369

Description: Work out a quartic binomial. (You would think that by this point it would be faster to use binom 11714, but it turns out to be just as much work to put it into this form after clearing all the sums and calculating binomial coefficients.) (Contributed by Mario Carneiro, 6-May-2015.)

**Assertion**
Ref	Expression
binom4	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑4) = (((𝐴↑4) + (4 · ((𝐴↑3) · 𝐵))) + ((6 · ((𝐴↑2) · (𝐵↑2))) + ((4 · (𝐴 · (𝐵↑3))) + (𝐵↑4)))))

**Proof of Theorem binom4**
Step	Hyp	Ref	Expression
1		df-4 9079	. . . 4 ⊢ 4 = (3 + 1)
2	1	oveq2i 5945	. . 3 ⊢ ((𝐴 + 𝐵)↑4) = ((𝐴 + 𝐵)↑(3 + 1))
3		addcl 8032	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
4		3nn0 9295	. . . 4 ⊢ 3 ∈ ℕ₀
5		expp1 10672	. . . 4 ⊢ (((𝐴 + 𝐵) ∈ ℂ ∧ 3 ∈ ℕ₀) → ((𝐴 + 𝐵)↑(3 + 1)) = (((𝐴 + 𝐵)↑3) · (𝐴 + 𝐵)))
6	3, 4, 5	sylancl 413	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑(3 + 1)) = (((𝐴 + 𝐵)↑3) · (𝐴 + 𝐵)))
7	2, 6	eqtrid 2249	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑4) = (((𝐴 + 𝐵)↑3) · (𝐴 + 𝐵)))
8		binom3 10783	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑3) = (((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3))))
9	8	oveq1d 5949	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵)↑3) · (𝐴 + 𝐵)) = ((((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3))) · (𝐴 + 𝐵)))
10		simpl 109	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈ ℂ)
11		expcl 10683	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝐴↑3) ∈ ℂ)
12	10, 4, 11	sylancl 413	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑3) ∈ ℂ)
13		3cn 9093	. . . . . . 7 ⊢ 3 ∈ ℂ
14	10	sqcld 10797	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑2) ∈ ℂ)
15		simpr 110	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
16	14, 15	mulcld 8075	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) · 𝐵) ∈ ℂ)
17		mulcl 8034	. . . . . . 7 ⊢ ((3 ∈ ℂ ∧ ((𝐴↑2) · 𝐵) ∈ ℂ) → (3 · ((𝐴↑2) · 𝐵)) ∈ ℂ)
18	13, 16, 17	sylancr 414	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (3 · ((𝐴↑2) · 𝐵)) ∈ ℂ)
19	12, 18	addcld 8074	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) ∈ ℂ)
20	15	sqcld 10797	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑2) ∈ ℂ)
21	10, 20	mulcld 8075	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · (𝐵↑2)) ∈ ℂ)
22		mulcl 8034	. . . . . . 7 ⊢ ((3 ∈ ℂ ∧ (𝐴 · (𝐵↑2)) ∈ ℂ) → (3 · (𝐴 · (𝐵↑2))) ∈ ℂ)
23	13, 21, 22	sylancr 414	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (3 · (𝐴 · (𝐵↑2))) ∈ ℂ)
24		expcl 10683	. . . . . . 7 ⊢ ((𝐵 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝐵↑3) ∈ ℂ)
25	15, 4, 24	sylancl 413	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑3) ∈ ℂ)
26	23, 25	addcld 8074	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3)) ∈ ℂ)
27	19, 26	addcld 8074	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3))) ∈ ℂ)
28	27, 10, 15	adddid 8079	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3))) · (𝐴 + 𝐵)) = (((((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3))) · 𝐴) + ((((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3))) · 𝐵)))
29	1	oveq2i 5945	. . . . . . . . 9 ⊢ (𝐴↑4) = (𝐴↑(3 + 1))
30		expp1 10672	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝐴↑(3 + 1)) = ((𝐴↑3) · 𝐴))
31	10, 4, 30	sylancl 413	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑(3 + 1)) = ((𝐴↑3) · 𝐴))
32	29, 31	eqtr2id 2250	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑3) · 𝐴) = (𝐴↑4))
33	13	a1i 9	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 3 ∈ ℂ)
34	33, 16, 10	mulassd 8078	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3 · ((𝐴↑2) · 𝐵)) · 𝐴) = (3 · (((𝐴↑2) · 𝐵) · 𝐴)))
35	14, 15, 10	mul32d 8207	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑2) · 𝐵) · 𝐴) = (((𝐴↑2) · 𝐴) · 𝐵))
36		df-3 9078	. . . . . . . . . . . . . 14 ⊢ 3 = (2 + 1)
37	36	oveq2i 5945	. . . . . . . . . . . . 13 ⊢ (𝐴↑3) = (𝐴↑(2 + 1))
38		2nn0 9294	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℕ₀
39		expp1 10672	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ 2 ∈ ℕ₀) → (𝐴↑(2 + 1)) = ((𝐴↑2) · 𝐴))
40	10, 38, 39	sylancl 413	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑(2 + 1)) = ((𝐴↑2) · 𝐴))
41	37, 40	eqtr2id 2250	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) · 𝐴) = (𝐴↑3))
42	41	oveq1d 5949	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑2) · 𝐴) · 𝐵) = ((𝐴↑3) · 𝐵))
43	35, 42	eqtrd 2237	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑2) · 𝐵) · 𝐴) = ((𝐴↑3) · 𝐵))
44	43	oveq2d 5950	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (3 · (((𝐴↑2) · 𝐵) · 𝐴)) = (3 · ((𝐴↑3) · 𝐵)))
45	34, 44	eqtrd 2237	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3 · ((𝐴↑2) · 𝐵)) · 𝐴) = (3 · ((𝐴↑3) · 𝐵)))
46	32, 45	oveq12d 5952	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑3) · 𝐴) + ((3 · ((𝐴↑2) · 𝐵)) · 𝐴)) = ((𝐴↑4) + (3 · ((𝐴↑3) · 𝐵))))
47	12, 10, 18, 46	joinlmuladdmuld 8082	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) · 𝐴) = ((𝐴↑4) + (3 · ((𝐴↑3) · 𝐵))))
48	33, 21, 10	mulassd 8078	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3 · (𝐴 · (𝐵↑2))) · 𝐴) = (3 · ((𝐴 · (𝐵↑2)) · 𝐴)))
49	10, 20, 10	mul32d 8207	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · (𝐵↑2)) · 𝐴) = ((𝐴 · 𝐴) · (𝐵↑2)))
50	10	sqvald 10796	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑2) = (𝐴 · 𝐴))
51	50	oveq1d 5949	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) · (𝐵↑2)) = ((𝐴 · 𝐴) · (𝐵↑2)))
52	49, 51	eqtr4d 2240	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · (𝐵↑2)) · 𝐴) = ((𝐴↑2) · (𝐵↑2)))
53	52	oveq2d 5950	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (3 · ((𝐴 · (𝐵↑2)) · 𝐴)) = (3 · ((𝐴↑2) · (𝐵↑2))))
54	48, 53	eqtrd 2237	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3 · (𝐴 · (𝐵↑2))) · 𝐴) = (3 · ((𝐴↑2) · (𝐵↑2))))
55	25, 10	mulcomd 8076	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐵↑3) · 𝐴) = (𝐴 · (𝐵↑3)))
56	54, 55	oveq12d 5952	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((3 · (𝐴 · (𝐵↑2))) · 𝐴) + ((𝐵↑3) · 𝐴)) = ((3 · ((𝐴↑2) · (𝐵↑2))) + (𝐴 · (𝐵↑3))))
57	23, 10, 25, 56	joinlmuladdmuld 8082	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3)) · 𝐴) = ((3 · ((𝐴↑2) · (𝐵↑2))) + (𝐴 · (𝐵↑3))))
58	47, 57	oveq12d 5952	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) · 𝐴) + (((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3)) · 𝐴)) = (((𝐴↑4) + (3 · ((𝐴↑3) · 𝐵))) + ((3 · ((𝐴↑2) · (𝐵↑2))) + (𝐴 · (𝐵↑3)))))
59	19, 10, 26, 58	joinlmuladdmuld 8082	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3))) · 𝐴) = (((𝐴↑4) + (3 · ((𝐴↑3) · 𝐵))) + ((3 · ((𝐴↑2) · (𝐵↑2))) + (𝐴 · (𝐵↑3)))))
60	19, 26, 15	adddird 8080	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3))) · 𝐵) = ((((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) · 𝐵) + (((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3)) · 𝐵)))
61	33, 16, 15	mulassd 8078	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3 · ((𝐴↑2) · 𝐵)) · 𝐵) = (3 · (((𝐴↑2) · 𝐵) · 𝐵)))
62	14, 15, 15	mulassd 8078	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑2) · 𝐵) · 𝐵) = ((𝐴↑2) · (𝐵 · 𝐵)))
63	15	sqvald 10796	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑2) = (𝐵 · 𝐵))
64	63	oveq2d 5950	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) · (𝐵↑2)) = ((𝐴↑2) · (𝐵 · 𝐵)))
65	62, 64	eqtr4d 2240	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑2) · 𝐵) · 𝐵) = ((𝐴↑2) · (𝐵↑2)))
66	65	oveq2d 5950	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (3 · (((𝐴↑2) · 𝐵) · 𝐵)) = (3 · ((𝐴↑2) · (𝐵↑2))))
67	61, 66	eqtrd 2237	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3 · ((𝐴↑2) · 𝐵)) · 𝐵) = (3 · ((𝐴↑2) · (𝐵↑2))))
68	67	oveq2d 5950	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑3) · 𝐵) + ((3 · ((𝐴↑2) · 𝐵)) · 𝐵)) = (((𝐴↑3) · 𝐵) + (3 · ((𝐴↑2) · (𝐵↑2)))))
69	12, 15, 18, 68	joinlmuladdmuld 8082	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) · 𝐵) = (((𝐴↑3) · 𝐵) + (3 · ((𝐴↑2) · (𝐵↑2)))))
70	33, 21, 15	mulassd 8078	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3 · (𝐴 · (𝐵↑2))) · 𝐵) = (3 · ((𝐴 · (𝐵↑2)) · 𝐵)))
71	10, 20, 15	mulassd 8078	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · (𝐵↑2)) · 𝐵) = (𝐴 · ((𝐵↑2) · 𝐵)))
72	36	oveq2i 5945	. . . . . . . . . . . . 13 ⊢ (𝐵↑3) = (𝐵↑(2 + 1))
73		expp1 10672	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℂ ∧ 2 ∈ ℕ₀) → (𝐵↑(2 + 1)) = ((𝐵↑2) · 𝐵))
74	15, 38, 73	sylancl 413	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑(2 + 1)) = ((𝐵↑2) · 𝐵))
75	72, 74	eqtr2id 2250	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐵↑2) · 𝐵) = (𝐵↑3))
76	75	oveq2d 5950	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · ((𝐵↑2) · 𝐵)) = (𝐴 · (𝐵↑3)))
77	71, 76	eqtrd 2237	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · (𝐵↑2)) · 𝐵) = (𝐴 · (𝐵↑3)))
78	77	oveq2d 5950	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (3 · ((𝐴 · (𝐵↑2)) · 𝐵)) = (3 · (𝐴 · (𝐵↑3))))
79	70, 78	eqtrd 2237	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3 · (𝐴 · (𝐵↑2))) · 𝐵) = (3 · (𝐴 · (𝐵↑3))))
80	1	oveq2i 5945	. . . . . . . . 9 ⊢ (𝐵↑4) = (𝐵↑(3 + 1))
81		expp1 10672	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝐵↑(3 + 1)) = ((𝐵↑3) · 𝐵))
82	15, 4, 81	sylancl 413	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑(3 + 1)) = ((𝐵↑3) · 𝐵))
83	80, 82	eqtr2id 2250	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐵↑3) · 𝐵) = (𝐵↑4))
84	79, 83	oveq12d 5952	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((3 · (𝐴 · (𝐵↑2))) · 𝐵) + ((𝐵↑3) · 𝐵)) = ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4)))
85	23, 15, 25, 84	joinlmuladdmuld 8082	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3)) · 𝐵) = ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4)))
86	69, 85	oveq12d 5952	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) · 𝐵) + (((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3)) · 𝐵)) = ((((𝐴↑3) · 𝐵) + (3 · ((𝐴↑2) · (𝐵↑2)))) + ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4))))
87	12, 15	mulcld 8075	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑3) · 𝐵) ∈ ℂ)
88	14, 20	mulcld 8075	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) · (𝐵↑2)) ∈ ℂ)
89		mulcl 8034	. . . . . . 7 ⊢ ((3 ∈ ℂ ∧ ((𝐴↑2) · (𝐵↑2)) ∈ ℂ) → (3 · ((𝐴↑2) · (𝐵↑2))) ∈ ℂ)
90	13, 88, 89	sylancr 414	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (3 · ((𝐴↑2) · (𝐵↑2))) ∈ ℂ)
91	10, 25	mulcld 8075	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · (𝐵↑3)) ∈ ℂ)
92		mulcl 8034	. . . . . . . 8 ⊢ ((3 ∈ ℂ ∧ (𝐴 · (𝐵↑3)) ∈ ℂ) → (3 · (𝐴 · (𝐵↑3))) ∈ ℂ)
93	13, 91, 92	sylancr 414	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (3 · (𝐴 · (𝐵↑3))) ∈ ℂ)
94		4nn0 9296	. . . . . . . 8 ⊢ 4 ∈ ℕ₀
95		expcl 10683	. . . . . . . 8 ⊢ ((𝐵 ∈ ℂ ∧ 4 ∈ ℕ₀) → (𝐵↑4) ∈ ℂ)
96	15, 94, 95	sylancl 413	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑4) ∈ ℂ)
97	93, 96	addcld 8074	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4)) ∈ ℂ)
98	87, 90, 97	addassd 8077	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑3) · 𝐵) + (3 · ((𝐴↑2) · (𝐵↑2)))) + ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4))) = (((𝐴↑3) · 𝐵) + ((3 · ((𝐴↑2) · (𝐵↑2))) + ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4)))))
99	60, 86, 98	3eqtrd 2241	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3))) · 𝐵) = (((𝐴↑3) · 𝐵) + ((3 · ((𝐴↑2) · (𝐵↑2))) + ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4)))))
100	59, 99	oveq12d 5952	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3))) · 𝐴) + ((((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3))) · 𝐵)) = ((((𝐴↑4) + (3 · ((𝐴↑3) · 𝐵))) + ((3 · ((𝐴↑2) · (𝐵↑2))) + (𝐴 · (𝐵↑3)))) + (((𝐴↑3) · 𝐵) + ((3 · ((𝐴↑2) · (𝐵↑2))) + ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4))))))
101		expcl 10683	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 4 ∈ ℕ₀) → (𝐴↑4) ∈ ℂ)
102	10, 94, 101	sylancl 413	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑4) ∈ ℂ)
103		mulcl 8034	. . . . . . 7 ⊢ ((3 ∈ ℂ ∧ ((𝐴↑3) · 𝐵) ∈ ℂ) → (3 · ((𝐴↑3) · 𝐵)) ∈ ℂ)
104	13, 87, 103	sylancr 414	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (3 · ((𝐴↑3) · 𝐵)) ∈ ℂ)
105	102, 104	addcld 8074	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑4) + (3 · ((𝐴↑3) · 𝐵))) ∈ ℂ)
106	90, 91	addcld 8074	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3 · ((𝐴↑2) · (𝐵↑2))) + (𝐴 · (𝐵↑3))) ∈ ℂ)
107	90, 97	addcld 8074	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3 · ((𝐴↑2) · (𝐵↑2))) + ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4))) ∈ ℂ)
108	105, 106, 87, 107	add4d 8223	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑4) + (3 · ((𝐴↑3) · 𝐵))) + ((3 · ((𝐴↑2) · (𝐵↑2))) + (𝐴 · (𝐵↑3)))) + (((𝐴↑3) · 𝐵) + ((3 · ((𝐴↑2) · (𝐵↑2))) + ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4))))) = ((((𝐴↑4) + (3 · ((𝐴↑3) · 𝐵))) + ((𝐴↑3) · 𝐵)) + (((3 · ((𝐴↑2) · (𝐵↑2))) + (𝐴 · (𝐵↑3))) + ((3 · ((𝐴↑2) · (𝐵↑2))) + ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4))))))
109	102, 104, 87	addassd 8077	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑4) + (3 · ((𝐴↑3) · 𝐵))) + ((𝐴↑3) · 𝐵)) = ((𝐴↑4) + ((3 · ((𝐴↑3) · 𝐵)) + ((𝐴↑3) · 𝐵))))
110	1	oveq1i 5944	. . . . . . . . 9 ⊢ (4 · ((𝐴↑3) · 𝐵)) = ((3 + 1) · ((𝐴↑3) · 𝐵))
111		ax-1cn 8000	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
112	111	a1i 9	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 1 ∈ ℂ)
113	33, 112, 87	adddird 8080	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3 + 1) · ((𝐴↑3) · 𝐵)) = ((3 · ((𝐴↑3) · 𝐵)) + (1 · ((𝐴↑3) · 𝐵))))
114	110, 113	eqtrid 2249	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (4 · ((𝐴↑3) · 𝐵)) = ((3 · ((𝐴↑3) · 𝐵)) + (1 · ((𝐴↑3) · 𝐵))))
115	87	mulid2d 8073	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1 · ((𝐴↑3) · 𝐵)) = ((𝐴↑3) · 𝐵))
116	115	oveq2d 5950	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3 · ((𝐴↑3) · 𝐵)) + (1 · ((𝐴↑3) · 𝐵))) = ((3 · ((𝐴↑3) · 𝐵)) + ((𝐴↑3) · 𝐵)))
117	114, 116	eqtrd 2237	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (4 · ((𝐴↑3) · 𝐵)) = ((3 · ((𝐴↑3) · 𝐵)) + ((𝐴↑3) · 𝐵)))
118	117	oveq2d 5950	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑4) + (4 · ((𝐴↑3) · 𝐵))) = ((𝐴↑4) + ((3 · ((𝐴↑3) · 𝐵)) + ((𝐴↑3) · 𝐵))))
119	109, 118	eqtr4d 2240	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑4) + (3 · ((𝐴↑3) · 𝐵))) + ((𝐴↑3) · 𝐵)) = ((𝐴↑4) + (4 · ((𝐴↑3) · 𝐵))))
120	90, 91, 90, 97	add4d 8223	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((3 · ((𝐴↑2) · (𝐵↑2))) + (𝐴 · (𝐵↑3))) + ((3 · ((𝐴↑2) · (𝐵↑2))) + ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4)))) = (((3 · ((𝐴↑2) · (𝐵↑2))) + (3 · ((𝐴↑2) · (𝐵↑2)))) + ((𝐴 · (𝐵↑3)) + ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4)))))
121		3p3e6 9161	. . . . . . . . 9 ⊢ (3 + 3) = 6
122	121	oveq1i 5944	. . . . . . . 8 ⊢ ((3 + 3) · ((𝐴↑2) · (𝐵↑2))) = (6 · ((𝐴↑2) · (𝐵↑2)))
123	33, 33, 88	adddird 8080	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3 + 3) · ((𝐴↑2) · (𝐵↑2))) = ((3 · ((𝐴↑2) · (𝐵↑2))) + (3 · ((𝐴↑2) · (𝐵↑2)))))
124	122, 123	eqtr3id 2251	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (6 · ((𝐴↑2) · (𝐵↑2))) = ((3 · ((𝐴↑2) · (𝐵↑2))) + (3 · ((𝐴↑2) · (𝐵↑2)))))
125		3p1e4 9154	. . . . . . . . . . . . 13 ⊢ (3 + 1) = 4
126	13, 111, 125	addcomli 8199	. . . . . . . . . . . 12 ⊢ (1 + 3) = 4
127	126	oveq1i 5944	. . . . . . . . . . 11 ⊢ ((1 + 3) · (𝐴 · (𝐵↑3))) = (4 · (𝐴 · (𝐵↑3)))
128	112, 33, 91	adddird 8080	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((1 + 3) · (𝐴 · (𝐵↑3))) = ((1 · (𝐴 · (𝐵↑3))) + (3 · (𝐴 · (𝐵↑3)))))
129	127, 128	eqtr3id 2251	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (4 · (𝐴 · (𝐵↑3))) = ((1 · (𝐴 · (𝐵↑3))) + (3 · (𝐴 · (𝐵↑3)))))
130	91	mulid2d 8073	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1 · (𝐴 · (𝐵↑3))) = (𝐴 · (𝐵↑3)))
131	130	oveq1d 5949	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((1 · (𝐴 · (𝐵↑3))) + (3 · (𝐴 · (𝐵↑3)))) = ((𝐴 · (𝐵↑3)) + (3 · (𝐴 · (𝐵↑3)))))
132	129, 131	eqtrd 2237	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (4 · (𝐴 · (𝐵↑3))) = ((𝐴 · (𝐵↑3)) + (3 · (𝐴 · (𝐵↑3)))))
133	132	oveq1d 5949	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((4 · (𝐴 · (𝐵↑3))) + (𝐵↑4)) = (((𝐴 · (𝐵↑3)) + (3 · (𝐴 · (𝐵↑3)))) + (𝐵↑4)))
134	91, 93, 96	addassd 8077	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 · (𝐵↑3)) + (3 · (𝐴 · (𝐵↑3)))) + (𝐵↑4)) = ((𝐴 · (𝐵↑3)) + ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4))))
135	133, 134	eqtrd 2237	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((4 · (𝐴 · (𝐵↑3))) + (𝐵↑4)) = ((𝐴 · (𝐵↑3)) + ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4))))
136	124, 135	oveq12d 5952	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((6 · ((𝐴↑2) · (𝐵↑2))) + ((4 · (𝐴 · (𝐵↑3))) + (𝐵↑4))) = (((3 · ((𝐴↑2) · (𝐵↑2))) + (3 · ((𝐴↑2) · (𝐵↑2)))) + ((𝐴 · (𝐵↑3)) + ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4)))))
137	120, 136	eqtr4d 2240	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((3 · ((𝐴↑2) · (𝐵↑2))) + (𝐴 · (𝐵↑3))) + ((3 · ((𝐴↑2) · (𝐵↑2))) + ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4)))) = ((6 · ((𝐴↑2) · (𝐵↑2))) + ((4 · (𝐴 · (𝐵↑3))) + (𝐵↑4))))
138	119, 137	oveq12d 5952	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑4) + (3 · ((𝐴↑3) · 𝐵))) + ((𝐴↑3) · 𝐵)) + (((3 · ((𝐴↑2) · (𝐵↑2))) + (𝐴 · (𝐵↑3))) + ((3 · ((𝐴↑2) · (𝐵↑2))) + ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4))))) = (((𝐴↑4) + (4 · ((𝐴↑3) · 𝐵))) + ((6 · ((𝐴↑2) · (𝐵↑2))) + ((4 · (𝐴 · (𝐵↑3))) + (𝐵↑4)))))
139	108, 138	eqtrd 2237	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑4) + (3 · ((𝐴↑3) · 𝐵))) + ((3 · ((𝐴↑2) · (𝐵↑2))) + (𝐴 · (𝐵↑3)))) + (((𝐴↑3) · 𝐵) + ((3 · ((𝐴↑2) · (𝐵↑2))) + ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4))))) = (((𝐴↑4) + (4 · ((𝐴↑3) · 𝐵))) + ((6 · ((𝐴↑2) · (𝐵↑2))) + ((4 · (𝐴 · (𝐵↑3))) + (𝐵↑4)))))
140	28, 100, 139	3eqtrd 2241	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3))) · (𝐴 + 𝐵)) = (((𝐴↑4) + (4 · ((𝐴↑3) · 𝐵))) + ((6 · ((𝐴↑2) · (𝐵↑2))) + ((4 · (𝐴 · (𝐵↑3))) + (𝐵↑4)))))
141	7, 9, 140	3eqtrd 2241	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑4) = (((𝐴↑4) + (4 · ((𝐴↑3) · 𝐵))) + ((6 · ((𝐴↑2) · (𝐵↑2))) + ((4 · (𝐴 · (𝐵↑3))) + (𝐵↑4)))))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 = wceq 1372 ∈ wcel 2175 (class class class)co 5934 ℂcc 7905 1c1 7908 + caddc 7910 · cmul 7912 2c2 9069 3c3 9070 4c4 9071 6c6 9073 ℕ₀cn0 9277 ↑cexp 10664

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1469 ax-7 1470 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-8 1526 ax-10 1527 ax-11 1528 ax-i12 1529 ax-bndl 1531 ax-4 1532 ax-17 1548 ax-i9 1552 ax-ial 1556 ax-i5r 1557 ax-13 2177 ax-14 2178 ax-ext 2186 ax-coll 4158 ax-sep 4161 ax-nul 4169 ax-pow 4217 ax-pr 4252 ax-un 4478 ax-setind 4583 ax-iinf 4634 ax-cnex 7998 ax-resscn 7999 ax-1cn 8000 ax-1re 8001 ax-icn 8002 ax-addcl 8003 ax-addrcl 8004 ax-mulcl 8005 ax-mulrcl 8006 ax-addcom 8007 ax-mulcom 8008 ax-addass 8009 ax-mulass 8010 ax-distr 8011 ax-i2m1 8012 ax-0lt1 8013 ax-1rid 8014 ax-0id 8015 ax-rnegex 8016 ax-precex 8017 ax-cnre 8018 ax-pre-ltirr 8019 ax-pre-ltwlin 8020 ax-pre-lttrn 8021 ax-pre-apti 8022 ax-pre-ltadd 8023 ax-pre-mulgt0 8024 ax-pre-mulext 8025

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1375 df-fal 1378 df-nf 1483 df-sb 1785 df-eu 2056 df-mo 2057 df-clab 2191 df-cleq 2197 df-clel 2200 df-nfc 2336 df-ne 2376 df-nel 2471 df-ral 2488 df-rex 2489 df-reu 2490 df-rmo 2491 df-rab 2492 df-v 2773 df-sbc 2998 df-csb 3093 df-dif 3167 df-un 3169 df-in 3171 df-ss 3178 df-nul 3460 df-if 3571 df-pw 3617 df-sn 3638 df-pr 3639 df-op 3641 df-uni 3850 df-int 3885 df-iun 3928 df-br 4044 df-opab 4105 df-mpt 4106 df-tr 4142 df-id 4338 df-po 4341 df-iso 4342 df-iord 4411 df-on 4413 df-ilim 4414 df-suc 4416 df-iom 4637 df-xp 4679 df-rel 4680 df-cnv 4681 df-co 4682 df-dm 4683 df-rn 4684 df-res 4685 df-ima 4686 df-iota 5229 df-fun 5270 df-fn 5271 df-f 5272 df-f1 5273 df-fo 5274 df-f1o 5275 df-fv 5276 df-riota 5889 df-ov 5937 df-oprab 5938 df-mpo 5939 df-1st 6216 df-2nd 6217 df-recs 6381 df-frec 6467 df-pnf 8091 df-mnf 8092 df-xr 8093 df-ltxr 8094 df-le 8095 df-sub 8227 df-neg 8228 df-reap 8630 df-ap 8637 df-div 8728 df-inn 9019 df-2 9077 df-3 9078 df-4 9079 df-5 9080 df-6 9081 df-n0 9278 df-z 9355 df-uz 9631 df-seqfrec 10574 df-exp 10665

This theorem is referenced by: (None)

W3C validator