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 ( 𝐵 ↑𝑐 𝑋 ) ) = 𝑋 )