Database
REAL AND COMPLEX NUMBERS
Elementary real and complex functions
Real and imaginary parts; conjugate
im1
Next ⟩
rei
Metamath Proof Explorer
Ascii
Structured
Theorem
im1
Description:
The imaginary part of one.
(Contributed by
Scott Fenton
, 9-Jun-2006)
Ref
Expression
Assertion
im1
⊢
( ℑ ‘ 1 ) = 0
Proof
Step
Hyp
Ref
Expression
1
1re
⊢
1 ∈ ℝ
2
reim0
⊢
( 1 ∈ ℝ → ( ℑ ‘ 1 ) = 0 )
3
1
2
ax-mp
⊢
( ℑ ‘ 1 ) = 0