This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ≠ 0 ) → ( log ‘ ( ∗ ‘ 𝐴 ) ) = ( ∗ ‘ ( log ‘ 𝐴 ) ) )

Proof

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