Proof of Theorem bhmafibid1
| Step | Hyp | Ref
| Expression |
| 1 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → 𝐴 ∈
ℝ) |
| 2 | 1 | recnd 11289 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → 𝐴 ∈
ℂ) |
| 3 | | ax-icn 11214 |
. . . . . . . . . 10
⊢ i ∈
ℂ |
| 4 | 3 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → i
∈ ℂ) |
| 5 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → 𝐵 ∈
ℝ) |
| 6 | 5 | recnd 11289 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → 𝐵 ∈
ℂ) |
| 7 | 4, 6 | mulcld 11281 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (i
· 𝐵) ∈
ℂ) |
| 8 | 2, 7 | addcld 11280 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (𝐴 + (i · 𝐵)) ∈ ℂ) |
| 9 | | simprl 771 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → 𝐶 ∈
ℝ) |
| 10 | 9 | recnd 11289 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → 𝐶 ∈
ℂ) |
| 11 | | simprr 773 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → 𝐷 ∈
ℝ) |
| 12 | 11 | recnd 11289 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → 𝐷 ∈
ℂ) |
| 13 | 4, 12 | mulcld 11281 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (i
· 𝐷) ∈
ℂ) |
| 14 | 10, 13 | addcld 11280 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (𝐶 + (i · 𝐷)) ∈ ℂ) |
| 15 | 8, 14 | mulcld 11281 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) ∈ ℂ) |
| 16 | 15 | replimd 15236 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) = ((ℜ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷)))) + (i · (ℑ‘((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))))))) |
| 17 | 8, 14 | remuld 15257 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) →
(ℜ‘((𝐴 + (i
· 𝐵)) ·
(𝐶 + (i · 𝐷)))) = (((ℜ‘(𝐴 + (i · 𝐵))) · (ℜ‘(𝐶 + (i · 𝐷)))) − ((ℑ‘(𝐴 + (i · 𝐵))) · (ℑ‘(𝐶 + (i · 𝐷)))))) |
| 18 | 1, 5 | crred 15270 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) →
(ℜ‘(𝐴 + (i
· 𝐵))) = 𝐴) |
| 19 | 9, 11 | crred 15270 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) →
(ℜ‘(𝐶 + (i
· 𝐷))) = 𝐶) |
| 20 | 18, 19 | oveq12d 7449 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) →
((ℜ‘(𝐴 + (i
· 𝐵))) ·
(ℜ‘(𝐶 + (i
· 𝐷)))) = (𝐴 · 𝐶)) |
| 21 | 1, 5 | crimd 15271 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) →
(ℑ‘(𝐴 + (i
· 𝐵))) = 𝐵) |
| 22 | 9, 11 | crimd 15271 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) →
(ℑ‘(𝐶 + (i
· 𝐷))) = 𝐷) |
| 23 | 21, 22 | oveq12d 7449 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) →
((ℑ‘(𝐴 + (i
· 𝐵))) ·
(ℑ‘(𝐶 + (i
· 𝐷)))) = (𝐵 · 𝐷)) |
| 24 | 20, 23 | oveq12d 7449 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) →
(((ℜ‘(𝐴 + (i
· 𝐵))) ·
(ℜ‘(𝐶 + (i
· 𝐷)))) −
((ℑ‘(𝐴 + (i
· 𝐵))) ·
(ℑ‘(𝐶 + (i
· 𝐷))))) = ((𝐴 · 𝐶) − (𝐵 · 𝐷))) |
| 25 | 17, 24 | eqtrd 2777 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) →
(ℜ‘((𝐴 + (i
· 𝐵)) ·
(𝐶 + (i · 𝐷)))) = ((𝐴 · 𝐶) − (𝐵 · 𝐷))) |
| 26 | 8, 14 | immuld 15258 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) →
(ℑ‘((𝐴 + (i
· 𝐵)) ·
(𝐶 + (i · 𝐷)))) = (((ℜ‘(𝐴 + (i · 𝐵))) · (ℑ‘(𝐶 + (i · 𝐷)))) + ((ℑ‘(𝐴 + (i · 𝐵))) · (ℜ‘(𝐶 + (i · 𝐷)))))) |
| 27 | 18, 22 | oveq12d 7449 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) →
((ℜ‘(𝐴 + (i
· 𝐵))) ·
(ℑ‘(𝐶 + (i
· 𝐷)))) = (𝐴 · 𝐷)) |
| 28 | 21, 19 | oveq12d 7449 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) →
((ℑ‘(𝐴 + (i
· 𝐵))) ·
(ℜ‘(𝐶 + (i
· 𝐷)))) = (𝐵 · 𝐶)) |
| 29 | 27, 28 | oveq12d 7449 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) →
(((ℜ‘(𝐴 + (i
· 𝐵))) ·
(ℑ‘(𝐶 + (i
· 𝐷)))) +
((ℑ‘(𝐴 + (i
· 𝐵))) ·
(ℜ‘(𝐶 + (i
· 𝐷))))) = ((𝐴 · 𝐷) + (𝐵 · 𝐶))) |
| 30 | 26, 29 | eqtrd 2777 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) →
(ℑ‘((𝐴 + (i
· 𝐵)) ·
(𝐶 + (i · 𝐷)))) = ((𝐴 · 𝐷) + (𝐵 · 𝐶))) |
| 31 | 30 | oveq2d 7447 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (i
· (ℑ‘((𝐴
+ (i · 𝐵)) ·
(𝐶 + (i · 𝐷))))) = (i · ((𝐴 · 𝐷) + (𝐵 · 𝐶)))) |
| 32 | 25, 31 | oveq12d 7449 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) →
((ℜ‘((𝐴 + (i
· 𝐵)) ·
(𝐶 + (i · 𝐷)))) + (i ·
(ℑ‘((𝐴 + (i
· 𝐵)) ·
(𝐶 + (i · 𝐷)))))) = (((𝐴 · 𝐶) − (𝐵 · 𝐷)) + (i · ((𝐴 · 𝐷) + (𝐵 · 𝐶))))) |
| 33 | 16, 32 | eqtrd 2777 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) = (((𝐴 · 𝐶) − (𝐵 · 𝐷)) + (i · ((𝐴 · 𝐷) + (𝐵 · 𝐶))))) |
| 34 | 33 | fveq2d 6910 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) →
(abs‘((𝐴 + (i
· 𝐵)) ·
(𝐶 + (i · 𝐷)))) = (abs‘(((𝐴 · 𝐶) − (𝐵 · 𝐷)) + (i · ((𝐴 · 𝐷) + (𝐵 · 𝐶)))))) |
| 35 | 34 | oveq1d 7446 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) →
((abs‘((𝐴 + (i
· 𝐵)) ·
(𝐶 + (i · 𝐷))))↑2) =
((abs‘(((𝐴 ·
𝐶) − (𝐵 · 𝐷)) + (i · ((𝐴 · 𝐷) + (𝐵 · 𝐶)))))↑2)) |
| 36 | 8, 14 | absmuld 15493 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) →
(abs‘((𝐴 + (i
· 𝐵)) ·
(𝐶 + (i · 𝐷)))) = ((abs‘(𝐴 + (i · 𝐵))) · (abs‘(𝐶 + (i · 𝐷))))) |
| 37 | 36 | oveq1d 7446 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) →
((abs‘((𝐴 + (i
· 𝐵)) ·
(𝐶 + (i · 𝐷))))↑2) =
(((abs‘(𝐴 + (i
· 𝐵))) ·
(abs‘(𝐶 + (i ·
𝐷))))↑2)) |
| 38 | 8 | abscld 15475 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) →
(abs‘(𝐴 + (i ·
𝐵))) ∈
ℝ) |
| 39 | 38 | recnd 11289 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) →
(abs‘(𝐴 + (i ·
𝐵))) ∈
ℂ) |
| 40 | 14 | abscld 15475 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) →
(abs‘(𝐶 + (i ·
𝐷))) ∈
ℝ) |
| 41 | 40 | recnd 11289 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) →
(abs‘(𝐶 + (i ·
𝐷))) ∈
ℂ) |
| 42 | 39, 41 | sqmuld 14198 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) →
(((abs‘(𝐴 + (i
· 𝐵))) ·
(abs‘(𝐶 + (i ·
𝐷))))↑2) =
(((abs‘(𝐴 + (i
· 𝐵)))↑2)
· ((abs‘(𝐶 +
(i · 𝐷)))↑2))) |
| 43 | | absreimsq 15331 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((abs‘(𝐴 + (i
· 𝐵)))↑2) =
((𝐴↑2) + (𝐵↑2))) |
| 44 | | absreimsq 15331 |
. . . 4
⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) →
((abs‘(𝐶 + (i
· 𝐷)))↑2) =
((𝐶↑2) + (𝐷↑2))) |
| 45 | 43, 44 | oveqan12d 7450 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) →
(((abs‘(𝐴 + (i
· 𝐵)))↑2)
· ((abs‘(𝐶 +
(i · 𝐷)))↑2)) =
(((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2)))) |
| 46 | 37, 42, 45 | 3eqtrd 2781 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) →
((abs‘((𝐴 + (i
· 𝐵)) ·
(𝐶 + (i · 𝐷))))↑2) = (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2)))) |
| 47 | 1, 9 | remulcld 11291 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (𝐴 · 𝐶) ∈ ℝ) |
| 48 | 5, 11 | remulcld 11291 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (𝐵 · 𝐷) ∈ ℝ) |
| 49 | 47, 48 | resubcld 11691 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 · 𝐶) − (𝐵 · 𝐷)) ∈ ℝ) |
| 50 | 1, 11 | remulcld 11291 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (𝐴 · 𝐷) ∈ ℝ) |
| 51 | 5, 9 | remulcld 11291 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (𝐵 · 𝐶) ∈ ℝ) |
| 52 | 50, 51 | readdcld 11290 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 · 𝐷) + (𝐵 · 𝐶)) ∈ ℝ) |
| 53 | | absreimsq 15331 |
. . 3
⊢ ((((𝐴 · 𝐶) − (𝐵 · 𝐷)) ∈ ℝ ∧ ((𝐴 · 𝐷) + (𝐵 · 𝐶)) ∈ ℝ) →
((abs‘(((𝐴 ·
𝐶) − (𝐵 · 𝐷)) + (i · ((𝐴 · 𝐷) + (𝐵 · 𝐶)))))↑2) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2))) |
| 54 | 49, 52, 53 | syl2anc 584 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) →
((abs‘(((𝐴 ·
𝐶) − (𝐵 · 𝐷)) + (i · ((𝐴 · 𝐷) + (𝐵 · 𝐶)))))↑2) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2))) |
| 55 | 35, 46, 54 | 3eqtr3d 2785 |
1
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) →
(((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2))) |