# Metamath Proof Explorer

## Theorem binom2

Description: The square of a binomial. (Contributed by FL, 10-Dec-2006)

Ref Expression
Assertion binom2 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {\left({A}+{B}\right)}^{2}={{A}}^{2}+2{A}{B}+{{B}}^{2}$

### Proof

Step Hyp Ref Expression
1 oveq1 ${⊢}{A}=if\left({A}\in ℂ,{A},0\right)\to {A}+{B}=if\left({A}\in ℂ,{A},0\right)+{B}$
2 1 oveq1d ${⊢}{A}=if\left({A}\in ℂ,{A},0\right)\to {\left({A}+{B}\right)}^{2}={\left(if\left({A}\in ℂ,{A},0\right)+{B}\right)}^{2}$
3 oveq1 ${⊢}{A}=if\left({A}\in ℂ,{A},0\right)\to {{A}}^{2}={if\left({A}\in ℂ,{A},0\right)}^{2}$
4 oveq1 ${⊢}{A}=if\left({A}\in ℂ,{A},0\right)\to {A}{B}=if\left({A}\in ℂ,{A},0\right){B}$
5 4 oveq2d ${⊢}{A}=if\left({A}\in ℂ,{A},0\right)\to 2{A}{B}=2if\left({A}\in ℂ,{A},0\right){B}$
6 3 5 oveq12d ${⊢}{A}=if\left({A}\in ℂ,{A},0\right)\to {{A}}^{2}+2{A}{B}={if\left({A}\in ℂ,{A},0\right)}^{2}+2if\left({A}\in ℂ,{A},0\right){B}$
7 6 oveq1d ${⊢}{A}=if\left({A}\in ℂ,{A},0\right)\to {{A}}^{2}+2{A}{B}+{{B}}^{2}={if\left({A}\in ℂ,{A},0\right)}^{2}+2if\left({A}\in ℂ,{A},0\right){B}+{{B}}^{2}$
8 2 7 eqeq12d ${⊢}{A}=if\left({A}\in ℂ,{A},0\right)\to \left({\left({A}+{B}\right)}^{2}={{A}}^{2}+2{A}{B}+{{B}}^{2}↔{\left(if\left({A}\in ℂ,{A},0\right)+{B}\right)}^{2}={if\left({A}\in ℂ,{A},0\right)}^{2}+2if\left({A}\in ℂ,{A},0\right){B}+{{B}}^{2}\right)$
9 oveq2 ${⊢}{B}=if\left({B}\in ℂ,{B},0\right)\to if\left({A}\in ℂ,{A},0\right)+{B}=if\left({A}\in ℂ,{A},0\right)+if\left({B}\in ℂ,{B},0\right)$
10 9 oveq1d ${⊢}{B}=if\left({B}\in ℂ,{B},0\right)\to {\left(if\left({A}\in ℂ,{A},0\right)+{B}\right)}^{2}={\left(if\left({A}\in ℂ,{A},0\right)+if\left({B}\in ℂ,{B},0\right)\right)}^{2}$
11 oveq2 ${⊢}{B}=if\left({B}\in ℂ,{B},0\right)\to if\left({A}\in ℂ,{A},0\right){B}=if\left({A}\in ℂ,{A},0\right)if\left({B}\in ℂ,{B},0\right)$
12 11 oveq2d ${⊢}{B}=if\left({B}\in ℂ,{B},0\right)\to 2if\left({A}\in ℂ,{A},0\right){B}=2if\left({A}\in ℂ,{A},0\right)if\left({B}\in ℂ,{B},0\right)$
13 12 oveq2d ${⊢}{B}=if\left({B}\in ℂ,{B},0\right)\to {if\left({A}\in ℂ,{A},0\right)}^{2}+2if\left({A}\in ℂ,{A},0\right){B}={if\left({A}\in ℂ,{A},0\right)}^{2}+2if\left({A}\in ℂ,{A},0\right)if\left({B}\in ℂ,{B},0\right)$
14 oveq1 ${⊢}{B}=if\left({B}\in ℂ,{B},0\right)\to {{B}}^{2}={if\left({B}\in ℂ,{B},0\right)}^{2}$
15 13 14 oveq12d ${⊢}{B}=if\left({B}\in ℂ,{B},0\right)\to {if\left({A}\in ℂ,{A},0\right)}^{2}+2if\left({A}\in ℂ,{A},0\right){B}+{{B}}^{2}={if\left({A}\in ℂ,{A},0\right)}^{2}+2if\left({A}\in ℂ,{A},0\right)if\left({B}\in ℂ,{B},0\right)+{if\left({B}\in ℂ,{B},0\right)}^{2}$
16 10 15 eqeq12d ${⊢}{B}=if\left({B}\in ℂ,{B},0\right)\to \left({\left(if\left({A}\in ℂ,{A},0\right)+{B}\right)}^{2}={if\left({A}\in ℂ,{A},0\right)}^{2}+2if\left({A}\in ℂ,{A},0\right){B}+{{B}}^{2}↔{\left(if\left({A}\in ℂ,{A},0\right)+if\left({B}\in ℂ,{B},0\right)\right)}^{2}={if\left({A}\in ℂ,{A},0\right)}^{2}+2if\left({A}\in ℂ,{A},0\right)if\left({B}\in ℂ,{B},0\right)+{if\left({B}\in ℂ,{B},0\right)}^{2}\right)$
17 0cn ${⊢}0\in ℂ$
18 17 elimel ${⊢}if\left({A}\in ℂ,{A},0\right)\in ℂ$
19 17 elimel ${⊢}if\left({B}\in ℂ,{B},0\right)\in ℂ$
20 18 19 binom2i ${⊢}{\left(if\left({A}\in ℂ,{A},0\right)+if\left({B}\in ℂ,{B},0\right)\right)}^{2}={if\left({A}\in ℂ,{A},0\right)}^{2}+2if\left({A}\in ℂ,{A},0\right)if\left({B}\in ℂ,{B},0\right)+{if\left({B}\in ℂ,{B},0\right)}^{2}$
21 8 16 20 dedth2h ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {\left({A}+{B}\right)}^{2}={{A}}^{2}+2{A}{B}+{{B}}^{2}$