Metamath Proof Explorer

Theorem absdiv

Description: Absolute value distributes over division. (Contributed by NM, 27-Apr-2005)

Ref Expression
Assertion absdiv 
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( abs ` ( A / B ) ) = ( ( abs ` A ) / ( abs ` B ) ) )

Proof

Step Hyp Ref Expression
1 divcl 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A / B ) e. CC )
2 abscl 
 |-  ( ( A / B ) e. CC -> ( abs ` ( A / B ) ) e. RR )
3 1 2 syl 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( abs ` ( A / B ) ) e. RR )
4 3 recnd 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( abs ` ( A / B ) ) e. CC )
5 absrpcl 
 |-  ( ( B e. CC /\ B =/= 0 ) -> ( abs ` B ) e. RR+ )
6 5 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( abs ` B ) e. RR+ )
7 6 rpcnd 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( abs ` B ) e. CC )
8 6 rpne0d 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( abs ` B ) =/= 0 )
9 4 7 8 divcan4d 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( ( abs ` ( A / B ) ) x. ( abs ` B ) ) / ( abs ` B ) ) = ( abs ` ( A / B ) ) )
10 simp2 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> B e. CC )
11 absmul 
 |-  ( ( ( A / B ) e. CC /\ B e. CC ) -> ( abs ` ( ( A / B ) x. B ) ) = ( ( abs ` ( A / B ) ) x. ( abs ` B ) ) )
12 1 10 11 syl2anc 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( abs ` ( ( A / B ) x. B ) ) = ( ( abs ` ( A / B ) ) x. ( abs ` B ) ) )
13 divcan1 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / B ) x. B ) = A )
14 13 fveq2d 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( abs ` ( ( A / B ) x. B ) ) = ( abs ` A ) )
15 12 14 eqtr3d 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( abs ` ( A / B ) ) x. ( abs ` B ) ) = ( abs ` A ) )
16 15 oveq1d 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( ( abs ` ( A / B ) ) x. ( abs ` B ) ) / ( abs ` B ) ) = ( ( abs ` A ) / ( abs ` B ) ) )
17 9 16 eqtr3d 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( abs ` ( A / B ) ) = ( ( abs ` A ) / ( abs ` B ) ) )