Metamath Proof Explorer

Theorem imdiv

Description: Imaginary part of a division. Related to immul2 . (Contributed by Mario Carneiro, 20-Jun-2015)

Ref Expression
Assertion imdiv ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ B ≠ 0 → ℑ ⁡ A B = ℑ ⁡ A B

Proof

Step Hyp Ref Expression
1 ancom ⊢ B ∈ ℝ ∧ B ≠ 0 ∧ A ∈ ℂ ↔ A ∈ ℂ ∧ B ∈ ℝ ∧ B ≠ 0
2 3anass ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ B ≠ 0 ↔ A ∈ ℂ ∧ B ∈ ℝ ∧ B ≠ 0
3 1 2 bitr4i ⊢ B ∈ ℝ ∧ B ≠ 0 ∧ A ∈ ℂ ↔ A ∈ ℂ ∧ B ∈ ℝ ∧ B ≠ 0
4 rereccl ⊢ B ∈ ℝ ∧ B ≠ 0 → 1 B ∈ ℝ
5 4 anim1i ⊢ B ∈ ℝ ∧ B ≠ 0 ∧ A ∈ ℂ → 1 B ∈ ℝ ∧ A ∈ ℂ
6 3 5 sylbir ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ B ≠ 0 → 1 B ∈ ℝ ∧ A ∈ ℂ
7 immul2 ⊢ 1 B ∈ ℝ ∧ A ∈ ℂ → ℑ ⁡ 1 B ⁢ A = 1 B ⁢ ℑ ⁡ A
8 6 7 syl ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ B ≠ 0 → ℑ ⁡ 1 B ⁢ A = 1 B ⁢ ℑ ⁡ A
9 recn ⊢ B ∈ ℝ → B ∈ ℂ
10 divrec2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B = 1 B ⁢ A
11 10 fveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → ℑ ⁡ A B = ℑ ⁡ 1 B ⁢ A
12 9 11 syl3an2 ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ B ≠ 0 → ℑ ⁡ A B = ℑ ⁡ 1 B ⁢ A
13 imcl ⊢ A ∈ ℂ → ℑ ⁡ A ∈ ℝ
14 13 recnd ⊢ A ∈ ℂ → ℑ ⁡ A ∈ ℂ
15 14 3ad2ant1 ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ B ≠ 0 → ℑ ⁡ A ∈ ℂ
16 9 3ad2ant2 ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ B ≠ 0 → B ∈ ℂ
17 simp3 ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ B ≠ 0 → B ≠ 0
18 15 16 17 divrec2d ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ B ≠ 0 → ℑ ⁡ A B = 1 B ⁢ ℑ ⁡ A
19 8 12 18 3eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ B ≠ 0 → ℑ ⁡ A B = ℑ ⁡ A B