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