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

Metamath Proof Explorer

Theorem logneg

Description: The natural logarithm of a negative real number. (Contributed by Mario Carneiro, 13-May-2014) (Revised by Mario Carneiro, 3-Apr-2015)

Ref Expression
Assertion logneg ( 𝐴 ∈ ℝ+ → ( log ‘ - 𝐴 ) = ( ( log ‘ 𝐴 ) + ( i · π ) ) )

Proof

Step Hyp Ref Expression
1 relogcl ⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℝ )
2 1 recnd ⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℂ )
3 ax-icn ⊢ i ∈ ℂ
4 picn ⊢ π ∈ ℂ
5 3 4 mulcli ⊢ ( i · π ) ∈ ℂ
6 efadd ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℂ ∧ ( i · π ) ∈ ℂ ) → ( exp ‘ ( ( log ‘ 𝐴 ) + ( i · π ) ) ) = ( ( exp ‘ ( log ‘ 𝐴 ) ) · ( exp ‘ ( i · π ) ) ) )
7 2 5 6 sylancl ⊢ ( 𝐴 ∈ ℝ+ → ( exp ‘ ( ( log ‘ 𝐴 ) + ( i · π ) ) ) = ( ( exp ‘ ( log ‘ 𝐴 ) ) · ( exp ‘ ( i · π ) ) ) )
8 efipi ⊢ ( exp ‘ ( i · π ) ) = - 1
9 8 oveq2i ⊢ ( ( exp ‘ ( log ‘ 𝐴 ) ) · ( exp ‘ ( i · π ) ) ) = ( ( exp ‘ ( log ‘ 𝐴 ) ) · - 1 )
10 reeflog ⊢ ( 𝐴 ∈ ℝ+ → ( exp ‘ ( log ‘ 𝐴 ) ) = 𝐴 )
11 10 oveq1d ⊢ ( 𝐴 ∈ ℝ+ → ( ( exp ‘ ( log ‘ 𝐴 ) ) · - 1 ) = ( 𝐴 · - 1 ) )
12 9 11 eqtrid ⊢ ( 𝐴 ∈ ℝ+ → ( ( exp ‘ ( log ‘ 𝐴 ) ) · ( exp ‘ ( i · π ) ) ) = ( 𝐴 · - 1 ) )
13 rpcn ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ )
14 neg1cn ⊢ - 1 ∈ ℂ
15 mulcom ⊢ ( ( 𝐴 ∈ ℂ ∧ - 1 ∈ ℂ ) → ( 𝐴 · - 1 ) = ( - 1 · 𝐴 ) )
16 13 14 15 sylancl ⊢ ( 𝐴 ∈ ℝ+ → ( 𝐴 · - 1 ) = ( - 1 · 𝐴 ) )
17 13 mulm1d ⊢ ( 𝐴 ∈ ℝ+ → ( - 1 · 𝐴 ) = - 𝐴 )
18 16 17 eqtrd ⊢ ( 𝐴 ∈ ℝ+ → ( 𝐴 · - 1 ) = - 𝐴 )
19 7 12 18 3eqtrd ⊢ ( 𝐴 ∈ ℝ+ → ( exp ‘ ( ( log ‘ 𝐴 ) + ( i · π ) ) ) = - 𝐴 )
20 19 fveq2d ⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ ( exp ‘ ( ( log ‘ 𝐴 ) + ( i · π ) ) ) ) = ( log ‘ - 𝐴 ) )
21 addcl ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℂ ∧ ( i · π ) ∈ ℂ ) → ( ( log ‘ 𝐴 ) + ( i · π ) ) ∈ ℂ )
22 2 5 21 sylancl ⊢ ( 𝐴 ∈ ℝ+ → ( ( log ‘ 𝐴 ) + ( i · π ) ) ∈ ℂ )
23 pipos ⊢ 0 < π
24 pire ⊢ π ∈ ℝ
25 lt0neg2 ⊢ ( π ∈ ℝ → ( 0 < π ↔ - π < 0 ) )
26 24 25 ax-mp ⊢ ( 0 < π ↔ - π < 0 )
27 23 26 mpbi ⊢ - π < 0
28 24 renegcli ⊢ - π ∈ ℝ
29 0re ⊢ 0 ∈ ℝ
30 28 29 24 lttri ⊢ ( ( - π < 0 ∧ 0 < π ) → - π < π )
31 27 23 30 mp2an ⊢ - π < π
32 crim ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℝ ∧ π ∈ ℝ ) → ( ℑ ‘ ( ( log ‘ 𝐴 ) + ( i · π ) ) ) = π )
33 1 24 32 sylancl ⊢ ( 𝐴 ∈ ℝ+ → ( ℑ ‘ ( ( log ‘ 𝐴 ) + ( i · π ) ) ) = π )
34 31 33 breqtrrid ⊢ ( 𝐴 ∈ ℝ+ → - π < ( ℑ ‘ ( ( log ‘ 𝐴 ) + ( i · π ) ) ) )
35 24 leidi ⊢ π ≤ π
36 33 35 eqbrtrdi ⊢ ( 𝐴 ∈ ℝ+ → ( ℑ ‘ ( ( log ‘ 𝐴 ) + ( i · π ) ) ) ≤ π )
37 ellogrn ⊢ ( ( ( log ‘ 𝐴 ) + ( i · π ) ) ∈ ran log ↔ ( ( ( log ‘ 𝐴 ) + ( i · π ) ) ∈ ℂ ∧ - π < ( ℑ ‘ ( ( log ‘ 𝐴 ) + ( i · π ) ) ) ∧ ( ℑ ‘ ( ( log ‘ 𝐴 ) + ( i · π ) ) ) ≤ π ) )
38 22 34 36 37 syl3anbrc ⊢ ( 𝐴 ∈ ℝ+ → ( ( log ‘ 𝐴 ) + ( i · π ) ) ∈ ran log )
39 logef ⊢ ( ( ( log ‘ 𝐴 ) + ( i · π ) ) ∈ ran log → ( log ‘ ( exp ‘ ( ( log ‘ 𝐴 ) + ( i · π ) ) ) ) = ( ( log ‘ 𝐴 ) + ( i · π ) ) )
40 38 39 syl ⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ ( exp ‘ ( ( log ‘ 𝐴 ) + ( i · π ) ) ) ) = ( ( log ‘ 𝐴 ) + ( i · π ) ) )
41 20 40 eqtr3d ⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ - 𝐴 ) = ( ( log ‘ 𝐴 ) + ( i · π ) ) )