Description: The real part of a complex number is real. (Contributed by NM, 9-May-1999) (Revised by Mario Carneiro, 6-Nov-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | recl | โข ( ๐ด โ โ โ ( โ โ ๐ด ) โ โ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reval | โข ( ๐ด โ โ โ ( โ โ ๐ด ) = ( ( ๐ด + ( โ โ ๐ด ) ) / 2 ) ) | |
2 | cjth | โข ( ๐ด โ โ โ ( ( ๐ด + ( โ โ ๐ด ) ) โ โ โง ( i ยท ( ๐ด โ ( โ โ ๐ด ) ) ) โ โ ) ) | |
3 | 2 | simpld | โข ( ๐ด โ โ โ ( ๐ด + ( โ โ ๐ด ) ) โ โ ) |
4 | 3 | rehalfcld | โข ( ๐ด โ โ โ ( ( ๐ด + ( โ โ ๐ด ) ) / 2 ) โ โ ) |
5 | 1 4 | eqeltrd | โข ( ๐ด โ โ โ ( โ โ ๐ด ) โ โ ) |