Metamath Proof Explorer

Theorem subdivcomb1

Description: Bring a term in a subtraction into the numerator. (Contributed by Scott Fenton, 3-Jul-2013)

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

Proof

Step Hyp Ref Expression
1 simp3l 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> C e. CC )
2 simp1 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> A e. CC )
3 1 2 mulcld 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( C x. A ) e. CC )
4 divsubdir 
 |-  ( ( ( C x. A ) e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( C x. A ) - B ) / C ) = ( ( ( C x. A ) / C ) - ( B / C ) ) )
5 3 4 syld3an1 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( C x. A ) - B ) / C ) = ( ( ( C x. A ) / C ) - ( B / C ) ) )
6 divcan3 
 |-  ( ( A e. CC /\ C e. CC /\ C =/= 0 ) -> ( ( C x. A ) / C ) = A )
7 6 3expb 
 |-  ( ( A e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( C x. A ) / C ) = A )
8 7 3adant2 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( C x. A ) / C ) = A )
9 8 oveq1d 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( C x. A ) / C ) - ( B / C ) ) = ( A - ( B / C ) ) )
10 5 9 eqtrd 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( C x. A ) - B ) / C ) = ( A - ( B / C ) ) )