Metamath Proof Explorer

Theorem emcllem2

Description: Lemma for emcl . F is increasing, and G is decreasing. (Contributed by Mario Carneiro, 11-Jul-2014)

Ref Expression
Hypotheses emcl.1 
|- F = ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` n ) ) )
emcl.2 
|- G = ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` ( n + 1 ) ) ) )
Assertion emcllem2 
|- ( N e. NN -> ( ( F ` ( N + 1 ) ) <_ ( F ` N ) /\ ( G ` N ) <_ ( G ` ( N + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 emcl.1 
 |-  F = ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` n ) ) )
2 emcl.2 
 |-  G = ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` ( n + 1 ) ) ) )
3 peano2nn 
 |-  ( N e. NN -> ( N + 1 ) e. NN )
4 3 nnrecred 
 |-  ( N e. NN -> ( 1 / ( N + 1 ) ) e. RR )
5 3 nnrpd 
 |-  ( N e. NN -> ( N + 1 ) e. RR+ )
6 5 relogcld 
 |-  ( N e. NN -> ( log ` ( N + 1 ) ) e. RR )
7 nnrp 
 |-  ( N e. NN -> N e. RR+ )
8 7 relogcld 
 |-  ( N e. NN -> ( log ` N ) e. RR )
9 6 8 resubcld 
 |-  ( N e. NN -> ( ( log ` ( N + 1 ) ) - ( log ` N ) ) e. RR )
10 fzfid 
 |-  ( N e. NN -> ( 1 ... N ) e. Fin )
11 elfznn 
 |-  ( m e. ( 1 ... N ) -> m e. NN )
12 11 adantl 
 |-  ( ( N e. NN /\ m e. ( 1 ... N ) ) -> m e. NN )
13 12 nnrecred 
 |-  ( ( N e. NN /\ m e. ( 1 ... N ) ) -> ( 1 / m ) e. RR )
14 10 13 fsumrecl 
 |-  ( N e. NN -> sum_ m e. ( 1 ... N ) ( 1 / m ) e. RR )
15 5 rpreccld 
 |-  ( N e. NN -> ( 1 / ( N + 1 ) ) e. RR+ )
16 15 rpge0d 
 |-  ( N e. NN -> 0 <_ ( 1 / ( N + 1 ) ) )
17 1div1e1 
 |-  ( 1 / 1 ) = 1
18 1re 
 |-  1 e. RR
19 ltaddrp 
 |-  ( ( 1 e. RR /\ N e. RR+ ) -> 1 < ( 1 + N ) )
20 18 7 19 sylancr 
 |-  ( N e. NN -> 1 < ( 1 + N ) )
21 ax-1cn 
 |-  1 e. CC
22 nncn 
 |-  ( N e. NN -> N e. CC )
23 addcom 
 |-  ( ( 1 e. CC /\ N e. CC ) -> ( 1 + N ) = ( N + 1 ) )
24 21 22 23 sylancr 
 |-  ( N e. NN -> ( 1 + N ) = ( N + 1 ) )
25 20 24 breqtrd 
 |-  ( N e. NN -> 1 < ( N + 1 ) )
26 17 25 eqbrtrid 
 |-  ( N e. NN -> ( 1 / 1 ) < ( N + 1 ) )
27 3 nnred 
 |-  ( N e. NN -> ( N + 1 ) e. RR )
28 3 nngt0d 
 |-  ( N e. NN -> 0 < ( N + 1 ) )
29 0lt1 
 |-  0 < 1
30 ltrec1 
 |-  ( ( ( 1 e. RR /\ 0 < 1 ) /\ ( ( N + 1 ) e. RR /\ 0 < ( N + 1 ) ) ) -> ( ( 1 / 1 ) < ( N + 1 ) <-> ( 1 / ( N + 1 ) ) < 1 ) )
31 18 29 30 mpanl12 
 |-  ( ( ( N + 1 ) e. RR /\ 0 < ( N + 1 ) ) -> ( ( 1 / 1 ) < ( N + 1 ) <-> ( 1 / ( N + 1 ) ) < 1 ) )
32 27 28 31 syl2anc 
 |-  ( N e. NN -> ( ( 1 / 1 ) < ( N + 1 ) <-> ( 1 / ( N + 1 ) ) < 1 ) )
33 26 32 mpbid 
 |-  ( N e. NN -> ( 1 / ( N + 1 ) ) < 1 )
34 4 16 33 eflegeo 
 |-  ( N e. NN -> ( exp ` ( 1 / ( N + 1 ) ) ) <_ ( 1 / ( 1 - ( 1 / ( N + 1 ) ) ) ) )
35 27 recnd 
 |-  ( N e. NN -> ( N + 1 ) e. CC )
36 nnne0 
 |-  ( N e. NN -> N =/= 0 )
37 3 nnne0d 
 |-  ( N e. NN -> ( N + 1 ) =/= 0 )
38 22 35 36 37 recdivd 
 |-  ( N e. NN -> ( 1 / ( N / ( N + 1 ) ) ) = ( ( N + 1 ) / N ) )
39 1cnd 
 |-  ( N e. NN -> 1 e. CC )
40 35 39 35 37 divsubdird 
 |-  ( N e. NN -> ( ( ( N + 1 ) - 1 ) / ( N + 1 ) ) = ( ( ( N + 1 ) / ( N + 1 ) ) - ( 1 / ( N + 1 ) ) ) )
41 pncan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - 1 ) = N )
42 22 21 41 sylancl 
 |-  ( N e. NN -> ( ( N + 1 ) - 1 ) = N )
43 42 oveq1d 
 |-  ( N e. NN -> ( ( ( N + 1 ) - 1 ) / ( N + 1 ) ) = ( N / ( N + 1 ) ) )
44 35 37 dividd 
 |-  ( N e. NN -> ( ( N + 1 ) / ( N + 1 ) ) = 1 )
45 44 oveq1d 
 |-  ( N e. NN -> ( ( ( N + 1 ) / ( N + 1 ) ) - ( 1 / ( N + 1 ) ) ) = ( 1 - ( 1 / ( N + 1 ) ) ) )
46 40 43 45 3eqtr3rd 
 |-  ( N e. NN -> ( 1 - ( 1 / ( N + 1 ) ) ) = ( N / ( N + 1 ) ) )
47 46 oveq2d 
 |-  ( N e. NN -> ( 1 / ( 1 - ( 1 / ( N + 1 ) ) ) ) = ( 1 / ( N / ( N + 1 ) ) ) )
48 5 7 rpdivcld 
 |-  ( N e. NN -> ( ( N + 1 ) / N ) e. RR+ )
49 48 reeflogd 
 |-  ( N e. NN -> ( exp ` ( log ` ( ( N + 1 ) / N ) ) ) = ( ( N + 1 ) / N ) )
50 38 47 49 3eqtr4d 
 |-  ( N e. NN -> ( 1 / ( 1 - ( 1 / ( N + 1 ) ) ) ) = ( exp ` ( log ` ( ( N + 1 ) / N ) ) ) )
51 34 50 breqtrd 
 |-  ( N e. NN -> ( exp ` ( 1 / ( N + 1 ) ) ) <_ ( exp ` ( log ` ( ( N + 1 ) / N ) ) ) )
52 5 7 relogdivd 
 |-  ( N e. NN -> ( log ` ( ( N + 1 ) / N ) ) = ( ( log ` ( N + 1 ) ) - ( log ` N ) ) )
53 52 9 eqeltrd 
 |-  ( N e. NN -> ( log ` ( ( N + 1 ) / N ) ) e. RR )
54 efle 
 |-  ( ( ( 1 / ( N + 1 ) ) e. RR /\ ( log ` ( ( N + 1 ) / N ) ) e. RR ) -> ( ( 1 / ( N + 1 ) ) <_ ( log ` ( ( N + 1 ) / N ) ) <-> ( exp ` ( 1 / ( N + 1 ) ) ) <_ ( exp ` ( log ` ( ( N + 1 ) / N ) ) ) ) )
55 4 53 54 syl2anc 
 |-  ( N e. NN -> ( ( 1 / ( N + 1 ) ) <_ ( log ` ( ( N + 1 ) / N ) ) <-> ( exp ` ( 1 / ( N + 1 ) ) ) <_ ( exp ` ( log ` ( ( N + 1 ) / N ) ) ) ) )
56 51 55 mpbird 
 |-  ( N e. NN -> ( 1 / ( N + 1 ) ) <_ ( log ` ( ( N + 1 ) / N ) ) )
57 56 52 breqtrd 
 |-  ( N e. NN -> ( 1 / ( N + 1 ) ) <_ ( ( log ` ( N + 1 ) ) - ( log ` N ) ) )
58 4 9 14 57 leadd2dd 
 |-  ( N e. NN -> ( sum_ m e. ( 1 ... N ) ( 1 / m ) + ( 1 / ( N + 1 ) ) ) <_ ( sum_ m e. ( 1 ... N ) ( 1 / m ) + ( ( log ` ( N + 1 ) ) - ( log ` N ) ) ) )
59 id 
 |-  ( N e. NN -> N e. NN )
60 nnuz 
 |-  NN = ( ZZ>= ` 1 )
61 59 60 eleqtrdi 
 |-  ( N e. NN -> N e. ( ZZ>= ` 1 ) )
62 elfznn 
 |-  ( m e. ( 1 ... ( N + 1 ) ) -> m e. NN )
63 62 adantl 
 |-  ( ( N e. NN /\ m e. ( 1 ... ( N + 1 ) ) ) -> m e. NN )
64 63 nnrecred 
 |-  ( ( N e. NN /\ m e. ( 1 ... ( N + 1 ) ) ) -> ( 1 / m ) e. RR )
65 64 recnd 
 |-  ( ( N e. NN /\ m e. ( 1 ... ( N + 1 ) ) ) -> ( 1 / m ) e. CC )
66 oveq2 
 |-  ( m = ( N + 1 ) -> ( 1 / m ) = ( 1 / ( N + 1 ) ) )
67 61 65 66 fsump1 
 |-  ( N e. NN -> sum_ m e. ( 1 ... ( N + 1 ) ) ( 1 / m ) = ( sum_ m e. ( 1 ... N ) ( 1 / m ) + ( 1 / ( N + 1 ) ) ) )
68 6 recnd 
 |-  ( N e. NN -> ( log ` ( N + 1 ) ) e. CC )
69 14 recnd 
 |-  ( N e. NN -> sum_ m e. ( 1 ... N ) ( 1 / m ) e. CC )
70 8 recnd 
 |-  ( N e. NN -> ( log ` N ) e. CC )
71 68 69 70 addsub12d 
 |-  ( N e. NN -> ( ( log ` ( N + 1 ) ) + ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` N ) ) ) = ( sum_ m e. ( 1 ... N ) ( 1 / m ) + ( ( log ` ( N + 1 ) ) - ( log ` N ) ) ) )
72 58 67 71 3brtr4d 
 |-  ( N e. NN -> sum_ m e. ( 1 ... ( N + 1 ) ) ( 1 / m ) <_ ( ( log ` ( N + 1 ) ) + ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` N ) ) ) )
73 fzfid 
 |-  ( N e. NN -> ( 1 ... ( N + 1 ) ) e. Fin )
74 73 64 fsumrecl 
 |-  ( N e. NN -> sum_ m e. ( 1 ... ( N + 1 ) ) ( 1 / m ) e. RR )
75 14 8 resubcld 
 |-  ( N e. NN -> ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` N ) ) e. RR )
76 74 6 75 lesubadd2d 
 |-  ( N e. NN -> ( ( sum_ m e. ( 1 ... ( N + 1 ) ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) <_ ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` N ) ) <-> sum_ m e. ( 1 ... ( N + 1 ) ) ( 1 / m ) <_ ( ( log ` ( N + 1 ) ) + ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` N ) ) ) ) )
77 72 76 mpbird 
 |-  ( N e. NN -> ( sum_ m e. ( 1 ... ( N + 1 ) ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) <_ ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` N ) ) )
78 oveq2 
 |-  ( n = ( N + 1 ) -> ( 1 ... n ) = ( 1 ... ( N + 1 ) ) )
79 78 sumeq1d 
 |-  ( n = ( N + 1 ) -> sum_ m e. ( 1 ... n ) ( 1 / m ) = sum_ m e. ( 1 ... ( N + 1 ) ) ( 1 / m ) )
80 fveq2 
 |-  ( n = ( N + 1 ) -> ( log ` n ) = ( log ` ( N + 1 ) ) )
81 79 80 oveq12d 
 |-  ( n = ( N + 1 ) -> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` n ) ) = ( sum_ m e. ( 1 ... ( N + 1 ) ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) )
82 ovex 
 |-  ( sum_ m e. ( 1 ... ( N + 1 ) ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) e. _V
83 81 1 82 fvmpt 
 |-  ( ( N + 1 ) e. NN -> ( F ` ( N + 1 ) ) = ( sum_ m e. ( 1 ... ( N + 1 ) ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) )
84 3 83 syl 
 |-  ( N e. NN -> ( F ` ( N + 1 ) ) = ( sum_ m e. ( 1 ... ( N + 1 ) ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) )
85 oveq2 
 |-  ( n = N -> ( 1 ... n ) = ( 1 ... N ) )
86 85 sumeq1d 
 |-  ( n = N -> sum_ m e. ( 1 ... n ) ( 1 / m ) = sum_ m e. ( 1 ... N ) ( 1 / m ) )
87 fveq2 
 |-  ( n = N -> ( log ` n ) = ( log ` N ) )
88 86 87 oveq12d 
 |-  ( n = N -> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` n ) ) = ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` N ) ) )
89 ovex 
 |-  ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` N ) ) e. _V
90 88 1 89 fvmpt 
 |-  ( N e. NN -> ( F ` N ) = ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` N ) ) )
91 77 84 90 3brtr4d 
 |-  ( N e. NN -> ( F ` ( N + 1 ) ) <_ ( F ` N ) )
92 peano2nn 
 |-  ( ( N + 1 ) e. NN -> ( ( N + 1 ) + 1 ) e. NN )
93 3 92 syl 
 |-  ( N e. NN -> ( ( N + 1 ) + 1 ) e. NN )
94 93 nnrpd 
 |-  ( N e. NN -> ( ( N + 1 ) + 1 ) e. RR+ )
95 94 relogcld 
 |-  ( N e. NN -> ( log ` ( ( N + 1 ) + 1 ) ) e. RR )
96 95 6 resubcld 
 |-  ( N e. NN -> ( ( log ` ( ( N + 1 ) + 1 ) ) - ( log ` ( N + 1 ) ) ) e. RR )
97 logdifbnd 
 |-  ( ( N + 1 ) e. RR+ -> ( ( log ` ( ( N + 1 ) + 1 ) ) - ( log ` ( N + 1 ) ) ) <_ ( 1 / ( N + 1 ) ) )
98 5 97 syl 
 |-  ( N e. NN -> ( ( log ` ( ( N + 1 ) + 1 ) ) - ( log ` ( N + 1 ) ) ) <_ ( 1 / ( N + 1 ) ) )
99 96 4 14 98 leadd2dd 
 |-  ( N e. NN -> ( sum_ m e. ( 1 ... N ) ( 1 / m ) + ( ( log ` ( ( N + 1 ) + 1 ) ) - ( log ` ( N + 1 ) ) ) ) <_ ( sum_ m e. ( 1 ... N ) ( 1 / m ) + ( 1 / ( N + 1 ) ) ) )
100 95 recnd 
 |-  ( N e. NN -> ( log ` ( ( N + 1 ) + 1 ) ) e. CC )
101 69 68 100 subadd23d 
 |-  ( N e. NN -> ( ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) + ( log ` ( ( N + 1 ) + 1 ) ) ) = ( sum_ m e. ( 1 ... N ) ( 1 / m ) + ( ( log ` ( ( N + 1 ) + 1 ) ) - ( log ` ( N + 1 ) ) ) ) )
102 99 101 67 3brtr4d 
 |-  ( N e. NN -> ( ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) + ( log ` ( ( N + 1 ) + 1 ) ) ) <_ sum_ m e. ( 1 ... ( N + 1 ) ) ( 1 / m ) )
103 14 6 resubcld 
 |-  ( N e. NN -> ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) e. RR )
104 leaddsub 
 |-  ( ( ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) e. RR /\ ( log ` ( ( N + 1 ) + 1 ) ) e. RR /\ sum_ m e. ( 1 ... ( N + 1 ) ) ( 1 / m ) e. RR ) -> ( ( ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) + ( log ` ( ( N + 1 ) + 1 ) ) ) <_ sum_ m e. ( 1 ... ( N + 1 ) ) ( 1 / m ) <-> ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) <_ ( sum_ m e. ( 1 ... ( N + 1 ) ) ( 1 / m ) - ( log ` ( ( N + 1 ) + 1 ) ) ) ) )
105 103 95 74 104 syl3anc 
 |-  ( N e. NN -> ( ( ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) + ( log ` ( ( N + 1 ) + 1 ) ) ) <_ sum_ m e. ( 1 ... ( N + 1 ) ) ( 1 / m ) <-> ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) <_ ( sum_ m e. ( 1 ... ( N + 1 ) ) ( 1 / m ) - ( log ` ( ( N + 1 ) + 1 ) ) ) ) )
106 102 105 mpbid 
 |-  ( N e. NN -> ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) <_ ( sum_ m e. ( 1 ... ( N + 1 ) ) ( 1 / m ) - ( log ` ( ( N + 1 ) + 1 ) ) ) )
107 fvoveq1 
 |-  ( n = N -> ( log ` ( n + 1 ) ) = ( log ` ( N + 1 ) ) )
108 86 107 oveq12d 
 |-  ( n = N -> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` ( n + 1 ) ) ) = ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) )
109 ovex 
 |-  ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) e. _V
110 108 2 109 fvmpt 
 |-  ( N e. NN -> ( G ` N ) = ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) )
111 fvoveq1 
 |-  ( n = ( N + 1 ) -> ( log ` ( n + 1 ) ) = ( log ` ( ( N + 1 ) + 1 ) ) )
112 79 111 oveq12d 
 |-  ( n = ( N + 1 ) -> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` ( n + 1 ) ) ) = ( sum_ m e. ( 1 ... ( N + 1 ) ) ( 1 / m ) - ( log ` ( ( N + 1 ) + 1 ) ) ) )
113 ovex 
 |-  ( sum_ m e. ( 1 ... ( N + 1 ) ) ( 1 / m ) - ( log ` ( ( N + 1 ) + 1 ) ) ) e. _V
114 112 2 113 fvmpt 
 |-  ( ( N + 1 ) e. NN -> ( G ` ( N + 1 ) ) = ( sum_ m e. ( 1 ... ( N + 1 ) ) ( 1 / m ) - ( log ` ( ( N + 1 ) + 1 ) ) ) )
115 3 114 syl 
 |-  ( N e. NN -> ( G ` ( N + 1 ) ) = ( sum_ m e. ( 1 ... ( N + 1 ) ) ( 1 / m ) - ( log ` ( ( N + 1 ) + 1 ) ) ) )
116 106 110 115 3brtr4d 
 |-  ( N e. NN -> ( G ` N ) <_ ( G ` ( N + 1 ) ) )
117 91 116 jca 
 |-  ( N e. NN -> ( ( F ` ( N + 1 ) ) <_ ( F ` N ) /\ ( G ` N ) <_ ( G ` ( N + 1 ) ) ) )