Metamath Proof Explorer

Theorem emcllem3

Description: Lemma for emcl . The function H is the difference between F and 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 ) ) ) )
Assertion emcllem3 
|- ( N e. NN -> ( H ` N ) = ( ( F ` N ) - ( G ` N ) ) )

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 peano2nn 
 |-  ( N e. NN -> ( N + 1 ) e. NN )
5 4 nnrpd 
 |-  ( N e. NN -> ( N + 1 ) e. RR+ )
6 nnrp 
 |-  ( N e. NN -> N e. RR+ )
7 5 6 relogdivd 
 |-  ( N e. NN -> ( log ` ( ( N + 1 ) / N ) ) = ( ( log ` ( N + 1 ) ) - ( log ` N ) ) )
8 nncn 
 |-  ( N e. NN -> N e. CC )
9 1cnd 
 |-  ( N e. NN -> 1 e. CC )
10 nnne0 
 |-  ( N e. NN -> N =/= 0 )
11 8 9 8 10 divdird 
 |-  ( N e. NN -> ( ( N + 1 ) / N ) = ( ( N / N ) + ( 1 / N ) ) )
12 8 10 dividd 
 |-  ( N e. NN -> ( N / N ) = 1 )
13 12 oveq1d 
 |-  ( N e. NN -> ( ( N / N ) + ( 1 / N ) ) = ( 1 + ( 1 / N ) ) )
14 11 13 eqtr2d 
 |-  ( N e. NN -> ( 1 + ( 1 / N ) ) = ( ( N + 1 ) / N ) )
15 14 fveq2d 
 |-  ( N e. NN -> ( log ` ( 1 + ( 1 / N ) ) ) = ( log ` ( ( N + 1 ) / N ) ) )
16 fzfid 
 |-  ( N e. NN -> ( 1 ... N ) e. Fin )
17 elfznn 
 |-  ( m e. ( 1 ... N ) -> m e. NN )
18 17 adantl 
 |-  ( ( N e. NN /\ m e. ( 1 ... N ) ) -> m e. NN )
19 18 nnrecred 
 |-  ( ( N e. NN /\ m e. ( 1 ... N ) ) -> ( 1 / m ) e. RR )
20 16 19 fsumrecl 
 |-  ( N e. NN -> sum_ m e. ( 1 ... N ) ( 1 / m ) e. RR )
21 20 recnd 
 |-  ( N e. NN -> sum_ m e. ( 1 ... N ) ( 1 / m ) e. CC )
22 6 relogcld 
 |-  ( N e. NN -> ( log ` N ) e. RR )
23 22 recnd 
 |-  ( N e. NN -> ( log ` N ) e. CC )
24 5 relogcld 
 |-  ( N e. NN -> ( log ` ( N + 1 ) ) e. RR )
25 24 recnd 
 |-  ( N e. NN -> ( log ` ( N + 1 ) ) e. CC )
26 21 23 25 nnncan1d 
 |-  ( N e. NN -> ( ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` N ) ) - ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) ) = ( ( log ` ( N + 1 ) ) - ( log ` N ) ) )
27 7 15 26 3eqtr4d 
 |-  ( N e. NN -> ( log ` ( 1 + ( 1 / N ) ) ) = ( ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` N ) ) - ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) ) )
28 oveq2 
 |-  ( n = N -> ( 1 / n ) = ( 1 / N ) )
29 28 oveq2d 
 |-  ( n = N -> ( 1 + ( 1 / n ) ) = ( 1 + ( 1 / N ) ) )
30 29 fveq2d 
 |-  ( n = N -> ( log ` ( 1 + ( 1 / n ) ) ) = ( log ` ( 1 + ( 1 / N ) ) ) )
31 fvex 
 |-  ( log ` ( 1 + ( 1 / N ) ) ) e. _V
32 30 3 31 fvmpt 
 |-  ( N e. NN -> ( H ` N ) = ( log ` ( 1 + ( 1 / N ) ) ) )
33 oveq2 
 |-  ( n = N -> ( 1 ... n ) = ( 1 ... N ) )
34 33 sumeq1d 
 |-  ( n = N -> sum_ m e. ( 1 ... n ) ( 1 / m ) = sum_ m e. ( 1 ... N ) ( 1 / m ) )
35 fveq2 
 |-  ( n = N -> ( log ` n ) = ( log ` N ) )
36 34 35 oveq12d 
 |-  ( n = N -> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` n ) ) = ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` N ) ) )
37 ovex 
 |-  ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` N ) ) e. _V
38 36 1 37 fvmpt 
 |-  ( N e. NN -> ( F ` N ) = ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` N ) ) )
39 fvoveq1 
 |-  ( n = N -> ( log ` ( n + 1 ) ) = ( log ` ( N + 1 ) ) )
40 34 39 oveq12d 
 |-  ( n = N -> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` ( n + 1 ) ) ) = ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) )
41 ovex 
 |-  ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) e. _V
42 40 2 41 fvmpt 
 |-  ( N e. NN -> ( G ` N ) = ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) )
43 38 42 oveq12d 
 |-  ( N e. NN -> ( ( F ` N ) - ( G ` N ) ) = ( ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` N ) ) - ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) ) )
44 27 32 43 3eqtr4d 
 |-  ( N e. NN -> ( H ` N ) = ( ( F ` N ) - ( G ` N ) ) )