Proof of Theorem binom3
Step | Hyp | Ref
| Expression |
1 | | df-3 7754 |
. . . 4
⊢ 3 = (2 +
1) |
2 | 1 | oveq2i 5466 |
. . 3
⊢
((A + B)↑3) = ((A
+ B)↑(2 + 1)) |
3 | | addcl 6804 |
. . . 4
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (A + B) ∈
ℂ) |
4 | | 2nn0 7974 |
. . . 4
⊢ 2 ∈ ℕ0 |
5 | | expp1 8916 |
. . . 4
⊢
(((A + B) ∈ ℂ ∧ 2 ∈
ℕ0) → ((A + B)↑(2 + 1)) = (((A + B)↑2)
· (A + B))) |
6 | 3, 4, 5 | sylancl 392 |
. . 3
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((A + B)↑(2 + 1)) = (((A + B)↑2)
· (A + B))) |
7 | 2, 6 | syl5eq 2081 |
. 2
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((A + B)↑3) = (((A + B)↑2)
· (A + B))) |
8 | | sqcl 8969 |
. . . . 5
⊢
((A + B) ∈ ℂ
→ ((A + B)↑2) ∈
ℂ) |
9 | 3, 8 | syl 14 |
. . . 4
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((A + B)↑2) ∈
ℂ) |
10 | | simpl 102 |
. . . 4
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → A ∈ ℂ) |
11 | | simpr 103 |
. . . 4
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → B ∈ ℂ) |
12 | 9, 10, 11 | adddid 6849 |
. . 3
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (((A + B)↑2) · (A + B)) =
((((A + B)↑2) · A) + (((A +
B)↑2) · B))) |
13 | | binom2 9015 |
. . . . . 6
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((A + B)↑2) = (((A↑2) + (2 · (A · B)))
+ (B↑2))) |
14 | 13 | oveq1d 5470 |
. . . . 5
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (((A + B)↑2) · A) = ((((A↑2) + (2 · (A · B)))
+ (B↑2)) · A)) |
15 | | sqcl 8969 |
. . . . . . . 8
⊢ (A ∈ ℂ →
(A↑2) ∈ ℂ) |
16 | 10, 15 | syl 14 |
. . . . . . 7
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (A↑2) ∈ ℂ) |
17 | | 2cn 7766 |
. . . . . . . 8
⊢ 2 ∈ ℂ |
18 | | mulcl 6806 |
. . . . . . . 8
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (A · B) ∈
ℂ) |
19 | | mulcl 6806 |
. . . . . . . 8
⊢ ((2 ∈ ℂ ∧
(A · B) ∈ ℂ)
→ (2 · (A · B)) ∈
ℂ) |
20 | 17, 18, 19 | sylancr 393 |
. . . . . . 7
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (2 · (A ·
B)) ∈
ℂ) |
21 | 16, 20 | addcld 6844 |
. . . . . 6
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((A↑2) + (2 ·
(A · B))) ∈
ℂ) |
22 | | sqcl 8969 |
. . . . . . 7
⊢ (B ∈ ℂ →
(B↑2) ∈ ℂ) |
23 | 11, 22 | syl 14 |
. . . . . 6
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (B↑2) ∈ ℂ) |
24 | 21, 23, 10 | adddird 6850 |
. . . . 5
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((((A↑2) + (2 ·
(A · B))) + (B↑2)) · A) = ((((A↑2) + (2 · (A · B)))
· A) + ((B↑2) · A))) |
25 | 16, 20, 10 | adddird 6850 |
. . . . . . 7
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (((A↑2) + (2 ·
(A · B))) · A)
= (((A↑2) · A) + ((2 · (A · B))
· A))) |
26 | 1 | oveq2i 5466 |
. . . . . . . . 9
⊢ (A↑3) = (A↑(2 + 1)) |
27 | | expp1 8916 |
. . . . . . . . . 10
⊢
((A ∈ ℂ ∧ 2
∈ ℕ0) → (A↑(2 + 1)) = ((A↑2) · A)) |
28 | 10, 4, 27 | sylancl 392 |
. . . . . . . . 9
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (A↑(2 + 1)) =
((A↑2) · A)) |
29 | 26, 28 | syl5eq 2081 |
. . . . . . . 8
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (A↑3) = ((A↑2) · A)) |
30 | | sqval 8966 |
. . . . . . . . . . . . 13
⊢ (A ∈ ℂ →
(A↑2) = (A · A)) |
31 | 10, 30 | syl 14 |
. . . . . . . . . . . 12
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (A↑2) = (A · A)) |
32 | 31 | oveq1d 5470 |
. . . . . . . . . . 11
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((A↑2) ·
B) = ((A · A)
· B)) |
33 | 10, 10, 11 | mul32d 6963 |
. . . . . . . . . . 11
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((A · A) · B) =
((A · B) · A)) |
34 | 32, 33 | eqtrd 2069 |
. . . . . . . . . 10
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((A↑2) ·
B) = ((A · B)
· A)) |
35 | 34 | oveq2d 5471 |
. . . . . . . . 9
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (2 · ((A↑2)
· B)) = (2 · ((A · B)
· A))) |
36 | | 2cnd 7768 |
. . . . . . . . . 10
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → 2 ∈ ℂ) |
37 | 36, 18, 10 | mulassd 6848 |
. . . . . . . . 9
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((2 · (A ·
B)) · A) = (2 · ((A · B)
· A))) |
38 | 35, 37 | eqtr4d 2072 |
. . . . . . . 8
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (2 · ((A↑2)
· B)) = ((2 · (A · B))
· A)) |
39 | 29, 38 | oveq12d 5473 |
. . . . . . 7
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((A↑3) + (2 ·
((A↑2) · B))) = (((A↑2) · A) + ((2 · (A · B))
· A))) |
40 | 25, 39 | eqtr4d 2072 |
. . . . . 6
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (((A↑2) + (2 ·
(A · B))) · A)
= ((A↑3) + (2 · ((A↑2) · B)))) |
41 | 23, 10 | mulcomd 6846 |
. . . . . 6
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((B↑2) ·
A) = (A
· (B↑2))) |
42 | 40, 41 | oveq12d 5473 |
. . . . 5
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((((A↑2) + (2 ·
(A · B))) · A)
+ ((B↑2) · A)) = (((A↑3) + (2 · ((A↑2) · B))) + (A
· (B↑2)))) |
43 | 14, 24, 42 | 3eqtrd 2073 |
. . . 4
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (((A + B)↑2) · A) = (((A↑3) + (2 · ((A↑2) · B))) + (A
· (B↑2)))) |
44 | 13 | oveq1d 5470 |
. . . . 5
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (((A + B)↑2) · B) = ((((A↑2) + (2 · (A · B)))
+ (B↑2)) · B)) |
45 | 21, 23, 11 | adddird 6850 |
. . . . 5
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((((A↑2) + (2 ·
(A · B))) + (B↑2)) · B) = ((((A↑2) + (2 · (A · B)))
· B) + ((B↑2) · B))) |
46 | | sqval 8966 |
. . . . . . . . . . . . . 14
⊢ (B ∈ ℂ →
(B↑2) = (B · B)) |
47 | 11, 46 | syl 14 |
. . . . . . . . . . . . 13
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (B↑2) = (B · B)) |
48 | 47 | oveq2d 5471 |
. . . . . . . . . . . 12
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (A · (B↑2)) = (A
· (B · B))) |
49 | 10, 11, 11 | mulassd 6848 |
. . . . . . . . . . . 12
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((A · B) · B) =
(A · (B · B))) |
50 | 48, 49 | eqtr4d 2072 |
. . . . . . . . . . 11
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (A · (B↑2)) = ((A
· B) · B)) |
51 | 50 | oveq2d 5471 |
. . . . . . . . . 10
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (2 · (A ·
(B↑2))) = (2 · ((A · B)
· B))) |
52 | 36, 18, 11 | mulassd 6848 |
. . . . . . . . . 10
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((2 · (A ·
B)) · B) = (2 · ((A · B)
· B))) |
53 | 51, 52 | eqtr4d 2072 |
. . . . . . . . 9
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (2 · (A ·
(B↑2))) = ((2 · (A · B))
· B)) |
54 | 53 | oveq2d 5471 |
. . . . . . . 8
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (((A↑2) ·
B) + (2 · (A · (B↑2)))) = (((A↑2) · B) + ((2 · (A · B))
· B))) |
55 | 16, 20, 11 | adddird 6850 |
. . . . . . . 8
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (((A↑2) + (2 ·
(A · B))) · B)
= (((A↑2) · B) + ((2 · (A · B))
· B))) |
56 | 54, 55 | eqtr4d 2072 |
. . . . . . 7
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (((A↑2) ·
B) + (2 · (A · (B↑2)))) = (((A↑2) + (2 · (A · B)))
· B)) |
57 | 1 | oveq2i 5466 |
. . . . . . . 8
⊢ (B↑3) = (B↑(2 + 1)) |
58 | | expp1 8916 |
. . . . . . . . 9
⊢
((B ∈ ℂ ∧ 2
∈ ℕ0) → (B↑(2 + 1)) = ((B↑2) · B)) |
59 | 11, 4, 58 | sylancl 392 |
. . . . . . . 8
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (B↑(2 + 1)) =
((B↑2) · B)) |
60 | 57, 59 | syl5eq 2081 |
. . . . . . 7
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (B↑3) = ((B↑2) · B)) |
61 | 56, 60 | oveq12d 5473 |
. . . . . 6
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((((A↑2) ·
B) + (2 · (A · (B↑2)))) + (B↑3)) = ((((A↑2) + (2 · (A · B)))
· B) + ((B↑2) · B))) |
62 | 16, 11 | mulcld 6845 |
. . . . . . 7
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((A↑2) ·
B) ∈
ℂ) |
63 | 10, 23 | mulcld 6845 |
. . . . . . . 8
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (A · (B↑2)) ∈
ℂ) |
64 | | mulcl 6806 |
. . . . . . . 8
⊢ ((2 ∈ ℂ ∧
(A · (B↑2)) ∈
ℂ) → (2 · (A ·
(B↑2))) ∈ ℂ) |
65 | 17, 63, 64 | sylancr 393 |
. . . . . . 7
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (2 · (A ·
(B↑2))) ∈ ℂ) |
66 | | 3nn0 7975 |
. . . . . . . 8
⊢ 3 ∈ ℕ0 |
67 | | expcl 8927 |
. . . . . . . 8
⊢
((B ∈ ℂ ∧ 3
∈ ℕ0) → (B↑3) ∈
ℂ) |
68 | 11, 66, 67 | sylancl 392 |
. . . . . . 7
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (B↑3) ∈ ℂ) |
69 | 62, 65, 68 | addassd 6847 |
. . . . . 6
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((((A↑2) ·
B) + (2 · (A · (B↑2)))) + (B↑3)) = (((A↑2) · B) + ((2 · (A · (B↑2))) + (B↑3)))) |
70 | 61, 69 | eqtr3d 2071 |
. . . . 5
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((((A↑2) + (2 ·
(A · B))) · B)
+ ((B↑2) · B)) = (((A↑2) · B) + ((2 · (A · (B↑2))) + (B↑3)))) |
71 | 44, 45, 70 | 3eqtrd 2073 |
. . . 4
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (((A + B)↑2) · B) = (((A↑2) · B) + ((2 · (A · (B↑2))) + (B↑3)))) |
72 | 43, 71 | oveq12d 5473 |
. . 3
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((((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 8927 |
. . . . . 6
⊢
((A ∈ ℂ ∧ 3
∈ ℕ0) → (A↑3) ∈
ℂ) |
74 | 10, 66, 73 | sylancl 392 |
. . . . 5
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (A↑3) ∈ ℂ) |
75 | | mulcl 6806 |
. . . . . 6
⊢ ((2 ∈ ℂ ∧
((A↑2) · B) ∈ ℂ)
→ (2 · ((A↑2) ·
B)) ∈
ℂ) |
76 | 17, 62, 75 | sylancr 393 |
. . . . 5
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (2 · ((A↑2)
· B)) ∈ ℂ) |
77 | 74, 76 | addcld 6844 |
. . . 4
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((A↑3) + (2 ·
((A↑2) · B))) ∈
ℂ) |
78 | 65, 68 | addcld 6844 |
. . . 4
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((2 · (A ·
(B↑2))) + (B↑3)) ∈
ℂ) |
79 | 77, 63, 62, 78 | add4d 6977 |
. . 3
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((((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 2073 |
. 2
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (((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 6847 |
. . . 4
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (((A↑3) + (2 ·
((A↑2) · B))) + ((A↑2) · B)) = ((A↑3) + ((2 · ((A↑2) · B)) + ((A↑2) · B)))) |
82 | 1 | oveq1i 5465 |
. . . . . . 7
⊢ (3
· ((A↑2) · B)) = ((2 + 1) · ((A↑2) · B)) |
83 | | 1cnd 6841 |
. . . . . . . 8
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → 1 ∈ ℂ) |
84 | 36, 83, 62 | adddird 6850 |
. . . . . . 7
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((2 + 1) · ((A↑2) · B)) = ((2 · ((A↑2) · B)) + (1 · ((A↑2) · B)))) |
85 | 82, 84 | syl5eq 2081 |
. . . . . 6
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (3 · ((A↑2)
· B)) = ((2 · ((A↑2) · B)) + (1 · ((A↑2) · B)))) |
86 | 62 | mulid2d 6843 |
. . . . . . 7
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (1 · ((A↑2)
· B)) = ((A↑2) · B)) |
87 | 86 | oveq2d 5471 |
. . . . . 6
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((2 · ((A↑2)
· B)) + (1 · ((A↑2) · B))) = ((2 · ((A↑2) · B)) + ((A↑2) · B))) |
88 | 85, 87 | eqtrd 2069 |
. . . . 5
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (3 · ((A↑2)
· B)) = ((2 · ((A↑2) · B)) + ((A↑2) · B))) |
89 | 88 | oveq2d 5471 |
. . . 4
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((A↑3) + (3 ·
((A↑2) · B))) = ((A↑3) + ((2 · ((A↑2) · B)) + ((A↑2) · B)))) |
90 | 81, 89 | eqtr4d 2072 |
. . 3
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (((A↑3) + (2 ·
((A↑2) · B))) + ((A↑2) · B)) = ((A↑3) + (3 · ((A↑2) · B)))) |
91 | | 1p2e3 7822 |
. . . . . . . 8
⊢ (1 + 2) =
3 |
92 | 91 | oveq1i 5465 |
. . . . . . 7
⊢ ((1 + 2)
· (A · (B↑2))) = (3 · (A · (B↑2))) |
93 | 83, 36, 63 | adddird 6850 |
. . . . . . 7
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((1 + 2) · (A
· (B↑2))) = ((1 ·
(A · (B↑2))) + (2 · (A · (B↑2))))) |
94 | 92, 93 | syl5eqr 2083 |
. . . . . 6
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (3 · (A ·
(B↑2))) = ((1 · (A · (B↑2))) + (2 · (A · (B↑2))))) |
95 | 63 | mulid2d 6843 |
. . . . . . 7
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (1 · (A ·
(B↑2))) = (A · (B↑2))) |
96 | 95 | oveq1d 5470 |
. . . . . 6
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((1 · (A ·
(B↑2))) + (2 · (A · (B↑2)))) = ((A · (B↑2)) + (2 · (A · (B↑2))))) |
97 | 94, 96 | eqtrd 2069 |
. . . . 5
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (3 · (A ·
(B↑2))) = ((A · (B↑2)) + (2 · (A · (B↑2))))) |
98 | 97 | oveq1d 5470 |
. . . 4
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((3 · (A ·
(B↑2))) + (B↑3)) = (((A · (B↑2)) + (2 · (A · (B↑2)))) + (B↑3))) |
99 | 63, 65, 68 | addassd 6847 |
. . . 4
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (((A · (B↑2)) + (2 · (A · (B↑2)))) + (B↑3)) = ((A
· (B↑2)) + ((2 ·
(A · (B↑2))) + (B↑3)))) |
100 | 98, 99 | eqtr2d 2070 |
. . 3
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((A · (B↑2)) + ((2 · (A · (B↑2))) + (B↑3))) = ((3 · (A · (B↑2))) + (B↑3))) |
101 | 90, 100 | oveq12d 5473 |
. 2
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((((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 2073 |
1
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((A + B)↑3) = (((A↑3) + (3 · ((A↑2) · B))) + ((3 · (A · (B↑2))) + (B↑3)))) |