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 12985

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 11080	. . . 4 ⊢ 3 = (2 + 1)
2	1	oveq2i 6661	. . 3 ⊢ ((𝐴 + 𝐵)↑3) = ((𝐴 + 𝐵)↑(2 + 1))
3		addcl 10018	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
4		2nn0 11309	. . . 4 ⊢ 2 ∈ ℕ₀
5		expp1 12867	. . . 4 ⊢ (((𝐴 + 𝐵) ∈ ℂ ∧ 2 ∈ ℕ₀) → ((𝐴 + 𝐵)↑(2 + 1)) = (((𝐴 + 𝐵)↑2) · (𝐴 + 𝐵)))
6	3, 4, 5	sylancl 694	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑(2 + 1)) = (((𝐴 + 𝐵)↑2) · (𝐴 + 𝐵)))
7	2, 6	syl5eq 2668	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑3) = (((𝐴 + 𝐵)↑2) · (𝐴 + 𝐵)))
8		sqcl 12925	. . . . 5 ⊢ ((𝐴 + 𝐵) ∈ ℂ → ((𝐴 + 𝐵)↑2) ∈ ℂ)
9	3, 8	syl 17	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑2) ∈ ℂ)
10		simpl 473	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈ ℂ)
11		simpr 477	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
12	9, 10, 11	adddid 10064	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵)↑2) · (𝐴 + 𝐵)) = ((((𝐴 + 𝐵)↑2) · 𝐴) + (((𝐴 + 𝐵)↑2) · 𝐵)))
13		binom2 12979	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑2) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)))
14	13	oveq1d 6665	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵)↑2) · 𝐴) = ((((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)) · 𝐴))
15		sqcl 12925	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (𝐴↑2) ∈ ℂ)
16	10, 15	syl 17	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑2) ∈ ℂ)
17		2cn 11091	. . . . . . . 8 ⊢ 2 ∈ ℂ
18		mulcl 10020	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
19		mulcl 10020	. . . . . . . 8 ⊢ ((2 ∈ ℂ ∧ (𝐴 · 𝐵) ∈ ℂ) → (2 · (𝐴 · 𝐵)) ∈ ℂ)
20	17, 18, 19	sylancr 695	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2 · (𝐴 · 𝐵)) ∈ ℂ)
21	16, 20	addcld 10059	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) + (2 · (𝐴 · 𝐵))) ∈ ℂ)
22		sqcl 12925	. . . . . . 7 ⊢ (𝐵 ∈ ℂ → (𝐵↑2) ∈ ℂ)
23	11, 22	syl 17	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑2) ∈ ℂ)
24	21, 23, 10	adddird 10065	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)) · 𝐴) = ((((𝐴↑2) + (2 · (𝐴 · 𝐵))) · 𝐴) + ((𝐵↑2) · 𝐴)))
25	16, 20, 10	adddird 10065	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑2) + (2 · (𝐴 · 𝐵))) · 𝐴) = (((𝐴↑2) · 𝐴) + ((2 · (𝐴 · 𝐵)) · 𝐴)))
26	1	oveq2i 6661	. . . . . . . . 9 ⊢ (𝐴↑3) = (𝐴↑(2 + 1))
27		expp1 12867	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 2 ∈ ℕ₀) → (𝐴↑(2 + 1)) = ((𝐴↑2) · 𝐴))
28	10, 4, 27	sylancl 694	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑(2 + 1)) = ((𝐴↑2) · 𝐴))
29	26, 28	syl5eq 2668	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑3) = ((𝐴↑2) · 𝐴))
30		sqval 12922	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (𝐴↑2) = (𝐴 · 𝐴))
31	10, 30	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑2) = (𝐴 · 𝐴))
32	31	oveq1d 6665	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) · 𝐵) = ((𝐴 · 𝐴) · 𝐵))
33	10, 10, 11	mul32d 10246	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐴) · 𝐵) = ((𝐴 · 𝐵) · 𝐴))
34	32, 33	eqtrd 2656	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) · 𝐵) = ((𝐴 · 𝐵) · 𝐴))
35	34	oveq2d 6666	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2 · ((𝐴↑2) · 𝐵)) = (2 · ((𝐴 · 𝐵) · 𝐴)))
36		2cnd 11093	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 2 ∈ ℂ)
37	36, 18, 10	mulassd 10063	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((2 · (𝐴 · 𝐵)) · 𝐴) = (2 · ((𝐴 · 𝐵) · 𝐴)))
38	35, 37	eqtr4d 2659	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2 · ((𝐴↑2) · 𝐵)) = ((2 · (𝐴 · 𝐵)) · 𝐴))
39	29, 38	oveq12d 6668	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))) = (((𝐴↑2) · 𝐴) + ((2 · (𝐴 · 𝐵)) · 𝐴)))
40	25, 39	eqtr4d 2659	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑2) + (2 · (𝐴 · 𝐵))) · 𝐴) = ((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))))
41	23, 10	mulcomd 10061	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐵↑2) · 𝐴) = (𝐴 · (𝐵↑2)))
42	40, 41	oveq12d 6668	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑2) + (2 · (𝐴 · 𝐵))) · 𝐴) + ((𝐵↑2) · 𝐴)) = (((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))) + (𝐴 · (𝐵↑2))))
43	14, 24, 42	3eqtrd 2660	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵)↑2) · 𝐴) = (((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))) + (𝐴 · (𝐵↑2))))
44	13	oveq1d 6665	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵)↑2) · 𝐵) = ((((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)) · 𝐵))
45	21, 23, 11	adddird 10065	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)) · 𝐵) = ((((𝐴↑2) + (2 · (𝐴 · 𝐵))) · 𝐵) + ((𝐵↑2) · 𝐵)))
46		sqval 12922	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ ℂ → (𝐵↑2) = (𝐵 · 𝐵))
47	11, 46	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑2) = (𝐵 · 𝐵))
48	47	oveq2d 6666	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · (𝐵↑2)) = (𝐴 · (𝐵 · 𝐵)))
49	10, 11, 11	mulassd 10063	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐵) = (𝐴 · (𝐵 · 𝐵)))
50	48, 49	eqtr4d 2659	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · (𝐵↑2)) = ((𝐴 · 𝐵) · 𝐵))
51	50	oveq2d 6666	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2 · (𝐴 · (𝐵↑2))) = (2 · ((𝐴 · 𝐵) · 𝐵)))
52	36, 18, 11	mulassd 10063	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((2 · (𝐴 · 𝐵)) · 𝐵) = (2 · ((𝐴 · 𝐵) · 𝐵)))
53	51, 52	eqtr4d 2659	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2 · (𝐴 · (𝐵↑2))) = ((2 · (𝐴 · 𝐵)) · 𝐵))
54	53	oveq2d 6666	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑2) · 𝐵) + (2 · (𝐴 · (𝐵↑2)))) = (((𝐴↑2) · 𝐵) + ((2 · (𝐴 · 𝐵)) · 𝐵)))
55	16, 20, 11	adddird 10065	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑2) + (2 · (𝐴 · 𝐵))) · 𝐵) = (((𝐴↑2) · 𝐵) + ((2 · (𝐴 · 𝐵)) · 𝐵)))
56	54, 55	eqtr4d 2659	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑2) · 𝐵) + (2 · (𝐴 · (𝐵↑2)))) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) · 𝐵))
57	1	oveq2i 6661	. . . . . . . 8 ⊢ (𝐵↑3) = (𝐵↑(2 + 1))
58		expp1 12867	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℂ ∧ 2 ∈ ℕ₀) → (𝐵↑(2 + 1)) = ((𝐵↑2) · 𝐵))
59	11, 4, 58	sylancl 694	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑(2 + 1)) = ((𝐵↑2) · 𝐵))
60	57, 59	syl5eq 2668	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑3) = ((𝐵↑2) · 𝐵))
61	56, 60	oveq12d 6668	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑2) · 𝐵) + (2 · (𝐴 · (𝐵↑2)))) + (𝐵↑3)) = ((((𝐴↑2) + (2 · (𝐴 · 𝐵))) · 𝐵) + ((𝐵↑2) · 𝐵)))
62	16, 11	mulcld 10060	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) · 𝐵) ∈ ℂ)
63	10, 23	mulcld 10060	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · (𝐵↑2)) ∈ ℂ)
64		mulcl 10020	. . . . . . . 8 ⊢ ((2 ∈ ℂ ∧ (𝐴 · (𝐵↑2)) ∈ ℂ) → (2 · (𝐴 · (𝐵↑2))) ∈ ℂ)
65	17, 63, 64	sylancr 695	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2 · (𝐴 · (𝐵↑2))) ∈ ℂ)
66		3nn0 11310	. . . . . . . 8 ⊢ 3 ∈ ℕ₀
67		expcl 12878	. . . . . . . 8 ⊢ ((𝐵 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝐵↑3) ∈ ℂ)
68	11, 66, 67	sylancl 694	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑3) ∈ ℂ)
69	62, 65, 68	addassd 10062	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑2) · 𝐵) + (2 · (𝐴 · (𝐵↑2)))) + (𝐵↑3)) = (((𝐴↑2) · 𝐵) + ((2 · (𝐴 · (𝐵↑2))) + (𝐵↑3))))
70	61, 69	eqtr3d 2658	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑2) + (2 · (𝐴 · 𝐵))) · 𝐵) + ((𝐵↑2) · 𝐵)) = (((𝐴↑2) · 𝐵) + ((2 · (𝐴 · (𝐵↑2))) + (𝐵↑3))))
71	44, 45, 70	3eqtrd 2660	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵)↑2) · 𝐵) = (((𝐴↑2) · 𝐵) + ((2 · (𝐴 · (𝐵↑2))) + (𝐵↑3))))
72	43, 71	oveq12d 6668	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐵)↑2) · 𝐴) + (((𝐴 + 𝐵)↑2) · 𝐵)) = ((((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))) + (𝐴 · (𝐵↑2))) + (((𝐴↑2) · 𝐵) + ((2 · (𝐴 · (𝐵↑2))) + (𝐵↑3)))))
73		expcl 12878	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝐴↑3) ∈ ℂ)
74	10, 66, 73	sylancl 694	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑3) ∈ ℂ)
75		mulcl 10020	. . . . . 6 ⊢ ((2 ∈ ℂ ∧ ((𝐴↑2) · 𝐵) ∈ ℂ) → (2 · ((𝐴↑2) · 𝐵)) ∈ ℂ)
76	17, 62, 75	sylancr 695	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2 · ((𝐴↑2) · 𝐵)) ∈ ℂ)
77	74, 76	addcld 10059	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))) ∈ ℂ)
78	65, 68	addcld 10059	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((2 · (𝐴 · (𝐵↑2))) + (𝐵↑3)) ∈ ℂ)
79	77, 63, 62, 78	add4d 10264	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))) + (𝐴 · (𝐵↑2))) + (((𝐴↑2) · 𝐵) + ((2 · (𝐴 · (𝐵↑2))) + (𝐵↑3)))) = ((((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))) + ((𝐴↑2) · 𝐵)) + ((𝐴 · (𝐵↑2)) + ((2 · (𝐴 · (𝐵↑2))) + (𝐵↑3)))))
80	12, 72, 79	3eqtrd 2660	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵)↑2) · (𝐴 + 𝐵)) = ((((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))) + ((𝐴↑2) · 𝐵)) + ((𝐴 · (𝐵↑2)) + ((2 · (𝐴 · (𝐵↑2))) + (𝐵↑3)))))
81	74, 76, 62	addassd 10062	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))) + ((𝐴↑2) · 𝐵)) = ((𝐴↑3) + ((2 · ((𝐴↑2) · 𝐵)) + ((𝐴↑2) · 𝐵))))
82	1	oveq1i 6660	. . . . . . 7 ⊢ (3 · ((𝐴↑2) · 𝐵)) = ((2 + 1) · ((𝐴↑2) · 𝐵))
83		1cnd 10056	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 1 ∈ ℂ)
84	36, 83, 62	adddird 10065	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((2 + 1) · ((𝐴↑2) · 𝐵)) = ((2 · ((𝐴↑2) · 𝐵)) + (1 · ((𝐴↑2) · 𝐵))))
85	82, 84	syl5eq 2668	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (3 · ((𝐴↑2) · 𝐵)) = ((2 · ((𝐴↑2) · 𝐵)) + (1 · ((𝐴↑2) · 𝐵))))
86	62	mulid2d 10058	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1 · ((𝐴↑2) · 𝐵)) = ((𝐴↑2) · 𝐵))
87	86	oveq2d 6666	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((2 · ((𝐴↑2) · 𝐵)) + (1 · ((𝐴↑2) · 𝐵))) = ((2 · ((𝐴↑2) · 𝐵)) + ((𝐴↑2) · 𝐵)))
88	85, 87	eqtrd 2656	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (3 · ((𝐴↑2) · 𝐵)) = ((2 · ((𝐴↑2) · 𝐵)) + ((𝐴↑2) · 𝐵)))
89	88	oveq2d 6666	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) = ((𝐴↑3) + ((2 · ((𝐴↑2) · 𝐵)) + ((𝐴↑2) · 𝐵))))
90	81, 89	eqtr4d 2659	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))) + ((𝐴↑2) · 𝐵)) = ((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))))
91		1p2e3 11152	. . . . . . . 8 ⊢ (1 + 2) = 3
92	91	oveq1i 6660	. . . . . . 7 ⊢ ((1 + 2) · (𝐴 · (𝐵↑2))) = (3 · (𝐴 · (𝐵↑2)))
93	83, 36, 63	adddird 10065	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((1 + 2) · (𝐴 · (𝐵↑2))) = ((1 · (𝐴 · (𝐵↑2))) + (2 · (𝐴 · (𝐵↑2)))))
94	92, 93	syl5eqr 2670	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (3 · (𝐴 · (𝐵↑2))) = ((1 · (𝐴 · (𝐵↑2))) + (2 · (𝐴 · (𝐵↑2)))))
95	63	mulid2d 10058	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1 · (𝐴 · (𝐵↑2))) = (𝐴 · (𝐵↑2)))
96	95	oveq1d 6665	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((1 · (𝐴 · (𝐵↑2))) + (2 · (𝐴 · (𝐵↑2)))) = ((𝐴 · (𝐵↑2)) + (2 · (𝐴 · (𝐵↑2)))))
97	94, 96	eqtrd 2656	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (3 · (𝐴 · (𝐵↑2))) = ((𝐴 · (𝐵↑2)) + (2 · (𝐴 · (𝐵↑2)))))
98	97	oveq1d 6665	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3)) = (((𝐴 · (𝐵↑2)) + (2 · (𝐴 · (𝐵↑2)))) + (𝐵↑3)))
99	63, 65, 68	addassd 10062	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 · (𝐵↑2)) + (2 · (𝐴 · (𝐵↑2)))) + (𝐵↑3)) = ((𝐴 · (𝐵↑2)) + ((2 · (𝐴 · (𝐵↑2))) + (𝐵↑3))))
100	98, 99	eqtr2d 2657	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · (𝐵↑2)) + ((2 · (𝐴 · (𝐵↑2))) + (𝐵↑3))) = ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3)))
101	90, 100	oveq12d 6668	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))) + ((𝐴↑2) · 𝐵)) + ((𝐴 · (𝐵↑2)) + ((2 · (𝐴 · (𝐵↑2))) + (𝐵↑3)))) = (((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3))))
102	7, 80, 101	3eqtrd 2660	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑3) = (((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 384 = wceq 1483 ∈ wcel 1990 (class class class)co 6650 ℂcc 9934 1c1 9937 + caddc 9939 · cmul 9941 2c2 11070 3c3 11071 ℕ₀cn0 11292 ↑cexp 12860

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-2 11079 df-3 11080 df-n0 11293 df-z 11378 df-uz 11688 df-seq 12802 df-exp 12861

This theorem is referenced by: dcubic1lem 24570 mcubic 24574 binom4 24577

W3C validator