Description: Multiplication of a number and its reciprocal. (Contributed by Mario Carneiro, 27May2016)
Ref  Expression  

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

reccld.2   ( ph > A =/= 0 ) 

Assertion  recidd   ( ph > ( A x. ( 1 / A ) ) = 1 ) 
Step  Hyp  Ref  Expression 

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

2  reccld.2   ( ph > A =/= 0 ) 

3  recid   ( ( A e. CC /\ A =/= 0 ) > ( A x. ( 1 / A ) ) = 1 ) 

4  1 2 3  syl2anc   ( ph > ( A x. ( 1 / A ) ) = 1 ) 