Metamath Proof Explorer

Theorem divcan5

Description: Cancellation of common factor in a ratio. (Contributed by NM, 9-Jan-2006)

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

Proof

Step Hyp Ref Expression
1 divid 
 |-  ( ( C e. CC /\ C =/= 0 ) -> ( C / C ) = 1 )
2 1 oveq1d 
 |-  ( ( C e. CC /\ C =/= 0 ) -> ( ( C / C ) x. ( A / B ) ) = ( 1 x. ( A / B ) ) )
3 2 3ad2ant3 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( C / C ) x. ( A / B ) ) = ( 1 x. ( A / B ) ) )
4 simp3l 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> C e. CC )
5 simp1 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> A e. CC )
6 simp3 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( C e. CC /\ C =/= 0 ) )
7 simp2 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( B e. CC /\ B =/= 0 ) )
8 divmuldiv 
 |-  ( ( ( C e. CC /\ A e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) ) -> ( ( C / C ) x. ( A / B ) ) = ( ( C x. A ) / ( C x. B ) ) )
9 4 5 6 7 8 syl22anc 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( C / C ) x. ( A / B ) ) = ( ( C x. A ) / ( C x. B ) ) )
10 divcl 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A / B ) e. CC )
11 10 3expb 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( A / B ) e. CC )
12 11 mulid2d 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( 1 x. ( A / B ) ) = ( A / B ) )
13 12 3adant3 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( 1 x. ( A / B ) ) = ( A / B ) )
14 3 9 13 3eqtr3d 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( C x. A ) / ( C x. B ) ) = ( A / B ) )