Metamath Proof Explorer

Theorem divdiv1

Description: Division into a fraction. (Contributed by NM, 31-Dec-2007)

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

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 /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( 1 e. CC /\ 1 =/= 0 ) ) ) -> ( ( A / B ) / ( C / 1 ) ) = ( ( A x. 1 ) / ( B x. C ) ) )
5 3 4 mpanr2 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / B ) / ( C / 1 ) ) = ( ( A x. 1 ) / ( B x. C ) ) )
6 5 3impa 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / B ) / ( C / 1 ) ) = ( ( A x. 1 ) / ( B x. C ) ) )
7 div1 
 |-  ( C e. CC -> ( C / 1 ) = C )
8 7 oveq2d 
 |-  ( C e. CC -> ( ( A / B ) / ( C / 1 ) ) = ( ( A / B ) / C ) )
9 8 ad2antrl 
 |-  ( ( ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / B ) / ( C / 1 ) ) = ( ( A / B ) / C ) )
10 9 3adant1 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / B ) / ( C / 1 ) ) = ( ( A / B ) / C ) )
11 mulid1 
 |-  ( A e. CC -> ( A x. 1 ) = A )
12 11 oveq1d 
 |-  ( A e. CC -> ( ( A x. 1 ) / ( B x. C ) ) = ( A / ( B x. C ) ) )
13 12 3ad2ant1 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A x. 1 ) / ( B x. C ) ) = ( A / ( B x. C ) ) )
14 6 10 13 3eqtr3d 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / B ) / C ) = ( A / ( B x. C ) ) )