Metamath Proof Explorer

Theorem divcan7

Description: Cancel equal divisors in a division. (Contributed by Jeff Hankins, 29-Sep-2013)

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

Proof

Step Hyp Ref Expression
1 divdivdiv 
 |-  ( ( ( A e. CC /\ ( C e. CC /\ C =/= 0 ) ) /\ ( ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) ) -> ( ( A / C ) / ( B / C ) ) = ( ( A x. C ) / ( C x. B ) ) )
2 1 3impdir 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / C ) / ( B / C ) ) = ( ( A x. C ) / ( C x. B ) ) )
3 mulcom 
 |-  ( ( A e. CC /\ C e. CC ) -> ( A x. C ) = ( C x. A ) )
4 3 adantrr 
 |-  ( ( A e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( A x. C ) = ( C x. A ) )
5 4 3adant2 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( A x. C ) = ( C x. A ) )
6 5 oveq1d 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A x. C ) / ( C x. B ) ) = ( ( C x. A ) / ( C x. B ) ) )
7 divcan5 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( C x. A ) / ( C x. B ) ) = ( A / B ) )
8 2 6 7 3eqtrd 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / C ) / ( B / C ) ) = ( A / B ) )