Metamath Proof Explorer

Theorem logbrec

Description: Logarithm of a reciprocal changes sign. See logrec . Particular case of Property 3 of Cohen4 p. 361. (Contributed by Thierry Arnoux, 27-Sep-2017)

Ref Expression
Assertion logbrec ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ+ ) → ( 𝐵 logb ( 1 / 𝐴 ) ) = - ( 𝐵 logb 𝐴 ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ+ ) → 𝐴 ∈ ℝ+ )
2 1 rpreccld ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ+ ) → ( 1 / 𝐴 ) ∈ ℝ+ )
3 relogbval ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 1 / 𝐴 ) ∈ ℝ+ ) → ( 𝐵 logb ( 1 / 𝐴 ) ) = ( ( log ‘ ( 1 / 𝐴 ) ) / ( log ‘ 𝐵 ) ) )
4 2 3 syldan ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ+ ) → ( 𝐵 logb ( 1 / 𝐴 ) ) = ( ( log ‘ ( 1 / 𝐴 ) ) / ( log ‘ 𝐵 ) ) )
5 relogbval ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ+ ) → ( 𝐵 logb 𝐴 ) = ( ( log ‘ 𝐴 ) / ( log ‘ 𝐵 ) ) )
6 5 negeqd ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ+ ) → - ( 𝐵 logb 𝐴 ) = - ( ( log ‘ 𝐴 ) / ( log ‘ 𝐵 ) ) )
7 1 rpcnd ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ+ ) → 𝐴 ∈ ℂ )
8 1 rpne0d ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ+ ) → 𝐴 ≠ 0 )
9 7 8 logcld ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ+ ) → ( log ‘ 𝐴 ) ∈ ℂ )
10 zgt1rpn0n1 ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
11 10 simp1d ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 𝐵 ∈ ℝ+ )
12 11 adantr ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ+ ) → 𝐵 ∈ ℝ+ )
13 12 relogcld ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ+ ) → ( log ‘ 𝐵 ) ∈ ℝ )
14 13 recnd ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ+ ) → ( log ‘ 𝐵 ) ∈ ℂ )
15 10 simp3d ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 𝐵 ≠ 1 )
16 15 adantr ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ+ ) → 𝐵 ≠ 1 )
17 logne0 ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → ( log ‘ 𝐵 ) ≠ 0 )
18 12 16 17 syl2anc ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ+ ) → ( log ‘ 𝐵 ) ≠ 0 )
19 9 14 18 divnegd ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ+ ) → - ( ( log ‘ 𝐴 ) / ( log ‘ 𝐵 ) ) = ( - ( log ‘ 𝐴 ) / ( log ‘ 𝐵 ) ) )
20 7 8 reccld ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ+ ) → ( 1 / 𝐴 ) ∈ ℂ )
21 7 8 recne0d ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ+ ) → ( 1 / 𝐴 ) ≠ 0 )
22 20 21 logcld ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ+ ) → ( log ‘ ( 1 / 𝐴 ) ) ∈ ℂ )
23 1 relogcld ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ+ ) → ( log ‘ 𝐴 ) ∈ ℝ )
24 23 reim0d ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ+ ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) = 0 )
25 0re ⊢ 0 ∈ ℝ
26 pipos ⊢ 0 < π
27 25 26 gtneii ⊢ π ≠ 0
28 27 a1i ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ+ ) → π ≠ 0 )
29 28 necomd ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ+ ) → 0 ≠ π )
30 24 29 eqnetrd ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ+ ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ≠ π )
31 logrec ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≠ π ) → ( log ‘ 𝐴 ) = - ( log ‘ ( 1 / 𝐴 ) ) )
32 7 8 30 31 syl3anc ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ+ ) → ( log ‘ 𝐴 ) = - ( log ‘ ( 1 / 𝐴 ) ) )
33 32 eqcomd ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ+ ) → - ( log ‘ ( 1 / 𝐴 ) ) = ( log ‘ 𝐴 ) )
34 22 33 negcon1ad ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ+ ) → - ( log ‘ 𝐴 ) = ( log ‘ ( 1 / 𝐴 ) ) )
35 34 oveq1d ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ+ ) → ( - ( log ‘ 𝐴 ) / ( log ‘ 𝐵 ) ) = ( ( log ‘ ( 1 / 𝐴 ) ) / ( log ‘ 𝐵 ) ) )
36 6 19 35 3eqtrd ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ+ ) → - ( 𝐵 logb 𝐴 ) = ( ( log ‘ ( 1 / 𝐴 ) ) / ( log ‘ 𝐵 ) ) )
37 4 36 eqtr4d ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ+ ) → ( 𝐵 logb ( 1 / 𝐴 ) ) = - ( 𝐵 logb 𝐴 ) )