Metamath Proof Explorer

Theorem divdiv2

Description: Division by a fraction. (Contributed by NM, 27-Dec-2008)

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

Proof

Step Hyp Ref Expression
1 ax-1cn 
 |-  1 e. CC
2 ax-1ne0 
 |-  1 =/= 0
3 1 2 pm3.2i 
 |-  ( 1 e. CC /\ 1 =/= 0 )
4 divdivdiv 
 |-  ( ( ( A e. CC /\ ( 1 e. CC /\ 1 =/= 0 ) ) /\ ( ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) ) -> ( ( A / 1 ) / ( B / C ) ) = ( ( A x. C ) / ( 1 x. B ) ) )
5 3 4 mpanl2 
 |-  ( ( A e. CC /\ ( ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) ) -> ( ( A / 1 ) / ( B / C ) ) = ( ( A x. C ) / ( 1 x. B ) ) )
6 5 3impb 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / 1 ) / ( B / C ) ) = ( ( A x. C ) / ( 1 x. B ) ) )
7 div1 
 |-  ( A e. CC -> ( A / 1 ) = A )
8 7 3ad2ant1 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( A / 1 ) = A )
9 8 oveq1d 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / 1 ) / ( B / C ) ) = ( A / ( B / C ) ) )
10 mulid2 
 |-  ( B e. CC -> ( 1 x. B ) = B )
11 10 ad2antrl 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( 1 x. B ) = B )
12 11 3adant3 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( 1 x. B ) = B )
13 12 oveq2d 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A x. C ) / ( 1 x. B ) ) = ( ( A x. C ) / B ) )
14 6 9 13 3eqtr3d 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( A / ( B / C ) ) = ( ( A x. C ) / B ) )