Theorem logimclad

Description: The imaginary part of the logarithm is in ( -upi (,] pi ) . Alternate form of logimcld . (Contributed by David Moews, 28-Feb-2017)

	Ref	Expression
Hypotheses	logimcld.1	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
	logimcld.2	⊢ ( 𝜑 → 𝑋 ≠ 0 )
Assertion	logimclad	⊢ ( 𝜑 → ( ℑ ‘ ( log ‘ 𝑋 ) ) ∈ ( - π (,] π ) )

Proof

Step	Hyp	Ref	Expression
1		logimcld.1	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
2		logimcld.2	⊢ ( 𝜑 → 𝑋 ≠ 0 )
3	1 2	logcld	⊢ ( 𝜑 → ( log ‘ 𝑋 ) ∈ ℂ )
4	3	imcld	⊢ ( 𝜑 → ( ℑ ‘ ( log ‘ 𝑋 ) ) ∈ ℝ )
5	1 2	logimcld	⊢ ( 𝜑 → ( - π < ( ℑ ‘ ( log ‘ 𝑋 ) ) ∧ ( ℑ ‘ ( log ‘ 𝑋 ) ) ≤ π ) )
6	5	simpld	⊢ ( 𝜑 → - π < ( ℑ ‘ ( log ‘ 𝑋 ) ) )
7	5	simprd	⊢ ( 𝜑 → ( ℑ ‘ ( log ‘ 𝑋 ) ) ≤ π )
8		pire	⊢ π ∈ ℝ
9	8	renegcli	⊢ - π ∈ ℝ
10	9	rexri	⊢ - π ∈ ℝ*
11		elioc2	⊢ ( ( - π ∈ ℝ* ∧ π ∈ ℝ ) → ( ( ℑ ‘ ( log ‘ 𝑋 ) ) ∈ ( - π (,] π ) ↔ ( ( ℑ ‘ ( log ‘ 𝑋 ) ) ∈ ℝ ∧ - π < ( ℑ ‘ ( log ‘ 𝑋 ) ) ∧ ( ℑ ‘ ( log ‘ 𝑋 ) ) ≤ π ) ) )
12	10 8 11	mp2an	⊢ ( ( ℑ ‘ ( log ‘ 𝑋 ) ) ∈ ( - π (,] π ) ↔ ( ( ℑ ‘ ( log ‘ 𝑋 ) ) ∈ ℝ ∧ - π < ( ℑ ‘ ( log ‘ 𝑋 ) ) ∧ ( ℑ ‘ ( log ‘ 𝑋 ) ) ≤ π ) )
13	4 6 7 12	syl3anbrc	⊢ ( 𝜑 → ( ℑ ‘ ( log ‘ 𝑋 ) ) ∈ ( - π (,] π ) )