Description: A real number equals its complex conjugate. Proposition 103.4(f) of Gleason p. 133. (Contributed by Mario Carneiro, 29May2016)
Ref  Expression  

Hypothesis  crred.1   ( ph > A e. RR ) 

Assertion  cjred   ( ph > ( * ` A ) = A ) 
Step  Hyp  Ref  Expression 

1  crred.1   ( ph > A e. RR ) 

2  cjre   ( A e. RR > ( * ` A ) = A ) 

3  1 2  syl   ( ph > ( * ` A ) = A ) 