Metamath Proof Explorer

Theorem binom2

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

Ref Expression
Assertion binom2 ⊢A∈ℂ∧B∈ℂ→A+B2=A2+2⁢A⁢B+B2

Proof

Step Hyp Ref Expression
1 oveq1 ⊢A=ifA∈ℂA0→A+B=ifA∈ℂA0+B
2 1 oveq1d ⊢A=ifA∈ℂA0→A+B2=ifA∈ℂA0+B2
3 oveq1 ⊢A=ifA∈ℂA0→A2=ifA∈ℂA02
4 oveq1 ⊢A=ifA∈ℂA0→A⁢B=ifA∈ℂA0⁢B
5 4 oveq2d ⊢A=ifA∈ℂA0→2⁢A⁢B=2⁢ifA∈ℂA0⁢B
6 3 5 oveq12d ⊢A=ifA∈ℂA0→A2+2⁢A⁢B=ifA∈ℂA02+2⁢ifA∈ℂA0⁢B
7 6 oveq1d ⊢A=ifA∈ℂA0→A2+2⁢A⁢B+B2=ifA∈ℂA02+2⁢ifA∈ℂA0⁢B+B2
8 2 7 eqeq12d ⊢A=ifA∈ℂA0→A+B2=A2+2⁢A⁢B+B2↔ifA∈ℂA0+B2=ifA∈ℂA02+2⁢ifA∈ℂA0⁢B+B2
9 oveq2 ⊢B=ifB∈ℂB0→ifA∈ℂA0+B=ifA∈ℂA0+ifB∈ℂB0
10 9 oveq1d ⊢B=ifB∈ℂB0→ifA∈ℂA0+B2=ifA∈ℂA0+ifB∈ℂB02
11 oveq2 ⊢B=ifB∈ℂB0→ifA∈ℂA0⁢B=ifA∈ℂA0⁢ifB∈ℂB0
12 11 oveq2d ⊢B=ifB∈ℂB0→2⁢ifA∈ℂA0⁢B=2⁢ifA∈ℂA0⁢ifB∈ℂB0
13 12 oveq2d ⊢B=ifB∈ℂB0→ifA∈ℂA02+2⁢ifA∈ℂA0⁢B=ifA∈ℂA02+2⁢ifA∈ℂA0⁢ifB∈ℂB0
14 oveq1 ⊢B=ifB∈ℂB0→B2=ifB∈ℂB02
15 13 14 oveq12d ⊢B=ifB∈ℂB0→ifA∈ℂA02+2⁢ifA∈ℂA0⁢B+B2=ifA∈ℂA02+2⁢ifA∈ℂA0⁢ifB∈ℂB0+ifB∈ℂB02
16 10 15 eqeq12d ⊢B=ifB∈ℂB0→ifA∈ℂA0+B2=ifA∈ℂA02+2⁢ifA∈ℂA0⁢B+B2↔ifA∈ℂA0+ifB∈ℂB02=ifA∈ℂA02+2⁢ifA∈ℂA0⁢ifB∈ℂB0+ifB∈ℂB02
17 0cn ⊢0∈ℂ
18 17 elimel ⊢ifA∈ℂA0∈ℂ
19 17 elimel ⊢ifB∈ℂB0∈ℂ
20 18 19 binom2i ⊢ifA∈ℂA0+ifB∈ℂB02=ifA∈ℂA02+2⁢ifA∈ℂA0⁢ifB∈ℂB0+ifB∈ℂB02
21 8 16 20 dedth2h ⊢A∈ℂ∧B∈ℂ→A+B2=A2+2⁢A⁢B+B2