Metamath Proof Explorer

Theorem divdiv32

Description: Swap denominators in a division. (Contributed by NM, 2-Aug-2004)

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

Proof

Step Hyp Ref Expression
1 reccl 
 |-  ( ( B e. CC /\ B =/= 0 ) -> ( 1 / B ) e. CC )
2 div23 
 |-  ( ( A e. CC /\ ( 1 / B ) e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A x. ( 1 / B ) ) / C ) = ( ( A / C ) x. ( 1 / B ) ) )
3 1 2 syl3an2 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A x. ( 1 / B ) ) / C ) = ( ( A / C ) x. ( 1 / B ) ) )
4 divrec 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A / B ) = ( A x. ( 1 / B ) ) )
5 4 3expb 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( A / B ) = ( A x. ( 1 / B ) ) )
6 5 3adant3 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( A / B ) = ( A x. ( 1 / B ) ) )
7 6 oveq1d 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / B ) / C ) = ( ( A x. ( 1 / B ) ) / C ) )
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 divrec 
 |-  ( ( ( A / C ) e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / C ) / B ) = ( ( A / C ) x. ( 1 / B ) ) )
11 9 10 syl3an1 
 |-  ( ( ( A e. CC /\ ( C e. CC /\ C =/= 0 ) ) /\ B e. CC /\ B =/= 0 ) -> ( ( A / C ) / B ) = ( ( A / C ) x. ( 1 / B ) ) )
12 11 3expb 
 |-  ( ( ( A e. CC /\ ( C e. CC /\ C =/= 0 ) ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( A / C ) / B ) = ( ( A / C ) x. ( 1 / B ) ) )
13 12 3impa 
 |-  ( ( A e. CC /\ ( C e. CC /\ C =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( A / C ) / B ) = ( ( A / C ) x. ( 1 / B ) ) )
14 13 3com23 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / C ) / B ) = ( ( A / C ) x. ( 1 / B ) ) )
15 3 7 14 3eqtr4d 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / B ) / C ) = ( ( A / C ) / B ) )