Metamath Proof Explorer

Theorem logbchbase

Description: Change of base for logarithms. Property in Cohen4 p. 367. (Contributed by AV, 11-Jun-2020)

Ref Expression
Assertion logbchbase ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐴 logb 𝑋 ) = ( ( 𝐵 logb 𝑋 ) / ( 𝐵 logb 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 eldifsn ⊢ ( 𝑋 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑋 ∈ ℂ ∧ 𝑋 ≠ 0 ) )
2 logcl ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑋 ≠ 0 ) → ( log ‘ 𝑋 ) ∈ ℂ )
3 1 2 sylbi ⊢ ( 𝑋 ∈ ( ℂ ∖ { 0 } ) → ( log ‘ 𝑋 ) ∈ ℂ )
4 3 3ad2ant3 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( log ‘ 𝑋 ) ∈ ℂ )
5 logcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ℂ )
6 5 3adant3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( log ‘ 𝐴 ) ∈ ℂ )
7 logccne0 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( log ‘ 𝐴 ) ≠ 0 )
8 6 7 jca ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( log ‘ 𝐴 ) ∈ ℂ ∧ ( log ‘ 𝐴 ) ≠ 0 ) )
9 8 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( ( log ‘ 𝐴 ) ∈ ℂ ∧ ( log ‘ 𝐴 ) ≠ 0 ) )
10 logcl ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( log ‘ 𝐵 ) ∈ ℂ )
11 10 3adant3 ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( log ‘ 𝐵 ) ∈ ℂ )
12 logccne0 ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( log ‘ 𝐵 ) ≠ 0 )
13 11 12 jca ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( ( log ‘ 𝐵 ) ∈ ℂ ∧ ( log ‘ 𝐵 ) ≠ 0 ) )
14 13 3ad2ant2 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( ( log ‘ 𝐵 ) ∈ ℂ ∧ ( log ‘ 𝐵 ) ≠ 0 ) )
15 divcan7 ⊢ ( ( ( log ‘ 𝑋 ) ∈ ℂ ∧ ( ( log ‘ 𝐴 ) ∈ ℂ ∧ ( log ‘ 𝐴 ) ≠ 0 ) ∧ ( ( log ‘ 𝐵 ) ∈ ℂ ∧ ( log ‘ 𝐵 ) ≠ 0 ) ) → ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) / ( ( log ‘ 𝐴 ) / ( log ‘ 𝐵 ) ) ) = ( ( log ‘ 𝑋 ) / ( log ‘ 𝐴 ) ) )
16 4 9 14 15 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) / ( ( log ‘ 𝐴 ) / ( log ‘ 𝐵 ) ) ) = ( ( log ‘ 𝑋 ) / ( log ‘ 𝐴 ) ) )
17 eldifpr ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ↔ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
18 logbval ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 logb 𝑋 ) = ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) )
19 17 18 sylanbr ⊢ ( ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 logb 𝑋 ) = ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) )
20 19 3adant1 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 logb 𝑋 ) = ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) )
21 17 biimpri ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) )
22 eldifsn ⊢ ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) )
23 22 biimpri ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ( ℂ ∖ { 0 } ) )
24 23 3adant3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 𝐴 ∈ ( ℂ ∖ { 0 } ) )
25 logbval ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 logb 𝐴 ) = ( ( log ‘ 𝐴 ) / ( log ‘ 𝐵 ) ) )
26 21 24 25 syl2anr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ) → ( 𝐵 logb 𝐴 ) = ( ( log ‘ 𝐴 ) / ( log ‘ 𝐵 ) ) )
27 26 3adant3 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 logb 𝐴 ) = ( ( log ‘ 𝐴 ) / ( log ‘ 𝐵 ) ) )
28 20 27 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝐵 logb 𝑋 ) / ( 𝐵 logb 𝐴 ) ) = ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) / ( ( log ‘ 𝐴 ) / ( log ‘ 𝐵 ) ) ) )
29 eldifpr ⊢ ( 𝐴 ∈ ( ℂ ∖ { 0 , 1 } ) ↔ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) )
30 logbval ⊢ ( ( 𝐴 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐴 logb 𝑋 ) = ( ( log ‘ 𝑋 ) / ( log ‘ 𝐴 ) ) )
31 29 30 sylanbr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐴 logb 𝑋 ) = ( ( log ‘ 𝑋 ) / ( log ‘ 𝐴 ) ) )
32 31 3adant2 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐴 logb 𝑋 ) = ( ( log ‘ 𝑋 ) / ( log ‘ 𝐴 ) ) )
33 16 28 32 3eqtr4rd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐴 logb 𝑋 ) = ( ( 𝐵 logb 𝑋 ) / ( 𝐵 logb 𝐴 ) ) )