Metamath Proof Explorer


Theorem reim0

Description: The imaginary part of a real number is 0. (Contributed by NM, 18-Mar-2005) (Revised by Mario Carneiro, 7-Nov-2013)

Ref Expression
Assertion reim0 ( ๐ด โˆˆ โ„ โ†’ ( โ„‘ โ€˜ ๐ด ) = 0 )

Proof

Step Hyp Ref Expression
1 recn โŠข ( ๐ด โˆˆ โ„ โ†’ ๐ด โˆˆ โ„‚ )
2 it0e0 โŠข ( i ยท 0 ) = 0
3 2 oveq2i โŠข ( ๐ด + ( i ยท 0 ) ) = ( ๐ด + 0 )
4 addrid โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( ๐ด + 0 ) = ๐ด )
5 3 4 eqtrid โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( ๐ด + ( i ยท 0 ) ) = ๐ด )
6 1 5 syl โŠข ( ๐ด โˆˆ โ„ โ†’ ( ๐ด + ( i ยท 0 ) ) = ๐ด )
7 6 fveq2d โŠข ( ๐ด โˆˆ โ„ โ†’ ( โ„‘ โ€˜ ( ๐ด + ( i ยท 0 ) ) ) = ( โ„‘ โ€˜ ๐ด ) )
8 0re โŠข 0 โˆˆ โ„
9 crim โŠข ( ( ๐ด โˆˆ โ„ โˆง 0 โˆˆ โ„ ) โ†’ ( โ„‘ โ€˜ ( ๐ด + ( i ยท 0 ) ) ) = 0 )
10 8 9 mpan2 โŠข ( ๐ด โˆˆ โ„ โ†’ ( โ„‘ โ€˜ ( ๐ด + ( i ยท 0 ) ) ) = 0 )
11 7 10 eqtr3d โŠข ( ๐ด โˆˆ โ„ โ†’ ( โ„‘ โ€˜ ๐ด ) = 0 )