![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > log1 | Structured version Visualization version GIF version |
Description: The natural logarithm of 1. One case of Property 1a of [Cohen] p. 301. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
Ref | Expression |
---|---|
log1 | ⊢ (log‘1) = 0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ef0 15265 | . 2 ⊢ (exp‘0) = 1 | |
2 | 1rp 12232 | . . 3 ⊢ 1 ∈ ℝ+ | |
3 | 0re 10478 | . . 3 ⊢ 0 ∈ ℝ | |
4 | relogeftb 24837 | . . 3 ⊢ ((1 ∈ ℝ+ ∧ 0 ∈ ℝ) → ((log‘1) = 0 ↔ (exp‘0) = 1)) | |
5 | 2, 3, 4 | mp2an 688 | . 2 ⊢ ((log‘1) = 0 ↔ (exp‘0) = 1) |
6 | 1, 5 | mpbir 232 | 1 ⊢ (log‘1) = 0 |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 = wceq 1520 ∈ wcel 2079 ‘cfv 6217 ℝcr 10371 0cc0 10372 1c1 10373 ℝ+crp 12228 expce 15236 logclog 24807 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-10 2110 ax-11 2124 ax-12 2139 ax-13 2342 ax-ext 2767 ax-rep 5075 ax-sep 5088 ax-nul 5095 ax-pow 5150 ax-pr 5214 ax-un 7310 ax-inf2 8939 ax-cnex 10428 ax-resscn 10429 ax-1cn 10430 ax-icn 10431 ax-addcl 10432 ax-addrcl 10433 ax-mulcl 10434 ax-mulrcl 10435 ax-mulcom 10436 ax-addass 10437 ax-mulass 10438 ax-distr 10439 ax-i2m1 10440 ax-1ne0 10441 ax-1rid 10442 ax-rnegex 10443 ax-rrecex 10444 ax-cnre 10445 ax-pre-lttri 10446 ax-pre-lttrn 10447 ax-pre-ltadd 10448 ax-pre-mulgt0 10449 ax-pre-sup 10450 ax-addf 10451 ax-mulf 10452 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1079 df-3an 1080 df-tru 1523 df-fal 1533 df-ex 1760 df-nf 1764 df-sb 2041 df-mo 2574 df-eu 2610 df-clab 2774 df-cleq 2786 df-clel 2861 df-nfc 2933 df-ne 2983 df-nel 3089 df-ral 3108 df-rex 3109 df-reu 3110 df-rmo 3111 df-rab 3112 df-v 3434 df-sbc 3702 df-csb 3807 df-dif 3857 df-un 3859 df-in 3861 df-ss 3869 df-pss 3871 df-nul 4207 df-if 4376 df-pw 4449 df-sn 4467 df-pr 4469 df-tp 4471 df-op 4473 df-uni 4740 df-int 4777 df-iun 4821 df-iin 4822 df-br 4957 df-opab 5019 df-mpt 5036 df-tr 5058 df-id 5340 df-eprel 5345 df-po 5354 df-so 5355 df-fr 5394 df-se 5395 df-we 5396 df-xp 5441 df-rel 5442 df-cnv 5443 df-co 5444 df-dm 5445 df-rn 5446 df-res 5447 df-ima 5448 df-pred 6015 df-ord 6061 df-on 6062 df-lim 6063 df-suc 6064 df-iota 6181 df-fun 6219 df-fn 6220 df-f 6221 df-f1 6222 df-fo 6223 df-f1o 6224 df-fv 6225 df-isom 6226 df-riota 6968 df-ov 7010 df-oprab 7011 df-mpo 7012 df-of 7258 df-om 7428 df-1st 7536 df-2nd 7537 df-supp 7673 df-wrecs 7789 df-recs 7851 df-rdg 7889 df-1o 7944 df-2o 7945 df-oadd 7948 df-er 8130 df-map 8249 df-pm 8250 df-ixp 8301 df-en 8348 df-dom 8349 df-sdom 8350 df-fin 8351 df-fsupp 8670 df-fi 8711 df-sup 8742 df-inf 8743 df-oi 8810 df-card 9203 df-pnf 10512 df-mnf 10513 df-xr 10514 df-ltxr 10515 df-le 10516 df-sub 10708 df-neg 10709 df-div 11135 df-nn 11476 df-2 11537 df-3 11538 df-4 11539 df-5 11540 df-6 11541 df-7 11542 df-8 11543 df-9 11544 df-n0 11735 df-z 11819 df-dec 11937 df-uz 12083 df-q 12187 df-rp 12229 df-xneg 12346 df-xadd 12347 df-xmul 12348 df-ioo 12581 df-ioc 12582 df-ico 12583 df-icc 12584 df-fz 12732 df-fzo 12873 df-fl 13000 df-mod 13076 df-seq 13208 df-exp 13268 df-fac 13472 df-bc 13501 df-hash 13529 df-shft 14248 df-cj 14280 df-re 14281 df-im 14282 df-sqrt 14416 df-abs 14417 df-limsup 14650 df-clim 14667 df-rlim 14668 df-sum 14865 df-ef 15242 df-sin 15244 df-cos 15245 df-pi 15247 df-struct 16302 df-ndx 16303 df-slot 16304 df-base 16306 df-sets 16307 df-ress 16308 df-plusg 16395 df-mulr 16396 df-starv 16397 df-sca 16398 df-vsca 16399 df-ip 16400 df-tset 16401 df-ple 16402 df-ds 16404 df-unif 16405 df-hom 16406 df-cco 16407 df-rest 16513 df-topn 16514 df-0g 16532 df-gsum 16533 df-topgen 16534 df-pt 16535 df-prds 16538 df-xrs 16592 df-qtop 16597 df-imas 16598 df-xps 16600 df-mre 16674 df-mrc 16675 df-acs 16677 df-mgm 17669 df-sgrp 17711 df-mnd 17722 df-submnd 17763 df-mulg 17970 df-cntz 18176 df-cmn 18623 df-psmet 20207 df-xmet 20208 df-met 20209 df-bl 20210 df-mopn 20211 df-fbas 20212 df-fg 20213 df-cnfld 20216 df-top 21174 df-topon 21191 df-topsp 21213 df-bases 21226 df-cld 21299 df-ntr 21300 df-cls 21301 df-nei 21378 df-lp 21416 df-perf 21417 df-cn 21507 df-cnp 21508 df-haus 21595 df-tx 21842 df-hmeo 22035 df-fil 22126 df-fm 22218 df-flim 22219 df-flf 22220 df-xms 22601 df-ms 22602 df-tms 22603 df-cncf 23157 df-limc 24135 df-dv 24136 df-log 24809 |
This theorem is referenced by: logm1 24841 logfac 24853 rplogcl 24856 logge0 24857 logge0b 24883 loggt0b 24884 logtayl 24912 1cxp 24924 loglesqrt 25008 logb1 25016 efrlim 25217 emcllem5 25247 emcllem7 25249 harmonicbnd3 25255 lgamgulmlem2 25277 lgamgulmlem5 25280 lgambdd 25284 lgamcvg2 25302 lgam1 25311 prmorcht 25425 vmalelog 25451 pclogsum 25461 logfacubnd 25467 logfacbnd3 25469 logfacrlim 25470 logexprlim 25471 chebbnd1lem1 25715 rpvmasumlem 25733 dchrvmasumlem2 25744 dchrvmasumiflem1 25747 dchrisum0fno1 25757 dchrisum0re 25759 dirith2 25774 mulog2sumlem2 25781 log2sumbnd 25790 selberg2lem 25796 chpdifbndlem1 25799 chpdifbndlem2 25800 logdivbnd 25802 pntrlog2bndlem5 25827 pntlemn 25846 pntlemj 25849 pntlemk 25852 ostth3 25884 xrge0iifcnv 30749 xrge0iif1 30754 reglogltb 38924 reglogleb 38925 reglog1 38929 regt1loggt0 44031 |
Copyright terms: Public domain | W3C validator |