This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC REAL AND COMPLEX FUNCTIONS Basic trigonometry The natural logarithm on complex numbers logimcld
Description: The imaginary part of the logarithm is in ( -upi (,] pi ) .
Deduction form of logimcl . Compare logimclad . (Contributed by David Moews , 28-Feb-2017)
Ref
Expression
Hypotheses
logimcld.1 ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
logimcld.2 ⊢ ( 𝜑 → 𝑋 ≠ 0 )
Assertion
logimcld ⊢ ( 𝜑 → ( - π < ( ℑ ‘ ( log ‘ 𝑋 ) ) ∧ ( ℑ ‘ ( log ‘ 𝑋 ) ) ≤ π ) )
Proof
Step
Hyp
Ref
Expression
1
logimcld.1 ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
2
logimcld.2 ⊢ ( 𝜑 → 𝑋 ≠ 0 )
3
logimcl ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑋 ≠ 0 ) → ( - π < ( ℑ ‘ ( log ‘ 𝑋 ) ) ∧ ( ℑ ‘ ( log ‘ 𝑋 ) ) ≤ π ) )
4
1 2 3
syl2anc ⊢ ( 𝜑 → ( - π < ( ℑ ‘ ( log ‘ 𝑋 ) ) ∧ ( ℑ ‘ ( log ‘ 𝑋 ) ) ≤ π ) )