cxplogb - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cxplogb		Structured version Visualization version GIF version

Theorem cxplogb 27096

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

**Assertion**
Ref	Expression
cxplogb	⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝑋 ∈ (ℂ ∖ {0})) → (𝐵↑_𝑐(𝐵 log_b 𝑋)) = 𝑋)

**Proof of Theorem cxplogb**
Step	Hyp	Ref	Expression
1		logbval 27076	. . 3 ⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝑋 ∈ (ℂ ∖ {0})) → (𝐵 log_b 𝑋) = ((log‘𝑋) / (log‘𝐵)))
2	1	oveq2d 7428	. 2 ⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝑋 ∈ (ℂ ∖ {0})) → (𝐵↑_𝑐(𝐵 log_b 𝑋)) = (𝐵↑_𝑐((log‘𝑋) / (log‘𝐵))))
3		eldifi 4078	. . . 4 ⊢ (𝐵 ∈ (ℂ ∖ {0, 1}) → 𝐵 ∈ ℂ)
4	3	adantr 486	. . 3 ⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝑋 ∈ (ℂ ∖ {0})) → 𝐵 ∈ ℂ)
5		eldif 3909	. . . . 5 ⊢ (𝐵 ∈ (ℂ ∖ {0, 1}) ↔ (𝐵 ∈ ℂ ∧ ¬ 𝐵 ∈ {0, 1}))
6		0elpr01 11282	. . . . . . . 8 ⊢ 0 ∈ {0, 1}
7		eleq1 2849	. . . . . . . 8 ⊢ (𝐵 = 0 → (𝐵 ∈ {0, 1} ↔ 0 ∈ {0, 1}))
8	6, 7	mpbiri 261	. . . . . . 7 ⊢ (𝐵 = 0 → 𝐵 ∈ {0, 1})
9	8	necon3bi 2982	. . . . . 6 ⊢ (¬ 𝐵 ∈ {0, 1} → 𝐵 ≠ 0)
10	9	adantl 487	. . . . 5 ⊢ ((𝐵 ∈ ℂ ∧ ¬ 𝐵 ∈ {0, 1}) → 𝐵 ≠ 0)
11	5, 10	sylbi 220	. . . 4 ⊢ (𝐵 ∈ (ℂ ∖ {0, 1}) → 𝐵 ≠ 0)
12	11	adantr 486	. . 3 ⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝑋 ∈ (ℂ ∖ {0})) → 𝐵 ≠ 0)
13		eldif 3909	. . . . . . 7 ⊢ (𝑋 ∈ (ℂ ∖ {0}) ↔ (𝑋 ∈ ℂ ∧ ¬ 𝑋 ∈ {0}))
14		c0ex 11281	. . . . . . . . . . 11 ⊢ 0 ∈ V
15	14	snid 4623	. . . . . . . . . 10 ⊢ 0 ∈ {0}
16		eleq1 2849	. . . . . . . . . 10 ⊢ (𝑋 = 0 → (𝑋 ∈ {0} ↔ 0 ∈ {0}))
17	15, 16	mpbiri 261	. . . . . . . . 9 ⊢ (𝑋 = 0 → 𝑋 ∈ {0})
18	17	necon3bi 2982	. . . . . . . 8 ⊢ (¬ 𝑋 ∈ {0} → 𝑋 ≠ 0)
19	18	anim2i 629	. . . . . . 7 ⊢ ((𝑋 ∈ ℂ ∧ ¬ 𝑋 ∈ {0}) → (𝑋 ∈ ℂ ∧ 𝑋 ≠ 0))
20	13, 19	sylbi 220	. . . . . 6 ⊢ (𝑋 ∈ (ℂ ∖ {0}) → (𝑋 ∈ ℂ ∧ 𝑋 ≠ 0))
21		logcl 26878	. . . . . 6 ⊢ ((𝑋 ∈ ℂ ∧ 𝑋 ≠ 0) → (log‘𝑋) ∈ ℂ)
22	20, 21	syl 18	. . . . 5 ⊢ (𝑋 ∈ (ℂ ∖ {0}) → (log‘𝑋) ∈ ℂ)
23	22	adantl 487	. . . 4 ⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝑋 ∈ (ℂ ∖ {0})) → (log‘𝑋) ∈ ℂ)
24	9	anim2i 629	. . . . . . 7 ⊢ ((𝐵 ∈ ℂ ∧ ¬ 𝐵 ∈ {0, 1}) → (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0))
25	5, 24	sylbi 220	. . . . . 6 ⊢ (𝐵 ∈ (ℂ ∖ {0, 1}) → (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0))
26		logcl 26878	. . . . . 6 ⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (log‘𝐵) ∈ ℂ)
27	25, 26	syl 18	. . . . 5 ⊢ (𝐵 ∈ (ℂ ∖ {0, 1}) → (log‘𝐵) ∈ ℂ)
28	27	adantr 486	. . . 4 ⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝑋 ∈ (ℂ ∖ {0})) → (log‘𝐵) ∈ ℂ)
29		eldifpr 4619	. . . . . 6 ⊢ (𝐵 ∈ (ℂ ∖ {0, 1}) ↔ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1))
30	29	birani 509	. . . . 5 ⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝑋 ∈ (ℂ ∖ {0})) → (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1))
31		logccne0 26888	. . . . 5 ⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → (log‘𝐵) ≠ 0)
32	30, 31	syl 18	. . . 4 ⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝑋 ∈ (ℂ ∖ {0})) → (log‘𝐵) ≠ 0)
33	23, 28, 32	divcld 12074	. . 3 ⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝑋 ∈ (ℂ ∖ {0})) → ((log‘𝑋) / (log‘𝐵)) ∈ ℂ)
34	4, 12, 33	cxpefd 27022	. 2 ⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝑋 ∈ (ℂ ∖ {0})) → (𝐵↑_𝑐((log‘𝑋) / (log‘𝐵))) = (exp‘(((log‘𝑋) / (log‘𝐵)) · (log‘𝐵))))
35		eldifsn 4748	. . . . . . 7 ⊢ (𝑋 ∈ (ℂ ∖ {0}) ↔ (𝑋 ∈ ℂ ∧ 𝑋 ≠ 0))
36	35, 21	sylbi 220	. . . . . 6 ⊢ (𝑋 ∈ (ℂ ∖ {0}) → (log‘𝑋) ∈ ℂ)
37	36	adantl 487	. . . . 5 ⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝑋 ∈ (ℂ ∖ {0})) → (log‘𝑋) ∈ ℂ)
38	29, 31	sylbi 220	. . . . . 6 ⊢ (𝐵 ∈ (ℂ ∖ {0, 1}) → (log‘𝐵) ≠ 0)
39	38	adantr 486	. . . . 5 ⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝑋 ∈ (ℂ ∖ {0})) → (log‘𝐵) ≠ 0)
40	37, 28, 39	divcan1d 12075	. . . 4 ⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝑋 ∈ (ℂ ∖ {0})) → (((log‘𝑋) / (log‘𝐵)) · (log‘𝐵)) = (log‘𝑋))
41	40	fveq2d 6881	. . 3 ⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝑋 ∈ (ℂ ∖ {0})) → (exp‘(((log‘𝑋) / (log‘𝐵)) · (log‘𝐵))) = (exp‘(log‘𝑋)))
42		eflog 26886	. . . . 5 ⊢ ((𝑋 ∈ ℂ ∧ 𝑋 ≠ 0) → (exp‘(log‘𝑋)) = 𝑋)
43	35, 42	sylbi 220	. . . 4 ⊢ (𝑋 ∈ (ℂ ∖ {0}) → (exp‘(log‘𝑋)) = 𝑋)
44	43	adantl 487	. . 3 ⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝑋 ∈ (ℂ ∖ {0})) → (exp‘(log‘𝑋)) = 𝑋)
45	41, 44	eqtrd 2796	. 2 ⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝑋 ∈ (ℂ ∖ {0})) → (exp‘(((log‘𝑋) / (log‘𝐵)) · (log‘𝐵))) = 𝑋)
46	2, 34, 45	3eqtrd 2800	1 ⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝑋 ∈ (ℂ ∖ {0})) → (𝐵↑_𝑐(𝐵 log_b 𝑋)) = 𝑋)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2956 ∖ cdif 3896 {csn 4584 {cpr 4586 ‘cfv 6531 (class class class)co 7412 ℂcc 11179 0cc0 11181 1c1 11182 · cmul 11186 / cdiv 11954 expce 16207 logclog 26864 ↑_𝑐ccxp 26865 log_b clogb 27074

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7740 ax-inf2 9626 ax-cnex 11237 ax-resscn 11238 ax-1cn 11239 ax-icn 11240 ax-addcl 11241 ax-addrcl 11242 ax-mulcl 11243 ax-mulrcl 11244 ax-mulcom 11245 ax-addass 11246 ax-mulass 11247 ax-distr 11248 ax-i2m1 11249 ax-1ne0 11250 ax-1rid 11251 ax-rnegex 11252 ax-rrecex 11253 ax-cnre 11254 ax-pre-lttri 11255 ax-pre-lttrn 11256 ax-pre-ltadd 11257 ax-pre-mulgt0 11258 ax-pre-sup 11259 ax-addf 11260

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6297 df-ord 6358 df-on 6359 df-lim 6360 df-suc 6361 df-iota 6487 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-isom 6540 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-of 7682 df-om 7867 df-1st 7990 df-2nd 7991 df-supp 8162 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8460 df-2o 8461 df-er 8701 df-map 8833 df-pm 8834 df-ixp 8910 df-en 8958 df-dom 8959 df-sdom 8960 df-fin 8961 df-fsupp 9338 df-fi 9387 df-sup 9418 df-inf 9419 df-oi 9488 df-card 10001 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11524 df-neg 11525 df-div 11955 df-nn 12317 df-2 12386 df-3 12387 df-4 12388 df-5 12389 df-6 12390 df-7 12391 df-8 12392 df-9 12393 df-n0 12588 df-z 12675 df-dec 12796 df-uz 12947 df-q 13057 df-rp 13102 df-xneg 13222 df-xadd 13223 df-xmul 13224 df-ioo 13461 df-ioc 13462 df-ico 13463 df-icc 13464 df-fz 13621 df-fzo 13769 df-fl 13912 df-mod 13990 df-seq 14125 df-exp 14185 df-fac 14398 df-bc 14427 df-hash 14455 df-shft 15200 df-cj 15246 df-re 15247 df-im 15248 df-sqrt 15382 df-abs 15383 df-limsup 15618 df-clim 15635 df-rlim 15636 df-sum 15834 df-ef 16213 df-sin 16215 df-cos 16216 df-pi 16218 df-struct 17305 df-sets 17322 df-slot 17340 df-ndx 17352 df-base 17368 df-ress 17389 df-plusg 17421 df-mulr 17422 df-starv 17423 df-sca 17424 df-vsca 17425 df-ip 17426 df-tset 17427 df-ple 17428 df-ds 17430 df-unif 17431 df-hom 17432 df-cco 17433 df-rest 17573 df-topn 17574 df-0g 17592 df-gsum 17593 df-topgen 17594 df-pt 17595 df-prds 17598 df-xrs 17654 df-qtop 17659 df-imas 17660 df-xps 17662 df-mre 17736 df-mrc 17737 df-acs 17739 df-mgm 18796 df-sgrp 18888 df-mnd 18904 df-submnd 18959 df-mulg 19258 df-cntz 19511 df-cmn 19976 df-psmet 21650 df-xmet 21651 df-met 21652 df-bl 21653 df-mopn 21654 df-fbas 21655 df-fg 21656 df-cnfld 21659 df-top 23192 df-topon 23209 df-topsp 23231 df-bases 23244 df-cld 23317 df-ntr 23318 df-cls 23319 df-nei 23396 df-lp 23434 df-perf 23435 df-cn 23525 df-cnp 23526 df-haus 23613 df-tx 23861 df-hmeo 24054 df-fil 24145 df-fm 24237 df-flim 24238 df-flf 24239 df-xms 24619 df-ms 24620 df-tms 24621 df-cncf 25179 df-limc 26166 df-dv 26167 df-log 26866 df-cxp 26867 df-logb 27075

This theorem is used by: relogbcxpb 27097 logbgcd1irr 27104 sqrt2cxp2logb9e3 27109 aks4d1p1p4 43089 aks4d1p6 43099 aks6d1c7lem1 43198 fllogbd 49616 nnpw2blen 49636 dignn0ldlem 49658

W3C validator