Metamath Proof Explorer


Theorem binom2i

Description: The square of a binomial. (Contributed by NM, 11-Aug-1999)

Ref Expression
Hypotheses binom2.1 𝐴 ∈ ℂ
binom2.2 𝐵 ∈ ℂ
Assertion binom2i ( ( 𝐴 + 𝐵 ) ↑ 2 ) = ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) )

Proof

Step Hyp Ref Expression
1 binom2.1 𝐴 ∈ ℂ
2 binom2.2 𝐵 ∈ ℂ
3 1 2 addcli ( 𝐴 + 𝐵 ) ∈ ℂ
4 3 1 2 adddii ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) = ( ( ( 𝐴 + 𝐵 ) · 𝐴 ) + ( ( 𝐴 + 𝐵 ) · 𝐵 ) )
5 1 2 1 adddiri ( ( 𝐴 + 𝐵 ) · 𝐴 ) = ( ( 𝐴 · 𝐴 ) + ( 𝐵 · 𝐴 ) )
6 2 1 mulcomi ( 𝐵 · 𝐴 ) = ( 𝐴 · 𝐵 )
7 6 oveq2i ( ( 𝐴 · 𝐴 ) + ( 𝐵 · 𝐴 ) ) = ( ( 𝐴 · 𝐴 ) + ( 𝐴 · 𝐵 ) )
8 5 7 eqtri ( ( 𝐴 + 𝐵 ) · 𝐴 ) = ( ( 𝐴 · 𝐴 ) + ( 𝐴 · 𝐵 ) )
9 1 2 2 adddiri ( ( 𝐴 + 𝐵 ) · 𝐵 ) = ( ( 𝐴 · 𝐵 ) + ( 𝐵 · 𝐵 ) )
10 8 9 oveq12i ( ( ( 𝐴 + 𝐵 ) · 𝐴 ) + ( ( 𝐴 + 𝐵 ) · 𝐵 ) ) = ( ( ( 𝐴 · 𝐴 ) + ( 𝐴 · 𝐵 ) ) + ( ( 𝐴 · 𝐵 ) + ( 𝐵 · 𝐵 ) ) )
11 1 1 mulcli ( 𝐴 · 𝐴 ) ∈ ℂ
12 1 2 mulcli ( 𝐴 · 𝐵 ) ∈ ℂ
13 11 12 addcli ( ( 𝐴 · 𝐴 ) + ( 𝐴 · 𝐵 ) ) ∈ ℂ
14 2 2 mulcli ( 𝐵 · 𝐵 ) ∈ ℂ
15 13 12 14 addassi ( ( ( ( 𝐴 · 𝐴 ) + ( 𝐴 · 𝐵 ) ) + ( 𝐴 · 𝐵 ) ) + ( 𝐵 · 𝐵 ) ) = ( ( ( 𝐴 · 𝐴 ) + ( 𝐴 · 𝐵 ) ) + ( ( 𝐴 · 𝐵 ) + ( 𝐵 · 𝐵 ) ) )
16 11 12 12 addassi ( ( ( 𝐴 · 𝐴 ) + ( 𝐴 · 𝐵 ) ) + ( 𝐴 · 𝐵 ) ) = ( ( 𝐴 · 𝐴 ) + ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐵 ) ) )
17 16 oveq1i ( ( ( ( 𝐴 · 𝐴 ) + ( 𝐴 · 𝐵 ) ) + ( 𝐴 · 𝐵 ) ) + ( 𝐵 · 𝐵 ) ) = ( ( ( 𝐴 · 𝐴 ) + ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 · 𝐵 ) )
18 10 15 17 3eqtr2i ( ( ( 𝐴 + 𝐵 ) · 𝐴 ) + ( ( 𝐴 + 𝐵 ) · 𝐵 ) ) = ( ( ( 𝐴 · 𝐴 ) + ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 · 𝐵 ) )
19 4 18 eqtri ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) = ( ( ( 𝐴 · 𝐴 ) + ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 · 𝐵 ) )
20 3 sqvali ( ( 𝐴 + 𝐵 ) ↑ 2 ) = ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) )
21 1 sqvali ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 )
22 12 2timesi ( 2 · ( 𝐴 · 𝐵 ) ) = ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐵 ) )
23 21 22 oveq12i ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) = ( ( 𝐴 · 𝐴 ) + ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐵 ) ) )
24 2 sqvali ( 𝐵 ↑ 2 ) = ( 𝐵 · 𝐵 )
25 23 24 oveq12i ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) = ( ( ( 𝐴 · 𝐴 ) + ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 · 𝐵 ) )
26 19 20 25 3eqtr4i ( ( 𝐴 + 𝐵 ) ↑ 2 ) = ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) )