Metamath Proof Explorer


Theorem logrec

Description: Logarithm of a reciprocal changes sign. (Contributed by Saveliy Skresanov, 28-Dec-2016)

Ref Expression
Assertion logrec ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≠ π ) → ( log ‘ 𝐴 ) = - ( log ‘ ( 1 / 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 reccl ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 1 / 𝐴 ) ∈ ℂ )
2 recne0 ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 1 / 𝐴 ) ≠ 0 )
3 eflog ( ( ( 1 / 𝐴 ) ∈ ℂ ∧ ( 1 / 𝐴 ) ≠ 0 ) → ( exp ‘ ( log ‘ ( 1 / 𝐴 ) ) ) = ( 1 / 𝐴 ) )
4 1 2 3 syl2anc ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( log ‘ ( 1 / 𝐴 ) ) ) = ( 1 / 𝐴 ) )
5 4 eqcomd ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 1 / 𝐴 ) = ( exp ‘ ( log ‘ ( 1 / 𝐴 ) ) ) )
6 5 oveq2d ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 1 / ( 1 / 𝐴 ) ) = ( 1 / ( exp ‘ ( log ‘ ( 1 / 𝐴 ) ) ) ) )
7 eflog ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( log ‘ 𝐴 ) ) = 𝐴 )
8 recrec ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 1 / ( 1 / 𝐴 ) ) = 𝐴 )
9 7 8 eqtr4d ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( log ‘ 𝐴 ) ) = ( 1 / ( 1 / 𝐴 ) ) )
10 1 2 logcld ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ ( 1 / 𝐴 ) ) ∈ ℂ )
11 efneg ( ( log ‘ ( 1 / 𝐴 ) ) ∈ ℂ → ( exp ‘ - ( log ‘ ( 1 / 𝐴 ) ) ) = ( 1 / ( exp ‘ ( log ‘ ( 1 / 𝐴 ) ) ) ) )
12 10 11 syl ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ - ( log ‘ ( 1 / 𝐴 ) ) ) = ( 1 / ( exp ‘ ( log ‘ ( 1 / 𝐴 ) ) ) ) )
13 6 9 12 3eqtr4d ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( log ‘ 𝐴 ) ) = ( exp ‘ - ( log ‘ ( 1 / 𝐴 ) ) ) )
14 13 3adant3 ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≠ π ) → ( exp ‘ ( log ‘ 𝐴 ) ) = ( exp ‘ - ( log ‘ ( 1 / 𝐴 ) ) ) )
15 14 fveq2d ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≠ π ) → ( log ‘ ( exp ‘ ( log ‘ 𝐴 ) ) ) = ( log ‘ ( exp ‘ - ( log ‘ ( 1 / 𝐴 ) ) ) ) )
16 logrncl ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ran log )
17 16 3adant3 ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≠ π ) → ( log ‘ 𝐴 ) ∈ ran log )
18 logef ( ( log ‘ 𝐴 ) ∈ ran log → ( log ‘ ( exp ‘ ( log ‘ 𝐴 ) ) ) = ( log ‘ 𝐴 ) )
19 17 18 syl ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≠ π ) → ( log ‘ ( exp ‘ ( log ‘ 𝐴 ) ) ) = ( log ‘ 𝐴 ) )
20 df-ne ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ≠ π ↔ ¬ ( ℑ ‘ ( log ‘ 𝐴 ) ) = π )
21 lognegb ( ( ( 1 / 𝐴 ) ∈ ℂ ∧ ( 1 / 𝐴 ) ≠ 0 ) → ( - ( 1 / 𝐴 ) ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ ( 1 / 𝐴 ) ) ) = π ) )
22 1 2 21 syl2anc ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( - ( 1 / 𝐴 ) ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ ( 1 / 𝐴 ) ) ) = π ) )
23 22 biimprd ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( ℑ ‘ ( log ‘ ( 1 / 𝐴 ) ) ) = π → - ( 1 / 𝐴 ) ∈ ℝ+ ) )
24 ax-1cn 1 ∈ ℂ
25 divneg2 ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → - ( 1 / 𝐴 ) = ( 1 / - 𝐴 ) )
26 24 25 mp3an1 ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → - ( 1 / 𝐴 ) = ( 1 / - 𝐴 ) )
27 26 eleq1d ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( - ( 1 / 𝐴 ) ∈ ℝ+ ↔ ( 1 / - 𝐴 ) ∈ ℝ+ ) )
28 23 27 sylibd ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( ℑ ‘ ( log ‘ ( 1 / 𝐴 ) ) ) = π → ( 1 / - 𝐴 ) ∈ ℝ+ ) )
29 negcl ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
30 negeq0 ( 𝐴 ∈ ℂ → ( 𝐴 = 0 ↔ - 𝐴 = 0 ) )
31 30 necon3bid ( 𝐴 ∈ ℂ → ( 𝐴 ≠ 0 ↔ - 𝐴 ≠ 0 ) )
32 31 biimpa ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → - 𝐴 ≠ 0 )
33 rpreccl ( ( 1 / - 𝐴 ) ∈ ℝ+ → ( 1 / ( 1 / - 𝐴 ) ) ∈ ℝ+ )
34 recrec ( ( - 𝐴 ∈ ℂ ∧ - 𝐴 ≠ 0 ) → ( 1 / ( 1 / - 𝐴 ) ) = - 𝐴 )
35 34 eleq1d ( ( - 𝐴 ∈ ℂ ∧ - 𝐴 ≠ 0 ) → ( ( 1 / ( 1 / - 𝐴 ) ) ∈ ℝ+ ↔ - 𝐴 ∈ ℝ+ ) )
36 33 35 syl5ib ( ( - 𝐴 ∈ ℂ ∧ - 𝐴 ≠ 0 ) → ( ( 1 / - 𝐴 ) ∈ ℝ+ → - 𝐴 ∈ ℝ+ ) )
37 29 32 36 syl2an2r ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( 1 / - 𝐴 ) ∈ ℝ+ → - 𝐴 ∈ ℝ+ ) )
38 28 37 syld ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( ℑ ‘ ( log ‘ ( 1 / 𝐴 ) ) ) = π → - 𝐴 ∈ ℝ+ ) )
39 lognegb ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( - 𝐴 ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ 𝐴 ) ) = π ) )
40 38 39 sylibd ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( ℑ ‘ ( log ‘ ( 1 / 𝐴 ) ) ) = π → ( ℑ ‘ ( log ‘ 𝐴 ) ) = π ) )
41 40 con3d ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ¬ ( ℑ ‘ ( log ‘ 𝐴 ) ) = π → ¬ ( ℑ ‘ ( log ‘ ( 1 / 𝐴 ) ) ) = π ) )
42 41 3impia ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ ¬ ( ℑ ‘ ( log ‘ 𝐴 ) ) = π ) → ¬ ( ℑ ‘ ( log ‘ ( 1 / 𝐴 ) ) ) = π )
43 20 42 syl3an3b ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≠ π ) → ¬ ( ℑ ‘ ( log ‘ ( 1 / 𝐴 ) ) ) = π )
44 logrncl ( ( ( 1 / 𝐴 ) ∈ ℂ ∧ ( 1 / 𝐴 ) ≠ 0 ) → ( log ‘ ( 1 / 𝐴 ) ) ∈ ran log )
45 1 2 44 syl2anc ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ ( 1 / 𝐴 ) ) ∈ ran log )
46 logreclem ( ( ( log ‘ ( 1 / 𝐴 ) ) ∈ ran log ∧ ¬ ( ℑ ‘ ( log ‘ ( 1 / 𝐴 ) ) ) = π ) → - ( log ‘ ( 1 / 𝐴 ) ) ∈ ran log )
47 45 46 stoic3 ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ ¬ ( ℑ ‘ ( log ‘ ( 1 / 𝐴 ) ) ) = π ) → - ( log ‘ ( 1 / 𝐴 ) ) ∈ ran log )
48 43 47 syld3an3 ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≠ π ) → - ( log ‘ ( 1 / 𝐴 ) ) ∈ ran log )
49 logef ( - ( log ‘ ( 1 / 𝐴 ) ) ∈ ran log → ( log ‘ ( exp ‘ - ( log ‘ ( 1 / 𝐴 ) ) ) ) = - ( log ‘ ( 1 / 𝐴 ) ) )
50 48 49 syl ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≠ π ) → ( log ‘ ( exp ‘ - ( log ‘ ( 1 / 𝐴 ) ) ) ) = - ( log ‘ ( 1 / 𝐴 ) ) )
51 15 19 50 3eqtr3d ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≠ π ) → ( log ‘ 𝐴 ) = - ( log ‘ ( 1 / 𝐴 ) ) )