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 A0<AlogA=logAiπ

Proof

Step Hyp Ref Expression
1 imcl AA
2 gt0ne0 A0<AA0
3 1 2 sylan A0<AA0
4 fveq2 A=0A=0
5 im0 0=0
6 4 5 eqtrdi A=0A=0
7 6 necon3i A0A0
8 3 7 syl A0<AA0
9 logcl AA0logA
10 8 9 syldan A0<AlogA
11 ax-icn i
12 picn π
13 11 12 mulcli iπ
14 efsub logAiπelogAiπ=elogAeiπ
15 10 13 14 sylancl A0<AelogAiπ=elogAeiπ
16 eflog AA0elogA=A
17 8 16 syldan A0<AelogA=A
18 efipi eiπ=1
19 18 a1i A0<Aeiπ=1
20 17 19 oveq12d A0<AelogAeiπ=A1
21 ax-1cn 1
22 ax-1ne0 10
23 divneg2 A110A1=A1
24 21 22 23 mp3an23 AA1=A1
25 div1 AA1=A
26 25 negeqd AA1=A
27 24 26 eqtr3d AA1=A
28 27 adantr A0<AA1=A
29 15 20 28 3eqtrd A0<AelogAiπ=A
30 29 fveq2d A0<AlogelogAiπ=logA
31 subcl logAiπlogAiπ
32 10 13 31 sylancl A0<AlogAiπ
33 argimgt0 A0<AlogA0π
34 eliooord logA0π0<logAlogA<π
35 33 34 syl A0<A0<logAlogA<π
36 35 simpld A0<A0<logA
37 imcl logAlogA
38 10 37 syl A0<AlogA
39 pire π
40 39 renegcli π
41 ltaddpos2 logAπ0<logAπ<logA+π
42 38 40 41 sylancl A0<A0<logAπ<logA+π
43 36 42 mpbid A0<Aπ<logA+π
44 38 recnd A0<AlogA
45 negsub logAπlogA+π=logAπ
46 44 12 45 sylancl A0<AlogA+π=logAπ
47 43 46 breqtrd A0<Aπ<logAπ
48 imsub logAiπlogAiπ=logAiπ
49 10 13 48 sylancl A0<AlogAiπ=logAiπ
50 reim ππ=iπ
51 12 50 ax-mp π=iπ
52 rere ππ=π
53 39 52 ax-mp π=π
54 51 53 eqtr3i iπ=π
55 54 oveq2i logAiπ=logAπ
56 49 55 eqtrdi A0<AlogAiπ=logAπ
57 47 56 breqtrrd A0<Aπ<logAiπ
58 resubcl logAπlogAπ
59 38 39 58 sylancl A0<AlogAπ
60 39 a1i A0<Aπ
61 0re 0
62 pipos 0<π
63 61 39 62 ltleii 0π
64 subge02 logAπ0πlogAπlogA
65 38 39 64 sylancl A0<A0πlogAπlogA
66 63 65 mpbii A0<AlogAπlogA
67 logimcl AA0π<logAlogAπ
68 8 67 syldan A0<Aπ<logAlogAπ
69 68 simprd A0<AlogAπ
70 59 38 60 66 69 letrd A0<AlogAππ
71 56 70 eqbrtrd A0<AlogAiππ
72 ellogrn logAiπranloglogAiππ<logAiπlogAiππ
73 32 57 71 72 syl3anbrc A0<AlogAiπranlog
74 logef logAiπranloglogelogAiπ=logAiπ
75 73 74 syl A0<AlogelogAiπ=logAiπ
76 30 75 eqtr3d A0<AlogA=logAiπ