Metamath Proof Explorer


Theorem cjreb

Description: A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of Gleason p. 133. (Contributed by NM, 2-Jul-2005) (Revised by Mario Carneiro, 14-Jul-2014)

Ref Expression
Assertion cjreb AAA=A

Proof

Step Hyp Ref Expression
1 recl AA
2 1 recnd AA
3 ax-icn i
4 imcl AA
5 4 recnd AA
6 mulcl iAiA
7 3 5 6 sylancr AiA
8 2 7 negsubd AA+iA=AiA
9 mulneg2 iAiA=iA
10 3 5 9 sylancr AiA=iA
11 10 oveq2d AA+iA=A+iA
12 remim AA=AiA
13 8 11 12 3eqtr4rd AA=A+iA
14 replim AA=A+iA
15 13 14 eqeq12d AA=AA+iA=A+iA
16 5 negcld AA
17 mulcl iAiA
18 3 16 17 sylancr AiA
19 2 18 7 addcand AA+iA=A+iAiA=iA
20 eqcom A=AA=A
21 5 eqnegd AA=AA=0
22 20 21 syl5bb AA=AA=0
23 ine0 i0
24 3 23 pm3.2i ii0
25 24 a1i Aii0
26 mulcan AAii0iA=iAA=A
27 16 5 25 26 syl3anc AiA=iAA=A
28 reim0b AAA=0
29 22 27 28 3bitr4d AiA=iAA
30 15 19 29 3bitrrd AAA=A