Metamath Proof Explorer


Theorem harmonicbnd

Description: A bound on the harmonic series, as compared to the natural logarithm. (Contributed by Mario Carneiro, 9-Apr-2016)

Ref Expression
Assertion harmonicbnd Nm=1N1mlogNγ1

Proof

Step Hyp Ref Expression
1 oveq2 n=N1n=1N
2 1 sumeq1d n=Nm=1n1m=m=1N1m
3 fveq2 n=Nlogn=logN
4 2 3 oveq12d n=Nm=1n1mlogn=m=1N1mlogN
5 4 eleq1d n=Nm=1n1mlognγ1m=1N1mlogNγ1
6 eqid nm=1n1mlogn=nm=1n1mlogn
7 eqid nm=1n1mlogn+1=nm=1n1mlogn+1
8 eqid nlog1+1n=nlog1+1n
9 oveq2 k=n1k=1n
10 9 oveq2d k=n1+1k=1+1n
11 10 fveq2d k=nlog1+1k=log1+1n
12 9 11 oveq12d k=n1klog1+1k=1nlog1+1n
13 12 cbvmptv k1klog1+1k=n1nlog1+1n
14 6 7 8 13 emcllem7 γ1log21nm=1n1mlogn:γ1nm=1n1mlogn+1:1log2γ
15 14 simp2i nm=1n1mlogn:γ1
16 6 fmpt nm=1n1mlognγ1nm=1n1mlogn:γ1
17 15 16 mpbir nm=1n1mlognγ1
18 5 17 vtoclri Nm=1N1mlogNγ1