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 ) )