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→ℑ⁡AB=ℑ⁡AB

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→1B∈ℝ
5 4 anim1i ⊢B∈ℝ∧B≠0∧A∈ℂ→1B∈ℝ∧A∈ℂ
6 3 5 sylbir ⊢A∈ℂ∧B∈ℝ∧B≠0→1B∈ℝ∧A∈ℂ
7 immul2 ⊢1B∈ℝ∧A∈ℂ→ℑ⁡1B⁢A=1B⁢ℑ⁡A
8 6 7 syl ⊢A∈ℂ∧B∈ℝ∧B≠0→ℑ⁡1B⁢A=1B⁢ℑ⁡A
9 recn ⊢B∈ℝ→B∈ℂ
10 divrec2 ⊢A∈ℂ∧B∈ℂ∧B≠0→AB=1B⁢A
11 10 fveq2d ⊢A∈ℂ∧B∈ℂ∧B≠0→ℑ⁡AB=ℑ⁡1B⁢A
12 9 11 syl3an2 ⊢A∈ℂ∧B∈ℝ∧B≠0→ℑ⁡AB=ℑ⁡1B⁢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→ℑ⁡AB=1B⁢ℑ⁡A
19 8 12 18 3eqtr4d ⊢A∈ℂ∧B∈ℝ∧B≠0→ℑ⁡AB=ℑ⁡AB