Metamath Proof Explorer


Theorem divasszi

Description: An associative law for division. (Contributed by NM, 12-Aug-1999)

Ref Expression
Hypotheses divclz.1
|- A e. CC
divclz.2
|- B e. CC
divmulz.3
|- C e. CC
Assertion divasszi
|- ( C =/= 0 -> ( ( A x. B ) / C ) = ( A x. ( B / C ) ) )

Proof

Step Hyp Ref Expression
1 divclz.1
 |-  A e. CC
2 divclz.2
 |-  B e. CC
3 divmulz.3
 |-  C e. CC
4 divass
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A x. B ) / C ) = ( A x. ( B / C ) ) )
5 1 2 4 mp3an12
 |-  ( ( C e. CC /\ C =/= 0 ) -> ( ( A x. B ) / C ) = ( A x. ( B / C ) ) )
6 3 5 mpan
 |-  ( C =/= 0 -> ( ( A x. B ) / C ) = ( A x. ( B / C ) ) )