![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rplogbval | GIF version |
Description: Define the value of the logb function, the logarithm generalized to an arbitrary base, when used as infix. Most Metamath statements select variables in order of their use, but to make the order clearer we use "B" for base and "X" for the argument of the logarithm function here. (Contributed by David A. Wheeler, 21-Jan-2017.) (Revised by Jim Kingdon, 3-Jul-2024.) |
Ref | Expression |
---|---|
rplogbval | ⊢ ((𝐵 ∈ ℝ+ ∧ 𝐵 # 1 ∧ 𝑋 ∈ ℝ+) → (𝐵 logb 𝑋) = ((log‘𝑋) / (log‘𝐵))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rpcn 9636 | . . . 4 ⊢ (𝐵 ∈ ℝ+ → 𝐵 ∈ ℂ) | |
2 | 1 | 3ad2ant1 1018 | . . 3 ⊢ ((𝐵 ∈ ℝ+ ∧ 𝐵 # 1 ∧ 𝑋 ∈ ℝ+) → 𝐵 ∈ ℂ) |
3 | rpne0 9643 | . . . 4 ⊢ (𝐵 ∈ ℝ+ → 𝐵 ≠ 0) | |
4 | 3 | 3ad2ant1 1018 | . . 3 ⊢ ((𝐵 ∈ ℝ+ ∧ 𝐵 # 1 ∧ 𝑋 ∈ ℝ+) → 𝐵 ≠ 0) |
5 | simp2 998 | . . . 4 ⊢ ((𝐵 ∈ ℝ+ ∧ 𝐵 # 1 ∧ 𝑋 ∈ ℝ+) → 𝐵 # 1) | |
6 | 1cnd 7951 | . . . . 5 ⊢ ((𝐵 ∈ ℝ+ ∧ 𝐵 # 1 ∧ 𝑋 ∈ ℝ+) → 1 ∈ ℂ) | |
7 | apne 8557 | . . . . 5 ⊢ ((𝐵 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐵 # 1 → 𝐵 ≠ 1)) | |
8 | 2, 6, 7 | syl2anc 411 | . . . 4 ⊢ ((𝐵 ∈ ℝ+ ∧ 𝐵 # 1 ∧ 𝑋 ∈ ℝ+) → (𝐵 # 1 → 𝐵 ≠ 1)) |
9 | 5, 8 | mpd 13 | . . 3 ⊢ ((𝐵 ∈ ℝ+ ∧ 𝐵 # 1 ∧ 𝑋 ∈ ℝ+) → 𝐵 ≠ 1) |
10 | eldifpr 3618 | . . 3 ⊢ (𝐵 ∈ (ℂ ∖ {0, 1}) ↔ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1)) | |
11 | 2, 4, 9, 10 | syl3anbrc 1181 | . 2 ⊢ ((𝐵 ∈ ℝ+ ∧ 𝐵 # 1 ∧ 𝑋 ∈ ℝ+) → 𝐵 ∈ (ℂ ∖ {0, 1})) |
12 | rpcn 9636 | . . . 4 ⊢ (𝑋 ∈ ℝ+ → 𝑋 ∈ ℂ) | |
13 | 12 | 3ad2ant3 1020 | . . 3 ⊢ ((𝐵 ∈ ℝ+ ∧ 𝐵 # 1 ∧ 𝑋 ∈ ℝ+) → 𝑋 ∈ ℂ) |
14 | rpne0 9643 | . . . 4 ⊢ (𝑋 ∈ ℝ+ → 𝑋 ≠ 0) | |
15 | 14 | 3ad2ant3 1020 | . . 3 ⊢ ((𝐵 ∈ ℝ+ ∧ 𝐵 # 1 ∧ 𝑋 ∈ ℝ+) → 𝑋 ≠ 0) |
16 | eldifsn 3718 | . . 3 ⊢ (𝑋 ∈ (ℂ ∖ {0}) ↔ (𝑋 ∈ ℂ ∧ 𝑋 ≠ 0)) | |
17 | 13, 15, 16 | sylanbrc 417 | . 2 ⊢ ((𝐵 ∈ ℝ+ ∧ 𝐵 # 1 ∧ 𝑋 ∈ ℝ+) → 𝑋 ∈ (ℂ ∖ {0})) |
18 | simp3 999 | . . . 4 ⊢ ((𝐵 ∈ ℝ+ ∧ 𝐵 # 1 ∧ 𝑋 ∈ ℝ+) → 𝑋 ∈ ℝ+) | |
19 | 18 | relogcld 13936 | . . 3 ⊢ ((𝐵 ∈ ℝ+ ∧ 𝐵 # 1 ∧ 𝑋 ∈ ℝ+) → (log‘𝑋) ∈ ℝ) |
20 | simp1 997 | . . . 4 ⊢ ((𝐵 ∈ ℝ+ ∧ 𝐵 # 1 ∧ 𝑋 ∈ ℝ+) → 𝐵 ∈ ℝ+) | |
21 | 20 | relogcld 13936 | . . 3 ⊢ ((𝐵 ∈ ℝ+ ∧ 𝐵 # 1 ∧ 𝑋 ∈ ℝ+) → (log‘𝐵) ∈ ℝ) |
22 | 20, 5 | logrpap0d 13932 | . . 3 ⊢ ((𝐵 ∈ ℝ+ ∧ 𝐵 # 1 ∧ 𝑋 ∈ ℝ+) → (log‘𝐵) # 0) |
23 | 19, 21, 22 | redivclapd 8768 | . 2 ⊢ ((𝐵 ∈ ℝ+ ∧ 𝐵 # 1 ∧ 𝑋 ∈ ℝ+) → ((log‘𝑋) / (log‘𝐵)) ∈ ℝ) |
24 | fveq2 5510 | . . . 4 ⊢ (𝑥 = 𝐵 → (log‘𝑥) = (log‘𝐵)) | |
25 | 24 | oveq2d 5884 | . . 3 ⊢ (𝑥 = 𝐵 → ((log‘𝑦) / (log‘𝑥)) = ((log‘𝑦) / (log‘𝐵))) |
26 | fveq2 5510 | . . . 4 ⊢ (𝑦 = 𝑋 → (log‘𝑦) = (log‘𝑋)) | |
27 | 26 | oveq1d 5883 | . . 3 ⊢ (𝑦 = 𝑋 → ((log‘𝑦) / (log‘𝐵)) = ((log‘𝑋) / (log‘𝐵))) |
28 | df-logb 13995 | . . 3 ⊢ logb = (𝑥 ∈ (ℂ ∖ {0, 1}), 𝑦 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑦) / (log‘𝑥))) | |
29 | 25, 27, 28 | ovmpog 6002 | . 2 ⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝑋 ∈ (ℂ ∖ {0}) ∧ ((log‘𝑋) / (log‘𝐵)) ∈ ℝ) → (𝐵 logb 𝑋) = ((log‘𝑋) / (log‘𝐵))) |
30 | 11, 17, 23, 29 | syl3anc 1238 | 1 ⊢ ((𝐵 ∈ ℝ+ ∧ 𝐵 # 1 ∧ 𝑋 ∈ ℝ+) → (𝐵 logb 𝑋) = ((log‘𝑋) / (log‘𝐵))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 978 = wceq 1353 ∈ wcel 2148 ≠ wne 2347 ∖ cdif 3126 {csn 3591 {cpr 3592 class class class wbr 4000 ‘cfv 5211 (class class class)co 5868 ℂcc 7787 ℝcr 7788 0cc0 7789 1c1 7790 # cap 8515 / cdiv 8605 ℝ+crp 9627 logclog 13910 logb clogb 13994 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-coll 4115 ax-sep 4118 ax-nul 4126 ax-pow 4171 ax-pr 4205 ax-un 4429 ax-setind 4532 ax-iinf 4583 ax-cnex 7880 ax-resscn 7881 ax-1cn 7882 ax-1re 7883 ax-icn 7884 ax-addcl 7885 ax-addrcl 7886 ax-mulcl 7887 ax-mulrcl 7888 ax-addcom 7889 ax-mulcom 7890 ax-addass 7891 ax-mulass 7892 ax-distr 7893 ax-i2m1 7894 ax-0lt1 7895 ax-1rid 7896 ax-0id 7897 ax-rnegex 7898 ax-precex 7899 ax-cnre 7900 ax-pre-ltirr 7901 ax-pre-ltwlin 7902 ax-pre-lttrn 7903 ax-pre-apti 7904 ax-pre-ltadd 7905 ax-pre-mulgt0 7906 ax-pre-mulext 7907 ax-arch 7908 ax-caucvg 7909 ax-pre-suploc 7910 ax-addf 7911 ax-mulf 7912 |
This theorem depends on definitions: df-bi 117 df-stab 831 df-dc 835 df-3or 979 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-nel 2443 df-ral 2460 df-rex 2461 df-reu 2462 df-rmo 2463 df-rab 2464 df-v 2739 df-sbc 2963 df-csb 3058 df-dif 3131 df-un 3133 df-in 3135 df-ss 3142 df-nul 3423 df-if 3535 df-pw 3576 df-sn 3597 df-pr 3598 df-op 3600 df-uni 3808 df-int 3843 df-iun 3886 df-disj 3978 df-br 4001 df-opab 4062 df-mpt 4063 df-tr 4099 df-id 4289 df-po 4292 df-iso 4293 df-iord 4362 df-on 4364 df-ilim 4365 df-suc 4367 df-iom 4586 df-xp 4628 df-rel 4629 df-cnv 4630 df-co 4631 df-dm 4632 df-rn 4633 df-res 4634 df-ima 4635 df-iota 5173 df-fun 5213 df-fn 5214 df-f 5215 df-f1 5216 df-fo 5217 df-f1o 5218 df-fv 5219 df-isom 5220 df-riota 5824 df-ov 5871 df-oprab 5872 df-mpo 5873 df-of 6076 df-1st 6134 df-2nd 6135 df-recs 6299 df-irdg 6364 df-frec 6385 df-1o 6410 df-oadd 6414 df-er 6528 df-map 6643 df-pm 6644 df-en 6734 df-dom 6735 df-fin 6736 df-sup 6976 df-inf 6977 df-pnf 7971 df-mnf 7972 df-xr 7973 df-ltxr 7974 df-le 7975 df-sub 8107 df-neg 8108 df-reap 8509 df-ap 8516 df-div 8606 df-inn 8896 df-2 8954 df-3 8955 df-4 8956 df-n0 9153 df-z 9230 df-uz 9505 df-q 9596 df-rp 9628 df-xneg 9746 df-xadd 9747 df-ioo 9866 df-ico 9868 df-icc 9869 df-fz 9983 df-fzo 10116 df-seqfrec 10419 df-exp 10493 df-fac 10677 df-bc 10699 df-ihash 10727 df-shft 10795 df-cj 10822 df-re 10823 df-im 10824 df-rsqrt 10978 df-abs 10979 df-clim 11258 df-sumdc 11333 df-ef 11627 df-e 11628 df-rest 12625 df-topgen 12644 df-psmet 13120 df-xmet 13121 df-met 13122 df-bl 13123 df-mopn 13124 df-top 13129 df-topon 13142 df-bases 13174 df-ntr 13229 df-cn 13321 df-cnp 13322 df-tx 13386 df-cncf 13691 df-limced 13758 df-dvap 13759 df-relog 13912 df-logb 13995 |
This theorem is referenced by: rplogbcl 13997 rplogbid1 13998 rplogb1 13999 rpelogb 14000 rplogbchbase 14001 relogbval 14002 rplogbreexp 14004 rprelogbmul 14006 rpcxplogb 14015 logbgt0b 14017 |
Copyright terms: Public domain | W3C validator |