Theorem nnlogbexp

Description: Identity law for general logarithm with integer base. (Contributed by Stefan O'Rear, 19-Sep-2014) (Revised by Thierry Arnoux, 27-Sep-2017)

	Ref	Expression
Assertion	nnlogbexp	⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( 𝐵 logb ( 𝐵 ↑ 𝑀 ) ) = 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		zgt1rpn0n1	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
2	1	adantr	⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
3	2	simp1d	⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → 𝐵 ∈ ℝ+ )
4	3	rpcnd	⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → 𝐵 ∈ ℂ )
5	4	adantr	⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 = 0 ) → 𝐵 ∈ ℂ )
6	2	simp2d	⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → 𝐵 ≠ 0 )
7	6	adantr	⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 = 0 ) → 𝐵 ≠ 0 )
8	2	simp3d	⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → 𝐵 ≠ 1 )
9	8	adantr	⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 = 0 ) → 𝐵 ≠ 1 )
10		logb1	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( 𝐵 logb 1 ) = 0 )
11	5 7 9 10	syl3anc	⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 = 0 ) → ( 𝐵 logb 1 ) = 0 )
12		simpr	⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 = 0 ) → 𝑀 = 0 )
13	12	oveq2d	⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 = 0 ) → ( 𝐵 ↑ 𝑀 ) = ( 𝐵 ↑ 0 ) )
14	5	exp0d	⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 = 0 ) → ( 𝐵 ↑ 0 ) = 1 )
15	13 14	eqtrd	⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 = 0 ) → ( 𝐵 ↑ 𝑀 ) = 1 )
16	15	oveq2d	⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 = 0 ) → ( 𝐵 logb ( 𝐵 ↑ 𝑀 ) ) = ( 𝐵 logb 1 ) )
17	11 16 12	3eqtr4d	⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 = 0 ) → ( 𝐵 logb ( 𝐵 ↑ 𝑀 ) ) = 𝑀 )
18	4	adantr	⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → 𝐵 ∈ ℂ )
19	6	adantr	⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → 𝐵 ≠ 0 )
20	8	adantr	⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → 𝐵 ≠ 1 )
21		eldifpr	⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ↔ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
22	18 19 20 21	syl3anbrc	⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) )
23	3	adantr	⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → 𝐵 ∈ ℝ+ )
24		simpr	⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → 𝑀 ∈ ℤ )
25	24	adantr	⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → 𝑀 ∈ ℤ )
26	23 25	rpexpcld	⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → ( 𝐵 ↑ 𝑀 ) ∈ ℝ+ )
27	26	rpcnne0d	⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → ( ( 𝐵 ↑ 𝑀 ) ∈ ℂ ∧ ( 𝐵 ↑ 𝑀 ) ≠ 0 ) )
28		eldifsn	⊢ ( ( 𝐵 ↑ 𝑀 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( 𝐵 ↑ 𝑀 ) ∈ ℂ ∧ ( 𝐵 ↑ 𝑀 ) ≠ 0 ) )
29	27 28	sylibr	⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → ( 𝐵 ↑ 𝑀 ) ∈ ( ℂ ∖ { 0 } ) )
30		logbval	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐵 ↑ 𝑀 ) ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 logb ( 𝐵 ↑ 𝑀 ) ) = ( ( log ‘ ( 𝐵 ↑ 𝑀 ) ) / ( log ‘ 𝐵 ) ) )
31	22 29 30	syl2anc	⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → ( 𝐵 logb ( 𝐵 ↑ 𝑀 ) ) = ( ( log ‘ ( 𝐵 ↑ 𝑀 ) ) / ( log ‘ 𝐵 ) ) )
32	24	zred	⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → 𝑀 ∈ ℝ )
33	32	adantr	⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → 𝑀 ∈ ℝ )
34	23 33	logcxpd	⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → ( log ‘ ( 𝐵 ↑𝑐 𝑀 ) ) = ( 𝑀 · ( log ‘ 𝐵 ) ) )
35	18 19 25	cxpexpzd	⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → ( 𝐵 ↑𝑐 𝑀 ) = ( 𝐵 ↑ 𝑀 ) )
36	35	fveq2d	⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → ( log ‘ ( 𝐵 ↑𝑐 𝑀 ) ) = ( log ‘ ( 𝐵 ↑ 𝑀 ) ) )
37	34 36	eqtr3d	⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → ( 𝑀 · ( log ‘ 𝐵 ) ) = ( log ‘ ( 𝐵 ↑ 𝑀 ) ) )
38	37	oveq1d	⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → ( ( 𝑀 · ( log ‘ 𝐵 ) ) / ( log ‘ 𝐵 ) ) = ( ( log ‘ ( 𝐵 ↑ 𝑀 ) ) / ( log ‘ 𝐵 ) ) )
39	33	recnd	⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → 𝑀 ∈ ℂ )
40	18 19	logcld	⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → ( log ‘ 𝐵 ) ∈ ℂ )
41		logne0	⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → ( log ‘ 𝐵 ) ≠ 0 )
42	23 20 41	syl2anc	⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → ( log ‘ 𝐵 ) ≠ 0 )
43	39 40 42	divcan4d	⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → ( ( 𝑀 · ( log ‘ 𝐵 ) ) / ( log ‘ 𝐵 ) ) = 𝑀 )
44	31 38 43	3eqtr2d	⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → ( 𝐵 logb ( 𝐵 ↑ 𝑀 ) ) = 𝑀 )
45	17 44	pm2.61dane	⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( 𝐵 logb ( 𝐵 ↑ 𝑀 ) ) = 𝑀 )