Metamath Proof Explorer

Theorem divneg

Description: Move negative sign inside of a division. (Contributed by NM, 17-Sep-2004)

Ref Expression
Assertion divneg 
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> -u ( A / B ) = ( -u A / B ) )

Proof

Step Hyp Ref Expression
1 reccl 
 |-  ( ( B e. CC /\ B =/= 0 ) -> ( 1 / B ) e. CC )
2 mulneg1 
 |-  ( ( A e. CC /\ ( 1 / B ) e. CC ) -> ( -u A x. ( 1 / B ) ) = -u ( A x. ( 1 / B ) ) )
3 1 2 sylan2 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( -u A x. ( 1 / B ) ) = -u ( A x. ( 1 / B ) ) )
4 3 3impb 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( -u A x. ( 1 / B ) ) = -u ( A x. ( 1 / B ) ) )
5 negcl 
 |-  ( A e. CC -> -u A e. CC )
6 divrec 
 |-  ( ( -u A e. CC /\ B e. CC /\ B =/= 0 ) -> ( -u A / B ) = ( -u A x. ( 1 / B ) ) )
7 5 6 syl3an1 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( -u A / B ) = ( -u A x. ( 1 / B ) ) )
8 divrec 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A / B ) = ( A x. ( 1 / B ) ) )
9 8 negeqd 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> -u ( A / B ) = -u ( A x. ( 1 / B ) ) )
10 4 7 9 3eqtr4rd 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> -u ( A / B ) = ( -u A / B ) )