Description: A bound on the harmonic series, as compared to the natural logarithm. (Contributed by Mario Carneiro, 13-Apr-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | harmonicubnd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fzfid | |
|
2 | elfznn | |
|
3 | 2 | adantl | |
4 | 3 | nnrecred | |
5 | 1 4 | fsumrecl | |
6 | flge1nn | |
|
7 | 6 | nnrpd | |
8 | 7 | relogcld | |
9 | peano2re | |
|
10 | 8 9 | syl | |
11 | simpl | |
|
12 | 0red | |
|
13 | 1re | |
|
14 | 13 | a1i | |
15 | 0lt1 | |
|
16 | 15 | a1i | |
17 | simpr | |
|
18 | 12 14 11 16 17 | ltletrd | |
19 | 11 18 | elrpd | |
20 | 19 | relogcld | |
21 | peano2re | |
|
22 | 20 21 | syl | |
23 | harmonicbnd | |
|
24 | 6 23 | syl | |
25 | emre | |
|
26 | 25 13 | elicc2i | |
27 | 26 | simp3bi | |
28 | 24 27 | syl | |
29 | 5 8 14 | lesubadd2d | |
30 | 28 29 | mpbid | |
31 | flle | |
|
32 | 31 | adantr | |
33 | 7 19 | logled | |
34 | 32 33 | mpbid | |
35 | 8 20 14 34 | leadd1dd | |
36 | 5 10 22 30 35 | letrd | |