Metamath Proof Explorer

Theorem rediv

Description: Real part of a division. Related to remul2 . (Contributed by David A. Wheeler, 10-Jun-2015)

Ref Expression
Assertion rediv 
|- ( ( A e. CC /\ B e. RR /\ B =/= 0 ) -> ( Re ` ( A / B ) ) = ( ( Re ` 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 remul2 
 |-  ( ( ( 1 / B ) e. RR /\ A e. CC ) -> ( Re ` ( ( 1 / B ) x. A ) ) = ( ( 1 / B ) x. ( Re ` A ) ) )
8 6 7 syl 
 |-  ( ( A e. CC /\ B e. RR /\ B =/= 0 ) -> ( Re ` ( ( 1 / B ) x. A ) ) = ( ( 1 / B ) x. ( Re ` 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 ) -> ( Re ` ( A / B ) ) = ( Re ` ( ( 1 / B ) x. A ) ) )
12 9 11 syl3an2 
 |-  ( ( A e. CC /\ B e. RR /\ B =/= 0 ) -> ( Re ` ( A / B ) ) = ( Re ` ( ( 1 / B ) x. A ) ) )
13 recl 
 |-  ( A e. CC -> ( Re ` A ) e. RR )
14 13 recnd 
 |-  ( A e. CC -> ( Re ` A ) e. CC )
15 14 3ad2ant1 
 |-  ( ( A e. CC /\ B e. RR /\ B =/= 0 ) -> ( Re ` 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 ) -> ( ( Re ` A ) / B ) = ( ( 1 / B ) x. ( Re ` A ) ) )
19 8 12 18 3eqtr4d 
 |-  ( ( A e. CC /\ B e. RR /\ B =/= 0 ) -> ( Re ` ( A / B ) ) = ( ( Re ` A ) / B ) )