Description: The reciprocal of a ratio. (Contributed by Mario Carneiro, 27May2016)
Ref  Expression  

Hypotheses  div1d.1   ( ph > A e. CC ) 

divcld.2   ( ph > B e. CC ) 

divne0d.3   ( ph > A =/= 0 ) 

divne0d.4   ( ph > B =/= 0 ) 

Assertion  recdivd   ( ph > ( 1 / ( A / B ) ) = ( B / A ) ) 
Step  Hyp  Ref  Expression 

1  div1d.1   ( ph > A e. CC ) 

2  divcld.2   ( ph > B e. CC ) 

3  divne0d.3   ( ph > A =/= 0 ) 

4  divne0d.4   ( ph > B =/= 0 ) 

5  recdiv   ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) > ( 1 / ( A / B ) ) = ( B / A ) ) 

6  1 3 2 4 5  syl22anc   ( ph > ( 1 / ( A / B ) ) = ( B / A ) ) 