Metamath Proof Explorer


Theorem divdiv23zi

Description: Swap denominators in a division. (Contributed by NM, 15-Sep-1999)

Ref Expression
Hypotheses divclz.1
|- A e. CC
divclz.2
|- B e. CC
divmulz.3
|- C e. CC
Assertion divdiv23zi
|- ( ( B =/= 0 /\ C =/= 0 ) -> ( ( A / B ) / C ) = ( ( A / C ) / B ) )

Proof

Step Hyp Ref Expression
1 divclz.1
 |-  A e. CC
2 divclz.2
 |-  B e. CC
3 divmulz.3
 |-  C e. CC
4 divdiv32
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / B ) / C ) = ( ( A / C ) / B ) )
5 1 4 mp3an1
 |-  ( ( ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / B ) / C ) = ( ( A / C ) / B ) )
6 3 5 mpanr1
 |-  ( ( ( B e. CC /\ B =/= 0 ) /\ C =/= 0 ) -> ( ( A / B ) / C ) = ( ( A / C ) / B ) )
7 2 6 mpanl1
 |-  ( ( B =/= 0 /\ C =/= 0 ) -> ( ( A / B ) / C ) = ( ( A / C ) / B ) )