Metamath Proof Explorer

Theorem divass

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

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

Proof

Step Hyp Ref Expression
1 reccl 
 |-  ( ( C e. CC /\ C =/= 0 ) -> ( 1 / C ) e. CC )
2 mulass 
 |-  ( ( A e. CC /\ B e. CC /\ ( 1 / C ) e. CC ) -> ( ( A x. B ) x. ( 1 / C ) ) = ( A x. ( B x. ( 1 / C ) ) ) )
3 1 2 syl3an3 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A x. B ) x. ( 1 / C ) ) = ( A x. ( B x. ( 1 / C ) ) ) )
4 mulcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
5 4 3adant3 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( A x. B ) e. CC )
6 simp3l 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> C e. CC )
7 simp3r 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> C =/= 0 )
8 divrec 
 |-  ( ( ( A x. B ) e. CC /\ C e. CC /\ C =/= 0 ) -> ( ( A x. B ) / C ) = ( ( A x. B ) x. ( 1 / C ) ) )
9 5 6 7 8 syl3anc 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A x. B ) / C ) = ( ( A x. B ) x. ( 1 / C ) ) )
10 simp2 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> B e. CC )
11 divrec 
 |-  ( ( B e. CC /\ C e. CC /\ C =/= 0 ) -> ( B / C ) = ( B x. ( 1 / C ) ) )
12 10 6 7 11 syl3anc 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( B / C ) = ( B x. ( 1 / C ) ) )
13 12 oveq2d 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( A x. ( B / C ) ) = ( A x. ( B x. ( 1 / C ) ) ) )
14 3 9 13 3eqtr4d 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A x. B ) / C ) = ( A x. ( B / C ) ) )