Metamath Proof Explorer

Theorem div12

Description: A commutative/associative law for division. (Contributed by NM, 30-Apr-2005)

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

Proof

Step Hyp Ref Expression
1 divcl 
 |-  ( ( B e. CC /\ C e. CC /\ C =/= 0 ) -> ( B / C ) e. CC )
2 1 3expb 
 |-  ( ( B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( B / C ) e. CC )
3 mulcom 
 |-  ( ( A e. CC /\ ( B / C ) e. CC ) -> ( A x. ( B / C ) ) = ( ( B / C ) x. A ) )
4 2 3 sylan2 
 |-  ( ( A e. CC /\ ( B e. CC /\ ( C e. CC /\ C =/= 0 ) ) ) -> ( A x. ( B / C ) ) = ( ( B / C ) x. A ) )
5 4 3impb 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( A x. ( B / C ) ) = ( ( B / C ) x. A ) )
6 div13 
 |-  ( ( B e. CC /\ ( C e. CC /\ C =/= 0 ) /\ A e. CC ) -> ( ( B / C ) x. A ) = ( ( A / C ) x. B ) )
7 6 3comr 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( B / C ) x. A ) = ( ( A / C ) x. B ) )
8 divcl 
 |-  ( ( A e. CC /\ C e. CC /\ C =/= 0 ) -> ( A / C ) e. CC )
9 8 3expb 
 |-  ( ( A e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( A / C ) e. CC )
10 mulcom 
 |-  ( ( ( A / C ) e. CC /\ B e. CC ) -> ( ( A / C ) x. B ) = ( B x. ( A / C ) ) )
11 9 10 stoic3 
 |-  ( ( A e. CC /\ ( C e. CC /\ C =/= 0 ) /\ B e. CC ) -> ( ( A / C ) x. B ) = ( B x. ( A / C ) ) )
12 11 3com23 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / C ) x. B ) = ( B x. ( A / C ) ) )
13 5 7 12 3eqtrd 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( A x. ( B / C ) ) = ( B x. ( A / C ) ) )