Metamath Proof Explorer


Theorem logcj

Description: The natural logarithm distributes under conjugation away from the branch cut. (Contributed by Mario Carneiro, 25-Feb-2015)

Ref Expression
Assertion logcj A A 0 log A = log A

Proof

Step Hyp Ref Expression
1 fveq2 A = 0 A = 0
2 im0 0 = 0
3 1 2 syl6eq A = 0 A = 0
4 3 necon3i A 0 A 0
5 logcl A A 0 log A
6 4 5 sylan2 A A 0 log A
7 efcj log A e log A = e log A
8 6 7 syl A A 0 e log A = e log A
9 eflog A A 0 e log A = A
10 4 9 sylan2 A A 0 e log A = A
11 10 fveq2d A A 0 e log A = A
12 8 11 eqtrd A A 0 e log A = A
13 cjcl A A
14 13 adantr A A 0 A
15 simpr A A 0 A 0
16 15 4 syl A A 0 A 0
17 cjne0 A A 0 A 0
18 17 adantr A A 0 A 0 A 0
19 16 18 mpbid A A 0 A 0
20 6 cjcld A A 0 log A
21 6 imcld A A 0 log A
22 pire π
23 22 a1i A A 0 π
24 logimcl A A 0 π < log A log A π
25 4 24 sylan2 A A 0 π < log A log A π
26 25 simprd A A 0 log A π
27 rpre A + A
28 27 renegcld A + A
29 negneg A A = A
30 29 adantr A A 0 A = A
31 30 eleq1d A A 0 A A
32 28 31 syl5ib A A 0 A + A
33 lognegb A A 0 A + log A = π
34 4 33 sylan2 A A 0 A + log A = π
35 reim0b A A A = 0
36 35 adantr A A 0 A A = 0
37 32 34 36 3imtr3d A A 0 log A = π A = 0
38 37 necon3d A A 0 A 0 log A π
39 15 38 mpd A A 0 log A π
40 39 necomd A A 0 π log A
41 21 23 26 40 leneltd A A 0 log A < π
42 ltneg log A π log A < π π < log A
43 21 22 42 sylancl A A 0 log A < π π < log A
44 41 43 mpbid A A 0 π < log A
45 6 imcjd A A 0 log A = log A
46 44 45 breqtrrd A A 0 π < log A
47 25 simpld A A 0 π < log A
48 22 renegcli π
49 ltle π log A π < log A π log A
50 48 21 49 sylancr A A 0 π < log A π log A
51 47 50 mpd A A 0 π log A
52 lenegcon1 π log A π log A log A π
53 22 21 52 sylancr A A 0 π log A log A π
54 51 53 mpbid A A 0 log A π
55 45 54 eqbrtrd A A 0 log A π
56 ellogrn log A ran log log A π < log A log A π
57 20 46 55 56 syl3anbrc A A 0 log A ran log
58 logeftb A A 0 log A ran log log A = log A e log A = A
59 14 19 57 58 syl3anc A A 0 log A = log A e log A = A
60 12 59 mpbird A A 0 log A = log A