Step |
Hyp |
Ref |
Expression |
1 |
|
recn |
⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ ) |
2 |
|
ax-icn |
⊢ i ∈ ℂ |
3 |
|
recn |
⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ ) |
4 |
|
mulcl |
⊢ ( ( i ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · 𝐵 ) ∈ ℂ ) |
5 |
2 3 4
|
sylancr |
⊢ ( 𝐵 ∈ ℝ → ( i · 𝐵 ) ∈ ℂ ) |
6 |
|
addcl |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( i · 𝐵 ) ∈ ℂ ) → ( 𝐴 + ( i · 𝐵 ) ) ∈ ℂ ) |
7 |
1 5 6
|
syl2an |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + ( i · 𝐵 ) ) ∈ ℂ ) |
8 |
|
absvalsq2 |
⊢ ( ( 𝐴 + ( i · 𝐵 ) ) ∈ ℂ → ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) = ( ( ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) ) |
9 |
7 8
|
syl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) = ( ( ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) ) |
10 |
|
crre |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = 𝐴 ) |
11 |
10
|
oveq1d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) = ( 𝐴 ↑ 2 ) ) |
12 |
|
crim |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = 𝐵 ) |
13 |
12
|
oveq1d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) = ( 𝐵 ↑ 2 ) ) |
14 |
11 13
|
oveq12d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) |
15 |
9 14
|
eqtrd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) |