MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eflog Structured version   Unicode version

Theorem eflog 22130
Description: Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.)
Assertion
Ref Expression
eflog  |-  ( ( A  e.  CC  /\  A  =/=  0 )  -> 
( exp `  ( log `  A ) )  =  A )

Proof of Theorem eflog
StepHypRef Expression
1 dflog2 22114 . . . 4  |-  log  =  `' ( exp  |`  ran  log )
21fveq1i 5776 . . 3  |-  ( log `  A )  =  ( `' ( exp  |`  ran  log ) `  A )
32fveq2i 5778 . 2  |-  ( ( exp  |`  ran  log ) `  ( log `  A
) )  =  ( ( exp  |`  ran  log ) `  ( `' ( exp  |`  ran  log ) `  A ) )
4 logrncl 22121 . . 3  |-  ( ( A  e.  CC  /\  A  =/=  0 )  -> 
( log `  A
)  e.  ran  log )
5 fvres 5789 . . 3  |-  ( ( log `  A )  e.  ran  log  ->  ( ( exp  |`  ran  log ) `  ( log `  A ) )  =  ( exp `  ( log `  A ) ) )
64, 5syl 16 . 2  |-  ( ( A  e.  CC  /\  A  =/=  0 )  -> 
( ( exp  |`  ran  log ) `  ( log `  A ) )  =  ( exp `  ( log `  A ) ) )
7 eldifsn 4084 . . 3  |-  ( A  e.  ( CC  \  { 0 } )  <-> 
( A  e.  CC  /\  A  =/=  0 ) )
8 eff1o2 22117 . . . 4  |-  ( exp  |`  ran  log ) : ran  log -1-1-onto-> ( CC  \  {
0 } )
9 f1ocnvfv2 6069 . . . 4  |-  ( ( ( exp  |`  ran  log ) : ran  log -1-1-onto-> ( CC  \  {
0 } )  /\  A  e.  ( CC  \  { 0 } ) )  ->  ( ( exp  |`  ran  log ) `  ( `' ( exp  |`  ran  log ) `  A ) )  =  A )
108, 9mpan 670 . . 3  |-  ( A  e.  ( CC  \  { 0 } )  ->  ( ( exp  |`  ran  log ) `  ( `' ( exp  |`  ran  log ) `  A )
)  =  A )
117, 10sylbir 213 . 2  |-  ( ( A  e.  CC  /\  A  =/=  0 )  -> 
( ( exp  |`  ran  log ) `  ( `' ( exp  |`  ran  log ) `  A ) )  =  A )
123, 6, 113eqtr3a 2514 1  |-  ( ( A  e.  CC  /\  A  =/=  0 )  -> 
( exp `  ( log `  A ) )  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1370    e. wcel 1757    =/= wne 2641    \ cdif 3409   {csn 3961   `'ccnv 4923   ran crn 4925    |` cres 4926   -1-1-onto->wf1o 5501   ` cfv 5502   CCcc 9367   0cc0 9369   expce 13435   logclog 22108
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-rep 4487  ax-sep 4497  ax-nul 4505  ax-pow 4554  ax-pr 4615  ax-un 6458  ax-inf2 7934  ax-cnex 9425  ax-resscn 9426  ax-1cn 9427  ax-icn 9428  ax-addcl 9429  ax-addrcl 9430  ax-mulcl 9431  ax-mulrcl 9432  ax-mulcom 9433  ax-addass 9434  ax-mulass 9435  ax-distr 9436  ax-i2m1 9437  ax-1ne0 9438  ax-1rid 9439  ax-rnegex 9440  ax-rrecex 9441  ax-cnre 9442  ax-pre-lttri 9443  ax-pre-lttrn 9444  ax-pre-ltadd 9445  ax-pre-mulgt0 9446  ax-pre-sup 9447  ax-addf 9448  ax-mulf 9449
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-fal 1376  df-ex 1588  df-nf 1591  df-sb 1702  df-eu 2263  df-mo 2264  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-nel 2644  df-ral 2797  df-rex 2798  df-reu 2799  df-rmo 2800  df-rab 2801  df-v 3056  df-sbc 3271  df-csb 3373  df-dif 3415  df-un 3417  df-in 3419  df-ss 3426  df-pss 3428  df-nul 3722  df-if 3876  df-pw 3946  df-sn 3962  df-pr 3964  df-tp 3966  df-op 3968  df-uni 4176  df-int 4213  df-iun 4257  df-iin 4258  df-br 4377  df-opab 4435  df-mpt 4436  df-tr 4470  df-eprel 4716  df-id 4720  df-po 4725  df-so 4726  df-fr 4763  df-se 4764  df-we 4765  df-ord 4806  df-on 4807  df-lim 4808  df-suc 4809  df-xp 4930  df-rel 4931  df-cnv 4932  df-co 4933  df-dm 4934  df-rn 4935  df-res 4936  df-ima 4937  df-iota 5465  df-fun 5504  df-fn 5505  df-f 5506  df-f1 5507  df-fo 5508  df-f1o 5509  df-fv 5510  df-isom 5511  df-riota 6137  df-ov 6179  df-oprab 6180  df-mpt2 6181  df-of 6406  df-om 6563  df-1st 6663  df-2nd 6664  df-supp 6777  df-recs 6918  df-rdg 6952  df-1o 7006  df-2o 7007  df-oadd 7010  df-er 7187  df-map 7302  df-pm 7303  df-ixp 7350  df-en 7397  df-dom 7398  df-sdom 7399  df-fin 7400  df-fsupp 7708  df-fi 7748  df-sup 7778  df-oi 7811  df-card 8196  df-cda 8424  df-pnf 9507  df-mnf 9508  df-xr 9509  df-ltxr 9510  df-le 9511  df-sub 9684  df-neg 9685  df-div 10081  df-nn 10410  df-2 10467  df-3 10468  df-4 10469  df-5 10470  df-6 10471  df-7 10472  df-8 10473  df-9 10474  df-10 10475  df-n0 10667  df-z 10734  df-dec 10843  df-uz 10949  df-q 11041  df-rp 11079  df-xneg 11176  df-xadd 11177  df-xmul 11178  df-ioo 11391  df-ioc 11392  df-ico 11393  df-icc 11394  df-fz 11525  df-fzo 11636  df-fl 11729  df-mod 11796  df-seq 11894  df-exp 11953  df-fac 12139  df-bc 12166  df-hash 12191  df-shft 12644  df-cj 12676  df-re 12677  df-im 12678  df-sqr 12812  df-abs 12813  df-limsup 13037  df-clim 13054  df-rlim 13055  df-sum 13252  df-ef 13441  df-sin 13443  df-cos 13444  df-pi 13446  df-struct 14264  df-ndx 14265  df-slot 14266  df-base 14267  df-sets 14268  df-ress 14269  df-plusg 14339  df-mulr 14340  df-starv 14341  df-sca 14342  df-vsca 14343  df-ip 14344  df-tset 14345  df-ple 14346  df-ds 14348  df-unif 14349  df-hom 14350  df-cco 14351  df-rest 14449  df-topn 14450  df-0g 14468  df-gsum 14469  df-topgen 14470  df-pt 14471  df-prds 14474  df-xrs 14528  df-qtop 14533  df-imas 14534  df-xps 14536  df-mre 14612  df-mrc 14613  df-acs 14615  df-mnd 15503  df-submnd 15553  df-mulg 15636  df-cntz 15923  df-cmn 16369  df-psmet 17904  df-xmet 17905  df-met 17906  df-bl 17907  df-mopn 17908  df-fbas 17909  df-fg 17910  df-cnfld 17914  df-top 18605  df-bases 18607  df-topon 18608  df-topsp 18609  df-cld 18725  df-ntr 18726  df-cls 18727  df-nei 18804  df-lp 18842  df-perf 18843  df-cn 18933  df-cnp 18934  df-haus 19021  df-tx 19237  df-hmeo 19430  df-fil 19521  df-fm 19613  df-flim 19614  df-flf 19615  df-xms 19997  df-ms 19998  df-tms 19999  df-cncf 20556  df-limc 21443  df-dv 21444  df-log 22110
This theorem is referenced by:  reeflog  22131  lognegb  22140  explog  22144  relog  22147  eflogeq  22152  logcj  22157  efiarg  22158  logimul  22165  logneg2  22166  logmul2  22167  logdiv2  22168  logcnlem4  22192  cxpeq  22297  ang180lem1  22307  logrec  22317  asinneg  22383  efiasin  22385  efiatan2  22414  2efiatan  22415  atantan  22420  birthdaylem2  22448  logeq0im1  26573  logccne0OLD  26574  gamcvg  27162  gamp1  27164  gamcvg2lem  27165  iprodgam  27626  stirlinglem14  30006
  Copyright terms: Public domain W3C validator