Metamath Proof Explorer


Theorem harmonicubnd

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

Ref Expression
Assertion harmonicubnd A1Am=1A1mlogA+1

Proof

Step Hyp Ref Expression
1 fzfid A1A1AFin
2 elfznn m1Am
3 2 adantl A1Am1Am
4 3 nnrecred A1Am1A1m
5 1 4 fsumrecl A1Am=1A1m
6 flge1nn A1AA
7 6 nnrpd A1AA+
8 7 relogcld A1AlogA
9 peano2re logAlogA+1
10 8 9 syl A1AlogA+1
11 simpl A1AA
12 0red A1A0
13 1re 1
14 13 a1i A1A1
15 0lt1 0<1
16 15 a1i A1A0<1
17 simpr A1A1A
18 12 14 11 16 17 ltletrd A1A0<A
19 11 18 elrpd A1AA+
20 19 relogcld A1AlogA
21 peano2re logAlogA+1
22 20 21 syl A1AlogA+1
23 harmonicbnd Am=1A1mlogAγ1
24 6 23 syl A1Am=1A1mlogAγ1
25 emre γ
26 25 13 elicc2i m=1A1mlogAγ1m=1A1mlogAγm=1A1mlogAm=1A1mlogA1
27 26 simp3bi m=1A1mlogAγ1m=1A1mlogA1
28 24 27 syl A1Am=1A1mlogA1
29 5 8 14 lesubadd2d A1Am=1A1mlogA1m=1A1mlogA+1
30 28 29 mpbid A1Am=1A1mlogA+1
31 flle AAA
32 31 adantr A1AAA
33 7 19 logled A1AAAlogAlogA
34 32 33 mpbid A1AlogAlogA
35 8 20 14 34 leadd1dd A1AlogA+1logA+1
36 5 10 22 30 35 letrd A1Am=1A1mlogA+1