Proof of Theorem crim
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | recn 11246 | . . . 4
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) | 
| 2 |  | ax-icn 11215 | . . . . 5
⊢ i ∈
ℂ | 
| 3 |  | recn 11246 | . . . . 5
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) | 
| 4 |  | mulcl 11240 | . . . . 5
⊢ ((i
∈ ℂ ∧ 𝐵
∈ ℂ) → (i · 𝐵) ∈ ℂ) | 
| 5 | 2, 3, 4 | sylancr 587 | . . . 4
⊢ (𝐵 ∈ ℝ → (i
· 𝐵) ∈
ℂ) | 
| 6 |  | addcl 11238 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ (i
· 𝐵) ∈ ℂ)
→ (𝐴 + (i ·
𝐵)) ∈
ℂ) | 
| 7 | 1, 5, 6 | syl2an 596 | . . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + (i · 𝐵)) ∈ ℂ) | 
| 8 |  | imval 15147 | . . 3
⊢ ((𝐴 + (i · 𝐵)) ∈ ℂ →
(ℑ‘(𝐴 + (i
· 𝐵))) =
(ℜ‘((𝐴 + (i
· 𝐵)) /
i))) | 
| 9 | 7, 8 | syl 17 | . 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(ℑ‘(𝐴 + (i
· 𝐵))) =
(ℜ‘((𝐴 + (i
· 𝐵)) /
i))) | 
| 10 | 2, 4 | mpan 690 | . . . . . 6
⊢ (𝐵 ∈ ℂ → (i
· 𝐵) ∈
ℂ) | 
| 11 |  | ine0 11699 | . . . . . . 7
⊢ i ≠
0 | 
| 12 |  | divdir 11948 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ (i
· 𝐵) ∈ ℂ
∧ (i ∈ ℂ ∧ i ≠ 0)) → ((𝐴 + (i · 𝐵)) / i) = ((𝐴 / i) + ((i · 𝐵) / i))) | 
| 13 | 12 | 3expa 1118 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ (i
· 𝐵) ∈ ℂ)
∧ (i ∈ ℂ ∧ i ≠ 0)) → ((𝐴 + (i · 𝐵)) / i) = ((𝐴 / i) + ((i · 𝐵) / i))) | 
| 14 | 2, 11, 13 | mpanr12 705 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ (i
· 𝐵) ∈ ℂ)
→ ((𝐴 + (i ·
𝐵)) / i) = ((𝐴 / i) + ((i · 𝐵) / i))) | 
| 15 | 10, 14 | sylan2 593 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + (i · 𝐵)) / i) = ((𝐴 / i) + ((i · 𝐵) / i))) | 
| 16 |  | divrec2 11940 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ i ∈
ℂ ∧ i ≠ 0) → (𝐴 / i) = ((1 / i) · 𝐴)) | 
| 17 | 2, 11, 16 | mp3an23 1454 | . . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝐴 / i) = ((1 / i) · 𝐴)) | 
| 18 |  | irec 14241 | . . . . . . . . 9
⊢ (1 / i) =
-i | 
| 19 | 18 | oveq1i 7442 | . . . . . . . 8
⊢ ((1 / i)
· 𝐴) = (-i ·
𝐴) | 
| 20 | 19 | a1i 11 | . . . . . . 7
⊢ (𝐴 ∈ ℂ → ((1 / i)
· 𝐴) = (-i ·
𝐴)) | 
| 21 |  | mulneg12 11702 | . . . . . . . 8
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (-i · 𝐴) = (i · -𝐴)) | 
| 22 | 2, 21 | mpan 690 | . . . . . . 7
⊢ (𝐴 ∈ ℂ → (-i
· 𝐴) = (i ·
-𝐴)) | 
| 23 | 17, 20, 22 | 3eqtrd 2780 | . . . . . 6
⊢ (𝐴 ∈ ℂ → (𝐴 / i) = (i · -𝐴)) | 
| 24 |  | divcan3 11949 | . . . . . . 7
⊢ ((𝐵 ∈ ℂ ∧ i ∈
ℂ ∧ i ≠ 0) → ((i · 𝐵) / i) = 𝐵) | 
| 25 | 2, 11, 24 | mp3an23 1454 | . . . . . 6
⊢ (𝐵 ∈ ℂ → ((i
· 𝐵) / i) = 𝐵) | 
| 26 | 23, 25 | oveqan12d 7451 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 / i) + ((i · 𝐵) / i)) = ((i · -𝐴) + 𝐵)) | 
| 27 |  | negcl 11509 | . . . . . . 7
⊢ (𝐴 ∈ ℂ → -𝐴 ∈
ℂ) | 
| 28 |  | mulcl 11240 | . . . . . . 7
⊢ ((i
∈ ℂ ∧ -𝐴
∈ ℂ) → (i · -𝐴) ∈ ℂ) | 
| 29 | 2, 27, 28 | sylancr 587 | . . . . . 6
⊢ (𝐴 ∈ ℂ → (i
· -𝐴) ∈
ℂ) | 
| 30 |  | addcom 11448 | . . . . . 6
⊢ (((i
· -𝐴) ∈ ℂ
∧ 𝐵 ∈ ℂ)
→ ((i · -𝐴) +
𝐵) = (𝐵 + (i · -𝐴))) | 
| 31 | 29, 30 | sylan 580 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((i
· -𝐴) + 𝐵) = (𝐵 + (i · -𝐴))) | 
| 32 | 15, 26, 31 | 3eqtrrd 2781 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 + (i · -𝐴)) = ((𝐴 + (i · 𝐵)) / i)) | 
| 33 | 1, 3, 32 | syl2an 596 | . . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 + (i · -𝐴)) = ((𝐴 + (i · 𝐵)) / i)) | 
| 34 | 33 | fveq2d 6909 | . 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(ℜ‘(𝐵 + (i
· -𝐴))) =
(ℜ‘((𝐴 + (i
· 𝐵)) /
i))) | 
| 35 |  | id 22 | . . 3
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℝ) | 
| 36 |  | renegcl 11573 | . . 3
⊢ (𝐴 ∈ ℝ → -𝐴 ∈
ℝ) | 
| 37 |  | crre 15154 | . . 3
⊢ ((𝐵 ∈ ℝ ∧ -𝐴 ∈ ℝ) →
(ℜ‘(𝐵 + (i
· -𝐴))) = 𝐵) | 
| 38 | 35, 36, 37 | syl2anr 597 | . 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(ℜ‘(𝐵 + (i
· -𝐴))) = 𝐵) | 
| 39 | 9, 34, 38 | 3eqtr2d 2782 | 1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(ℑ‘(𝐴 + (i
· 𝐵))) = 𝐵) |