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 𝑋 ) ) = 𝑋 )