Metamath Proof Explorer

Theorem divsubdir

Description: Distribution of division over subtraction. (Contributed by NM, 4-Mar-2005)

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

Proof

Step Hyp Ref Expression
1 negcl 
 |-  ( B e. CC -> -u B e. CC )
2 divdir 
 |-  ( ( A e. CC /\ -u B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A + -u B ) / C ) = ( ( A / C ) + ( -u B / C ) ) )
3 1 2 syl3an2 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A + -u B ) / C ) = ( ( A / C ) + ( -u B / C ) ) )
4 negsub 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + -u B ) = ( A - B ) )
5 4 oveq1d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + -u B ) / C ) = ( ( A - B ) / C ) )
6 5 3adant3 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A + -u B ) / C ) = ( ( A - B ) / C ) )
7 3 6 eqtr3d 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / C ) + ( -u B / C ) ) = ( ( A - B ) / C ) )
8 divneg 
 |-  ( ( B e. CC /\ C e. CC /\ C =/= 0 ) -> -u ( B / C ) = ( -u B / C ) )
9 8 3expb 
 |-  ( ( B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> -u ( B / C ) = ( -u B / C ) )
10 9 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> -u ( B / C ) = ( -u B / C ) )
11 10 oveq2d 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / C ) + -u ( B / C ) ) = ( ( A / C ) + ( -u B / C ) ) )
12 divcl 
 |-  ( ( A e. CC /\ C e. CC /\ C =/= 0 ) -> ( A / C ) e. CC )
13 12 3expb 
 |-  ( ( A e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( A / C ) e. CC )
14 13 3adant2 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( A / C ) e. CC )
15 divcl 
 |-  ( ( B e. CC /\ C e. CC /\ C =/= 0 ) -> ( B / C ) e. CC )
16 15 3expb 
 |-  ( ( B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( B / C ) e. CC )
17 16 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( B / C ) e. CC )
18 14 17 negsubd 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / C ) + -u ( B / C ) ) = ( ( A / C ) - ( B / C ) ) )
19 11 18 eqtr3d 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / C ) + ( -u B / C ) ) = ( ( A / C ) - ( B / C ) ) )
20 7 19 eqtr3d 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A - B ) / C ) = ( ( A / C ) - ( B / C ) ) )