| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > harmonicbnd3 | Structured version Visualization version GIF version | ||
| Description: A bound on the harmonic series, as compared to the natural logarithm. (Contributed by Mario Carneiro, 13-Apr-2016.) |
| Ref | Expression |
|---|---|
| harmonicbnd3 | ⊢ (𝑁 ∈ ℕ0 → (Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) − (log‘(𝑁 + 1))) ∈ (0[,]γ)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elnn0 12392 | . 2 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0)) | |
| 2 | 0re 11123 | . . . . 5 ⊢ 0 ∈ ℝ | |
| 3 | emre 26946 | . . . . 5 ⊢ γ ∈ ℝ | |
| 4 | 2re 12208 | . . . . . . . . 9 ⊢ 2 ∈ ℝ | |
| 5 | ere 16000 | . . . . . . . . 9 ⊢ e ∈ ℝ | |
| 6 | egt2lt3 16119 | . . . . . . . . . 10 ⊢ (2 < e ∧ e < 3) | |
| 7 | 6 | simpli 483 | . . . . . . . . 9 ⊢ 2 < e |
| 8 | 4, 5, 7 | ltleii 11245 | . . . . . . . 8 ⊢ 2 ≤ e |
| 9 | 2rp 12899 | . . . . . . . . 9 ⊢ 2 ∈ ℝ+ | |
| 10 | epr 16121 | . . . . . . . . 9 ⊢ e ∈ ℝ+ | |
| 11 | logleb 26542 | . . . . . . . . 9 ⊢ ((2 ∈ ℝ+ ∧ e ∈ ℝ+) → (2 ≤ e ↔ (log‘2) ≤ (log‘e))) | |
| 12 | 9, 10, 11 | mp2an 692 | . . . . . . . 8 ⊢ (2 ≤ e ↔ (log‘2) ≤ (log‘e)) |
| 13 | 8, 12 | mpbi 230 | . . . . . . 7 ⊢ (log‘2) ≤ (log‘e) |
| 14 | loge 26525 | . . . . . . 7 ⊢ (log‘e) = 1 | |
| 15 | 13, 14 | breqtri 5120 | . . . . . 6 ⊢ (log‘2) ≤ 1 |
| 16 | 1re 11121 | . . . . . . 7 ⊢ 1 ∈ ℝ | |
| 17 | relogcl 26514 | . . . . . . . 8 ⊢ (2 ∈ ℝ+ → (log‘2) ∈ ℝ) | |
| 18 | 9, 17 | ax-mp 5 | . . . . . . 7 ⊢ (log‘2) ∈ ℝ |
| 19 | 16, 18 | subge0i 11679 | . . . . . 6 ⊢ (0 ≤ (1 − (log‘2)) ↔ (log‘2) ≤ 1) |
| 20 | 15, 19 | mpbir 231 | . . . . 5 ⊢ 0 ≤ (1 − (log‘2)) |
| 21 | 3 | leidi 11660 | . . . . 5 ⊢ γ ≤ γ |
| 22 | iccss 13318 | . . . . 5 ⊢ (((0 ∈ ℝ ∧ γ ∈ ℝ) ∧ (0 ≤ (1 − (log‘2)) ∧ γ ≤ γ)) → ((1 − (log‘2))[,]γ) ⊆ (0[,]γ)) | |
| 23 | 2, 3, 20, 21, 22 | mp4an 693 | . . . 4 ⊢ ((1 − (log‘2))[,]γ) ⊆ (0[,]γ) |
| 24 | harmonicbnd2 26945 | . . . 4 ⊢ (𝑁 ∈ ℕ → (Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) − (log‘(𝑁 + 1))) ∈ ((1 − (log‘2))[,]γ)) | |
| 25 | 23, 24 | sselid 3928 | . . 3 ⊢ (𝑁 ∈ ℕ → (Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) − (log‘(𝑁 + 1))) ∈ (0[,]γ)) |
| 26 | oveq2 7362 | . . . . . . . . 9 ⊢ (𝑁 = 0 → (1...𝑁) = (1...0)) | |
| 27 | fz10 13449 | . . . . . . . . 9 ⊢ (1...0) = ∅ | |
| 28 | 26, 27 | eqtrdi 2784 | . . . . . . . 8 ⊢ (𝑁 = 0 → (1...𝑁) = ∅) |
| 29 | 28 | sumeq1d 15611 | . . . . . . 7 ⊢ (𝑁 = 0 → Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) = Σ𝑚 ∈ ∅ (1 / 𝑚)) |
| 30 | sum0 15632 | . . . . . . 7 ⊢ Σ𝑚 ∈ ∅ (1 / 𝑚) = 0 | |
| 31 | 29, 30 | eqtrdi 2784 | . . . . . 6 ⊢ (𝑁 = 0 → Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) = 0) |
| 32 | fv0p1e1 12252 | . . . . . . 7 ⊢ (𝑁 = 0 → (log‘(𝑁 + 1)) = (log‘1)) | |
| 33 | log1 26524 | . . . . . . 7 ⊢ (log‘1) = 0 | |
| 34 | 32, 33 | eqtrdi 2784 | . . . . . 6 ⊢ (𝑁 = 0 → (log‘(𝑁 + 1)) = 0) |
| 35 | 31, 34 | oveq12d 7372 | . . . . 5 ⊢ (𝑁 = 0 → (Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) − (log‘(𝑁 + 1))) = (0 − 0)) |
| 36 | 0m0e0 12249 | . . . . 5 ⊢ (0 − 0) = 0 | |
| 37 | 35, 36 | eqtrdi 2784 | . . . 4 ⊢ (𝑁 = 0 → (Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) − (log‘(𝑁 + 1))) = 0) |
| 38 | 2 | leidi 11660 | . . . . 5 ⊢ 0 ≤ 0 |
| 39 | emgt0 26947 | . . . . . 6 ⊢ 0 < γ | |
| 40 | 2, 3, 39 | ltleii 11245 | . . . . 5 ⊢ 0 ≤ γ |
| 41 | 2, 3 | elicc2i 13316 | . . . . 5 ⊢ (0 ∈ (0[,]γ) ↔ (0 ∈ ℝ ∧ 0 ≤ 0 ∧ 0 ≤ γ)) |
| 42 | 2, 38, 40, 41 | mpbir3an 1342 | . . . 4 ⊢ 0 ∈ (0[,]γ) |
| 43 | 37, 42 | eqeltrdi 2841 | . . 3 ⊢ (𝑁 = 0 → (Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) − (log‘(𝑁 + 1))) ∈ (0[,]γ)) |
| 44 | 25, 43 | jaoi 857 | . 2 ⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → (Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) − (log‘(𝑁 + 1))) ∈ (0[,]γ)) |
| 45 | 1, 44 | sylbi 217 | 1 ⊢ (𝑁 ∈ ℕ0 → (Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) − (log‘(𝑁 + 1))) ∈ (0[,]γ)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∨ wo 847 = wceq 1541 ∈ wcel 2113 ⊆ wss 3898 ∅c0 4282 class class class wbr 5095 ‘cfv 6488 (class class class)co 7354 ℝcr 11014 0cc0 11015 1c1 11016 + caddc 11018 < clt 11155 ≤ cle 11156 − cmin 11353 / cdiv 11783 ℕcn 12134 2c2 12189 3c3 12190 ℕ0cn0 12390 ℝ+crp 12894 [,]cicc 13252 ...cfz 13411 Σcsu 15597 eceu 15973 logclog 26493 γcem 26932 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7676 ax-inf2 9540 ax-cnex 11071 ax-resscn 11072 ax-1cn 11073 ax-icn 11074 ax-addcl 11075 ax-addrcl 11076 ax-mulcl 11077 ax-mulrcl 11078 ax-mulcom 11079 ax-addass 11080 ax-mulass 11081 ax-distr 11082 ax-i2m1 11083 ax-1ne0 11084 ax-1rid 11085 ax-rnegex 11086 ax-rrecex 11087 ax-cnre 11088 ax-pre-lttri 11089 ax-pre-lttrn 11090 ax-pre-ltadd 11091 ax-pre-mulgt0 11092 ax-pre-sup 11093 ax-addf 11094 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-rmo 3347 df-reu 3348 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4283 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-tp 4582 df-op 4584 df-uni 4861 df-int 4900 df-iun 4945 df-iin 4946 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-se 5575 df-we 5576 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-pred 6255 df-ord 6316 df-on 6317 df-lim 6318 df-suc 6319 df-iota 6444 df-fun 6490 df-fn 6491 df-f 6492 df-f1 6493 df-fo 6494 df-f1o 6495 df-fv 6496 df-isom 6497 df-riota 7311 df-ov 7357 df-oprab 7358 df-mpo 7359 df-of 7618 df-om 7805 df-1st 7929 df-2nd 7930 df-supp 8099 df-frecs 8219 df-wrecs 8250 df-recs 8299 df-rdg 8337 df-1o 8393 df-2o 8394 df-oadd 8397 df-er 8630 df-map 8760 df-pm 8761 df-ixp 8830 df-en 8878 df-dom 8879 df-sdom 8880 df-fin 8881 df-fsupp 9255 df-fi 9304 df-sup 9335 df-inf 9336 df-oi 9405 df-card 9841 df-pnf 11157 df-mnf 11158 df-xr 11159 df-ltxr 11160 df-le 11161 df-sub 11355 df-neg 11356 df-div 11784 df-nn 12135 df-2 12197 df-3 12198 df-4 12199 df-5 12200 df-6 12201 df-7 12202 df-8 12203 df-9 12204 df-n0 12391 df-xnn0 12464 df-z 12478 df-dec 12597 df-uz 12741 df-q 12851 df-rp 12895 df-xneg 13015 df-xadd 13016 df-xmul 13017 df-ioo 13253 df-ioc 13254 df-ico 13255 df-icc 13256 df-fz 13412 df-fzo 13559 df-fl 13700 df-mod 13778 df-seq 13913 df-exp 13973 df-fac 14185 df-bc 14214 df-hash 14242 df-shft 14978 df-cj 15010 df-re 15011 df-im 15012 df-sqrt 15146 df-abs 15147 df-limsup 15382 df-clim 15399 df-rlim 15400 df-sum 15598 df-ef 15978 df-e 15979 df-sin 15980 df-cos 15981 df-tan 15982 df-pi 15983 df-dvds 16168 df-struct 17062 df-sets 17079 df-slot 17097 df-ndx 17109 df-base 17125 df-ress 17146 df-plusg 17178 df-mulr 17179 df-starv 17180 df-sca 17181 df-vsca 17182 df-ip 17183 df-tset 17184 df-ple 17185 df-ds 17187 df-unif 17188 df-hom 17189 df-cco 17190 df-rest 17330 df-topn 17331 df-0g 17349 df-gsum 17350 df-topgen 17351 df-pt 17352 df-prds 17355 df-xrs 17410 df-qtop 17415 df-imas 17416 df-xps 17418 df-mre 17492 df-mrc 17493 df-acs 17495 df-mgm 18552 df-sgrp 18631 df-mnd 18647 df-submnd 18696 df-mulg 18985 df-cntz 19233 df-cmn 19698 df-psmet 21287 df-xmet 21288 df-met 21289 df-bl 21290 df-mopn 21291 df-fbas 21292 df-fg 21293 df-cnfld 21296 df-top 22812 df-topon 22829 df-topsp 22851 df-bases 22864 df-cld 22937 df-ntr 22938 df-cls 22939 df-nei 23016 df-lp 23054 df-perf 23055 df-cn 23145 df-cnp 23146 df-haus 23233 df-cmp 23305 df-tx 23480 df-hmeo 23673 df-fil 23764 df-fm 23856 df-flim 23857 df-flf 23858 df-xms 24238 df-ms 24239 df-tms 24240 df-cncf 24801 df-limc 25797 df-dv 25798 df-ulm 26316 df-log 26495 df-atan 26807 df-em 26933 |
| This theorem is referenced by: harmoniclbnd 26949 harmonicbnd4 26951 logdivbnd 27497 |
| Copyright terms: Public domain | W3C validator |