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 0elpr01 ⊢ 0 ∈ { 0 , 1 }
7 eleq1 ⊢ ( 𝐵 = 0 → ( 𝐵 ∈ { 0 , 1 } ↔ 0 ∈ { 0 , 1 } ) )
8 6 7 mpbiri ⊢ ( 𝐵 = 0 → 𝐵 ∈ { 0 , 1 } )
9 8 necon3bi ⊢ ( ¬ 𝐵 ∈ { 0 , 1 } → 𝐵 ≠ 0 )
10 9 adantl ⊢ ( ( 𝐵 ∈ ℂ ∧ ¬ 𝐵 ∈ { 0 , 1 } ) → 𝐵 ≠ 0 )
11 5 10 sylbi ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) → 𝐵 ≠ 0 )
12 11 adantr ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → 𝐵 ≠ 0 )
13 eldif ⊢ ( 𝑋 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑋 ∈ ℂ ∧ ¬ 𝑋 ∈ { 0 } ) )
14 c0ex ⊢ 0 ∈ V
15 14 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 13 19 sylbi ⊢ ( 𝑋 ∈ ( ℂ ∖ { 0 } ) → ( 𝑋 ∈ ℂ ∧ 𝑋 ≠ 0 ) )
21 logcl ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑋 ≠ 0 ) → ( log ‘ 𝑋 ) ∈ ℂ )
22 20 21 syl ⊢ ( 𝑋 ∈ ( ℂ ∖ { 0 } ) → ( log ‘ 𝑋 ) ∈ ℂ )
23 22 adantl ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( log ‘ 𝑋 ) ∈ ℂ )
24 9 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 birani ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
31 logccne0 ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( log ‘ 𝐵 ) ≠ 0 )
32 30 31 syl ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( log ‘ 𝐵 ) ≠ 0 )
33 23 28 32 divcld ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) ∈ ℂ )
34 4 12 33 cxpefd ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 ↑𝑐 ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) ) = ( exp ‘ ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) · ( log ‘ 𝐵 ) ) ) )
35 eldifsn ⊢ ( 𝑋 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑋 ∈ ℂ ∧ 𝑋 ≠ 0 ) )
36 35 21 sylbi ⊢ ( 𝑋 ∈ ( ℂ ∖ { 0 } ) → ( log ‘ 𝑋 ) ∈ ℂ )
37 36 adantl ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( log ‘ 𝑋 ) ∈ ℂ )
38 29 31 sylbi ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) → ( log ‘ 𝐵 ) ≠ 0 )
39 38 adantr ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( log ‘ 𝐵 ) ≠ 0 )
40 37 28 39 divcan1d ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) · ( log ‘ 𝐵 ) ) = ( log ‘ 𝑋 ) )
41 40 fveq2d ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( exp ‘ ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) · ( log ‘ 𝐵 ) ) ) = ( exp ‘ ( log ‘ 𝑋 ) ) )
42 eflog ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑋 ≠ 0 ) → ( exp ‘ ( log ‘ 𝑋 ) ) = 𝑋 )
43 35 42 sylbi ⊢ ( 𝑋 ∈ ( ℂ ∖ { 0 } ) → ( exp ‘ ( log ‘ 𝑋 ) ) = 𝑋 )
44 43 adantl ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( exp ‘ ( log ‘ 𝑋 ) ) = 𝑋 )
45 41 44 eqtrd ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( exp ‘ ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) · ( log ‘ 𝐵 ) ) ) = 𝑋 )
46 2 34 45 3eqtrd ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑋 ) ) = 𝑋 )