Proof of Theorem sqabssub
Step | Hyp | Ref
| Expression |
1 | | cjsub 13737 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(∗‘(𝐴 −
𝐵)) =
((∗‘𝐴) −
(∗‘𝐵))) |
2 | 1 | oveq2d 6565 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) · (∗‘(𝐴 − 𝐵))) = ((𝐴 − 𝐵) · ((∗‘𝐴) − (∗‘𝐵)))) |
3 | | cjcl 13693 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
(∗‘𝐴) ∈
ℂ) |
4 | | cjcl 13693 |
. . . . 5
⊢ (𝐵 ∈ ℂ →
(∗‘𝐵) ∈
ℂ) |
5 | 3, 4 | anim12i 588 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((∗‘𝐴) ∈
ℂ ∧ (∗‘𝐵) ∈ ℂ)) |
6 | | mulsub 10352 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧
((∗‘𝐴) ∈
ℂ ∧ (∗‘𝐵) ∈ ℂ)) → ((𝐴 − 𝐵) · ((∗‘𝐴) − (∗‘𝐵))) = (((𝐴 · (∗‘𝐴)) + ((∗‘𝐵) · 𝐵)) − ((𝐴 · (∗‘𝐵)) + ((∗‘𝐴) · 𝐵)))) |
7 | 5, 6 | mpdan 699 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) · ((∗‘𝐴) − (∗‘𝐵))) = (((𝐴 · (∗‘𝐴)) + ((∗‘𝐵) · 𝐵)) − ((𝐴 · (∗‘𝐵)) + ((∗‘𝐴) · 𝐵)))) |
8 | 2, 7 | eqtrd 2644 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) · (∗‘(𝐴 − 𝐵))) = (((𝐴 · (∗‘𝐴)) + ((∗‘𝐵) · 𝐵)) − ((𝐴 · (∗‘𝐵)) + ((∗‘𝐴) · 𝐵)))) |
9 | | subcl 10159 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ) |
10 | | absvalsq 13868 |
. . 3
⊢ ((𝐴 − 𝐵) ∈ ℂ → ((abs‘(𝐴 − 𝐵))↑2) = ((𝐴 − 𝐵) · (∗‘(𝐴 − 𝐵)))) |
11 | 9, 10 | syl 17 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((abs‘(𝐴 −
𝐵))↑2) = ((𝐴 − 𝐵) · (∗‘(𝐴 − 𝐵)))) |
12 | | absvalsq 13868 |
. . . 4
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴)↑2) =
(𝐴 ·
(∗‘𝐴))) |
13 | | absvalsq 13868 |
. . . . 5
⊢ (𝐵 ∈ ℂ →
((abs‘𝐵)↑2) =
(𝐵 ·
(∗‘𝐵))) |
14 | | mulcom 9901 |
. . . . . 6
⊢ ((𝐵 ∈ ℂ ∧
(∗‘𝐵) ∈
ℂ) → (𝐵 ·
(∗‘𝐵)) =
((∗‘𝐵)
· 𝐵)) |
15 | 4, 14 | mpdan 699 |
. . . . 5
⊢ (𝐵 ∈ ℂ → (𝐵 · (∗‘𝐵)) = ((∗‘𝐵) · 𝐵)) |
16 | 13, 15 | eqtrd 2644 |
. . . 4
⊢ (𝐵 ∈ ℂ →
((abs‘𝐵)↑2) =
((∗‘𝐵)
· 𝐵)) |
17 | 12, 16 | oveqan12d 6568 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((abs‘𝐴)↑2) +
((abs‘𝐵)↑2)) =
((𝐴 ·
(∗‘𝐴)) +
((∗‘𝐵)
· 𝐵))) |
18 | | mulcl 9899 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(∗‘𝐵) ∈
ℂ) → (𝐴 ·
(∗‘𝐵)) ∈
ℂ) |
19 | 4, 18 | sylan2 490 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · (∗‘𝐵)) ∈
ℂ) |
20 | 19 | addcjd 13800 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · (∗‘𝐵)) + (∗‘(𝐴 · (∗‘𝐵)))) = (2 ·
(ℜ‘(𝐴 ·
(∗‘𝐵))))) |
21 | | cjmul 13730 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(∗‘𝐵) ∈
ℂ) → (∗‘(𝐴 · (∗‘𝐵))) = ((∗‘𝐴) ·
(∗‘(∗‘𝐵)))) |
22 | 4, 21 | sylan2 490 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(∗‘(𝐴 ·
(∗‘𝐵))) =
((∗‘𝐴)
· (∗‘(∗‘𝐵)))) |
23 | | cjcj 13728 |
. . . . . . . 8
⊢ (𝐵 ∈ ℂ →
(∗‘(∗‘𝐵)) = 𝐵) |
24 | 23 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(∗‘(∗‘𝐵)) = 𝐵) |
25 | 24 | oveq2d 6565 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((∗‘𝐴)
· (∗‘(∗‘𝐵))) = ((∗‘𝐴) · 𝐵)) |
26 | 22, 25 | eqtrd 2644 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(∗‘(𝐴 ·
(∗‘𝐵))) =
((∗‘𝐴)
· 𝐵)) |
27 | 26 | oveq2d 6565 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · (∗‘𝐵)) + (∗‘(𝐴 · (∗‘𝐵)))) = ((𝐴 · (∗‘𝐵)) + ((∗‘𝐴) · 𝐵))) |
28 | 20, 27 | eqtr3d 2646 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2
· (ℜ‘(𝐴
· (∗‘𝐵)))) = ((𝐴 · (∗‘𝐵)) + ((∗‘𝐴) · 𝐵))) |
29 | 17, 28 | oveq12d 6567 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((((abs‘𝐴)↑2) +
((abs‘𝐵)↑2))
− (2 · (ℜ‘(𝐴 · (∗‘𝐵))))) = (((𝐴 · (∗‘𝐴)) + ((∗‘𝐵) · 𝐵)) − ((𝐴 · (∗‘𝐵)) + ((∗‘𝐴) · 𝐵)))) |
30 | 8, 11, 29 | 3eqtr4d 2654 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((abs‘(𝐴 −
𝐵))↑2) =
((((abs‘𝐴)↑2) +
((abs‘𝐵)↑2))
− (2 · (ℜ‘(𝐴 · (∗‘𝐵)))))) |