Metamath Proof Explorer

Theorem emcllem5

Description: Lemma for emcl . The partial sums of the series T , which is used in Definition df-em , is in fact the same as G . (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 ) ) ) )
emcl.4 
|- T = ( n e. NN |-> ( ( 1 / n ) - ( log ` ( 1 + ( 1 / n ) ) ) ) )
Assertion emcllem5 
|- G = seq 1 ( + , T )

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 emcl.4 
 |-  T = ( n e. NN |-> ( ( 1 / n ) - ( log ` ( 1 + ( 1 / n ) ) ) ) )
5 elfznn 
 |-  ( m e. ( 1 ... n ) -> m e. NN )
6 5 adantl 
 |-  ( ( n e. NN /\ m e. ( 1 ... n ) ) -> m e. NN )
7 6 nncnd 
 |-  ( ( n e. NN /\ m e. ( 1 ... n ) ) -> m e. CC )
8 1cnd 
 |-  ( ( n e. NN /\ m e. ( 1 ... n ) ) -> 1 e. CC )
9 6 nnne0d 
 |-  ( ( n e. NN /\ m e. ( 1 ... n ) ) -> m =/= 0 )
10 7 8 7 9 divdird 
 |-  ( ( n e. NN /\ m e. ( 1 ... n ) ) -> ( ( m + 1 ) / m ) = ( ( m / m ) + ( 1 / m ) ) )
11 7 9 dividd 
 |-  ( ( n e. NN /\ m e. ( 1 ... n ) ) -> ( m / m ) = 1 )
12 11 oveq1d 
 |-  ( ( n e. NN /\ m e. ( 1 ... n ) ) -> ( ( m / m ) + ( 1 / m ) ) = ( 1 + ( 1 / m ) ) )
13 10 12 eqtrd 
 |-  ( ( n e. NN /\ m e. ( 1 ... n ) ) -> ( ( m + 1 ) / m ) = ( 1 + ( 1 / m ) ) )
14 13 fveq2d 
 |-  ( ( n e. NN /\ m e. ( 1 ... n ) ) -> ( log ` ( ( m + 1 ) / m ) ) = ( log ` ( 1 + ( 1 / m ) ) ) )
15 peano2nn 
 |-  ( m e. NN -> ( m + 1 ) e. NN )
16 6 15 syl 
 |-  ( ( n e. NN /\ m e. ( 1 ... n ) ) -> ( m + 1 ) e. NN )
17 16 nnrpd 
 |-  ( ( n e. NN /\ m e. ( 1 ... n ) ) -> ( m + 1 ) e. RR+ )
18 6 nnrpd 
 |-  ( ( n e. NN /\ m e. ( 1 ... n ) ) -> m e. RR+ )
19 17 18 relogdivd 
 |-  ( ( n e. NN /\ m e. ( 1 ... n ) ) -> ( log ` ( ( m + 1 ) / m ) ) = ( ( log ` ( m + 1 ) ) - ( log ` m ) ) )
20 14 19 eqtr3d 
 |-  ( ( n e. NN /\ m e. ( 1 ... n ) ) -> ( log ` ( 1 + ( 1 / m ) ) ) = ( ( log ` ( m + 1 ) ) - ( log ` m ) ) )
21 20 sumeq2dv 
 |-  ( n e. NN -> sum_ m e. ( 1 ... n ) ( log ` ( 1 + ( 1 / m ) ) ) = sum_ m e. ( 1 ... n ) ( ( log ` ( m + 1 ) ) - ( log ` m ) ) )
22 fveq2 
 |-  ( x = m -> ( log ` x ) = ( log ` m ) )
23 fveq2 
 |-  ( x = ( m + 1 ) -> ( log ` x ) = ( log ` ( m + 1 ) ) )
24 fveq2 
 |-  ( x = 1 -> ( log ` x ) = ( log ` 1 ) )
25 fveq2 
 |-  ( x = ( n + 1 ) -> ( log ` x ) = ( log ` ( n + 1 ) ) )
26 nnz 
 |-  ( n e. NN -> n e. ZZ )
27 peano2nn 
 |-  ( n e. NN -> ( n + 1 ) e. NN )
28 nnuz 
 |-  NN = ( ZZ>= ` 1 )
29 27 28 eleqtrdi 
 |-  ( n e. NN -> ( n + 1 ) e. ( ZZ>= ` 1 ) )
30 elfznn 
 |-  ( x e. ( 1 ... ( n + 1 ) ) -> x e. NN )
31 30 adantl 
 |-  ( ( n e. NN /\ x e. ( 1 ... ( n + 1 ) ) ) -> x e. NN )
32 31 nnrpd 
 |-  ( ( n e. NN /\ x e. ( 1 ... ( n + 1 ) ) ) -> x e. RR+ )
33 32 relogcld 
 |-  ( ( n e. NN /\ x e. ( 1 ... ( n + 1 ) ) ) -> ( log ` x ) e. RR )
34 33 recnd 
 |-  ( ( n e. NN /\ x e. ( 1 ... ( n + 1 ) ) ) -> ( log ` x ) e. CC )
35 22 23 24 25 26 29 34 telfsum2 
 |-  ( n e. NN -> sum_ m e. ( 1 ... n ) ( ( log ` ( m + 1 ) ) - ( log ` m ) ) = ( ( log ` ( n + 1 ) ) - ( log ` 1 ) ) )
36 log1 
 |-  ( log ` 1 ) = 0
37 36 oveq2i 
 |-  ( ( log ` ( n + 1 ) ) - ( log ` 1 ) ) = ( ( log ` ( n + 1 ) ) - 0 )
38 27 nnrpd 
 |-  ( n e. NN -> ( n + 1 ) e. RR+ )
39 38 relogcld 
 |-  ( n e. NN -> ( log ` ( n + 1 ) ) e. RR )
40 39 recnd 
 |-  ( n e. NN -> ( log ` ( n + 1 ) ) e. CC )
41 40 subid1d 
 |-  ( n e. NN -> ( ( log ` ( n + 1 ) ) - 0 ) = ( log ` ( n + 1 ) ) )
42 37 41 syl5eq 
 |-  ( n e. NN -> ( ( log ` ( n + 1 ) ) - ( log ` 1 ) ) = ( log ` ( n + 1 ) ) )
43 21 35 42 3eqtrd 
 |-  ( n e. NN -> sum_ m e. ( 1 ... n ) ( log ` ( 1 + ( 1 / m ) ) ) = ( log ` ( n + 1 ) ) )
44 43 oveq2d 
 |-  ( n e. NN -> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - sum_ m e. ( 1 ... n ) ( log ` ( 1 + ( 1 / m ) ) ) ) = ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` ( n + 1 ) ) ) )
45 fzfid 
 |-  ( n e. NN -> ( 1 ... n ) e. Fin )
46 6 nnrecred 
 |-  ( ( n e. NN /\ m e. ( 1 ... n ) ) -> ( 1 / m ) e. RR )
47 46 recnd 
 |-  ( ( n e. NN /\ m e. ( 1 ... n ) ) -> ( 1 / m ) e. CC )
48 1rp 
 |-  1 e. RR+
49 18 rpreccld 
 |-  ( ( n e. NN /\ m e. ( 1 ... n ) ) -> ( 1 / m ) e. RR+ )
50 rpaddcl 
 |-  ( ( 1 e. RR+ /\ ( 1 / m ) e. RR+ ) -> ( 1 + ( 1 / m ) ) e. RR+ )
51 48 49 50 sylancr 
 |-  ( ( n e. NN /\ m e. ( 1 ... n ) ) -> ( 1 + ( 1 / m ) ) e. RR+ )
52 51 relogcld 
 |-  ( ( n e. NN /\ m e. ( 1 ... n ) ) -> ( log ` ( 1 + ( 1 / m ) ) ) e. RR )
53 52 recnd 
 |-  ( ( n e. NN /\ m e. ( 1 ... n ) ) -> ( log ` ( 1 + ( 1 / m ) ) ) e. CC )
54 45 47 53 fsumsub 
 |-  ( n e. NN -> sum_ m e. ( 1 ... n ) ( ( 1 / m ) - ( log ` ( 1 + ( 1 / m ) ) ) ) = ( sum_ m e. ( 1 ... n ) ( 1 / m ) - sum_ m e. ( 1 ... n ) ( log ` ( 1 + ( 1 / m ) ) ) ) )
55 oveq2 
 |-  ( n = m -> ( 1 / n ) = ( 1 / m ) )
56 55 oveq2d 
 |-  ( n = m -> ( 1 + ( 1 / n ) ) = ( 1 + ( 1 / m ) ) )
57 56 fveq2d 
 |-  ( n = m -> ( log ` ( 1 + ( 1 / n ) ) ) = ( log ` ( 1 + ( 1 / m ) ) ) )
58 55 57 oveq12d 
 |-  ( n = m -> ( ( 1 / n ) - ( log ` ( 1 + ( 1 / n ) ) ) ) = ( ( 1 / m ) - ( log ` ( 1 + ( 1 / m ) ) ) ) )
59 ovex 
 |-  ( ( 1 / m ) - ( log ` ( 1 + ( 1 / m ) ) ) ) e. _V
60 58 4 59 fvmpt 
 |-  ( m e. NN -> ( T ` m ) = ( ( 1 / m ) - ( log ` ( 1 + ( 1 / m ) ) ) ) )
61 6 60 syl 
 |-  ( ( n e. NN /\ m e. ( 1 ... n ) ) -> ( T ` m ) = ( ( 1 / m ) - ( log ` ( 1 + ( 1 / m ) ) ) ) )
62 id 
 |-  ( n e. NN -> n e. NN )
63 62 28 eleqtrdi 
 |-  ( n e. NN -> n e. ( ZZ>= ` 1 ) )
64 46 52 resubcld 
 |-  ( ( n e. NN /\ m e. ( 1 ... n ) ) -> ( ( 1 / m ) - ( log ` ( 1 + ( 1 / m ) ) ) ) e. RR )
65 64 recnd 
 |-  ( ( n e. NN /\ m e. ( 1 ... n ) ) -> ( ( 1 / m ) - ( log ` ( 1 + ( 1 / m ) ) ) ) e. CC )
66 61 63 65 fsumser 
 |-  ( n e. NN -> sum_ m e. ( 1 ... n ) ( ( 1 / m ) - ( log ` ( 1 + ( 1 / m ) ) ) ) = ( seq 1 ( + , T ) ` n ) )
67 54 66 eqtr3d 
 |-  ( n e. NN -> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - sum_ m e. ( 1 ... n ) ( log ` ( 1 + ( 1 / m ) ) ) ) = ( seq 1 ( + , T ) ` n ) )
68 44 67 eqtr3d 
 |-  ( n e. NN -> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` ( n + 1 ) ) ) = ( seq 1 ( + , T ) ` n ) )
69 68 mpteq2ia 
 |-  ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` ( n + 1 ) ) ) ) = ( n e. NN |-> ( seq 1 ( + , T ) ` n ) )
70 1z 
 |-  1 e. ZZ
71 seqfn 
 |-  ( 1 e. ZZ -> seq 1 ( + , T ) Fn ( ZZ>= ` 1 ) )
72 70 71 ax-mp 
 |-  seq 1 ( + , T ) Fn ( ZZ>= ` 1 )
73 28 fneq2i 
 |-  ( seq 1 ( + , T ) Fn NN <-> seq 1 ( + , T ) Fn ( ZZ>= ` 1 ) )
74 72 73 mpbir 
 |-  seq 1 ( + , T ) Fn NN
75 dffn5 
 |-  ( seq 1 ( + , T ) Fn NN <-> seq 1 ( + , T ) = ( n e. NN |-> ( seq 1 ( + , T ) ` n ) ) )
76 74 75 mpbi 
 |-  seq 1 ( + , T ) = ( n e. NN |-> ( seq 1 ( + , T ) ` n ) )
77 69 2 76 3eqtr4i 
 |-  G = seq 1 ( + , T )