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

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

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

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

2  div1   ( A e. CC > ( A / 1 ) = A ) 

3  1 2  syl   ( ph > ( A / 1 ) = A ) 