Proof of Theorem crim
Step | Hyp | Ref
| Expression |
1 | | recn 7894 |
. . . 4
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
2 | | ax-icn 7856 |
. . . . 5
⊢ i ∈
ℂ |
3 | | recn 7894 |
. . . . 5
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) |
4 | | mulcl 7888 |
. . . . 5
⊢ ((i
∈ ℂ ∧ 𝐵
∈ ℂ) → (i · 𝐵) ∈ ℂ) |
5 | 2, 3, 4 | sylancr 412 |
. . . 4
⊢ (𝐵 ∈ ℝ → (i
· 𝐵) ∈
ℂ) |
6 | | addcl 7886 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ (i
· 𝐵) ∈ ℂ)
→ (𝐴 + (i ·
𝐵)) ∈
ℂ) |
7 | 1, 5, 6 | syl2an 287 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + (i · 𝐵)) ∈ ℂ) |
8 | | imval 10801 |
. . 3
⊢ ((𝐴 + (i · 𝐵)) ∈ ℂ →
(ℑ‘(𝐴 + (i
· 𝐵))) =
(ℜ‘((𝐴 + (i
· 𝐵)) /
i))) |
9 | 7, 8 | syl 14 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(ℑ‘(𝐴 + (i
· 𝐵))) =
(ℜ‘((𝐴 + (i
· 𝐵)) /
i))) |
10 | 2, 4 | mpan 422 |
. . . . . 6
⊢ (𝐵 ∈ ℂ → (i
· 𝐵) ∈
ℂ) |
11 | | iap0 9088 |
. . . . . . 7
⊢ i #
0 |
12 | | divdirap 8601 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ (i
· 𝐵) ∈ ℂ
∧ (i ∈ ℂ ∧ i # 0)) → ((𝐴 + (i · 𝐵)) / i) = ((𝐴 / i) + ((i · 𝐵) / i))) |
13 | 12 | 3expa 1198 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ (i
· 𝐵) ∈ ℂ)
∧ (i ∈ ℂ ∧ i # 0)) → ((𝐴 + (i · 𝐵)) / i) = ((𝐴 / i) + ((i · 𝐵) / i))) |
14 | 2, 11, 13 | mpanr12 437 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ (i
· 𝐵) ∈ ℂ)
→ ((𝐴 + (i ·
𝐵)) / i) = ((𝐴 / i) + ((i · 𝐵) / i))) |
15 | 10, 14 | sylan2 284 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + (i · 𝐵)) / i) = ((𝐴 / i) + ((i · 𝐵) / i))) |
16 | | divrecap2 8593 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ i ∈
ℂ ∧ i # 0) → (𝐴 / i) = ((1 / i) · 𝐴)) |
17 | 2, 11, 16 | mp3an23 1324 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝐴 / i) = ((1 / i) · 𝐴)) |
18 | | irec 10562 |
. . . . . . . . 9
⊢ (1 / i) =
-i |
19 | 18 | oveq1i 5860 |
. . . . . . . 8
⊢ ((1 / i)
· 𝐴) = (-i ·
𝐴) |
20 | 19 | a1i 9 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → ((1 / i)
· 𝐴) = (-i ·
𝐴)) |
21 | | mulneg12 8303 |
. . . . . . . 8
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (-i · 𝐴) = (i · -𝐴)) |
22 | 2, 21 | mpan 422 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (-i
· 𝐴) = (i ·
-𝐴)) |
23 | 17, 20, 22 | 3eqtrd 2207 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (𝐴 / i) = (i · -𝐴)) |
24 | | divcanap3 8602 |
. . . . . . 7
⊢ ((𝐵 ∈ ℂ ∧ i ∈
ℂ ∧ i # 0) → ((i · 𝐵) / i) = 𝐵) |
25 | 2, 11, 24 | mp3an23 1324 |
. . . . . 6
⊢ (𝐵 ∈ ℂ → ((i
· 𝐵) / i) = 𝐵) |
26 | 23, 25 | oveqan12d 5869 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 / i) + ((i · 𝐵) / i)) = ((i · -𝐴) + 𝐵)) |
27 | | negcl 8106 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → -𝐴 ∈
ℂ) |
28 | | mulcl 7888 |
. . . . . . 7
⊢ ((i
∈ ℂ ∧ -𝐴
∈ ℂ) → (i · -𝐴) ∈ ℂ) |
29 | 2, 27, 28 | sylancr 412 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (i
· -𝐴) ∈
ℂ) |
30 | | addcom 8043 |
. . . . . 6
⊢ (((i
· -𝐴) ∈ ℂ
∧ 𝐵 ∈ ℂ)
→ ((i · -𝐴) +
𝐵) = (𝐵 + (i · -𝐴))) |
31 | 29, 30 | sylan 281 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((i
· -𝐴) + 𝐵) = (𝐵 + (i · -𝐴))) |
32 | 15, 26, 31 | 3eqtrrd 2208 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 + (i · -𝐴)) = ((𝐴 + (i · 𝐵)) / i)) |
33 | 1, 3, 32 | syl2an 287 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 + (i · -𝐴)) = ((𝐴 + (i · 𝐵)) / i)) |
34 | 33 | fveq2d 5498 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(ℜ‘(𝐵 + (i
· -𝐴))) =
(ℜ‘((𝐴 + (i
· 𝐵)) /
i))) |
35 | | id 19 |
. . 3
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℝ) |
36 | | renegcl 8167 |
. . 3
⊢ (𝐴 ∈ ℝ → -𝐴 ∈
ℝ) |
37 | | crre 10808 |
. . 3
⊢ ((𝐵 ∈ ℝ ∧ -𝐴 ∈ ℝ) →
(ℜ‘(𝐵 + (i
· -𝐴))) = 𝐵) |
38 | 35, 36, 37 | syl2anr 288 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(ℜ‘(𝐵 + (i
· -𝐴))) = 𝐵) |
39 | 9, 34, 38 | 3eqtr2d 2209 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(ℑ‘(𝐴 + (i
· 𝐵))) = 𝐵) |