Metamath Proof Explorer

Theorem recdiv

Description: The reciprocal of a ratio. (Contributed by NM, 3-Aug-2004)

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

Proof

Step Hyp Ref Expression
1 1div1e1 
 |-  ( 1 / 1 ) = 1
2 1 oveq1i 
 |-  ( ( 1 / 1 ) / ( A / B ) ) = ( 1 / ( A / B ) )
3 ax-1cn 
 |-  1 e. CC
4 ax-1ne0 
 |-  1 =/= 0
5 3 4 pm3.2i 
 |-  ( 1 e. CC /\ 1 =/= 0 )
6 divdivdiv 
 |-  ( ( ( 1 e. CC /\ ( 1 e. CC /\ 1 =/= 0 ) ) /\ ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) ) -> ( ( 1 / 1 ) / ( A / B ) ) = ( ( 1 x. B ) / ( 1 x. A ) ) )
7 3 5 6 mpanl12 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( 1 / 1 ) / ( A / B ) ) = ( ( 1 x. B ) / ( 1 x. A ) ) )
8 2 7 eqtr3id 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( 1 / ( A / B ) ) = ( ( 1 x. B ) / ( 1 x. A ) ) )
9 mullid 
 |-  ( B e. CC -> ( 1 x. B ) = B )
10 mullid 
 |-  ( A e. CC -> ( 1 x. A ) = A )
11 9 10 oveqan12rd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( 1 x. B ) / ( 1 x. A ) ) = ( B / A ) )
12 11 ad2ant2r 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( 1 x. B ) / ( 1 x. A ) ) = ( B / A ) )
13 8 12 eqtrd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( 1 / ( A / B ) ) = ( B / A ) )