This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( ℑ ‘ ( 𝐴 / 𝐵 ) ) = ( ( ℑ ‘ 𝐴 ) / 𝐵 ) )

Proof

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