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