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 ) → ( ℑ ‘ ( 𝐴 / 𝐵 ) ) = ( ( ℑ ‘ 𝐴 ) / 𝐵 ) )