Metamath Proof Explorer

Theorem subdivcomb2

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

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

Proof

Step Hyp Ref Expression
1 simp3l 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> C e. CC )
2 simp2 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> B e. CC )
3 1 2 mulcld 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( C x. B ) e. CC )
4 divsubdir 
 |-  ( ( A e. CC /\ ( C x. B ) e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A - ( C x. B ) ) / C ) = ( ( A / C ) - ( ( C x. B ) / C ) ) )
5 3 4 syld3an2 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A - ( C x. B ) ) / C ) = ( ( A / C ) - ( ( C x. B ) / C ) ) )
6 simprl 
 |-  ( ( B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> C e. CC )
7 simpl 
 |-  ( ( B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> B e. CC )
8 simpr 
 |-  ( ( B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( C e. CC /\ C =/= 0 ) )
9 div23 
 |-  ( ( C e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( C x. B ) / C ) = ( ( C / C ) x. B ) )
10 6 7 8 9 syl3anc 
 |-  ( ( B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( C x. B ) / C ) = ( ( C / C ) x. B ) )
11 divid 
 |-  ( ( C e. CC /\ C =/= 0 ) -> ( C / C ) = 1 )
12 11 oveq1d 
 |-  ( ( C e. CC /\ C =/= 0 ) -> ( ( C / C ) x. B ) = ( 1 x. B ) )
13 mulid2 
 |-  ( B e. CC -> ( 1 x. B ) = B )
14 12 13 sylan9eqr 
 |-  ( ( B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( C / C ) x. B ) = B )
15 10 14 eqtrd 
 |-  ( ( B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( C x. B ) / C ) = B )
16 15 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( C x. B ) / C ) = B )
17 16 oveq2d 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / C ) - ( ( C x. B ) / C ) ) = ( ( A / C ) - B ) )
18 5 17 eqtrd 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A - ( C x. B ) ) / C ) = ( ( A / C ) - B ) )