Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > loge | Structured version Visualization version GIF version |
Description: The natural logarithm of e. One case of Property 1b of [Cohen] p. 301. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
Ref | Expression |
---|---|
loge | ⊢ (log‘e) = 1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-e 15517 | . . 3 ⊢ e = (exp‘1) | |
2 | 1 | eqcomi 2748 | . 2 ⊢ (exp‘1) = e |
3 | epr 15656 | . . 3 ⊢ e ∈ ℝ+ | |
4 | 1re 10722 | . . 3 ⊢ 1 ∈ ℝ | |
5 | relogeftb 25331 | . . 3 ⊢ ((e ∈ ℝ+ ∧ 1 ∈ ℝ) → ((log‘e) = 1 ↔ (exp‘1) = e)) | |
6 | 3, 4, 5 | mp2an 692 | . 2 ⊢ ((log‘e) = 1 ↔ (exp‘1) = e) |
7 | 2, 6 | mpbir 234 | 1 ⊢ (log‘e) = 1 |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 = wceq 1542 ∈ wcel 2114 ‘cfv 6340 ℝcr 10617 1c1 10619 ℝ+crp 12475 expce 15510 eceu 15511 logclog 25301 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2711 ax-rep 5155 ax-sep 5168 ax-nul 5175 ax-pow 5233 ax-pr 5297 ax-un 7482 ax-inf2 9180 ax-cnex 10674 ax-resscn 10675 ax-1cn 10676 ax-icn 10677 ax-addcl 10678 ax-addrcl 10679 ax-mulcl 10680 ax-mulrcl 10681 ax-mulcom 10682 ax-addass 10683 ax-mulass 10684 ax-distr 10685 ax-i2m1 10686 ax-1ne0 10687 ax-1rid 10688 ax-rnegex 10689 ax-rrecex 10690 ax-cnre 10691 ax-pre-lttri 10692 ax-pre-lttrn 10693 ax-pre-ltadd 10694 ax-pre-mulgt0 10695 ax-pre-sup 10696 ax-addf 10697 ax-mulf 10698 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2075 df-mo 2541 df-eu 2571 df-clab 2718 df-cleq 2731 df-clel 2812 df-nfc 2882 df-ne 2936 df-nel 3040 df-ral 3059 df-rex 3060 df-reu 3061 df-rmo 3062 df-rab 3063 df-v 3401 df-sbc 3682 df-csb 3792 df-dif 3847 df-un 3849 df-in 3851 df-ss 3861 df-pss 3863 df-nul 4213 df-if 4416 df-pw 4491 df-sn 4518 df-pr 4520 df-tp 4522 df-op 4524 df-uni 4798 df-int 4838 df-iun 4884 df-iin 4885 df-br 5032 df-opab 5094 df-mpt 5112 df-tr 5138 df-id 5430 df-eprel 5435 df-po 5443 df-so 5444 df-fr 5484 df-se 5485 df-we 5486 df-xp 5532 df-rel 5533 df-cnv 5534 df-co 5535 df-dm 5536 df-rn 5537 df-res 5538 df-ima 5539 df-pred 6130 df-ord 6176 df-on 6177 df-lim 6178 df-suc 6179 df-iota 6298 df-fun 6342 df-fn 6343 df-f 6344 df-f1 6345 df-fo 6346 df-f1o 6347 df-fv 6348 df-isom 6349 df-riota 7130 df-ov 7176 df-oprab 7177 df-mpo 7178 df-of 7428 df-om 7603 df-1st 7717 df-2nd 7718 df-supp 7860 df-wrecs 7979 df-recs 8040 df-rdg 8078 df-1o 8134 df-2o 8135 df-er 8323 df-map 8442 df-pm 8443 df-ixp 8511 df-en 8559 df-dom 8560 df-sdom 8561 df-fin 8562 df-fsupp 8910 df-fi 8951 df-sup 8982 df-inf 8983 df-oi 9050 df-card 9444 df-pnf 10758 df-mnf 10759 df-xr 10760 df-ltxr 10761 df-le 10762 df-sub 10953 df-neg 10954 df-div 11379 df-nn 11720 df-2 11782 df-3 11783 df-4 11784 df-5 11785 df-6 11786 df-7 11787 df-8 11788 df-9 11789 df-n0 11980 df-z 12066 df-dec 12183 df-uz 12328 df-q 12434 df-rp 12476 df-xneg 12593 df-xadd 12594 df-xmul 12595 df-ioo 12828 df-ioc 12829 df-ico 12830 df-icc 12831 df-fz 12985 df-fzo 13128 df-fl 13256 df-mod 13332 df-seq 13464 df-exp 13525 df-fac 13729 df-bc 13758 df-hash 13786 df-shft 14519 df-cj 14551 df-re 14552 df-im 14553 df-sqrt 14687 df-abs 14688 df-limsup 14921 df-clim 14938 df-rlim 14939 df-sum 15139 df-ef 15516 df-e 15517 df-sin 15518 df-cos 15519 df-pi 15521 df-struct 16591 df-ndx 16592 df-slot 16593 df-base 16595 df-sets 16596 df-ress 16597 df-plusg 16684 df-mulr 16685 df-starv 16686 df-sca 16687 df-vsca 16688 df-ip 16689 df-tset 16690 df-ple 16691 df-ds 16693 df-unif 16694 df-hom 16695 df-cco 16696 df-rest 16802 df-topn 16803 df-0g 16821 df-gsum 16822 df-topgen 16823 df-pt 16824 df-prds 16827 df-xrs 16881 df-qtop 16886 df-imas 16887 df-xps 16889 df-mre 16963 df-mrc 16964 df-acs 16966 df-mgm 17971 df-sgrp 18020 df-mnd 18031 df-submnd 18076 df-mulg 18346 df-cntz 18568 df-cmn 19029 df-psmet 20212 df-xmet 20213 df-met 20214 df-bl 20215 df-mopn 20216 df-fbas 20217 df-fg 20218 df-cnfld 20221 df-top 21648 df-topon 21665 df-topsp 21687 df-bases 21700 df-cld 21773 df-ntr 21774 df-cls 21775 df-nei 21852 df-lp 21890 df-perf 21891 df-cn 21981 df-cnp 21982 df-haus 22069 df-tx 22316 df-hmeo 22509 df-fil 22600 df-fm 22692 df-flim 22693 df-flf 22694 df-xms 23076 df-ms 23077 df-tms 23078 df-cncf 23633 df-limc 24621 df-dv 24622 df-log 25303 |
This theorem is referenced by: logle1b 25379 loglt1b 25380 ecxp 25419 elogb 25511 logblog 25533 cxploglim2 25719 harmonicbnd3 25748 chebbnd1lem3 26210 chebbnd1 26211 mulog2sumlem1 26273 mulog2sumlem2 26274 selberg3lem1 26296 pntpbnd1a 26324 pntpbnd2 26326 pntlemk 26345 hgt750lem 32204 stirlinglem4 43183 etransclem46 43386 |
Copyright terms: Public domain | W3C validator |