Metamath Proof Explorer

Theorem logimul

Description: Multiplying a number by _i increases the logarithm of the number by _i _pi / 2 . (Contributed by Mario Carneiro, 4-Apr-2015)

Ref Expression
Assertion logimul ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( log ‘ ( i · 𝐴 ) ) = ( ( log ‘ 𝐴 ) + ( i · ( π / 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 logcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ℂ )
2 1 3adant3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( log ‘ 𝐴 ) ∈ ℂ )
3 ax-icn ⊢ i ∈ ℂ
4 halfpire ⊢ ( π / 2 ) ∈ ℝ
5 4 recni ⊢ ( π / 2 ) ∈ ℂ
6 3 5 mulcli ⊢ ( i · ( π / 2 ) ) ∈ ℂ
7 efadd ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℂ ∧ ( i · ( π / 2 ) ) ∈ ℂ ) → ( exp ‘ ( ( log ‘ 𝐴 ) + ( i · ( π / 2 ) ) ) ) = ( ( exp ‘ ( log ‘ 𝐴 ) ) · ( exp ‘ ( i · ( π / 2 ) ) ) ) )
8 2 6 7 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( exp ‘ ( ( log ‘ 𝐴 ) + ( i · ( π / 2 ) ) ) ) = ( ( exp ‘ ( log ‘ 𝐴 ) ) · ( exp ‘ ( i · ( π / 2 ) ) ) ) )
9 eflog ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( log ‘ 𝐴 ) ) = 𝐴 )
10 9 3adant3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( exp ‘ ( log ‘ 𝐴 ) ) = 𝐴 )
11 efhalfpi ⊢ ( exp ‘ ( i · ( π / 2 ) ) ) = i
12 11 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( exp ‘ ( i · ( π / 2 ) ) ) = i )
13 10 12 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( exp ‘ ( log ‘ 𝐴 ) ) · ( exp ‘ ( i · ( π / 2 ) ) ) ) = ( 𝐴 · i ) )
14 simp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → 𝐴 ∈ ℂ )
15 mulcom ⊢ ( ( 𝐴 ∈ ℂ ∧ i ∈ ℂ ) → ( 𝐴 · i ) = ( i · 𝐴 ) )
16 14 3 15 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( 𝐴 · i ) = ( i · 𝐴 ) )
17 8 13 16 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( exp ‘ ( ( log ‘ 𝐴 ) + ( i · ( π / 2 ) ) ) ) = ( i · 𝐴 ) )
18 17 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( log ‘ ( exp ‘ ( ( log ‘ 𝐴 ) + ( i · ( π / 2 ) ) ) ) ) = ( log ‘ ( i · 𝐴 ) ) )
19 addcl ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℂ ∧ ( i · ( π / 2 ) ) ∈ ℂ ) → ( ( log ‘ 𝐴 ) + ( i · ( π / 2 ) ) ) ∈ ℂ )
20 2 6 19 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( log ‘ 𝐴 ) + ( i · ( π / 2 ) ) ) ∈ ℂ )
21 pire ⊢ π ∈ ℝ
22 21 renegcli ⊢ - π ∈ ℝ
23 22 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → - π ∈ ℝ )
24 2 imcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ )
25 readdcl ⊢ ( ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ∧ ( π / 2 ) ∈ ℝ ) → ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + ( π / 2 ) ) ∈ ℝ )
26 24 4 25 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + ( π / 2 ) ) ∈ ℝ )
27 logimcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) )
28 27 3adant3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) )
29 28 simpld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) )
30 pirp ⊢ π ∈ ℝ+
31 rphalfcl ⊢ ( π ∈ ℝ+ → ( π / 2 ) ∈ ℝ+ )
32 30 31 ax-mp ⊢ ( π / 2 ) ∈ ℝ+
33 ltaddrp ⊢ ( ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ∧ ( π / 2 ) ∈ ℝ+ ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) < ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + ( π / 2 ) ) )
34 24 32 33 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) < ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + ( π / 2 ) ) )
35 23 24 26 29 34 lttrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → - π < ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + ( π / 2 ) ) )
36 imadd ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℂ ∧ ( i · ( π / 2 ) ) ∈ ℂ ) → ( ℑ ‘ ( ( log ‘ 𝐴 ) + ( i · ( π / 2 ) ) ) ) = ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + ( ℑ ‘ ( i · ( π / 2 ) ) ) ) )
37 2 6 36 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( ( log ‘ 𝐴 ) + ( i · ( π / 2 ) ) ) ) = ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + ( ℑ ‘ ( i · ( π / 2 ) ) ) ) )
38 reim ⊢ ( ( π / 2 ) ∈ ℂ → ( ℜ ‘ ( π / 2 ) ) = ( ℑ ‘ ( i · ( π / 2 ) ) ) )
39 5 38 ax-mp ⊢ ( ℜ ‘ ( π / 2 ) ) = ( ℑ ‘ ( i · ( π / 2 ) ) )
40 rere ⊢ ( ( π / 2 ) ∈ ℝ → ( ℜ ‘ ( π / 2 ) ) = ( π / 2 ) )
41 4 40 ax-mp ⊢ ( ℜ ‘ ( π / 2 ) ) = ( π / 2 )
42 39 41 eqtr3i ⊢ ( ℑ ‘ ( i · ( π / 2 ) ) ) = ( π / 2 )
43 42 oveq2i ⊢ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + ( ℑ ‘ ( i · ( π / 2 ) ) ) ) = ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + ( π / 2 ) )
44 37 43 eqtrdi ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( ( log ‘ 𝐴 ) + ( i · ( π / 2 ) ) ) ) = ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + ( π / 2 ) ) )
45 35 44 breqtrrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → - π < ( ℑ ‘ ( ( log ‘ 𝐴 ) + ( i · ( π / 2 ) ) ) ) )
46 argrege0 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) )
47 4 renegcli ⊢ - ( π / 2 ) ∈ ℝ
48 47 4 elicc2i ⊢ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) ↔ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ∧ - ( π / 2 ) ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ ( π / 2 ) ) )
49 48 simp3bi ⊢ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ ( π / 2 ) )
50 46 49 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ ( π / 2 ) )
51 21 recni ⊢ π ∈ ℂ
52 pidiv2halves ⊢ ( ( π / 2 ) + ( π / 2 ) ) = π
53 51 5 5 52 subaddrii ⊢ ( π − ( π / 2 ) ) = ( π / 2 )
54 50 53 breqtrrdi ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ ( π − ( π / 2 ) ) )
55 4 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( π / 2 ) ∈ ℝ )
56 21 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → π ∈ ℝ )
57 leaddsub ⊢ ( ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ∧ ( π / 2 ) ∈ ℝ ∧ π ∈ ℝ ) → ( ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + ( π / 2 ) ) ≤ π ↔ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ ( π − ( π / 2 ) ) ) )
58 24 55 56 57 syl3anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + ( π / 2 ) ) ≤ π ↔ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ ( π − ( π / 2 ) ) ) )
59 54 58 mpbird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + ( π / 2 ) ) ≤ π )
60 44 59 eqbrtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( ( log ‘ 𝐴 ) + ( i · ( π / 2 ) ) ) ) ≤ π )
61 ellogrn ⊢ ( ( ( log ‘ 𝐴 ) + ( i · ( π / 2 ) ) ) ∈ ran log ↔ ( ( ( log ‘ 𝐴 ) + ( i · ( π / 2 ) ) ) ∈ ℂ ∧ - π < ( ℑ ‘ ( ( log ‘ 𝐴 ) + ( i · ( π / 2 ) ) ) ) ∧ ( ℑ ‘ ( ( log ‘ 𝐴 ) + ( i · ( π / 2 ) ) ) ) ≤ π ) )
62 20 45 60 61 syl3anbrc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( log ‘ 𝐴 ) + ( i · ( π / 2 ) ) ) ∈ ran log )
63 logef ⊢ ( ( ( log ‘ 𝐴 ) + ( i · ( π / 2 ) ) ) ∈ ran log → ( log ‘ ( exp ‘ ( ( log ‘ 𝐴 ) + ( i · ( π / 2 ) ) ) ) ) = ( ( log ‘ 𝐴 ) + ( i · ( π / 2 ) ) ) )
64 62 63 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( log ‘ ( exp ‘ ( ( log ‘ 𝐴 ) + ( i · ( π / 2 ) ) ) ) ) = ( ( log ‘ 𝐴 ) + ( i · ( π / 2 ) ) ) )
65 18 64 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( log ‘ ( i · 𝐴 ) ) = ( ( log ‘ 𝐴 ) + ( i · ( π / 2 ) ) ) )