cu3addd

Description: Cube of sum of three numbers. (Contributed by Igor Ieskov, 14-Dec-2023)

	Ref	Expression
Hypotheses	cu3addd.1	$⊢ φ \to A \in ℂ$
	cu3addd.2	$⊢ φ \to B \in ℂ$
	cu3addd.3	$⊢ φ \to C \in ℂ$
Assertion	cu3addd	$⊢ φ \to {(A + B + C)}^{3} = (A^{3} + 3 A^{2} B + 3 A B^{2} + B^{3}) + (3 A^{2} C + 3 \cdot 2 A B C + 3 B^{2} C) + (3 A C^{2} + 3 B C^{2}) + C^{3}$

Proof

Step	Hyp	Ref	Expression
1		cu3addd.1	$⊢ φ \to A \in ℂ$
2		cu3addd.2	$⊢ φ \to B \in ℂ$
3		cu3addd.3	$⊢ φ \to C \in ℂ$
4	1 2	addcld	$⊢ φ \to A + B \in ℂ$
5	4 3	jca	$⊢ φ \to (A + B \in ℂ \land C \in ℂ)$
6		binom3	$⊢ (A + B \in ℂ \land C \in ℂ) \to {(A + B + C)}^{3} = {(A + B)}^{3} + 3 {(A + B)}^{2} C + 3 (A + B) C^{2} + C^{3}$
7	6	a1i	$⊢ φ \to ((A + B \in ℂ \land C \in ℂ) \to {(A + B + C)}^{3} = {(A + B)}^{3} + 3 {(A + B)}^{2} C + 3 (A + B) C^{2} + C^{3})$
8	5 7	mpd	$⊢ φ \to {(A + B + C)}^{3} = {(A + B)}^{3} + 3 {(A + B)}^{2} C + 3 (A + B) C^{2} + C^{3}$
9		binom3	$⊢ (A \in ℂ \land B \in ℂ) \to {(A + B)}^{3} = A^{3} + 3 A^{2} B + 3 A B^{2} + B^{3}$
10	1 2 9	syl2anc	$⊢ φ \to {(A + B)}^{3} = A^{3} + 3 A^{2} B + 3 A B^{2} + B^{3}$
11	10	oveq1d	$⊢ φ \to {(A + B)}^{3} + 3 {(A + B)}^{2} C = (A^{3} + 3 A^{2} B) + (3 A B^{2} + B^{3}) + 3 {(A + B)}^{2} C$
12	11	oveq1d	$⊢ φ \to {(A + B)}^{3} + 3 {(A + B)}^{2} C + 3 (A + B) C^{2} + C^{3} = (A^{3} + 3 A^{2} B + 3 A B^{2} + B^{3}) + 3 {(A + B)}^{2} C + 3 (A + B) C^{2} + C^{3}$
13	8 12	eqtrd	$⊢ φ \to {(A + B + C)}^{3} = (A^{3} + 3 A^{2} B + 3 A B^{2} + B^{3}) + 3 {(A + B)}^{2} C + 3 (A + B) C^{2} + C^{3}$
14	1 2	binom2d	$⊢ φ \to {(A + B)}^{2} = A^{2} + 2 A B + B^{2}$
15	14	oveq1d	$⊢ φ \to {(A + B)}^{2} C = (A^{2} + 2 A B + B^{2}) C$
16	15	oveq2d	$⊢ φ \to 3 {(A + B)}^{2} C = 3 (A^{2} + 2 A B + B^{2}) C$
17	16	oveq2d	$⊢ φ \to (A^{3} + 3 A^{2} B) + (3 A B^{2} + B^{3}) + 3 {(A + B)}^{2} C = (A^{3} + 3 A^{2} B) + (3 A B^{2} + B^{3}) + 3 (A^{2} + 2 A B + B^{2}) C$
18	17	oveq1d	$⊢ φ \to (A^{3} + 3 A^{2} B + 3 A B^{2} + B^{3}) + 3 {(A + B)}^{2} C + 3 (A + B) C^{2} + C^{3} = (A^{3} + 3 A^{2} B + 3 A B^{2} + B^{3}) + 3 (A^{2} + 2 A B + B^{2}) C + 3 (A + B) C^{2} + C^{3}$
19	13 18	eqtrd	$⊢ φ \to {(A + B + C)}^{3} = (A^{3} + 3 A^{2} B + 3 A B^{2} + B^{3}) + 3 (A^{2} + 2 A B + B^{2}) C + 3 (A + B) C^{2} + C^{3}$
20	1	sqcld	$⊢ φ \to A^{2} \in ℂ$
21		2cnd	$⊢ φ \to 2 \in ℂ$
22	1 2	mulcld	$⊢ φ \to A B \in ℂ$
23	21 22	mulcld	$⊢ φ \to 2 A B \in ℂ$
24	20 23	addcld	$⊢ φ \to A^{2} + 2 A B \in ℂ$
25	2	sqcld	$⊢ φ \to B^{2} \in ℂ$
26	24 25 3	adddird	$⊢ φ \to (A^{2} + 2 A B + B^{2}) C = (A^{2} + 2 A B) C + B^{2} C$
27	26	oveq2d	$⊢ φ \to 3 (A^{2} + 2 A B + B^{2}) C = 3 ((A^{2} + 2 A B) C + B^{2} C)$
28	27	oveq2d	$⊢ φ \to (A^{3} + 3 A^{2} B) + (3 A B^{2} + B^{3}) + 3 (A^{2} + 2 A B + B^{2}) C = (A^{3} + 3 A^{2} B) + (3 A B^{2} + B^{3}) + 3 ((A^{2} + 2 A B) C + B^{2} C)$
29	28	oveq1d	$⊢ φ \to (A^{3} + 3 A^{2} B + 3 A B^{2} + B^{3}) + 3 (A^{2} + 2 A B + B^{2}) C + 3 (A + B) C^{2} + C^{3} = (A^{3} + 3 A^{2} B + 3 A B^{2} + B^{3}) + 3 ((A^{2} + 2 A B) C + B^{2} C) + 3 (A + B) C^{2} + C^{3}$
30	19 29	eqtrd	$⊢ φ \to {(A + B + C)}^{3} = (A^{3} + 3 A^{2} B + 3 A B^{2} + B^{3}) + 3 ((A^{2} + 2 A B) C + B^{2} C) + 3 (A + B) C^{2} + C^{3}$
31	20 23 3	adddird	$⊢ φ \to (A^{2} + 2 A B) C = A^{2} C + 2 A B C$
32	31	oveq1d	$⊢ φ \to (A^{2} + 2 A B) C + B^{2} C = A^{2} C + 2 A B C + B^{2} C$
33	32	oveq2d	$⊢ φ \to 3 ((A^{2} + 2 A B) C + B^{2} C) = 3 (A^{2} C + 2 A B C + B^{2} C)$
34	33	oveq2d	$⊢ φ \to (A^{3} + 3 A^{2} B) + (3 A B^{2} + B^{3}) + 3 ((A^{2} + 2 A B) C + B^{2} C) = (A^{3} + 3 A^{2} B) + (3 A B^{2} + B^{3}) + 3 (A^{2} C + 2 A B C + B^{2} C)$
35	34	oveq1d	$⊢ φ \to (A^{3} + 3 A^{2} B + 3 A B^{2} + B^{3}) + 3 ((A^{2} + 2 A B) C + B^{2} C) + 3 (A + B) C^{2} + C^{3} = (A^{3} + 3 A^{2} B + 3 A B^{2} + B^{3}) + 3 (A^{2} C + 2 A B C + B^{2} C) + 3 (A + B) C^{2} + C^{3}$
36	30 35	eqtrd	$⊢ φ \to {(A + B + C)}^{3} = (A^{3} + 3 A^{2} B + 3 A B^{2} + B^{3}) + 3 (A^{2} C + 2 A B C + B^{2} C) + 3 (A + B) C^{2} + C^{3}$
37		3cn	$⊢ 3 \in ℂ$
38	37	a1i	$⊢ φ \to 3 \in ℂ$
39	20 3	mulcld	$⊢ φ \to A^{2} C \in ℂ$
40	23 3	mulcld	$⊢ φ \to 2 A B C \in ℂ$
41	39 40	addcld	$⊢ φ \to A^{2} C + 2 A B C \in ℂ$
42	25 3	mulcld	$⊢ φ \to B^{2} C \in ℂ$
43	38 41 42	adddid	$⊢ φ \to 3 (A^{2} C + 2 A B C + B^{2} C) = 3 (A^{2} C + 2 A B C) + 3 B^{2} C$
44	43	oveq2d	$⊢ φ \to (A^{3} + 3 A^{2} B) + (3 A B^{2} + B^{3}) + 3 (A^{2} C + 2 A B C + B^{2} C) = (A^{3} + 3 A^{2} B) + (3 A B^{2} + B^{3}) + 3 (A^{2} C + 2 A B C) + 3 B^{2} C$
45	44	oveq1d	$⊢ φ \to (A^{3} + 3 A^{2} B + 3 A B^{2} + B^{3}) + 3 (A^{2} C + 2 A B C + B^{2} C) + 3 (A + B) C^{2} + C^{3} = (A^{3} + 3 A^{2} B + 3 A B^{2} + B^{3}) + (3 (A^{2} C + 2 A B C) + 3 B^{2} C) + 3 (A + B) C^{2} + C^{3}$
46	36 45	eqtrd	$⊢ φ \to {(A + B + C)}^{3} = (A^{3} + 3 A^{2} B + 3 A B^{2} + B^{3}) + (3 (A^{2} C + 2 A B C) + 3 B^{2} C) + 3 (A + B) C^{2} + C^{3}$
47	38 39 40	adddid	$⊢ φ \to 3 (A^{2} C + 2 A B C) = 3 A^{2} C + 3 2 A B C$
48	47	oveq1d	$⊢ φ \to 3 (A^{2} C + 2 A B C) + 3 B^{2} C = 3 A^{2} C + 3 2 A B C + 3 B^{2} C$
49	48	oveq2d	$⊢ φ \to (A^{3} + 3 A^{2} B) + (3 A B^{2} + B^{3}) + 3 (A^{2} C + 2 A B C) + 3 B^{2} C = (A^{3} + 3 A^{2} B) + (3 A B^{2} + B^{3}) + (3 A^{2} C + 3 2 A B C) + 3 B^{2} C$
50	49	oveq1d	$⊢ φ \to (A^{3} + 3 A^{2} B + 3 A B^{2} + B^{3}) + (3 (A^{2} C + 2 A B C) + 3 B^{2} C) + 3 (A + B) C^{2} + C^{3} = (A^{3} + 3 A^{2} B + 3 A B^{2} + B^{3}) + (3 A^{2} C + 3 2 A B C + 3 B^{2} C) + 3 (A + B) C^{2} + C^{3}$
51	46 50	eqtrd	$⊢ φ \to {(A + B + C)}^{3} = (A^{3} + 3 A^{2} B + 3 A B^{2} + B^{3}) + (3 A^{2} C + 3 2 A B C + 3 B^{2} C) + 3 (A + B) C^{2} + C^{3}$
52	38 21 22	mulassd	$⊢ φ \to 3 \cdot 2 A B = 3 2 A B$
53	52	oveq1d	$⊢ φ \to 3 \cdot 2 A B C = 3 2 A B C$
54	38 23 3	mulassd	$⊢ φ \to 3 2 A B C = 3 2 A B C$
55	53 54	eqtrd	$⊢ φ \to 3 \cdot 2 A B C = 3 2 A B C$
56	55	oveq2d	$⊢ φ \to 3 A^{2} C + 3 \cdot 2 A B C = 3 A^{2} C + 3 2 A B C$
57	56	oveq1d	$⊢ φ \to 3 A^{2} C + 3 \cdot 2 A B C + 3 B^{2} C = 3 A^{2} C + 3 2 A B C + 3 B^{2} C$
58	57	oveq2d	$⊢ φ \to (A^{3} + 3 A^{2} B) + (3 A B^{2} + B^{3}) + (3 A^{2} C + 3 \cdot 2 A B C) + 3 B^{2} C = (A^{3} + 3 A^{2} B) + (3 A B^{2} + B^{3}) + (3 A^{2} C + 3 2 A B C) + 3 B^{2} C$
59	58	eqcomd	$⊢ φ \to (A^{3} + 3 A^{2} B) + (3 A B^{2} + B^{3}) + (3 A^{2} C + 3 2 A B C) + 3 B^{2} C = (A^{3} + 3 A^{2} B) + (3 A B^{2} + B^{3}) + (3 A^{2} C + 3 \cdot 2 A B C) + 3 B^{2} C$
60	59	oveq1d	$⊢ φ \to (A^{3} + 3 A^{2} B + 3 A B^{2} + B^{3}) + (3 A^{2} C + 3 2 A B C + 3 B^{2} C) + 3 (A + B) C^{2} + C^{3} = (A^{3} + 3 A^{2} B + 3 A B^{2} + B^{3}) + (3 A^{2} C + 3 \cdot 2 A B C + 3 B^{2} C) + 3 (A + B) C^{2} + C^{3}$
61	51 60	eqtrd	$⊢ φ \to {(A + B + C)}^{3} = (A^{3} + 3 A^{2} B + 3 A B^{2} + B^{3}) + (3 A^{2} C + 3 \cdot 2 A B C + 3 B^{2} C) + 3 (A + B) C^{2} + C^{3}$
62	3	sqcld	$⊢ φ \to C^{2} \in ℂ$
63	1 2 62	adddird	$⊢ φ \to (A + B) C^{2} = A C^{2} + B C^{2}$
64	63	oveq2d	$⊢ φ \to 3 (A + B) C^{2} = 3 (A C^{2} + B C^{2})$
65	64	oveq1d	$⊢ φ \to 3 (A + B) C^{2} + C^{3} = 3 (A C^{2} + B C^{2}) + C^{3}$
66	65	oveq2d	$⊢ φ \to (A^{3} + 3 A^{2} B + 3 A B^{2} + B^{3}) + (3 A^{2} C + 3 \cdot 2 A B C + 3 B^{2} C) + 3 (A + B) C^{2} + C^{3} = (A^{3} + 3 A^{2} B + 3 A B^{2} + B^{3}) + (3 A^{2} C + 3 \cdot 2 A B C + 3 B^{2} C) + 3 (A C^{2} + B C^{2}) + C^{3}$
67	61 66	eqtrd	$⊢ φ \to {(A + B + C)}^{3} = (A^{3} + 3 A^{2} B + 3 A B^{2} + B^{3}) + (3 A^{2} C + 3 \cdot 2 A B C + 3 B^{2} C) + 3 (A C^{2} + B C^{2}) + C^{3}$
68	1 62	mulcld	$⊢ φ \to A C^{2} \in ℂ$
69	2 62	mulcld	$⊢ φ \to B C^{2} \in ℂ$
70	38 68 69	adddid	$⊢ φ \to 3 (A C^{2} + B C^{2}) = 3 A C^{2} + 3 B C^{2}$
71	70	oveq1d	$⊢ φ \to 3 (A C^{2} + B C^{2}) + C^{3} = 3 A C^{2} + 3 B C^{2} + C^{3}$
72	71	oveq2d	$⊢ φ \to (A^{3} + 3 A^{2} B + 3 A B^{2} + B^{3}) + (3 A^{2} C + 3 \cdot 2 A B C + 3 B^{2} C) + 3 (A C^{2} + B C^{2}) + C^{3} = (A^{3} + 3 A^{2} B + 3 A B^{2} + B^{3}) + (3 A^{2} C + 3 \cdot 2 A B C + 3 B^{2} C) + (3 A C^{2} + 3 B C^{2}) + C^{3}$
73	67 72	eqtrd	$⊢ φ \to {(A + B + C)}^{3} = (A^{3} + 3 A^{2} B + 3 A B^{2} + B^{3}) + (3 A^{2} C + 3 \cdot 2 A B C + 3 B^{2} C) + (3 A C^{2} + 3 B C^{2}) + C^{3}$

Metamath Proof Explorer

Theorem cu3addd

Proof