Theorem imdiv

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

	Ref	Expression
Assertion	imdiv	|- ( ( A e. CC /\ B e. RR /\ B =/= 0 ) -> ( Im ` ( A / B ) ) = ( ( Im ` A ) / B ) )

Proof

Step	Hyp	Ref	Expression
1		ancom	|- ( ( ( B e. RR /\ B =/= 0 ) /\ A e. CC ) <-> ( A e. CC /\ ( B e. RR /\ B =/= 0 ) ) )
2		3anass	|- ( ( A e. CC /\ B e. RR /\ B =/= 0 ) <-> ( A e. CC /\ ( B e. RR /\ B =/= 0 ) ) )
3	1 2	bitr4i	|- ( ( ( B e. RR /\ B =/= 0 ) /\ A e. CC ) <-> ( A e. CC /\ B e. RR /\ B =/= 0 ) )
4		rereccl	|- ( ( B e. RR /\ B =/= 0 ) -> ( 1 / B ) e. RR )
5	4	anim1i	|- ( ( ( B e. RR /\ B =/= 0 ) /\ A e. CC ) -> ( ( 1 / B ) e. RR /\ A e. CC ) )
6	3 5	sylbir	|- ( ( A e. CC /\ B e. RR /\ B =/= 0 ) -> ( ( 1 / B ) e. RR /\ A e. CC ) )
7		immul2	|- ( ( ( 1 / B ) e. RR /\ A e. CC ) -> ( Im ` ( ( 1 / B ) x. A ) ) = ( ( 1 / B ) x. ( Im ` A ) ) )
8	6 7	syl	|- ( ( A e. CC /\ B e. RR /\ B =/= 0 ) -> ( Im ` ( ( 1 / B ) x. A ) ) = ( ( 1 / B ) x. ( Im ` A ) ) )
9		recn	|- ( B e. RR -> B e. CC )
10		divrec2	|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A / B ) = ( ( 1 / B ) x. A ) )
11	10	fveq2d	|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( Im ` ( A / B ) ) = ( Im ` ( ( 1 / B ) x. A ) ) )
12	9 11	syl3an2	|- ( ( A e. CC /\ B e. RR /\ B =/= 0 ) -> ( Im ` ( A / B ) ) = ( Im ` ( ( 1 / B ) x. A ) ) )
13		imcl	|- ( A e. CC -> ( Im ` A ) e. RR )
14	13	recnd	|- ( A e. CC -> ( Im ` A ) e. CC )
15	14	3ad2ant1	|- ( ( A e. CC /\ B e. RR /\ B =/= 0 ) -> ( Im ` A ) e. CC )
16	9	3ad2ant2	|- ( ( A e. CC /\ B e. RR /\ B =/= 0 ) -> B e. CC )
17		simp3	|- ( ( A e. CC /\ B e. RR /\ B =/= 0 ) -> B =/= 0 )
18	15 16 17	divrec2d	|- ( ( A e. CC /\ B e. RR /\ B =/= 0 ) -> ( ( Im ` A ) / B ) = ( ( 1 / B ) x. ( Im ` A ) ) )
19	8 12 18	3eqtr4d	|- ( ( A e. CC /\ B e. RR /\ B =/= 0 ) -> ( Im ` ( A / B ) ) = ( ( Im ` A ) / B ) )