Theorem binom2

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

	Ref	Expression
Assertion	binom2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) ↑ 2 ) = ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( 𝐴 = if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) → ( 𝐴 + 𝐵 ) = ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) + 𝐵 ) )
2	1	oveq1d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) → ( ( 𝐴 + 𝐵 ) ↑ 2 ) = ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) + 𝐵 ) ↑ 2 ) )
3		oveq1	⊢ ( 𝐴 = if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) → ( 𝐴 ↑ 2 ) = ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ↑ 2 ) )
4		oveq1	⊢ ( 𝐴 = if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) → ( 𝐴 · 𝐵 ) = ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) · 𝐵 ) )
5	4	oveq2d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) → ( 2 · ( 𝐴 · 𝐵 ) ) = ( 2 · ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) · 𝐵 ) ) )
6	3 5	oveq12d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) → ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) = ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ↑ 2 ) + ( 2 · ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) · 𝐵 ) ) ) )
7	6	oveq1d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) → ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) = ( ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ↑ 2 ) + ( 2 · ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) )
8	2 7	eqeq12d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) → ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) = ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) ↔ ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) + 𝐵 ) ↑ 2 ) = ( ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ↑ 2 ) + ( 2 · ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) ) )
9		oveq2	⊢ ( 𝐵 = if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) → ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) + 𝐵 ) = ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) + if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) ) )
10	9	oveq1d	⊢ ( 𝐵 = if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) → ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) + 𝐵 ) ↑ 2 ) = ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) + if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) ) ↑ 2 ) )
11		oveq2	⊢ ( 𝐵 = if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) → ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) · 𝐵 ) = ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) · if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) ) )
12	11	oveq2d	⊢ ( 𝐵 = if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) → ( 2 · ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) · 𝐵 ) ) = ( 2 · ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) · if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) ) ) )
13	12	oveq2d	⊢ ( 𝐵 = if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) → ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ↑ 2 ) + ( 2 · ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) · 𝐵 ) ) ) = ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ↑ 2 ) + ( 2 · ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) · if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) ) ) ) )
14		oveq1	⊢ ( 𝐵 = if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) → ( 𝐵 ↑ 2 ) = ( if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) ↑ 2 ) )
15	13 14	oveq12d	⊢ ( 𝐵 = if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) → ( ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ↑ 2 ) + ( 2 · ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) = ( ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ↑ 2 ) + ( 2 · ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) · if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) ) ) ) + ( if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) ↑ 2 ) ) )
16	10 15	eqeq12d	⊢ ( 𝐵 = if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) → ( ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) + 𝐵 ) ↑ 2 ) = ( ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ↑ 2 ) + ( 2 · ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) ↔ ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) + if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) ) ↑ 2 ) = ( ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ↑ 2 ) + ( 2 · ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) · if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) ) ) ) + ( if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) ↑ 2 ) ) ) )
17		0cn	⊢ 0 ∈ ℂ
18	17	elimel	⊢ if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ∈ ℂ
19	17	elimel	⊢ if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) ∈ ℂ
20	18 19	binom2i	⊢ ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) + if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) ) ↑ 2 ) = ( ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ↑ 2 ) + ( 2 · ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) · if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) ) ) ) + ( if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) ↑ 2 ) )
21	8 16 20	dedth2h	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) ↑ 2 ) = ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) )