Metamath Proof Explorer


Theorem recl

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 ( ๐ด โˆˆ โ„‚ โ†’ ( โ„œ โ€˜ ๐ด ) โˆˆ โ„ )

Proof

Step Hyp Ref Expression
1 reval โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( โ„œ โ€˜ ๐ด ) = ( ( ๐ด + ( โˆ— โ€˜ ๐ด ) ) / 2 ) )
2 cjth โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( ( ๐ด + ( โˆ— โ€˜ ๐ด ) ) โˆˆ โ„ โˆง ( i ยท ( ๐ด โˆ’ ( โˆ— โ€˜ ๐ด ) ) ) โˆˆ โ„ ) )
3 2 simpld โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( ๐ด + ( โˆ— โ€˜ ๐ด ) ) โˆˆ โ„ )
4 3 rehalfcld โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( ( ๐ด + ( โˆ— โ€˜ ๐ด ) ) / 2 ) โˆˆ โ„ )
5 1 4 eqeltrd โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( โ„œ โ€˜ ๐ด ) โˆˆ โ„ )