This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem relogbcxp

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

Ref Expression
Assertion relogbcxp ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ 𝑋 ∈ ℝ ) → ( 𝐵 logb ( 𝐵 ↑𝑐 𝑋 ) ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 eldifsn ⊢ ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ↔ ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) )
2 rpcn ⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℂ )
3 2 adantr ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → 𝐵 ∈ ℂ )
4 rpne0 ⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ≠ 0 )
5 4 adantr ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → 𝐵 ≠ 0 )
6 simpr ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → 𝐵 ≠ 1 )
7 eldifpr ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ↔ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
8 3 5 6 7 syl3anbrc ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) )
9 1 8 sylbi ⊢ ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) → 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) )
10 eldifi ⊢ ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) → 𝐵 ∈ ℝ+ )
11 10 2 syl ⊢ ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) → 𝐵 ∈ ℂ )
12 recn ⊢ ( 𝑋 ∈ ℝ → 𝑋 ∈ ℂ )
13 cxpcl ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝑋 ∈ ℂ ) → ( 𝐵 ↑𝑐 𝑋 ) ∈ ℂ )
14 11 12 13 syl2an ⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ 𝑋 ∈ ℝ ) → ( 𝐵 ↑𝑐 𝑋 ) ∈ ℂ )
15 11 adantr ⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ 𝑋 ∈ ℝ ) → 𝐵 ∈ ℂ )
16 1 5 sylbi ⊢ ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) → 𝐵 ≠ 0 )
17 16 adantr ⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ 𝑋 ∈ ℝ ) → 𝐵 ≠ 0 )
18 12 adantl ⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ 𝑋 ∈ ℝ ) → 𝑋 ∈ ℂ )
19 15 17 18 cxpne0d ⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ 𝑋 ∈ ℝ ) → ( 𝐵 ↑𝑐 𝑋 ) ≠ 0 )
20 eldifsn ⊢ ( ( 𝐵 ↑𝑐 𝑋 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( 𝐵 ↑𝑐 𝑋 ) ∈ ℂ ∧ ( 𝐵 ↑𝑐 𝑋 ) ≠ 0 ) )
21 14 19 20 sylanbrc ⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ 𝑋 ∈ ℝ ) → ( 𝐵 ↑𝑐 𝑋 ) ∈ ( ℂ ∖ { 0 } ) )
22 logbval ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐵 ↑𝑐 𝑋 ) ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 logb ( 𝐵 ↑𝑐 𝑋 ) ) = ( ( log ‘ ( 𝐵 ↑𝑐 𝑋 ) ) / ( log ‘ 𝐵 ) ) )
23 9 21 22 syl2an2r ⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ 𝑋 ∈ ℝ ) → ( 𝐵 logb ( 𝐵 ↑𝑐 𝑋 ) ) = ( ( log ‘ ( 𝐵 ↑𝑐 𝑋 ) ) / ( log ‘ 𝐵 ) ) )
24 logcxp ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝑋 ∈ ℝ ) → ( log ‘ ( 𝐵 ↑𝑐 𝑋 ) ) = ( 𝑋 · ( log ‘ 𝐵 ) ) )
25 10 24 sylan ⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ 𝑋 ∈ ℝ ) → ( log ‘ ( 𝐵 ↑𝑐 𝑋 ) ) = ( 𝑋 · ( log ‘ 𝐵 ) ) )
26 25 oveq1d ⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ 𝑋 ∈ ℝ ) → ( ( log ‘ ( 𝐵 ↑𝑐 𝑋 ) ) / ( log ‘ 𝐵 ) ) = ( ( 𝑋 · ( log ‘ 𝐵 ) ) / ( log ‘ 𝐵 ) ) )
27 eldif ⊢ ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ↔ ( 𝐵 ∈ ℝ+ ∧ ¬ 𝐵 ∈ { 1 } ) )
28 rpcnne0 ⊢ ( 𝐵 ∈ ℝ+ → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
29 28 adantr ⊢ ( ( 𝐵 ∈ ℝ+ ∧ ¬ 𝐵 ∈ { 1 } ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
30 27 29 sylbi ⊢ ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
31 logcl ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( log ‘ 𝐵 ) ∈ ℂ )
32 30 31 syl ⊢ ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) → ( log ‘ 𝐵 ) ∈ ℂ )
33 32 adantr ⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ 𝑋 ∈ ℝ ) → ( log ‘ 𝐵 ) ∈ ℂ )
34 logne0 ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → ( log ‘ 𝐵 ) ≠ 0 )
35 1 34 sylbi ⊢ ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) → ( log ‘ 𝐵 ) ≠ 0 )
36 35 adantr ⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ 𝑋 ∈ ℝ ) → ( log ‘ 𝐵 ) ≠ 0 )
37 18 33 36 divcan4d ⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ 𝑋 ∈ ℝ ) → ( ( 𝑋 · ( log ‘ 𝐵 ) ) / ( log ‘ 𝐵 ) ) = 𝑋 )
38 23 26 37 3eqtrd ⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ 𝑋 ∈ ℝ ) → ( 𝐵 logb ( 𝐵 ↑𝑐 𝑋 ) ) = 𝑋 )