Theorem 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 ‘ 𝑋 ) ) ≤ π ) )