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 A 0 < A log A = log A i π

Proof

Step Hyp Ref Expression
1 imcl A A
2 gt0ne0 A 0 < A A 0
3 1 2 sylan A 0 < A A 0
4 fveq2 A = 0 A = 0
5 im0 0 = 0
6 4 5 syl6eq A = 0 A = 0
7 6 necon3i A 0 A 0
8 3 7 syl A 0 < A A 0
9 logcl A A 0 log A
10 8 9 syldan A 0 < A log A
11 ax-icn i
12 picn π
13 11 12 mulcli i π
14 efsub log A i π e log A i π = e log A e i π
15 10 13 14 sylancl A 0 < A e log A i π = e log A e i π
16 eflog A A 0 e log A = A
17 8 16 syldan A 0 < A e log A = A
18 efipi e i π = 1
19 18 a1i A 0 < A e i π = 1
20 17 19 oveq12d A 0 < A e log A e i π = A 1
21 ax-1cn 1
22 ax-1ne0 1 0
23 divneg2 A 1 1 0 A 1 = A 1
24 21 22 23 mp3an23 A A 1 = A 1
25 div1 A A 1 = A
26 25 negeqd A A 1 = A
27 24 26 eqtr3d A A 1 = A
28 27 adantr A 0 < A A 1 = A
29 15 20 28 3eqtrd A 0 < A e log A i π = A
30 29 fveq2d A 0 < A log e log A i π = log A
31 subcl log A i π log A i π
32 10 13 31 sylancl A 0 < A log A i π
33 argimgt0 A 0 < A log A 0 π
34 eliooord log A 0 π 0 < log A log A < π
35 33 34 syl A 0 < A 0 < log A log A < π
36 35 simpld A 0 < A 0 < log A
37 imcl log A log A
38 10 37 syl A 0 < A log A
39 pire π
40 39 renegcli π
41 ltaddpos2 log A π 0 < log A π < log A + π
42 38 40 41 sylancl A 0 < A 0 < log A π < log A + π
43 36 42 mpbid A 0 < A π < log A + π
44 38 recnd A 0 < A log A
45 negsub log A π log A + π = log A π
46 44 12 45 sylancl A 0 < A log A + π = log A π
47 43 46 breqtrd A 0 < A π < log A π
48 imsub log A i π log A i π = log A i π
49 10 13 48 sylancl A 0 < A log A i π = log A 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 A i π = log A π
56 49 55 syl6eq A 0 < A log A i π = log A π
57 47 56 breqtrrd A 0 < A π < log A i π
58 resubcl log A π log A π
59 38 39 58 sylancl A 0 < A log A π
60 39 a1i A 0 < A π
61 0re 0
62 pipos 0 < π
63 61 39 62 ltleii 0 π
64 subge02 log A π 0 π log A π log A
65 38 39 64 sylancl A 0 < A 0 π log A π log A
66 63 65 mpbii A 0 < A log A π log A
67 logimcl A A 0 π < log A log A π
68 8 67 syldan A 0 < A π < log A log A π
69 68 simprd A 0 < A log A π
70 59 38 60 66 69 letrd A 0 < A log A π π
71 56 70 eqbrtrd A 0 < A log A i π π
72 ellogrn log A i π ran log log A i π π < log A i π log A i π π
73 32 57 71 72 syl3anbrc A 0 < A log A i π ran log
74 logef log A i π ran log log e log A i π = log A i π
75 73 74 syl A 0 < A log e log A i π = log A i π
76 30 75 eqtr3d A 0 < A log A = log A i π