binom4 - Intuitionistic Logic Explorer

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

Theorem binom4 14780

Description: Work out a quartic binomial. (You would think that by this point it would be faster to use binom 11509, 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 8997	. . . 4 ⊢ 4 = (3 + 1)
2	1	oveq2i 5901	. . 3 ⊢ ((𝐴 + 𝐵)↑4) = ((𝐴 + 𝐵)↑(3 + 1))
3		addcl 7953	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
4		3nn0 9211	. . . 4 ⊢ 3 ∈ ℕ₀
5		expp1 10544	. . . 4 ⊢ (((𝐴 + 𝐵) ∈ ℂ ∧ 3 ∈ ℕ₀) → ((𝐴 + 𝐵)↑(3 + 1)) = (((𝐴 + 𝐵)↑3) · (𝐴 + 𝐵)))
6	3, 4, 5	sylancl 413	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑(3 + 1)) = (((𝐴 + 𝐵)↑3) · (𝐴 + 𝐵)))
7	2, 6	eqtrid 2233	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑4) = (((𝐴 + 𝐵)↑3) · (𝐴 + 𝐵)))
8		binom3 10655	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑3) = (((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3))))
9	8	oveq1d 5905	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵)↑3) · (𝐴 + 𝐵)) = ((((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3))) · (𝐴 + 𝐵)))
10		simpl 109	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈ ℂ)
11		expcl 10555	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝐴↑3) ∈ ℂ)
12	10, 4, 11	sylancl 413	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑3) ∈ ℂ)
13		3cn 9011	. . . . . . 7 ⊢ 3 ∈ ℂ
14	10	sqcld 10669	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑2) ∈ ℂ)
15		simpr 110	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
16	14, 15	mulcld 7995	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) · 𝐵) ∈ ℂ)
17		mulcl 7955	. . . . . . 7 ⊢ ((3 ∈ ℂ ∧ ((𝐴↑2) · 𝐵) ∈ ℂ) → (3 · ((𝐴↑2) · 𝐵)) ∈ ℂ)
18	13, 16, 17	sylancr 414	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (3 · ((𝐴↑2) · 𝐵)) ∈ ℂ)
19	12, 18	addcld 7994	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) ∈ ℂ)
20	15	sqcld 10669	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑2) ∈ ℂ)
21	10, 20	mulcld 7995	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · (𝐵↑2)) ∈ ℂ)
22		mulcl 7955	. . . . . . 7 ⊢ ((3 ∈ ℂ ∧ (𝐴 · (𝐵↑2)) ∈ ℂ) → (3 · (𝐴 · (𝐵↑2))) ∈ ℂ)
23	13, 21, 22	sylancr 414	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (3 · (𝐴 · (𝐵↑2))) ∈ ℂ)
24		expcl 10555	. . . . . . 7 ⊢ ((𝐵 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝐵↑3) ∈ ℂ)
25	15, 4, 24	sylancl 413	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑3) ∈ ℂ)
26	23, 25	addcld 7994	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3)) ∈ ℂ)
27	19, 26	addcld 7994	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3))) ∈ ℂ)
28	27, 10, 15	adddid 7999	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3))) · (𝐴 + 𝐵)) = (((((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3))) · 𝐴) + ((((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3))) · 𝐵)))
29	1	oveq2i 5901	. . . . . . . . 9 ⊢ (𝐴↑4) = (𝐴↑(3 + 1))
30		expp1 10544	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝐴↑(3 + 1)) = ((𝐴↑3) · 𝐴))
31	10, 4, 30	sylancl 413	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑(3 + 1)) = ((𝐴↑3) · 𝐴))
32	29, 31	eqtr2id 2234	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑3) · 𝐴) = (𝐴↑4))
33	13	a1i 9	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 3 ∈ ℂ)
34	33, 16, 10	mulassd 7998	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3 · ((𝐴↑2) · 𝐵)) · 𝐴) = (3 · (((𝐴↑2) · 𝐵) · 𝐴)))
35	14, 15, 10	mul32d 8127	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑2) · 𝐵) · 𝐴) = (((𝐴↑2) · 𝐴) · 𝐵))
36		df-3 8996	. . . . . . . . . . . . . 14 ⊢ 3 = (2 + 1)
37	36	oveq2i 5901	. . . . . . . . . . . . 13 ⊢ (𝐴↑3) = (𝐴↑(2 + 1))
38		2nn0 9210	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℕ₀
39		expp1 10544	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ 2 ∈ ℕ₀) → (𝐴↑(2 + 1)) = ((𝐴↑2) · 𝐴))
40	10, 38, 39	sylancl 413	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑(2 + 1)) = ((𝐴↑2) · 𝐴))
41	37, 40	eqtr2id 2234	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) · 𝐴) = (𝐴↑3))
42	41	oveq1d 5905	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑2) · 𝐴) · 𝐵) = ((𝐴↑3) · 𝐵))
43	35, 42	eqtrd 2221	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑2) · 𝐵) · 𝐴) = ((𝐴↑3) · 𝐵))
44	43	oveq2d 5906	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (3 · (((𝐴↑2) · 𝐵) · 𝐴)) = (3 · ((𝐴↑3) · 𝐵)))
45	34, 44	eqtrd 2221	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3 · ((𝐴↑2) · 𝐵)) · 𝐴) = (3 · ((𝐴↑3) · 𝐵)))
46	32, 45	oveq12d 5908	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑3) · 𝐴) + ((3 · ((𝐴↑2) · 𝐵)) · 𝐴)) = ((𝐴↑4) + (3 · ((𝐴↑3) · 𝐵))))
47	12, 10, 18, 46	joinlmuladdmuld 8002	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) · 𝐴) = ((𝐴↑4) + (3 · ((𝐴↑3) · 𝐵))))
48	33, 21, 10	mulassd 7998	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3 · (𝐴 · (𝐵↑2))) · 𝐴) = (3 · ((𝐴 · (𝐵↑2)) · 𝐴)))
49	10, 20, 10	mul32d 8127	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · (𝐵↑2)) · 𝐴) = ((𝐴 · 𝐴) · (𝐵↑2)))
50	10	sqvald 10668	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑2) = (𝐴 · 𝐴))
51	50	oveq1d 5905	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) · (𝐵↑2)) = ((𝐴 · 𝐴) · (𝐵↑2)))
52	49, 51	eqtr4d 2224	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · (𝐵↑2)) · 𝐴) = ((𝐴↑2) · (𝐵↑2)))
53	52	oveq2d 5906	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (3 · ((𝐴 · (𝐵↑2)) · 𝐴)) = (3 · ((𝐴↑2) · (𝐵↑2))))
54	48, 53	eqtrd 2221	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3 · (𝐴 · (𝐵↑2))) · 𝐴) = (3 · ((𝐴↑2) · (𝐵↑2))))
55	25, 10	mulcomd 7996	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐵↑3) · 𝐴) = (𝐴 · (𝐵↑3)))
56	54, 55	oveq12d 5908	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((3 · (𝐴 · (𝐵↑2))) · 𝐴) + ((𝐵↑3) · 𝐴)) = ((3 · ((𝐴↑2) · (𝐵↑2))) + (𝐴 · (𝐵↑3))))
57	23, 10, 25, 56	joinlmuladdmuld 8002	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3)) · 𝐴) = ((3 · ((𝐴↑2) · (𝐵↑2))) + (𝐴 · (𝐵↑3))))
58	47, 57	oveq12d 5908	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) · 𝐴) + (((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3)) · 𝐴)) = (((𝐴↑4) + (3 · ((𝐴↑3) · 𝐵))) + ((3 · ((𝐴↑2) · (𝐵↑2))) + (𝐴 · (𝐵↑3)))))
59	19, 10, 26, 58	joinlmuladdmuld 8002	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3))) · 𝐴) = (((𝐴↑4) + (3 · ((𝐴↑3) · 𝐵))) + ((3 · ((𝐴↑2) · (𝐵↑2))) + (𝐴 · (𝐵↑3)))))
60	19, 26, 15	adddird 8000	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3))) · 𝐵) = ((((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) · 𝐵) + (((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3)) · 𝐵)))
61	33, 16, 15	mulassd 7998	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3 · ((𝐴↑2) · 𝐵)) · 𝐵) = (3 · (((𝐴↑2) · 𝐵) · 𝐵)))
62	14, 15, 15	mulassd 7998	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑2) · 𝐵) · 𝐵) = ((𝐴↑2) · (𝐵 · 𝐵)))
63	15	sqvald 10668	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑2) = (𝐵 · 𝐵))
64	63	oveq2d 5906	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) · (𝐵↑2)) = ((𝐴↑2) · (𝐵 · 𝐵)))
65	62, 64	eqtr4d 2224	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑2) · 𝐵) · 𝐵) = ((𝐴↑2) · (𝐵↑2)))
66	65	oveq2d 5906	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (3 · (((𝐴↑2) · 𝐵) · 𝐵)) = (3 · ((𝐴↑2) · (𝐵↑2))))
67	61, 66	eqtrd 2221	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3 · ((𝐴↑2) · 𝐵)) · 𝐵) = (3 · ((𝐴↑2) · (𝐵↑2))))
68	67	oveq2d 5906	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑3) · 𝐵) + ((3 · ((𝐴↑2) · 𝐵)) · 𝐵)) = (((𝐴↑3) · 𝐵) + (3 · ((𝐴↑2) · (𝐵↑2)))))
69	12, 15, 18, 68	joinlmuladdmuld 8002	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) · 𝐵) = (((𝐴↑3) · 𝐵) + (3 · ((𝐴↑2) · (𝐵↑2)))))
70	33, 21, 15	mulassd 7998	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3 · (𝐴 · (𝐵↑2))) · 𝐵) = (3 · ((𝐴 · (𝐵↑2)) · 𝐵)))
71	10, 20, 15	mulassd 7998	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · (𝐵↑2)) · 𝐵) = (𝐴 · ((𝐵↑2) · 𝐵)))
72	36	oveq2i 5901	. . . . . . . . . . . . 13 ⊢ (𝐵↑3) = (𝐵↑(2 + 1))
73		expp1 10544	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℂ ∧ 2 ∈ ℕ₀) → (𝐵↑(2 + 1)) = ((𝐵↑2) · 𝐵))
74	15, 38, 73	sylancl 413	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑(2 + 1)) = ((𝐵↑2) · 𝐵))
75	72, 74	eqtr2id 2234	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐵↑2) · 𝐵) = (𝐵↑3))
76	75	oveq2d 5906	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · ((𝐵↑2) · 𝐵)) = (𝐴 · (𝐵↑3)))
77	71, 76	eqtrd 2221	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · (𝐵↑2)) · 𝐵) = (𝐴 · (𝐵↑3)))
78	77	oveq2d 5906	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (3 · ((𝐴 · (𝐵↑2)) · 𝐵)) = (3 · (𝐴 · (𝐵↑3))))
79	70, 78	eqtrd 2221	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3 · (𝐴 · (𝐵↑2))) · 𝐵) = (3 · (𝐴 · (𝐵↑3))))
80	1	oveq2i 5901	. . . . . . . . 9 ⊢ (𝐵↑4) = (𝐵↑(3 + 1))
81		expp1 10544	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝐵↑(3 + 1)) = ((𝐵↑3) · 𝐵))
82	15, 4, 81	sylancl 413	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑(3 + 1)) = ((𝐵↑3) · 𝐵))
83	80, 82	eqtr2id 2234	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐵↑3) · 𝐵) = (𝐵↑4))
84	79, 83	oveq12d 5908	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((3 · (𝐴 · (𝐵↑2))) · 𝐵) + ((𝐵↑3) · 𝐵)) = ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4)))
85	23, 15, 25, 84	joinlmuladdmuld 8002	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3)) · 𝐵) = ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4)))
86	69, 85	oveq12d 5908	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) · 𝐵) + (((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3)) · 𝐵)) = ((((𝐴↑3) · 𝐵) + (3 · ((𝐴↑2) · (𝐵↑2)))) + ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4))))
87	12, 15	mulcld 7995	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑3) · 𝐵) ∈ ℂ)
88	14, 20	mulcld 7995	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) · (𝐵↑2)) ∈ ℂ)
89		mulcl 7955	. . . . . . 7 ⊢ ((3 ∈ ℂ ∧ ((𝐴↑2) · (𝐵↑2)) ∈ ℂ) → (3 · ((𝐴↑2) · (𝐵↑2))) ∈ ℂ)
90	13, 88, 89	sylancr 414	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (3 · ((𝐴↑2) · (𝐵↑2))) ∈ ℂ)
91	10, 25	mulcld 7995	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · (𝐵↑3)) ∈ ℂ)
92		mulcl 7955	. . . . . . . 8 ⊢ ((3 ∈ ℂ ∧ (𝐴 · (𝐵↑3)) ∈ ℂ) → (3 · (𝐴 · (𝐵↑3))) ∈ ℂ)
93	13, 91, 92	sylancr 414	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (3 · (𝐴 · (𝐵↑3))) ∈ ℂ)
94		4nn0 9212	. . . . . . . 8 ⊢ 4 ∈ ℕ₀
95		expcl 10555	. . . . . . . 8 ⊢ ((𝐵 ∈ ℂ ∧ 4 ∈ ℕ₀) → (𝐵↑4) ∈ ℂ)
96	15, 94, 95	sylancl 413	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑4) ∈ ℂ)
97	93, 96	addcld 7994	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4)) ∈ ℂ)
98	87, 90, 97	addassd 7997	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑3) · 𝐵) + (3 · ((𝐴↑2) · (𝐵↑2)))) + ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4))) = (((𝐴↑3) · 𝐵) + ((3 · ((𝐴↑2) · (𝐵↑2))) + ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4)))))
99	60, 86, 98	3eqtrd 2225	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3))) · 𝐵) = (((𝐴↑3) · 𝐵) + ((3 · ((𝐴↑2) · (𝐵↑2))) + ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4)))))
100	59, 99	oveq12d 5908	. . 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 10555	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 4 ∈ ℕ₀) → (𝐴↑4) ∈ ℂ)
102	10, 94, 101	sylancl 413	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑4) ∈ ℂ)
103		mulcl 7955	. . . . . . 7 ⊢ ((3 ∈ ℂ ∧ ((𝐴↑3) · 𝐵) ∈ ℂ) → (3 · ((𝐴↑3) · 𝐵)) ∈ ℂ)
104	13, 87, 103	sylancr 414	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (3 · ((𝐴↑3) · 𝐵)) ∈ ℂ)
105	102, 104	addcld 7994	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑4) + (3 · ((𝐴↑3) · 𝐵))) ∈ ℂ)
106	90, 91	addcld 7994	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3 · ((𝐴↑2) · (𝐵↑2))) + (𝐴 · (𝐵↑3))) ∈ ℂ)
107	90, 97	addcld 7994	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3 · ((𝐴↑2) · (𝐵↑2))) + ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4))) ∈ ℂ)
108	105, 106, 87, 107	add4d 8143	. . . 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 7997	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑4) + (3 · ((𝐴↑3) · 𝐵))) + ((𝐴↑3) · 𝐵)) = ((𝐴↑4) + ((3 · ((𝐴↑3) · 𝐵)) + ((𝐴↑3) · 𝐵))))
110	1	oveq1i 5900	. . . . . . . . 9 ⊢ (4 · ((𝐴↑3) · 𝐵)) = ((3 + 1) · ((𝐴↑3) · 𝐵))
111		ax-1cn 7921	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
112	111	a1i 9	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 1 ∈ ℂ)
113	33, 112, 87	adddird 8000	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3 + 1) · ((𝐴↑3) · 𝐵)) = ((3 · ((𝐴↑3) · 𝐵)) + (1 · ((𝐴↑3) · 𝐵))))
114	110, 113	eqtrid 2233	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (4 · ((𝐴↑3) · 𝐵)) = ((3 · ((𝐴↑3) · 𝐵)) + (1 · ((𝐴↑3) · 𝐵))))
115	87	mulid2d 7993	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1 · ((𝐴↑3) · 𝐵)) = ((𝐴↑3) · 𝐵))
116	115	oveq2d 5906	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3 · ((𝐴↑3) · 𝐵)) + (1 · ((𝐴↑3) · 𝐵))) = ((3 · ((𝐴↑3) · 𝐵)) + ((𝐴↑3) · 𝐵)))
117	114, 116	eqtrd 2221	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (4 · ((𝐴↑3) · 𝐵)) = ((3 · ((𝐴↑3) · 𝐵)) + ((𝐴↑3) · 𝐵)))
118	117	oveq2d 5906	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑4) + (4 · ((𝐴↑3) · 𝐵))) = ((𝐴↑4) + ((3 · ((𝐴↑3) · 𝐵)) + ((𝐴↑3) · 𝐵))))
119	109, 118	eqtr4d 2224	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑4) + (3 · ((𝐴↑3) · 𝐵))) + ((𝐴↑3) · 𝐵)) = ((𝐴↑4) + (4 · ((𝐴↑3) · 𝐵))))
120	90, 91, 90, 97	add4d 8143	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((3 · ((𝐴↑2) · (𝐵↑2))) + (𝐴 · (𝐵↑3))) + ((3 · ((𝐴↑2) · (𝐵↑2))) + ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4)))) = (((3 · ((𝐴↑2) · (𝐵↑2))) + (3 · ((𝐴↑2) · (𝐵↑2)))) + ((𝐴 · (𝐵↑3)) + ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4)))))
121		3p3e6 9078	. . . . . . . . 9 ⊢ (3 + 3) = 6
122	121	oveq1i 5900	. . . . . . . 8 ⊢ ((3 + 3) · ((𝐴↑2) · (𝐵↑2))) = (6 · ((𝐴↑2) · (𝐵↑2)))
123	33, 33, 88	adddird 8000	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3 + 3) · ((𝐴↑2) · (𝐵↑2))) = ((3 · ((𝐴↑2) · (𝐵↑2))) + (3 · ((𝐴↑2) · (𝐵↑2)))))
124	122, 123	eqtr3id 2235	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (6 · ((𝐴↑2) · (𝐵↑2))) = ((3 · ((𝐴↑2) · (𝐵↑2))) + (3 · ((𝐴↑2) · (𝐵↑2)))))
125		3p1e4 9071	. . . . . . . . . . . . 13 ⊢ (3 + 1) = 4
126	13, 111, 125	addcomli 8119	. . . . . . . . . . . 12 ⊢ (1 + 3) = 4
127	126	oveq1i 5900	. . . . . . . . . . 11 ⊢ ((1 + 3) · (𝐴 · (𝐵↑3))) = (4 · (𝐴 · (𝐵↑3)))
128	112, 33, 91	adddird 8000	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((1 + 3) · (𝐴 · (𝐵↑3))) = ((1 · (𝐴 · (𝐵↑3))) + (3 · (𝐴 · (𝐵↑3)))))
129	127, 128	eqtr3id 2235	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (4 · (𝐴 · (𝐵↑3))) = ((1 · (𝐴 · (𝐵↑3))) + (3 · (𝐴 · (𝐵↑3)))))
130	91	mulid2d 7993	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1 · (𝐴 · (𝐵↑3))) = (𝐴 · (𝐵↑3)))
131	130	oveq1d 5905	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((1 · (𝐴 · (𝐵↑3))) + (3 · (𝐴 · (𝐵↑3)))) = ((𝐴 · (𝐵↑3)) + (3 · (𝐴 · (𝐵↑3)))))
132	129, 131	eqtrd 2221	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (4 · (𝐴 · (𝐵↑3))) = ((𝐴 · (𝐵↑3)) + (3 · (𝐴 · (𝐵↑3)))))
133	132	oveq1d 5905	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((4 · (𝐴 · (𝐵↑3))) + (𝐵↑4)) = (((𝐴 · (𝐵↑3)) + (3 · (𝐴 · (𝐵↑3)))) + (𝐵↑4)))
134	91, 93, 96	addassd 7997	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 · (𝐵↑3)) + (3 · (𝐴 · (𝐵↑3)))) + (𝐵↑4)) = ((𝐴 · (𝐵↑3)) + ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4))))
135	133, 134	eqtrd 2221	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((4 · (𝐴 · (𝐵↑3))) + (𝐵↑4)) = ((𝐴 · (𝐵↑3)) + ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4))))
136	124, 135	oveq12d 5908	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((6 · ((𝐴↑2) · (𝐵↑2))) + ((4 · (𝐴 · (𝐵↑3))) + (𝐵↑4))) = (((3 · ((𝐴↑2) · (𝐵↑2))) + (3 · ((𝐴↑2) · (𝐵↑2)))) + ((𝐴 · (𝐵↑3)) + ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4)))))
137	120, 136	eqtr4d 2224	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((3 · ((𝐴↑2) · (𝐵↑2))) + (𝐴 · (𝐵↑3))) + ((3 · ((𝐴↑2) · (𝐵↑2))) + ((3 · (𝐴 · (𝐵↑3))) + (𝐵↑4)))) = ((6 · ((𝐴↑2) · (𝐵↑2))) + ((4 · (𝐴 · (𝐵↑3))) + (𝐵↑4))))
138	119, 137	oveq12d 5908	. . . 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 2221	. . 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 2225	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3))) · (𝐴 + 𝐵)) = (((𝐴↑4) + (4 · ((𝐴↑3) · 𝐵))) + ((6 · ((𝐴↑2) · (𝐵↑2))) + ((4 · (𝐴 · (𝐵↑3))) + (𝐵↑4)))))
141	7, 9, 140	3eqtrd 2225	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑4) = (((𝐴↑4) + (4 · ((𝐴↑3) · 𝐵))) + ((6 · ((𝐴↑2) · (𝐵↑2))) + ((4 · (𝐴 · (𝐵↑3))) + (𝐵↑4)))))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 = wceq 1363 ∈ wcel 2159 (class class class)co 5890 ℂcc 7826 1c1 7829 + caddc 7831 · cmul 7833 2c2 8987 3c3 8988 4c4 8989 6c6 8991 ℕ₀cn0 9193 ↑cexp 10536

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 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-13 2161 ax-14 2162 ax-ext 2170 ax-coll 4132 ax-sep 4135 ax-nul 4143 ax-pow 4188 ax-pr 4223 ax-un 4447 ax-setind 4550 ax-iinf 4601 ax-cnex 7919 ax-resscn 7920 ax-1cn 7921 ax-1re 7922 ax-icn 7923 ax-addcl 7924 ax-addrcl 7925 ax-mulcl 7926 ax-mulrcl 7927 ax-addcom 7928 ax-mulcom 7929 ax-addass 7930 ax-mulass 7931 ax-distr 7932 ax-i2m1 7933 ax-0lt1 7934 ax-1rid 7935 ax-0id 7936 ax-rnegex 7937 ax-precex 7938 ax-cnre 7939 ax-pre-ltirr 7940 ax-pre-ltwlin 7941 ax-pre-lttrn 7942 ax-pre-apti 7943 ax-pre-ltadd 7944 ax-pre-mulgt0 7945 ax-pre-mulext 7946

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 980 df-3an 981 df-tru 1366 df-fal 1369 df-nf 1471 df-sb 1773 df-eu 2040 df-mo 2041 df-clab 2175 df-cleq 2181 df-clel 2184 df-nfc 2320 df-ne 2360 df-nel 2455 df-ral 2472 df-rex 2473 df-reu 2474 df-rmo 2475 df-rab 2476 df-v 2753 df-sbc 2977 df-csb 3072 df-dif 3145 df-un 3147 df-in 3149 df-ss 3156 df-nul 3437 df-if 3549 df-pw 3591 df-sn 3612 df-pr 3613 df-op 3615 df-uni 3824 df-int 3859 df-iun 3902 df-br 4018 df-opab 4079 df-mpt 4080 df-tr 4116 df-id 4307 df-po 4310 df-iso 4311 df-iord 4380 df-on 4382 df-ilim 4383 df-suc 4385 df-iom 4604 df-xp 4646 df-rel 4647 df-cnv 4648 df-co 4649 df-dm 4650 df-rn 4651 df-res 4652 df-ima 4653 df-iota 5192 df-fun 5232 df-fn 5233 df-f 5234 df-f1 5235 df-fo 5236 df-f1o 5237 df-fv 5238 df-riota 5846 df-ov 5893 df-oprab 5894 df-mpo 5895 df-1st 6158 df-2nd 6159 df-recs 6323 df-frec 6409 df-pnf 8011 df-mnf 8012 df-xr 8013 df-ltxr 8014 df-le 8015 df-sub 8147 df-neg 8148 df-reap 8549 df-ap 8556 df-div 8647 df-inn 8937 df-2 8995 df-3 8996 df-4 8997 df-5 8998 df-6 8999 df-n0 9194 df-z 9271 df-uz 9546 df-seqfrec 10463 df-exp 10537

This theorem is referenced by: (None)

W3C validator