Metamath Proof Explorer

Theorem emcllem4

Description: Lemma for emcl . The difference between series F and G tends to zero. (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 ) ) ) )
emcl.3 
|- H = ( n e. NN |-> ( log ` ( 1 + ( 1 / n ) ) ) )
Assertion emcllem4 
|- H ~~> 0

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 emcl.3 
 |-  H = ( n e. NN |-> ( log ` ( 1 + ( 1 / n ) ) ) )
4 nnuz 
 |-  NN = ( ZZ>= ` 1 )
5 1zzd 
 |-  ( T. -> 1 e. ZZ )
6 ax-1cn 
 |-  1 e. CC
7 divcnv 
 |-  ( 1 e. CC -> ( n e. NN |-> ( 1 / n ) ) ~~> 0 )
8 6 7 mp1i 
 |-  ( T. -> ( n e. NN |-> ( 1 / n ) ) ~~> 0 )
9 nnex 
 |-  NN e. _V
10 9 mptex 
 |-  ( n e. NN |-> ( log ` ( 1 + ( 1 / n ) ) ) ) e. _V
11 3 10 eqeltri 
 |-  H e. _V
12 11 a1i 
 |-  ( T. -> H e. _V )
13 oveq2 
 |-  ( n = m -> ( 1 / n ) = ( 1 / m ) )
14 eqid 
 |-  ( n e. NN |-> ( 1 / n ) ) = ( n e. NN |-> ( 1 / n ) )
15 ovex 
 |-  ( 1 / m ) e. _V
16 13 14 15 fvmpt 
 |-  ( m e. NN -> ( ( n e. NN |-> ( 1 / n ) ) ` m ) = ( 1 / m ) )
17 16 adantl 
 |-  ( ( T. /\ m e. NN ) -> ( ( n e. NN |-> ( 1 / n ) ) ` m ) = ( 1 / m ) )
18 nnrecre 
 |-  ( m e. NN -> ( 1 / m ) e. RR )
19 18 adantl 
 |-  ( ( T. /\ m e. NN ) -> ( 1 / m ) e. RR )
20 17 19 eqeltrd 
 |-  ( ( T. /\ m e. NN ) -> ( ( n e. NN |-> ( 1 / n ) ) ` m ) e. RR )
21 13 oveq2d 
 |-  ( n = m -> ( 1 + ( 1 / n ) ) = ( 1 + ( 1 / m ) ) )
22 21 fveq2d 
 |-  ( n = m -> ( log ` ( 1 + ( 1 / n ) ) ) = ( log ` ( 1 + ( 1 / m ) ) ) )
23 fvex 
 |-  ( log ` ( 1 + ( 1 / m ) ) ) e. _V
24 22 3 23 fvmpt 
 |-  ( m e. NN -> ( H ` m ) = ( log ` ( 1 + ( 1 / m ) ) ) )
25 24 adantl 
 |-  ( ( T. /\ m e. NN ) -> ( H ` m ) = ( log ` ( 1 + ( 1 / m ) ) ) )
26 1rp 
 |-  1 e. RR+
27 nnrp 
 |-  ( m e. NN -> m e. RR+ )
28 27 adantl 
 |-  ( ( T. /\ m e. NN ) -> m e. RR+ )
29 28 rpreccld 
 |-  ( ( T. /\ m e. NN ) -> ( 1 / m ) e. RR+ )
30 rpaddcl 
 |-  ( ( 1 e. RR+ /\ ( 1 / m ) e. RR+ ) -> ( 1 + ( 1 / m ) ) e. RR+ )
31 26 29 30 sylancr 
 |-  ( ( T. /\ m e. NN ) -> ( 1 + ( 1 / m ) ) e. RR+ )
32 31 rpred 
 |-  ( ( T. /\ m e. NN ) -> ( 1 + ( 1 / m ) ) e. RR )
33 1re 
 |-  1 e. RR
34 ltaddrp 
 |-  ( ( 1 e. RR /\ ( 1 / m ) e. RR+ ) -> 1 < ( 1 + ( 1 / m ) ) )
35 33 29 34 sylancr 
 |-  ( ( T. /\ m e. NN ) -> 1 < ( 1 + ( 1 / m ) ) )
36 32 35 rplogcld 
 |-  ( ( T. /\ m e. NN ) -> ( log ` ( 1 + ( 1 / m ) ) ) e. RR+ )
37 25 36 eqeltrd 
 |-  ( ( T. /\ m e. NN ) -> ( H ` m ) e. RR+ )
38 37 rpred 
 |-  ( ( T. /\ m e. NN ) -> ( H ` m ) e. RR )
39 31 relogcld 
 |-  ( ( T. /\ m e. NN ) -> ( log ` ( 1 + ( 1 / m ) ) ) e. RR )
40 efgt1p 
 |-  ( ( 1 / m ) e. RR+ -> ( 1 + ( 1 / m ) ) < ( exp ` ( 1 / m ) ) )
41 29 40 syl 
 |-  ( ( T. /\ m e. NN ) -> ( 1 + ( 1 / m ) ) < ( exp ` ( 1 / m ) ) )
42 19 rpefcld 
 |-  ( ( T. /\ m e. NN ) -> ( exp ` ( 1 / m ) ) e. RR+ )
43 logltb 
 |-  ( ( ( 1 + ( 1 / m ) ) e. RR+ /\ ( exp ` ( 1 / m ) ) e. RR+ ) -> ( ( 1 + ( 1 / m ) ) < ( exp ` ( 1 / m ) ) <-> ( log ` ( 1 + ( 1 / m ) ) ) < ( log ` ( exp ` ( 1 / m ) ) ) ) )
44 31 42 43 syl2anc 
 |-  ( ( T. /\ m e. NN ) -> ( ( 1 + ( 1 / m ) ) < ( exp ` ( 1 / m ) ) <-> ( log ` ( 1 + ( 1 / m ) ) ) < ( log ` ( exp ` ( 1 / m ) ) ) ) )
45 41 44 mpbid 
 |-  ( ( T. /\ m e. NN ) -> ( log ` ( 1 + ( 1 / m ) ) ) < ( log ` ( exp ` ( 1 / m ) ) ) )
46 19 relogefd 
 |-  ( ( T. /\ m e. NN ) -> ( log ` ( exp ` ( 1 / m ) ) ) = ( 1 / m ) )
47 45 46 breqtrd 
 |-  ( ( T. /\ m e. NN ) -> ( log ` ( 1 + ( 1 / m ) ) ) < ( 1 / m ) )
48 39 19 47 ltled 
 |-  ( ( T. /\ m e. NN ) -> ( log ` ( 1 + ( 1 / m ) ) ) <_ ( 1 / m ) )
49 48 25 17 3brtr4d 
 |-  ( ( T. /\ m e. NN ) -> ( H ` m ) <_ ( ( n e. NN |-> ( 1 / n ) ) ` m ) )
50 37 rpge0d 
 |-  ( ( T. /\ m e. NN ) -> 0 <_ ( H ` m ) )
51 4 5 8 12 20 38 49 50 climsqz2 
 |-  ( T. -> H ~~> 0 )
52 51 mptru 
 |-  H ~~> 0