Metamath Proof Explorer

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 ‘ 𝐴 ) ) = π ) )