Metamath Proof Explorer

Theorem logneg2

Description: The logarithm of the negative of a number with positive imaginary part is _i x. _pi less than the original. (Compare logneg .) (Contributed by Mario Carneiro, 3-Apr-2015)

Ref Expression
Assertion logneg2 ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( log ‘ - 𝐴 ) = ( ( log ‘ 𝐴 ) − ( i · π ) ) )

Proof

Step Hyp Ref Expression
1 imcl ⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) ∈ ℝ )
2 gt0ne0 ⊢ ( ( ( ℑ ‘ 𝐴 ) ∈ ℝ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ 𝐴 ) ≠ 0 )
3 1 2 sylan ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ 𝐴 ) ≠ 0 )
4 fveq2 ⊢ ( 𝐴 = 0 → ( ℑ ‘ 𝐴 ) = ( ℑ ‘ 0 ) )
5 im0 ⊢ ( ℑ ‘ 0 ) = 0
6 4 5 eqtrdi ⊢ ( 𝐴 = 0 → ( ℑ ‘ 𝐴 ) = 0 )
7 6 necon3i ⊢ ( ( ℑ ‘ 𝐴 ) ≠ 0 → 𝐴 ≠ 0 )
8 3 7 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → 𝐴 ≠ 0 )
9 logcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ℂ )
10 8 9 syldan ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( log ‘ 𝐴 ) ∈ ℂ )
11 ax-icn ⊢ i ∈ ℂ
12 picn ⊢ π ∈ ℂ
13 11 12 mulcli ⊢ ( i · π ) ∈ ℂ
14 efsub ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℂ ∧ ( i · π ) ∈ ℂ ) → ( exp ‘ ( ( log ‘ 𝐴 ) − ( i · π ) ) ) = ( ( exp ‘ ( log ‘ 𝐴 ) ) / ( exp ‘ ( i · π ) ) ) )
15 10 13 14 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( exp ‘ ( ( log ‘ 𝐴 ) − ( i · π ) ) ) = ( ( exp ‘ ( log ‘ 𝐴 ) ) / ( exp ‘ ( i · π ) ) ) )
16 eflog ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( log ‘ 𝐴 ) ) = 𝐴 )
17 8 16 syldan ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( exp ‘ ( log ‘ 𝐴 ) ) = 𝐴 )
18 efipi ⊢ ( exp ‘ ( i · π ) ) = - 1
19 18 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( exp ‘ ( i · π ) ) = - 1 )
20 17 19 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ( exp ‘ ( log ‘ 𝐴 ) ) / ( exp ‘ ( i · π ) ) ) = ( 𝐴 / - 1 ) )
21 ax-1cn ⊢ 1 ∈ ℂ
22 ax-1ne0 ⊢ 1 ≠ 0
23 divneg2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ≠ 0 ) → - ( 𝐴 / 1 ) = ( 𝐴 / - 1 ) )
24 21 22 23 mp3an23 ⊢ ( 𝐴 ∈ ℂ → - ( 𝐴 / 1 ) = ( 𝐴 / - 1 ) )
25 div1 ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 / 1 ) = 𝐴 )
26 25 negeqd ⊢ ( 𝐴 ∈ ℂ → - ( 𝐴 / 1 ) = - 𝐴 )
27 24 26 eqtr3d ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 / - 1 ) = - 𝐴 )
28 27 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( 𝐴 / - 1 ) = - 𝐴 )
29 15 20 28 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( exp ‘ ( ( log ‘ 𝐴 ) − ( i · π ) ) ) = - 𝐴 )
30 29 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( log ‘ ( exp ‘ ( ( log ‘ 𝐴 ) − ( i · π ) ) ) ) = ( log ‘ - 𝐴 ) )
31 subcl ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℂ ∧ ( i · π ) ∈ ℂ ) → ( ( log ‘ 𝐴 ) − ( i · π ) ) ∈ ℂ )
32 10 13 31 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ( log ‘ 𝐴 ) − ( i · π ) ) ∈ ℂ )
33 argimgt0 ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ( 0 (,) π ) )
34 eliooord ⊢ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ( 0 (,) π ) → ( 0 < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) < π ) )
35 33 34 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( 0 < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) < π ) )
36 35 simpld ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → 0 < ( ℑ ‘ ( log ‘ 𝐴 ) ) )
37 imcl ⊢ ( ( log ‘ 𝐴 ) ∈ ℂ → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ )
38 10 37 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ )
39 pire ⊢ π ∈ ℝ
40 39 renegcli ⊢ - π ∈ ℝ
41 ltaddpos2 ⊢ ( ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ∧ - π ∈ ℝ ) → ( 0 < ( ℑ ‘ ( log ‘ 𝐴 ) ) ↔ - π < ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + - π ) ) )
42 38 40 41 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( 0 < ( ℑ ‘ ( log ‘ 𝐴 ) ) ↔ - π < ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + - π ) ) )
43 36 42 mpbid ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → - π < ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + - π ) )
44 38 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ )
45 negsub ⊢ ( ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ ∧ π ∈ ℂ ) → ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + - π ) = ( ( ℑ ‘ ( log ‘ 𝐴 ) ) − π ) )
46 44 12 45 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + - π ) = ( ( ℑ ‘ ( log ‘ 𝐴 ) ) − π ) )
47 43 46 breqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → - π < ( ( ℑ ‘ ( log ‘ 𝐴 ) ) − π ) )
48 imsub ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℂ ∧ ( i · π ) ∈ ℂ ) → ( ℑ ‘ ( ( log ‘ 𝐴 ) − ( i · π ) ) ) = ( ( ℑ ‘ ( log ‘ 𝐴 ) ) − ( ℑ ‘ ( i · π ) ) ) )
49 10 13 48 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ ( ( log ‘ 𝐴 ) − ( i · π ) ) ) = ( ( ℑ ‘ ( log ‘ 𝐴 ) ) − ( ℑ ‘ ( i · π ) ) ) )
50 reim ⊢ ( π ∈ ℂ → ( ℜ ‘ π ) = ( ℑ ‘ ( i · π ) ) )
51 12 50 ax-mp ⊢ ( ℜ ‘ π ) = ( ℑ ‘ ( i · π ) )
52 rere ⊢ ( π ∈ ℝ → ( ℜ ‘ π ) = π )
53 39 52 ax-mp ⊢ ( ℜ ‘ π ) = π
54 51 53 eqtr3i ⊢ ( ℑ ‘ ( i · π ) ) = π
55 54 oveq2i ⊢ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) − ( ℑ ‘ ( i · π ) ) ) = ( ( ℑ ‘ ( log ‘ 𝐴 ) ) − π )
56 49 55 eqtrdi ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ ( ( log ‘ 𝐴 ) − ( i · π ) ) ) = ( ( ℑ ‘ ( log ‘ 𝐴 ) ) − π ) )
57 47 56 breqtrrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → - π < ( ℑ ‘ ( ( log ‘ 𝐴 ) − ( i · π ) ) ) )
58 resubcl ⊢ ( ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ∧ π ∈ ℝ ) → ( ( ℑ ‘ ( log ‘ 𝐴 ) ) − π ) ∈ ℝ )
59 38 39 58 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ( ℑ ‘ ( log ‘ 𝐴 ) ) − π ) ∈ ℝ )
60 39 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → π ∈ ℝ )
61 0re ⊢ 0 ∈ ℝ
62 pipos ⊢ 0 < π
63 61 39 62 ltleii ⊢ 0 ≤ π
64 subge02 ⊢ ( ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ∧ π ∈ ℝ ) → ( 0 ≤ π ↔ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) − π ) ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
65 38 39 64 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( 0 ≤ π ↔ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) − π ) ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
66 63 65 mpbii ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ( ℑ ‘ ( log ‘ 𝐴 ) ) − π ) ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) )
67 logimcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) )
68 8 67 syldan ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) )
69 68 simprd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π )
70 59 38 60 66 69 letrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ( ℑ ‘ ( log ‘ 𝐴 ) ) − π ) ≤ π )
71 56 70 eqbrtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ ( ( log ‘ 𝐴 ) − ( i · π ) ) ) ≤ π )
72 ellogrn ⊢ ( ( ( log ‘ 𝐴 ) − ( i · π ) ) ∈ ran log ↔ ( ( ( log ‘ 𝐴 ) − ( i · π ) ) ∈ ℂ ∧ - π < ( ℑ ‘ ( ( log ‘ 𝐴 ) − ( i · π ) ) ) ∧ ( ℑ ‘ ( ( log ‘ 𝐴 ) − ( i · π ) ) ) ≤ π ) )
73 32 57 71 72 syl3anbrc ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ( log ‘ 𝐴 ) − ( i · π ) ) ∈ ran log )
74 logef ⊢ ( ( ( log ‘ 𝐴 ) − ( i · π ) ) ∈ ran log → ( log ‘ ( exp ‘ ( ( log ‘ 𝐴 ) − ( i · π ) ) ) ) = ( ( log ‘ 𝐴 ) − ( i · π ) ) )
75 73 74 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( log ‘ ( exp ‘ ( ( log ‘ 𝐴 ) − ( i · π ) ) ) ) = ( ( log ‘ 𝐴 ) − ( i · π ) ) )
76 30 75 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( log ‘ - 𝐴 ) = ( ( log ‘ 𝐴 ) − ( i · π ) ) )