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

Theorem logbval 26200
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 David A. Wheeler, 16-Jul-2017.)
Assertion
Ref Expression
logbval ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝑋 ∈ (ℂ ∖ {0})) → (𝐵 logb 𝑋) = ((log‘𝑋) / (log‘𝐵)))

Proof of Theorem logbval
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6879 . . 3 (𝑥 = 𝐵 → (log‘𝑥) = (log‘𝐵))
21oveq2d 7410 . 2 (𝑥 = 𝐵 → ((log‘𝑦) / (log‘𝑥)) = ((log‘𝑦) / (log‘𝐵)))
3 fveq2 6879 . . 3 (𝑦 = 𝑋 → (log‘𝑦) = (log‘𝑋))
43oveq1d 7409 . 2 (𝑦 = 𝑋 → ((log‘𝑦) / (log‘𝐵)) = ((log‘𝑋) / (log‘𝐵)))
5 df-logb 26199 . 2 logb = (𝑥 ∈ (ℂ ∖ {0, 1}), 𝑦 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑦) / (log‘𝑥)))
6 ovex 7427 . 2 ((log‘𝑋) / (log‘𝐵)) ∈ V
72, 4, 5, 6ovmpo 7552 1 ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝑋 ∈ (ℂ ∖ {0})) → (𝐵 logb 𝑋) = ((log‘𝑋) / (log‘𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wcel 2106  cdif 3942  {csn 4623  {cpr 4625  cfv 6533  (class class class)co 7394  cc 11092  0cc0 11094  1c1 11095   / cdiv 11855  logclog 25994   logb clogb 26198
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5293  ax-nul 5300  ax-pr 5421
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3775  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5143  df-opab 5205  df-id 5568  df-xp 5676  df-rel 5677  df-cnv 5678  df-co 5679  df-dm 5680  df-iota 6485  df-fun 6535  df-fv 6541  df-ov 7397  df-oprab 7398  df-mpo 7399  df-logb 26199
This theorem is referenced by:  logbcl  26201  logbid1  26202  logb1  26203  elogb  26204  logbchbase  26205  relogbval  26206  relogbcl  26207  relogbreexp  26209  relogbmul  26211  nnlogbexp  26215  relogbcxp  26219  cxplogb  26220  logbgt0b  26227  dvrelog2b  40800  dvrelogpow2b  40802  rege1logbrege0  46956  logb2aval  47521
  Copyright terms: Public domain W3C validator