Metamath Proof Explorer

Theorem cxplogb

Description: Identity law for the general logarithm. (Contributed by AV, 22-May-2020)

Ref Expression
Assertion cxplogb ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑋 ) ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 logbval ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 logb 𝑋 ) = ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) )
2 1 oveq2d ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑋 ) ) = ( 𝐵 ↑𝑐 ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) ) )
3 eldifi ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) → 𝐵 ∈ ℂ )
4 3 adantr ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → 𝐵 ∈ ℂ )
5 eldif ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ↔ ( 𝐵 ∈ ℂ ∧ ¬ 𝐵 ∈ { 0 , 1 } ) )
6 c0ex ⊢ 0 ∈ V
7 6 prid1 ⊢ 0 ∈ { 0 , 1 }
8 eleq1 ⊢ ( 𝐵 = 0 → ( 𝐵 ∈ { 0 , 1 } ↔ 0 ∈ { 0 , 1 } ) )
9 7 8 mpbiri ⊢ ( 𝐵 = 0 → 𝐵 ∈ { 0 , 1 } )
10 9 necon3bi ⊢ ( ¬ 𝐵 ∈ { 0 , 1 } → 𝐵 ≠ 0 )
11 10 adantl ⊢ ( ( 𝐵 ∈ ℂ ∧ ¬ 𝐵 ∈ { 0 , 1 } ) → 𝐵 ≠ 0 )
12 5 11 sylbi ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) → 𝐵 ≠ 0 )
13 12 adantr ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → 𝐵 ≠ 0 )
14 eldif ⊢ ( 𝑋 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑋 ∈ ℂ ∧ ¬ 𝑋 ∈ { 0 } ) )
15 6 snid ⊢ 0 ∈ { 0 }
16 eleq1 ⊢ ( 𝑋 = 0 → ( 𝑋 ∈ { 0 } ↔ 0 ∈ { 0 } ) )
17 15 16 mpbiri ⊢ ( 𝑋 = 0 → 𝑋 ∈ { 0 } )
18 17 necon3bi ⊢ ( ¬ 𝑋 ∈ { 0 } → 𝑋 ≠ 0 )
19 18 anim2i ⊢ ( ( 𝑋 ∈ ℂ ∧ ¬ 𝑋 ∈ { 0 } ) → ( 𝑋 ∈ ℂ ∧ 𝑋 ≠ 0 ) )
20 14 19 sylbi ⊢ ( 𝑋 ∈ ( ℂ ∖ { 0 } ) → ( 𝑋 ∈ ℂ ∧ 𝑋 ≠ 0 ) )
21 logcl ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑋 ≠ 0 ) → ( log ‘ 𝑋 ) ∈ ℂ )
22 20 21 syl ⊢ ( 𝑋 ∈ ( ℂ ∖ { 0 } ) → ( log ‘ 𝑋 ) ∈ ℂ )
23 22 adantl ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( log ‘ 𝑋 ) ∈ ℂ )
24 10 anim2i ⊢ ( ( 𝐵 ∈ ℂ ∧ ¬ 𝐵 ∈ { 0 , 1 } ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
25 5 24 sylbi ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
26 logcl ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( log ‘ 𝐵 ) ∈ ℂ )
27 25 26 syl ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) → ( log ‘ 𝐵 ) ∈ ℂ )
28 27 adantr ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( log ‘ 𝐵 ) ∈ ℂ )
29 eldifpr ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ↔ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
30 29 biimpi ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
31 30 adantr ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
32 logccne0 ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( log ‘ 𝐵 ) ≠ 0 )
33 31 32 syl ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( log ‘ 𝐵 ) ≠ 0 )
34 23 28 33 divcld ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) ∈ ℂ )
35 4 13 34 cxpefd ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 ↑𝑐 ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) ) = ( exp ‘ ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) · ( log ‘ 𝐵 ) ) ) )
36 eldifsn ⊢ ( 𝑋 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑋 ∈ ℂ ∧ 𝑋 ≠ 0 ) )
37 36 21 sylbi ⊢ ( 𝑋 ∈ ( ℂ ∖ { 0 } ) → ( log ‘ 𝑋 ) ∈ ℂ )
38 37 adantl ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( log ‘ 𝑋 ) ∈ ℂ )
39 29 32 sylbi ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) → ( log ‘ 𝐵 ) ≠ 0 )
40 39 adantr ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( log ‘ 𝐵 ) ≠ 0 )
41 38 28 40 divcan1d ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) · ( log ‘ 𝐵 ) ) = ( log ‘ 𝑋 ) )
42 41 fveq2d ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( exp ‘ ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) · ( log ‘ 𝐵 ) ) ) = ( exp ‘ ( log ‘ 𝑋 ) ) )
43 eflog ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑋 ≠ 0 ) → ( exp ‘ ( log ‘ 𝑋 ) ) = 𝑋 )
44 36 43 sylbi ⊢ ( 𝑋 ∈ ( ℂ ∖ { 0 } ) → ( exp ‘ ( log ‘ 𝑋 ) ) = 𝑋 )
45 44 adantl ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( exp ‘ ( log ‘ 𝑋 ) ) = 𝑋 )
46 42 45 eqtrd ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( exp ‘ ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) · ( log ‘ 𝐵 ) ) ) = 𝑋 )
47 2 35 46 3eqtrd ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑋 ) ) = 𝑋 )