Proof of Theorem binom3
| Step | Hyp | Ref
| Expression |
| 1 | | df-3 12330 |
. . . 4
⊢ 3 = (2 +
1) |
| 2 | 1 | oveq2i 7442 |
. . 3
⊢ ((𝐴 + 𝐵)↑3) = ((𝐴 + 𝐵)↑(2 + 1)) |
| 3 | | addcl 11237 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) |
| 4 | | 2nn0 12543 |
. . . 4
⊢ 2 ∈
ℕ0 |
| 5 | | expp1 14109 |
. . . 4
⊢ (((𝐴 + 𝐵) ∈ ℂ ∧ 2 ∈
ℕ0) → ((𝐴 + 𝐵)↑(2 + 1)) = (((𝐴 + 𝐵)↑2) · (𝐴 + 𝐵))) |
| 6 | 3, 4, 5 | sylancl 586 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑(2 + 1)) = (((𝐴 + 𝐵)↑2) · (𝐴 + 𝐵))) |
| 7 | 2, 6 | eqtrid 2789 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑3) = (((𝐴 + 𝐵)↑2) · (𝐴 + 𝐵))) |
| 8 | | sqcl 14158 |
. . . . 5
⊢ ((𝐴 + 𝐵) ∈ ℂ → ((𝐴 + 𝐵)↑2) ∈ ℂ) |
| 9 | 3, 8 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑2) ∈ ℂ) |
| 10 | | simpl 482 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈
ℂ) |
| 11 | | simpr 484 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈
ℂ) |
| 12 | 9, 10, 11 | adddid 11285 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵)↑2) · (𝐴 + 𝐵)) = ((((𝐴 + 𝐵)↑2) · 𝐴) + (((𝐴 + 𝐵)↑2) · 𝐵))) |
| 13 | | binom2 14256 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑2) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2))) |
| 14 | 13 | oveq1d 7446 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵)↑2) · 𝐴) = ((((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)) · 𝐴)) |
| 15 | | sqcl 14158 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (𝐴↑2) ∈
ℂ) |
| 16 | 10, 15 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑2) ∈
ℂ) |
| 17 | | 2cn 12341 |
. . . . . . . 8
⊢ 2 ∈
ℂ |
| 18 | | mulcl 11239 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) |
| 19 | | mulcl 11239 |
. . . . . . . 8
⊢ ((2
∈ ℂ ∧ (𝐴
· 𝐵) ∈ ℂ)
→ (2 · (𝐴
· 𝐵)) ∈
ℂ) |
| 20 | 17, 18, 19 | sylancr 587 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2
· (𝐴 · 𝐵)) ∈
ℂ) |
| 21 | 16, 20 | addcld 11280 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) + (2 · (𝐴 · 𝐵))) ∈ ℂ) |
| 22 | | sqcl 14158 |
. . . . . . 7
⊢ (𝐵 ∈ ℂ → (𝐵↑2) ∈
ℂ) |
| 23 | 11, 22 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑2) ∈
ℂ) |
| 24 | 21, 23, 10 | adddird 11286 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((((𝐴↑2) + (2 ·
(𝐴 · 𝐵))) + (𝐵↑2)) · 𝐴) = ((((𝐴↑2) + (2 · (𝐴 · 𝐵))) · 𝐴) + ((𝐵↑2) · 𝐴))) |
| 25 | 16, 20, 10 | adddird 11286 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑2) + (2 · (𝐴 · 𝐵))) · 𝐴) = (((𝐴↑2) · 𝐴) + ((2 · (𝐴 · 𝐵)) · 𝐴))) |
| 26 | 1 | oveq2i 7442 |
. . . . . . . . 9
⊢ (𝐴↑3) = (𝐴↑(2 + 1)) |
| 27 | | expp1 14109 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 2 ∈
ℕ0) → (𝐴↑(2 + 1)) = ((𝐴↑2) · 𝐴)) |
| 28 | 10, 4, 27 | sylancl 586 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑(2 + 1)) = ((𝐴↑2) · 𝐴)) |
| 29 | 26, 28 | eqtrid 2789 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑3) = ((𝐴↑2) · 𝐴)) |
| 30 | | sqval 14155 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ → (𝐴↑2) = (𝐴 · 𝐴)) |
| 31 | 10, 30 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑2) = (𝐴 · 𝐴)) |
| 32 | 31 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) · 𝐵) = ((𝐴 · 𝐴) · 𝐵)) |
| 33 | 10, 10, 11 | mul32d 11471 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐴) · 𝐵) = ((𝐴 · 𝐵) · 𝐴)) |
| 34 | 32, 33 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) · 𝐵) = ((𝐴 · 𝐵) · 𝐴)) |
| 35 | 34 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2
· ((𝐴↑2)
· 𝐵)) = (2 ·
((𝐴 · 𝐵) · 𝐴))) |
| 36 | | 2cnd 12344 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 2 ∈
ℂ) |
| 37 | 36, 18, 10 | mulassd 11284 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((2
· (𝐴 · 𝐵)) · 𝐴) = (2 · ((𝐴 · 𝐵) · 𝐴))) |
| 38 | 35, 37 | eqtr4d 2780 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2
· ((𝐴↑2)
· 𝐵)) = ((2 ·
(𝐴 · 𝐵)) · 𝐴)) |
| 39 | 29, 38 | oveq12d 7449 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))) = (((𝐴↑2) · 𝐴) + ((2 · (𝐴 · 𝐵)) · 𝐴))) |
| 40 | 25, 39 | eqtr4d 2780 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑2) + (2 · (𝐴 · 𝐵))) · 𝐴) = ((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵)))) |
| 41 | 23, 10 | mulcomd 11282 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐵↑2) · 𝐴) = (𝐴 · (𝐵↑2))) |
| 42 | 40, 41 | oveq12d 7449 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((((𝐴↑2) + (2 ·
(𝐴 · 𝐵))) · 𝐴) + ((𝐵↑2) · 𝐴)) = (((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))) + (𝐴 · (𝐵↑2)))) |
| 43 | 14, 24, 42 | 3eqtrd 2781 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵)↑2) · 𝐴) = (((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))) + (𝐴 · (𝐵↑2)))) |
| 44 | 13 | oveq1d 7446 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵)↑2) · 𝐵) = ((((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)) · 𝐵)) |
| 45 | 21, 23, 11 | adddird 11286 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((((𝐴↑2) + (2 ·
(𝐴 · 𝐵))) + (𝐵↑2)) · 𝐵) = ((((𝐴↑2) + (2 · (𝐴 · 𝐵))) · 𝐵) + ((𝐵↑2) · 𝐵))) |
| 46 | | sqval 14155 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ ℂ → (𝐵↑2) = (𝐵 · 𝐵)) |
| 47 | 11, 46 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑2) = (𝐵 · 𝐵)) |
| 48 | 47 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · (𝐵↑2)) = (𝐴 · (𝐵 · 𝐵))) |
| 49 | 10, 11, 11 | mulassd 11284 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐵) = (𝐴 · (𝐵 · 𝐵))) |
| 50 | 48, 49 | eqtr4d 2780 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · (𝐵↑2)) = ((𝐴 · 𝐵) · 𝐵)) |
| 51 | 50 | oveq2d 7447 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2
· (𝐴 · (𝐵↑2))) = (2 · ((𝐴 · 𝐵) · 𝐵))) |
| 52 | 36, 18, 11 | mulassd 11284 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((2
· (𝐴 · 𝐵)) · 𝐵) = (2 · ((𝐴 · 𝐵) · 𝐵))) |
| 53 | 51, 52 | eqtr4d 2780 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2
· (𝐴 · (𝐵↑2))) = ((2 · (𝐴 · 𝐵)) · 𝐵)) |
| 54 | 53 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑2) · 𝐵) + (2 · (𝐴 · (𝐵↑2)))) = (((𝐴↑2) · 𝐵) + ((2 · (𝐴 · 𝐵)) · 𝐵))) |
| 55 | 16, 20, 11 | adddird 11286 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑2) + (2 · (𝐴 · 𝐵))) · 𝐵) = (((𝐴↑2) · 𝐵) + ((2 · (𝐴 · 𝐵)) · 𝐵))) |
| 56 | 54, 55 | eqtr4d 2780 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑2) · 𝐵) + (2 · (𝐴 · (𝐵↑2)))) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) · 𝐵)) |
| 57 | 1 | oveq2i 7442 |
. . . . . . . 8
⊢ (𝐵↑3) = (𝐵↑(2 + 1)) |
| 58 | | expp1 14109 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℂ ∧ 2 ∈
ℕ0) → (𝐵↑(2 + 1)) = ((𝐵↑2) · 𝐵)) |
| 59 | 11, 4, 58 | sylancl 586 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑(2 + 1)) = ((𝐵↑2) · 𝐵)) |
| 60 | 57, 59 | eqtrid 2789 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑3) = ((𝐵↑2) · 𝐵)) |
| 61 | 56, 60 | oveq12d 7449 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((((𝐴↑2) ·
𝐵) + (2 · (𝐴 · (𝐵↑2)))) + (𝐵↑3)) = ((((𝐴↑2) + (2 · (𝐴 · 𝐵))) · 𝐵) + ((𝐵↑2) · 𝐵))) |
| 62 | 16, 11 | mulcld 11281 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) · 𝐵) ∈
ℂ) |
| 63 | 10, 23 | mulcld 11281 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · (𝐵↑2)) ∈ ℂ) |
| 64 | | mulcl 11239 |
. . . . . . . 8
⊢ ((2
∈ ℂ ∧ (𝐴
· (𝐵↑2)) ∈
ℂ) → (2 · (𝐴 · (𝐵↑2))) ∈ ℂ) |
| 65 | 17, 63, 64 | sylancr 587 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2
· (𝐴 · (𝐵↑2))) ∈
ℂ) |
| 66 | | 3nn0 12544 |
. . . . . . . 8
⊢ 3 ∈
ℕ0 |
| 67 | | expcl 14120 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℂ ∧ 3 ∈
ℕ0) → (𝐵↑3) ∈ ℂ) |
| 68 | 11, 66, 67 | sylancl 586 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑3) ∈
ℂ) |
| 69 | 62, 65, 68 | addassd 11283 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((((𝐴↑2) ·
𝐵) + (2 · (𝐴 · (𝐵↑2)))) + (𝐵↑3)) = (((𝐴↑2) · 𝐵) + ((2 · (𝐴 · (𝐵↑2))) + (𝐵↑3)))) |
| 70 | 61, 69 | eqtr3d 2779 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((((𝐴↑2) + (2 ·
(𝐴 · 𝐵))) · 𝐵) + ((𝐵↑2) · 𝐵)) = (((𝐴↑2) · 𝐵) + ((2 · (𝐴 · (𝐵↑2))) + (𝐵↑3)))) |
| 71 | 44, 45, 70 | 3eqtrd 2781 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵)↑2) · 𝐵) = (((𝐴↑2) · 𝐵) + ((2 · (𝐴 · (𝐵↑2))) + (𝐵↑3)))) |
| 72 | 43, 71 | oveq12d 7449 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((((𝐴 + 𝐵)↑2) · 𝐴) + (((𝐴 + 𝐵)↑2) · 𝐵)) = ((((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))) + (𝐴 · (𝐵↑2))) + (((𝐴↑2) · 𝐵) + ((2 · (𝐴 · (𝐵↑2))) + (𝐵↑3))))) |
| 73 | | expcl 14120 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 3 ∈
ℕ0) → (𝐴↑3) ∈ ℂ) |
| 74 | 10, 66, 73 | sylancl 586 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑3) ∈
ℂ) |
| 75 | | mulcl 11239 |
. . . . . 6
⊢ ((2
∈ ℂ ∧ ((𝐴↑2) · 𝐵) ∈ ℂ) → (2 · ((𝐴↑2) · 𝐵)) ∈
ℂ) |
| 76 | 17, 62, 75 | sylancr 587 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2
· ((𝐴↑2)
· 𝐵)) ∈
ℂ) |
| 77 | 74, 76 | addcld 11280 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))) ∈
ℂ) |
| 78 | 65, 68 | addcld 11280 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((2
· (𝐴 · (𝐵↑2))) + (𝐵↑3)) ∈ ℂ) |
| 79 | 77, 63, 62, 78 | add4d 11490 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((((𝐴↑3) + (2 ·
((𝐴↑2) · 𝐵))) + (𝐴 · (𝐵↑2))) + (((𝐴↑2) · 𝐵) + ((2 · (𝐴 · (𝐵↑2))) + (𝐵↑3)))) = ((((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))) + ((𝐴↑2) · 𝐵)) + ((𝐴 · (𝐵↑2)) + ((2 · (𝐴 · (𝐵↑2))) + (𝐵↑3))))) |
| 80 | 12, 72, 79 | 3eqtrd 2781 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵)↑2) · (𝐴 + 𝐵)) = ((((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))) + ((𝐴↑2) · 𝐵)) + ((𝐴 · (𝐵↑2)) + ((2 · (𝐴 · (𝐵↑2))) + (𝐵↑3))))) |
| 81 | 74, 76, 62 | addassd 11283 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))) + ((𝐴↑2) · 𝐵)) = ((𝐴↑3) + ((2 · ((𝐴↑2) · 𝐵)) + ((𝐴↑2) · 𝐵)))) |
| 82 | 1 | oveq1i 7441 |
. . . . . . 7
⊢ (3
· ((𝐴↑2)
· 𝐵)) = ((2 + 1)
· ((𝐴↑2)
· 𝐵)) |
| 83 | | 1cnd 11256 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 1 ∈
ℂ) |
| 84 | 36, 83, 62 | adddird 11286 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((2 + 1)
· ((𝐴↑2)
· 𝐵)) = ((2 ·
((𝐴↑2) · 𝐵)) + (1 · ((𝐴↑2) · 𝐵)))) |
| 85 | 82, 84 | eqtrid 2789 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (3
· ((𝐴↑2)
· 𝐵)) = ((2 ·
((𝐴↑2) · 𝐵)) + (1 · ((𝐴↑2) · 𝐵)))) |
| 86 | 62 | mullidd 11279 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1
· ((𝐴↑2)
· 𝐵)) = ((𝐴↑2) · 𝐵)) |
| 87 | 86 | oveq2d 7447 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((2
· ((𝐴↑2)
· 𝐵)) + (1 ·
((𝐴↑2) · 𝐵))) = ((2 · ((𝐴↑2) · 𝐵)) + ((𝐴↑2) · 𝐵))) |
| 88 | 85, 87 | eqtrd 2777 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (3
· ((𝐴↑2)
· 𝐵)) = ((2 ·
((𝐴↑2) · 𝐵)) + ((𝐴↑2) · 𝐵))) |
| 89 | 88 | oveq2d 7447 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) = ((𝐴↑3) + ((2 · ((𝐴↑2) · 𝐵)) + ((𝐴↑2) · 𝐵)))) |
| 90 | 81, 89 | eqtr4d 2780 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑3) + (2 · ((𝐴↑2) · 𝐵))) + ((𝐴↑2) · 𝐵)) = ((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵)))) |
| 91 | | 1p2e3 12409 |
. . . . . . . 8
⊢ (1 + 2) =
3 |
| 92 | 91 | oveq1i 7441 |
. . . . . . 7
⊢ ((1 + 2)
· (𝐴 · (𝐵↑2))) = (3 · (𝐴 · (𝐵↑2))) |
| 93 | 83, 36, 63 | adddird 11286 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((1 + 2)
· (𝐴 · (𝐵↑2))) = ((1 · (𝐴 · (𝐵↑2))) + (2 · (𝐴 · (𝐵↑2))))) |
| 94 | 92, 93 | eqtr3id 2791 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (3
· (𝐴 · (𝐵↑2))) = ((1 · (𝐴 · (𝐵↑2))) + (2 · (𝐴 · (𝐵↑2))))) |
| 95 | 63 | mullidd 11279 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1
· (𝐴 · (𝐵↑2))) = (𝐴 · (𝐵↑2))) |
| 96 | 95 | oveq1d 7446 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((1
· (𝐴 · (𝐵↑2))) + (2 · (𝐴 · (𝐵↑2)))) = ((𝐴 · (𝐵↑2)) + (2 · (𝐴 · (𝐵↑2))))) |
| 97 | 94, 96 | eqtrd 2777 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (3
· (𝐴 · (𝐵↑2))) = ((𝐴 · (𝐵↑2)) + (2 · (𝐴 · (𝐵↑2))))) |
| 98 | 97 | oveq1d 7446 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((3
· (𝐴 · (𝐵↑2))) + (𝐵↑3)) = (((𝐴 · (𝐵↑2)) + (2 · (𝐴 · (𝐵↑2)))) + (𝐵↑3))) |
| 99 | 63, 65, 68 | addassd 11283 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 · (𝐵↑2)) + (2 · (𝐴 · (𝐵↑2)))) + (𝐵↑3)) = ((𝐴 · (𝐵↑2)) + ((2 · (𝐴 · (𝐵↑2))) + (𝐵↑3)))) |
| 100 | 98, 99 | eqtr2d 2778 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · (𝐵↑2)) + ((2 · (𝐴 · (𝐵↑2))) + (𝐵↑3))) = ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3))) |
| 101 | 90, 100 | oveq12d 7449 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((((𝐴↑3) + (2 ·
((𝐴↑2) · 𝐵))) + ((𝐴↑2) · 𝐵)) + ((𝐴 · (𝐵↑2)) + ((2 · (𝐴 · (𝐵↑2))) + (𝐵↑3)))) = (((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3)))) |
| 102 | 7, 80, 101 | 3eqtrd 2781 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑3) = (((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3)))) |