Metamath Proof Explorer


Theorem cjrebd

Description: A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of Gleason p. 133. (Contributed by Mario Carneiro, 29-May-2016)

Ref Expression
Hypotheses recld.1
|- ( ph -> A e. CC )
cjrebd.2
|- ( ph -> ( * ` A ) = A )
Assertion cjrebd
|- ( ph -> A e. RR )

Proof

Step Hyp Ref Expression
1 recld.1
 |-  ( ph -> A e. CC )
2 cjrebd.2
 |-  ( ph -> ( * ` A ) = A )
3 cjreb
 |-  ( A e. CC -> ( A e. RR <-> ( * ` A ) = A ) )
4 1 3 syl
 |-  ( ph -> ( A e. RR <-> ( * ` A ) = A ) )
5 2 4 mpbird
 |-  ( ph -> A e. RR )