Description: A number divided by itself is one. (Contributed by Mario Carneiro, 27May2016)
Ref  Expression  

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

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

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

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

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

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

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