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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | recl | |
|
2 | 1 | recnd | |
3 | ax-icn | |
|
4 | imcl | |
|
5 | 4 | recnd | |
6 | mulcl | |
|
7 | 3 5 6 | sylancr | |
8 | 2 7 | negsubd | |
9 | mulneg2 | |
|
10 | 3 5 9 | sylancr | |
11 | 10 | oveq2d | |
12 | remim | |
|
13 | 8 11 12 | 3eqtr4rd | |
14 | replim | |
|
15 | 13 14 | eqeq12d | |
16 | 5 | negcld | |
17 | mulcl | |
|
18 | 3 16 17 | sylancr | |
19 | 2 18 7 | addcand | |
20 | eqcom | |
|
21 | 5 | eqnegd | |
22 | 20 21 | syl5bb | |
23 | ine0 | |
|
24 | 3 23 | pm3.2i | |
25 | 24 | a1i | |
26 | mulcan | |
|
27 | 16 5 25 26 | syl3anc | |
28 | reim0b | |
|
29 | 22 27 28 | 3bitr4d | |
30 | 15 19 29 | 3bitrrd | |