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 / 𝐴 ) ) )