Theorem lognegb

Description: If a number has imaginary part equal to _pi , then it is on the negative real axis and vice-versa. (Contributed by Mario Carneiro, 23-Sep-2014)

	Ref	Expression
Assertion	lognegb	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( - 𝐴 ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ 𝐴 ) ) = π ) )

Proof

Step	Hyp	Ref	Expression
1		logneg	⊢ ( - 𝐴 ∈ ℝ+ → ( log ‘ - - 𝐴 ) = ( ( log ‘ - 𝐴 ) + ( i · π ) ) )
2	1	fveq2d	⊢ ( - 𝐴 ∈ ℝ+ → ( ℑ ‘ ( log ‘ - - 𝐴 ) ) = ( ℑ ‘ ( ( log ‘ - 𝐴 ) + ( i · π ) ) ) )
3		relogcl	⊢ ( - 𝐴 ∈ ℝ+ → ( log ‘ - 𝐴 ) ∈ ℝ )
4		pire	⊢ π ∈ ℝ
5		crim	⊢ ( ( ( log ‘ - 𝐴 ) ∈ ℝ ∧ π ∈ ℝ ) → ( ℑ ‘ ( ( log ‘ - 𝐴 ) + ( i · π ) ) ) = π )
6	3 4 5	sylancl	⊢ ( - 𝐴 ∈ ℝ+ → ( ℑ ‘ ( ( log ‘ - 𝐴 ) + ( i · π ) ) ) = π )
7	2 6	eqtrd	⊢ ( - 𝐴 ∈ ℝ+ → ( ℑ ‘ ( log ‘ - - 𝐴 ) ) = π )
8		negneg	⊢ ( 𝐴 ∈ ℂ → - - 𝐴 = 𝐴 )
9	8	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → - - 𝐴 = 𝐴 )
10	9	fveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ - - 𝐴 ) = ( log ‘ 𝐴 ) )
11	10	fveqeq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( ℑ ‘ ( log ‘ - - 𝐴 ) ) = π ↔ ( ℑ ‘ ( log ‘ 𝐴 ) ) = π ) )
12	7 11	imbitrid	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( - 𝐴 ∈ ℝ+ → ( ℑ ‘ ( log ‘ 𝐴 ) ) = π ) )
13		logcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ℂ )
14	13	replimd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) = ( ( ℜ ‘ ( log ‘ 𝐴 ) ) + ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) )
15	14	fveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( log ‘ 𝐴 ) ) = ( exp ‘ ( ( ℜ ‘ ( log ‘ 𝐴 ) ) + ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) )
16		eflog	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( log ‘ 𝐴 ) ) = 𝐴 )
17	13	recld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℜ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ )
18	17	recnd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℜ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ )
19		ax-icn	⊢ i ∈ ℂ
20	13	imcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ )
21	20	recnd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ )
22		mulcl	⊢ ( ( i ∈ ℂ ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ ) → ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℂ )
23	19 21 22	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℂ )
24		efadd	⊢ ( ( ( ℜ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ ∧ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℂ ) → ( exp ‘ ( ( ℜ ‘ ( log ‘ 𝐴 ) ) + ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) = ( ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) · ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) )
25	18 23 24	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( ( ℜ ‘ ( log ‘ 𝐴 ) ) + ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) = ( ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) · ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) )
26	15 16 25	3eqtr3d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 𝐴 = ( ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) · ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) )
27		oveq2	⊢ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) = π → ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( i · π ) )
28	27	fveq2d	⊢ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) = π → ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( exp ‘ ( i · π ) ) )
29		efipi	⊢ ( exp ‘ ( i · π ) ) = - 1
30	28 29	eqtrdi	⊢ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) = π → ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = - 1 )
31	30	oveq2d	⊢ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) = π → ( ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) · ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) = ( ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) · - 1 ) )
32	31	eqeq2d	⊢ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) = π → ( 𝐴 = ( ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) · ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) ↔ 𝐴 = ( ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) · - 1 ) ) )
33	26 32	syl5ibcom	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( ℑ ‘ ( log ‘ 𝐴 ) ) = π → 𝐴 = ( ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) · - 1 ) ) )
34	17	rpefcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℝ+ )
35	34	rpcnd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℂ )
36		neg1cn	⊢ - 1 ∈ ℂ
37		mulcom	⊢ ( ( ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℂ ∧ - 1 ∈ ℂ ) → ( ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) · - 1 ) = ( - 1 · ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) ) )
38	35 36 37	sylancl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) · - 1 ) = ( - 1 · ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) ) )
39	35	mulm1d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( - 1 · ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) ) = - ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) )
40	38 39	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) · - 1 ) = - ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) )
41	40	negeqd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → - ( ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) · - 1 ) = - - ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) )
42	35	negnegd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → - - ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) = ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) )
43	41 42	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → - ( ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) · - 1 ) = ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) )
44	43 34	eqeltrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → - ( ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) · - 1 ) ∈ ℝ+ )
45		negeq	⊢ ( 𝐴 = ( ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) · - 1 ) → - 𝐴 = - ( ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) · - 1 ) )
46	45	eleq1d	⊢ ( 𝐴 = ( ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) · - 1 ) → ( - 𝐴 ∈ ℝ+ ↔ - ( ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) · - 1 ) ∈ ℝ+ ) )
47	44 46	syl5ibrcom	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝐴 = ( ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) · - 1 ) → - 𝐴 ∈ ℝ+ ) )
48	33 47	syld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( ℑ ‘ ( log ‘ 𝐴 ) ) = π → - 𝐴 ∈ ℝ+ ) )
49	12 48	impbid	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( - 𝐴 ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ 𝐴 ) ) = π ) )