binom3

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

		Ref	Expression
	Assertion	binom3	$⊢ (A \in ℂ \land B \in ℂ) \to {(A + B)}^{3} = A^{3} + 3 A^{2} B + 3 A B^{2} + B^{3}$

Proof

Step	Hyp	Ref	Expression
1		df-3	$⊢ 3 = 2 + 1$
2	1	oveq2i	$⊢ {(A + B)}^{3} = {(A + B)}^{2 + 1}$
3		addcl	$⊢ (A \in ℂ \land B \in ℂ) \to A + B \in ℂ$
4		2nn0	$⊢ 2 \in ℕ_{0}$
5		expp1	$⊢ (A + B \in ℂ \land 2 \in ℕ_{0}) \to {(A + B)}^{2 + 1} = {(A + B)}^{2} (A + B)$
6	3 4 5	sylancl	$⊢ (A \in ℂ \land B \in ℂ) \to {(A + B)}^{2 + 1} = {(A + B)}^{2} (A + B)$
7	2 6	syl5eq	$⊢ (A \in ℂ \land B \in ℂ) \to {(A + B)}^{3} = {(A + B)}^{2} (A + B)$
8		sqcl	$⊢ A + B \in ℂ \to {(A + B)}^{2} \in ℂ$
9	3 8	syl	$⊢ (A \in ℂ \land B \in ℂ) \to {(A + B)}^{2} \in ℂ$
10		simpl	$⊢ (A \in ℂ \land B \in ℂ) \to A \in ℂ$
11		simpr	$⊢ (A \in ℂ \land B \in ℂ) \to B \in ℂ$
12	9 10 11	adddid	$⊢ (A \in ℂ \land B \in ℂ) \to {(A + B)}^{2} (A + B) = {(A + B)}^{2} A + {(A + B)}^{2} B$
13		binom2	$⊢ (A \in ℂ \land B \in ℂ) \to {(A + B)}^{2} = A^{2} + 2 A B + B^{2}$
14	13	oveq1d	$⊢ (A \in ℂ \land B \in ℂ) \to {(A + B)}^{2} A = (A^{2} + 2 A B + B^{2}) A$
15		sqcl	$⊢ A \in ℂ \to A^{2} \in ℂ$
16	10 15	syl	$⊢ (A \in ℂ \land B \in ℂ) \to A^{2} \in ℂ$
17		2cn	$⊢ 2 \in ℂ$
18		mulcl	$⊢ (A \in ℂ \land B \in ℂ) \to A B \in ℂ$
19		mulcl	$⊢ (2 \in ℂ \land A B \in ℂ) \to 2 A B \in ℂ$
20	17 18 19	sylancr	$⊢ (A \in ℂ \land B \in ℂ) \to 2 A B \in ℂ$
21	16 20	addcld	$⊢ (A \in ℂ \land B \in ℂ) \to A^{2} + 2 A B \in ℂ$
22		sqcl	$⊢ B \in ℂ \to B^{2} \in ℂ$
23	11 22	syl	$⊢ (A \in ℂ \land B \in ℂ) \to B^{2} \in ℂ$
24	21 23 10	adddird	$⊢ (A \in ℂ \land B \in ℂ) \to (A^{2} + 2 A B + B^{2}) A = (A^{2} + 2 A B) A + B^{2} A$
25	16 20 10	adddird	$⊢ (A \in ℂ \land B \in ℂ) \to (A^{2} + 2 A B) A = A^{2} A + 2 A B A$
26	1	oveq2i	$⊢ A^{3} = A^{2 + 1}$
27		expp1	$⊢ (A \in ℂ \land 2 \in ℕ_{0}) \to A^{2 + 1} = A^{2} A$
28	10 4 27	sylancl	$⊢ (A \in ℂ \land B \in ℂ) \to A^{2 + 1} = A^{2} A$
29	26 28	syl5eq	$⊢ (A \in ℂ \land B \in ℂ) \to A^{3} = A^{2} A$
30		sqval	$⊢ A \in ℂ \to A^{2} = A A$
31	10 30	syl	$⊢ (A \in ℂ \land B \in ℂ) \to A^{2} = A A$
32	31	oveq1d	$⊢ (A \in ℂ \land B \in ℂ) \to A^{2} B = A A B$
33	10 10 11	mul32d	$⊢ (A \in ℂ \land B \in ℂ) \to A A B = A B A$
34	32 33	eqtrd	$⊢ (A \in ℂ \land B \in ℂ) \to A^{2} B = A B A$
35	34	oveq2d	$⊢ (A \in ℂ \land B \in ℂ) \to 2 A^{2} B = 2 A B A$
36		2cnd	$⊢ (A \in ℂ \land B \in ℂ) \to 2 \in ℂ$
37	36 18 10	mulassd	$⊢ (A \in ℂ \land B \in ℂ) \to 2 A B A = 2 A B A$
38	35 37	eqtr4d	$⊢ (A \in ℂ \land B \in ℂ) \to 2 A^{2} B = 2 A B A$
39	29 38	oveq12d	$⊢ (A \in ℂ \land B \in ℂ) \to A^{3} + 2 A^{2} B = A^{2} A + 2 A B A$
40	25 39	eqtr4d	$⊢ (A \in ℂ \land B \in ℂ) \to (A^{2} + 2 A B) A = A^{3} + 2 A^{2} B$
41	23 10	mulcomd	$⊢ (A \in ℂ \land B \in ℂ) \to B^{2} A = A B^{2}$
42	40 41	oveq12d	$⊢ (A \in ℂ \land B \in ℂ) \to (A^{2} + 2 A B) A + B^{2} A = A^{3} + 2 A^{2} B + A B^{2}$
43	14 24 42	3eqtrd	$⊢ (A \in ℂ \land B \in ℂ) \to {(A + B)}^{2} A = A^{3} + 2 A^{2} B + A B^{2}$
44	13	oveq1d	$⊢ (A \in ℂ \land B \in ℂ) \to {(A + B)}^{2} B = (A^{2} + 2 A B + B^{2}) B$
45	21 23 11	adddird	$⊢ (A \in ℂ \land B \in ℂ) \to (A^{2} + 2 A B + B^{2}) B = (A^{2} + 2 A B) B + B^{2} B$
46		sqval	$⊢ B \in ℂ \to B^{2} = B B$
47	11 46	syl	$⊢ (A \in ℂ \land B \in ℂ) \to B^{2} = B B$
48	47	oveq2d	$⊢ (A \in ℂ \land B \in ℂ) \to A B^{2} = A B B$
49	10 11 11	mulassd	$⊢ (A \in ℂ \land B \in ℂ) \to A B B = A B B$
50	48 49	eqtr4d	$⊢ (A \in ℂ \land B \in ℂ) \to A B^{2} = A B B$
51	50	oveq2d	$⊢ (A \in ℂ \land B \in ℂ) \to 2 A B^{2} = 2 A B B$
52	36 18 11	mulassd	$⊢ (A \in ℂ \land B \in ℂ) \to 2 A B B = 2 A B B$
53	51 52	eqtr4d	$⊢ (A \in ℂ \land B \in ℂ) \to 2 A B^{2} = 2 A B B$
54	53	oveq2d	$⊢ (A \in ℂ \land B \in ℂ) \to A^{2} B + 2 A B^{2} = A^{2} B + 2 A B B$
55	16 20 11	adddird	$⊢ (A \in ℂ \land B \in ℂ) \to (A^{2} + 2 A B) B = A^{2} B + 2 A B B$
56	54 55	eqtr4d	$⊢ (A \in ℂ \land B \in ℂ) \to A^{2} B + 2 A B^{2} = (A^{2} + 2 A B) B$
57	1	oveq2i	$⊢ B^{3} = B^{2 + 1}$
58		expp1	$⊢ (B \in ℂ \land 2 \in ℕ_{0}) \to B^{2 + 1} = B^{2} B$
59	11 4 58	sylancl	$⊢ (A \in ℂ \land B \in ℂ) \to B^{2 + 1} = B^{2} B$
60	57 59	syl5eq	$⊢ (A \in ℂ \land B \in ℂ) \to B^{3} = B^{2} B$
61	56 60	oveq12d	$⊢ (A \in ℂ \land B \in ℂ) \to A^{2} B + 2 A B^{2} + B^{3} = (A^{2} + 2 A B) B + B^{2} B$
62	16 11	mulcld	$⊢ (A \in ℂ \land B \in ℂ) \to A^{2} B \in ℂ$
63	10 23	mulcld	$⊢ (A \in ℂ \land B \in ℂ) \to A B^{2} \in ℂ$
64		mulcl	$⊢ (2 \in ℂ \land A B^{2} \in ℂ) \to 2 A B^{2} \in ℂ$
65	17 63 64	sylancr	$⊢ (A \in ℂ \land B \in ℂ) \to 2 A B^{2} \in ℂ$
66		3nn0	$⊢ 3 \in ℕ_{0}$
67		expcl	$⊢ (B \in ℂ \land 3 \in ℕ_{0}) \to B^{3} \in ℂ$
68	11 66 67	sylancl	$⊢ (A \in ℂ \land B \in ℂ) \to B^{3} \in ℂ$
69	62 65 68	addassd	$⊢ (A \in ℂ \land B \in ℂ) \to A^{2} B + 2 A B^{2} + B^{3} = A^{2} B + 2 A B^{2} + B^{3}$
70	61 69	eqtr3d	$⊢ (A \in ℂ \land B \in ℂ) \to (A^{2} + 2 A B) B + B^{2} B = A^{2} B + 2 A B^{2} + B^{3}$
71	44 45 70	3eqtrd	$⊢ (A \in ℂ \land B \in ℂ) \to {(A + B)}^{2} B = A^{2} B + 2 A B^{2} + B^{3}$
72	43 71	oveq12d	$⊢ (A \in ℂ \land B \in ℂ) \to {(A + B)}^{2} A + {(A + B)}^{2} B = (A^{3} + 2 A^{2} B) + A B^{2} + A^{2} B + (2 A B^{2} + B^{3})$
73		expcl	$⊢ (A \in ℂ \land 3 \in ℕ_{0}) \to A^{3} \in ℂ$
74	10 66 73	sylancl	$⊢ (A \in ℂ \land B \in ℂ) \to A^{3} \in ℂ$
75		mulcl	$⊢ (2 \in ℂ \land A^{2} B \in ℂ) \to 2 A^{2} B \in ℂ$
76	17 62 75	sylancr	$⊢ (A \in ℂ \land B \in ℂ) \to 2 A^{2} B \in ℂ$
77	74 76	addcld	$⊢ (A \in ℂ \land B \in ℂ) \to A^{3} + 2 A^{2} B \in ℂ$
78	65 68	addcld	$⊢ (A \in ℂ \land B \in ℂ) \to 2 A B^{2} + B^{3} \in ℂ$
79	77 63 62 78	add4d	$⊢ (A \in ℂ \land B \in ℂ) \to (A^{3} + 2 A^{2} B) + A B^{2} + A^{2} B + (2 A B^{2} + B^{3}) = (A^{3} + 2 A^{2} B) + A^{2} B + A B^{2} + (2 A B^{2} + B^{3})$
80	12 72 79	3eqtrd	$⊢ (A \in ℂ \land B \in ℂ) \to {(A + B)}^{2} (A + B) = (A^{3} + 2 A^{2} B) + A^{2} B + A B^{2} + (2 A B^{2} + B^{3})$
81	74 76 62	addassd	$⊢ (A \in ℂ \land B \in ℂ) \to A^{3} + 2 A^{2} B + A^{2} B = A^{3} + 2 A^{2} B + A^{2} B$
82	1	oveq1i	$⊢ 3 A^{2} B = (2 + 1) A^{2} B$
83		1cnd	$⊢ (A \in ℂ \land B \in ℂ) \to 1 \in ℂ$
84	36 83 62	adddird	$⊢ (A \in ℂ \land B \in ℂ) \to (2 + 1) A^{2} B = 2 A^{2} B + 1 A^{2} B$
85	82 84	syl5eq	$⊢ (A \in ℂ \land B \in ℂ) \to 3 A^{2} B = 2 A^{2} B + 1 A^{2} B$
86	62	mulid2d	$⊢ (A \in ℂ \land B \in ℂ) \to 1 A^{2} B = A^{2} B$
87	86	oveq2d	$⊢ (A \in ℂ \land B \in ℂ) \to 2 A^{2} B + 1 A^{2} B = 2 A^{2} B + A^{2} B$
88	85 87	eqtrd	$⊢ (A \in ℂ \land B \in ℂ) \to 3 A^{2} B = 2 A^{2} B + A^{2} B$
89	88	oveq2d	$⊢ (A \in ℂ \land B \in ℂ) \to A^{3} + 3 A^{2} B = A^{3} + 2 A^{2} B + A^{2} B$
90	81 89	eqtr4d	$⊢ (A \in ℂ \land B \in ℂ) \to A^{3} + 2 A^{2} B + A^{2} B = A^{3} + 3 A^{2} B$
91		1p2e3	$⊢ 1 + 2 = 3$
92	91	oveq1i	$⊢ (1 + 2) A B^{2} = 3 A B^{2}$
93	83 36 63	adddird	$⊢ (A \in ℂ \land B \in ℂ) \to (1 + 2) A B^{2} = 1 A B^{2} + 2 A B^{2}$
94	92 93	syl5eqr	$⊢ (A \in ℂ \land B \in ℂ) \to 3 A B^{2} = 1 A B^{2} + 2 A B^{2}$
95	63	mulid2d	$⊢ (A \in ℂ \land B \in ℂ) \to 1 A B^{2} = A B^{2}$
96	95	oveq1d	$⊢ (A \in ℂ \land B \in ℂ) \to 1 A B^{2} + 2 A B^{2} = A B^{2} + 2 A B^{2}$
97	94 96	eqtrd	$⊢ (A \in ℂ \land B \in ℂ) \to 3 A B^{2} = A B^{2} + 2 A B^{2}$
98	97	oveq1d	$⊢ (A \in ℂ \land B \in ℂ) \to 3 A B^{2} + B^{3} = A B^{2} + 2 A B^{2} + B^{3}$
99	63 65 68	addassd	$⊢ (A \in ℂ \land B \in ℂ) \to A B^{2} + 2 A B^{2} + B^{3} = A B^{2} + 2 A B^{2} + B^{3}$
100	98 99	eqtr2d	$⊢ (A \in ℂ \land B \in ℂ) \to A B^{2} + 2 A B^{2} + B^{3} = 3 A B^{2} + B^{3}$
101	90 100	oveq12d	$⊢ (A \in ℂ \land B \in ℂ) \to (A^{3} + 2 A^{2} B) + A^{2} B + A B^{2} + (2 A B^{2} + B^{3}) = A^{3} + 3 A^{2} B + 3 A B^{2} + B^{3}$
102	7 80 101	3eqtrd	$⊢ (A \in ℂ \land B \in ℂ) \to {(A + B)}^{3} = A^{3} + 3 A^{2} B + 3 A B^{2} + B^{3}$

Metamath Proof Explorer

Theorem binom3

Proof