binom3 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > binom3		Structured version Visualization version GIF version

Theorem binom3 14237

Description: The cube of a binomial. (Contributed by Mario Carneiro, 24-Apr-2015.)

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

**Proof of Theorem binom3**
Step	Hyp	Ref	Expression
1		df-3 12281	. . . 4 ⊢ 3 = (2 + 1)
2	1	oveq2i 7407	. . 3 ⊢ ((𝐴 + 𝐵)↑3) = ((𝐴 + 𝐵)↑(2 + 1))
3		addcl 11155	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
4		2nn0 12498	. . . 4 ⊢ 2 ∈ ℕ₀
5		expp1 14081	. . . 4 ⊢ (((𝐴 + 𝐵) ∈ ℂ ∧ 2 ∈ ℕ₀) → ((𝐴 + 𝐵)↑(2 + 1)) = (((𝐴 + 𝐵)↑2) · (𝐴 + 𝐵)))
6	3, 4, 5	sylancl 595	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑(2 + 1)) = (((𝐴 + 𝐵)↑2) · (𝐴 + 𝐵)))
7	2, 6	eqtrid 2809	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑3) = (((𝐴 + 𝐵)↑2) · (𝐴 + 𝐵)))
8		sqcl 14131	. . . . 5 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((𝐴 + 𝐵)↑2) ∈ ℂ)
9	3, 8	syl 17	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑2) ∈ ℂ)
10		simpl 486	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈ ℂ)
11		simpr 488	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
12	9, 10, 11	adddid 11206	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵)↑2) · (𝐴 + 𝐵)) = ((((𝐴 + 𝐵)↑2) · 𝐴) + (((𝐴 + 𝐵)↑2) · 𝐵)))
13		binom2 14230	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑2) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)))
14	13	oveq1d 7411	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵)↑2) · 𝐴) = ((((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)) · 𝐴))
15		sqcl 14131	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (𝐴↑2) ∈ ℂ)
16	10, 15	syl 17	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑2) ∈ ℂ)
17		2cn 12293	. . . . . . . 8 ⊢ 2 ∈ ℂ
18		mulcl 11157	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
19		mulcl 11157	. . . . . . . 8 ⊢ ((2 ∈ ℂ ∧ (𝐴 · 𝐵) ∈ ℂ) → (2 · (𝐴 · 𝐵)) ∈ ℂ)
20	17, 18, 19	sylancr 596	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2 · (𝐴 · 𝐵)) ∈ ℂ)
21	16, 20	addcld 11201	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) + (2 · (𝐴 · 𝐵))) ∈ ℂ)
22		sqcl 14131	. . . . . . 7 ⊢ (𝐵 ∈ ℂ → (𝐵↑2) ∈ ℂ)
23	11, 22	syl 17	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑2) ∈ ℂ)
24	21, 23, 10	adddird 11207	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)) · 𝐴) = ((((𝐴↑2) + (2 · (𝐴 · 𝐵))) · 𝐴) + ((𝐵↑2) · 𝐴)))
25	16, 20, 10	adddird 11207	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑2) + (2 · (𝐴 · 𝐵))) · 𝐴) = (((𝐴↑2) · 𝐴) + ((2 · (𝐴 · 𝐵)) · 𝐴)))
26	1	oveq2i 7407	. . . . . . . . 9 ⊢ (𝐴↑3) = (𝐴↑(2 + 1))
27		expp1 14081	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 2 ∈ ℕ₀) → (𝐴↑(2 + 1)) = ((𝐴↑2) · 𝐴))
28	10, 4, 27	sylancl 595	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑(2 + 1)) = ((𝐴↑2) · 𝐴))
29	26, 28	eqtrid 2809	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑3) = ((𝐴↑2) · 𝐴))
30		sqval 14127	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (𝐴↑2) = (𝐴 · 𝐴))
31	10, 30	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑2) = (𝐴 · 𝐴))
32	31	oveq1d 7411	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) · 𝐵) = ((𝐴 · 𝐴) · 𝐵))
33	10, 10, 11	mul32d 11393	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐴) · 𝐵) = ((𝐴 · 𝐵) · 𝐴))
34	32, 33	eqtrd 2797	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) · 𝐵) = ((𝐴 · 𝐵) · 𝐴))
35	34	oveq2d 7412	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2 · ((𝐴↑2) · 𝐵)) = (2 · ((𝐴 · 𝐵) · 𝐴)))
36		2cnd 12296	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 2 ∈ ℂ)
37	36, 18, 10	mulassd 11205	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((2 · (𝐴 · 𝐵)) · 𝐴) = (2 · ((𝐴 · 𝐵) · 𝐴)))
38	35, 37	eqtr4d 2800	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2 · ((𝐴↑2) · 𝐵)) = ((2 · (𝐴 · 𝐵)) · 𝐴))
39	29, 38	oveq12d 7414	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))) = (((𝐴↑2) · 𝐴) + ((2 · (𝐴 · 𝐵)) · 𝐴)))
40	25, 39	eqtr4d 2800	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑2) + (2 · (𝐴 · 𝐵))) · 𝐴) = ((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))))
41	23, 10	mulcomd 11203	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐵↑2) · 𝐴) = (𝐴 · (𝐵↑2)))
42	40, 41	oveq12d 7414	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑2) + (2 · (𝐴 · 𝐵))) · 𝐴) + ((𝐵↑2) · 𝐴)) = (((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))) + (𝐴 · (𝐵↑2))))
43	14, 24, 42	3eqtrd 2801	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵)↑2) · 𝐴) = (((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))) + (𝐴 · (𝐵↑2))))
44	13	oveq1d 7411	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵)↑2) · 𝐵) = ((((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)) · 𝐵))
45	21, 23, 11	adddird 11207	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)) · 𝐵) = ((((𝐴↑2) + (2 · (𝐴 · 𝐵))) · 𝐵) + ((𝐵↑2) · 𝐵)))
46		sqval 14127	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ ℂ → (𝐵↑2) = (𝐵 · 𝐵))
47	11, 46	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑2) = (𝐵 · 𝐵))
48	47	oveq2d 7412	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · (𝐵↑2)) = (𝐴 · (𝐵 · 𝐵)))
49	10, 11, 11	mulassd 11205	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐵) = (𝐴 · (𝐵 · 𝐵)))
50	48, 49	eqtr4d 2800	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · (𝐵↑2)) = ((𝐴 · 𝐵) · 𝐵))
51	50	oveq2d 7412	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2 · (𝐴 · (𝐵↑2))) = (2 · ((𝐴 · 𝐵) · 𝐵)))
52	36, 18, 11	mulassd 11205	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((2 · (𝐴 · 𝐵)) · 𝐵) = (2 · ((𝐴 · 𝐵) · 𝐵)))
53	51, 52	eqtr4d 2800	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2 · (𝐴 · (𝐵↑2))) = ((2 · (𝐴 · 𝐵)) · 𝐵))
54	53	oveq2d 7412	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑2) · 𝐵) + (2 · (𝐴 · (𝐵↑2)))) = (((𝐴↑2) · 𝐵) + ((2 · (𝐴 · 𝐵)) · 𝐵)))
55	16, 20, 11	adddird 11207	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑2) + (2 · (𝐴 · 𝐵))) · 𝐵) = (((𝐴↑2) · 𝐵) + ((2 · (𝐴 · 𝐵)) · 𝐵)))
56	54, 55	eqtr4d 2800	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑2) · 𝐵) + (2 · (𝐴 · (𝐵↑2)))) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) · 𝐵))
57	1	oveq2i 7407	. . . . . . . 8 ⊢ (𝐵↑3) = (𝐵↑(2 + 1))
58		expp1 14081	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℂ ∧ 2 ∈ ℕ₀) → (𝐵↑(2 + 1)) = ((𝐵↑2) · 𝐵))
59	11, 4, 58	sylancl 595	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑(2 + 1)) = ((𝐵↑2) · 𝐵))
60	57, 59	eqtrid 2809	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑3) = ((𝐵↑2) · 𝐵))
61	56, 60	oveq12d 7414	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑2) · 𝐵) + (2 · (𝐴 · (𝐵↑2)))) + (𝐵↑3)) = ((((𝐴↑2) + (2 · (𝐴 · 𝐵))) · 𝐵) + ((𝐵↑2) · 𝐵)))
62	16, 11	mulcld 11202	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) · 𝐵) ∈ ℂ)
63	10, 23	mulcld 11202	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · (𝐵↑2)) ∈ ℂ)
64		mulcl 11157	. . . . . . . 8 ⊢ ((2 ∈ ℂ ∧ (𝐴 · (𝐵↑2)) ∈ ℂ) → (2 · (𝐴 · (𝐵↑2))) ∈ ℂ)
65	17, 63, 64	sylancr 596	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2 · (𝐴 · (𝐵↑2))) ∈ ℂ)
66		3nn0 12499	. . . . . . . 8 ⊢ 3 ∈ ℕ₀
67		expcl 14092	. . . . . . . 8 ⊢ ((𝐵 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝐵↑3) ∈ ℂ)
68	11, 66, 67	sylancl 595	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑3) ∈ ℂ)
69	62, 65, 68	addassd 11204	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑2) · 𝐵) + (2 · (𝐴 · (𝐵↑2)))) + (𝐵↑3)) = (((𝐴↑2) · 𝐵) + ((2 · (𝐴 · (𝐵↑2))) + (𝐵↑3))))
70	61, 69	eqtr3d 2799	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑2) + (2 · (𝐴 · 𝐵))) · 𝐵) + ((𝐵↑2) · 𝐵)) = (((𝐴↑2) · 𝐵) + ((2 · (𝐴 · (𝐵↑2))) + (𝐵↑3))))
71	44, 45, 70	3eqtrd 2801	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵)↑2) · 𝐵) = (((𝐴↑2) · 𝐵) + ((2 · (𝐴 · (𝐵↑2))) + (𝐵↑3))))
72	43, 71	oveq12d 7414	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐵)↑2) · 𝐴) + (((𝐴 + 𝐵)↑2) · 𝐵)) = ((((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))) + (𝐴 · (𝐵↑2))) + (((𝐴↑2) · 𝐵) + ((2 · (𝐴 · (𝐵↑2))) + (𝐵↑3)))))
73		expcl 14092	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝐴↑3) ∈ ℂ)
74	10, 66, 73	sylancl 595	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑3) ∈ ℂ)
75		mulcl 11157	. . . . . 6 ⊢ ((2 ∈ ℂ ∧ ((𝐴↑2) · 𝐵) ∈ ℂ) → (2 · ((𝐴↑2) · 𝐵)) ∈ ℂ)
76	17, 62, 75	sylancr 596	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2 · ((𝐴↑2) · 𝐵)) ∈ ℂ)
77	74, 76	addcld 11201	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))) ∈ ℂ)
78	65, 68	addcld 11201	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((2 · (𝐴 · (𝐵↑2))) + (𝐵↑3)) ∈ ℂ)
79	77, 63, 62, 78	add4d 11412	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))) + (𝐴 · (𝐵↑2))) + (((𝐴↑2) · 𝐵) + ((2 · (𝐴 · (𝐵↑2))) + (𝐵↑3)))) = ((((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))) + ((𝐴↑2) · 𝐵)) + ((𝐴 · (𝐵↑2)) + ((2 · (𝐴 · (𝐵↑2))) + (𝐵↑3)))))
80	12, 72, 79	3eqtrd 2801	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵)↑2) · (𝐴 + 𝐵)) = ((((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))) + ((𝐴↑2) · 𝐵)) + ((𝐴 · (𝐵↑2)) + ((2 · (𝐴 · (𝐵↑2))) + (𝐵↑3)))))
81	74, 76, 62	addassd 11204	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))) + ((𝐴↑2) · 𝐵)) = ((𝐴↑3) + ((2 · ((𝐴↑2) · 𝐵)) + ((𝐴↑2) · 𝐵))))
82	1	oveq1i 7406	. . . . . . 7 ⊢ (3 · ((𝐴↑2) · 𝐵)) = ((2 + 1) · ((𝐴↑2) · 𝐵))
83		1cnd 11175	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 1 ∈ ℂ)
84	36, 83, 62	adddird 11207	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((2 + 1) · ((𝐴↑2) · 𝐵)) = ((2 · ((𝐴↑2) · 𝐵)) + (1 · ((𝐴↑2) · 𝐵))))
85	82, 84	eqtrid 2809	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (3 · ((𝐴↑2) · 𝐵)) = ((2 · ((𝐴↑2) · 𝐵)) + (1 · ((𝐴↑2) · 𝐵))))
86	62	mullidd 11200	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1 · ((𝐴↑2) · 𝐵)) = ((𝐴↑2) · 𝐵))
87	86	oveq2d 7412	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((2 · ((𝐴↑2) · 𝐵)) + (1 · ((𝐴↑2) · 𝐵))) = ((2 · ((𝐴↑2) · 𝐵)) + ((𝐴↑2) · 𝐵)))
88	85, 87	eqtrd 2797	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (3 · ((𝐴↑2) · 𝐵)) = ((2 · ((𝐴↑2) · 𝐵)) + ((𝐴↑2) · 𝐵)))
89	88	oveq2d 7412	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) = ((𝐴↑3) + ((2 · ((𝐴↑2) · 𝐵)) + ((𝐴↑2) · 𝐵))))
90	81, 89	eqtr4d 2800	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))) + ((𝐴↑2) · 𝐵)) = ((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))))
91		1p2e3 12360	. . . . . . . 8 ⊢ (1 + 2) = 3
92	91	oveq1i 7406	. . . . . . 7 ⊢ ((1 + 2) · (𝐴 · (𝐵↑2))) = (3 · (𝐴 · (𝐵↑2)))
93	83, 36, 63	adddird 11207	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((1 + 2) · (𝐴 · (𝐵↑2))) = ((1 · (𝐴 · (𝐵↑2))) + (2 · (𝐴 · (𝐵↑2)))))
94	92, 93	eqtr3id 2811	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (3 · (𝐴 · (𝐵↑2))) = ((1 · (𝐴 · (𝐵↑2))) + (2 · (𝐴 · (𝐵↑2)))))
95	63	mullidd 11200	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1 · (𝐴 · (𝐵↑2))) = (𝐴 · (𝐵↑2)))
96	95	oveq1d 7411	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((1 · (𝐴 · (𝐵↑2))) + (2 · (𝐴 · (𝐵↑2)))) = ((𝐴 · (𝐵↑2)) + (2 · (𝐴 · (𝐵↑2)))))
97	94, 96	eqtrd 2797	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (3 · (𝐴 · (𝐵↑2))) = ((𝐴 · (𝐵↑2)) + (2 · (𝐴 · (𝐵↑2)))))
98	97	oveq1d 7411	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3)) = (((𝐴 · (𝐵↑2)) + (2 · (𝐴 · (𝐵↑2)))) + (𝐵↑3)))
99	63, 65, 68	addassd 11204	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 · (𝐵↑2)) + (2 · (𝐴 · (𝐵↑2)))) + (𝐵↑3)) = ((𝐴 · (𝐵↑2)) + ((2 · (𝐴 · (𝐵↑2))) + (𝐵↑3))))
100	98, 99	eqtr2d 2798	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · (𝐵↑2)) + ((2 · (𝐴 · (𝐵↑2))) + (𝐵↑3))) = ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3)))
101	90, 100	oveq12d 7414	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))) + ((𝐴↑2) · 𝐵)) + ((𝐴 · (𝐵↑2)) + ((2 · (𝐴 · (𝐵↑2))) + (𝐵↑3)))) = (((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3))))
102	7, 80, 101	3eqtrd 2801	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑3) = (((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 = wceq 1560 ∈ wcel 2142 (class class class)co 7396 ℂcc 11071 1c1 11074 + caddc 11076 · cmul 11078 2c2 12272 3c3 12273 ℕ₀cn0 12481 ↑cexp 14074

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-sep 5246 ax-nul 5256 ax-pow 5322 ax-pr 5390 ax-un 7718 ax-cnex 11129 ax-resscn 11130 ax-1cn 11131 ax-icn 11132 ax-addcl 11133 ax-addrcl 11134 ax-mulcl 11135 ax-mulrcl 11136 ax-mulcom 11137 ax-addass 11138 ax-mulass 11139 ax-distr 11140 ax-i2m1 11141 ax-1ne0 11142 ax-1rid 11143 ax-rnegex 11144 ax-rrecex 11145 ax-cnre 11146 ax-pre-lttri 11147 ax-pre-lttrn 11148 ax-pre-ltadd 11149 ax-pre-mulgt0 11150

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1099 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-nf 1804 df-sb 2091 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3062 df-ral 3077 df-rex 3087 df-reu 3368 df-rab 3415 df-v 3456 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4481 df-pw 4557 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-iun 4951 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-we 5602 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-pred 6288 df-ord 6349 df-on 6350 df-lim 6351 df-suc 6352 df-iota 6477 df-fun 6523 df-fn 6524 df-f 6525 df-f1 6526 df-fo 6527 df-f1o 6528 df-fv 6529 df-riota 7353 df-ov 7399 df-oprab 7400 df-mpo 7401 df-om 7847 df-2nd 7971 df-frecs 8262 df-wrecs 8293 df-recs 8342 df-rdg 8381 df-er 8678 df-en 8928 df-dom 8929 df-sdom 8930 df-pnf 11218 df-mnf 11219 df-xr 11220 df-ltxr 11221 df-le 11222 df-sub 11416 df-neg 11417 df-nn 12211 df-2 12280 df-3 12281 df-n0 12482 df-z 12569 df-uz 12840 df-seq 14015 df-exp 14075

This theorem is referenced by: dcubic1lem 26908 mcubic 26912 binom4 26915 cos9thpiminplylem5 34083 cu3addd 43262 3cubeslem3r 43268

W3C validator