Metamath Proof Explorer

Theorem emcllem6

Description: Lemma for emcl . By the previous lemmas, F and G must approach a common limit, which is gamma by definition. (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 emcllem6 
|- ( F ~~> gamma /\ G ~~> gamma )

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 nnuz 
 |-  NN = ( ZZ>= ` 1 )
6 1zzd 
 |-  ( T. -> 1 e. ZZ )
7 oveq2 
 |-  ( n = k -> ( 1 / n ) = ( 1 / k ) )
8 7 oveq2d 
 |-  ( n = k -> ( 1 + ( 1 / n ) ) = ( 1 + ( 1 / k ) ) )
9 8 fveq2d 
 |-  ( n = k -> ( log ` ( 1 + ( 1 / n ) ) ) = ( log ` ( 1 + ( 1 / k ) ) ) )
10 7 9 oveq12d 
 |-  ( n = k -> ( ( 1 / n ) - ( log ` ( 1 + ( 1 / n ) ) ) ) = ( ( 1 / k ) - ( log ` ( 1 + ( 1 / k ) ) ) ) )
11 ovex 
 |-  ( ( 1 / k ) - ( log ` ( 1 + ( 1 / k ) ) ) ) e. _V
12 10 4 11 fvmpt 
 |-  ( k e. NN -> ( T ` k ) = ( ( 1 / k ) - ( log ` ( 1 + ( 1 / k ) ) ) ) )
13 12 adantl 
 |-  ( ( T. /\ k e. NN ) -> ( T ` k ) = ( ( 1 / k ) - ( log ` ( 1 + ( 1 / k ) ) ) ) )
14 nnrecre 
 |-  ( k e. NN -> ( 1 / k ) e. RR )
15 14 adantl 
 |-  ( ( T. /\ k e. NN ) -> ( 1 / k ) e. RR )
16 1rp 
 |-  1 e. RR+
17 nnrp 
 |-  ( k e. NN -> k e. RR+ )
18 17 rpreccld 
 |-  ( k e. NN -> ( 1 / k ) e. RR+ )
19 18 adantl 
 |-  ( ( T. /\ k e. NN ) -> ( 1 / k ) e. RR+ )
20 rpaddcl 
 |-  ( ( 1 e. RR+ /\ ( 1 / k ) e. RR+ ) -> ( 1 + ( 1 / k ) ) e. RR+ )
21 16 19 20 sylancr 
 |-  ( ( T. /\ k e. NN ) -> ( 1 + ( 1 / k ) ) e. RR+ )
22 21 relogcld 
 |-  ( ( T. /\ k e. NN ) -> ( log ` ( 1 + ( 1 / k ) ) ) e. RR )
23 15 22 resubcld 
 |-  ( ( T. /\ k e. NN ) -> ( ( 1 / k ) - ( log ` ( 1 + ( 1 / k ) ) ) ) e. RR )
24 23 recnd 
 |-  ( ( T. /\ k e. NN ) -> ( ( 1 / k ) - ( log ` ( 1 + ( 1 / k ) ) ) ) e. CC )
25 1 2 3 4 emcllem5 
 |-  G = seq 1 ( + , T )
26 1 2 emcllem1 
 |-  ( F : NN --> RR /\ G : NN --> RR )
27 26 simpri 
 |-  G : NN --> RR
28 27 a1i 
 |-  ( T. -> G : NN --> RR )
29 1 2 emcllem2 
 |-  ( k e. NN -> ( ( F ` ( k + 1 ) ) <_ ( F ` k ) /\ ( G ` k ) <_ ( G ` ( k + 1 ) ) ) )
30 29 simprd 
 |-  ( k e. NN -> ( G ` k ) <_ ( G ` ( k + 1 ) ) )
31 30 adantl 
 |-  ( ( T. /\ k e. NN ) -> ( G ` k ) <_ ( G ` ( k + 1 ) ) )
32 1nn 
 |-  1 e. NN
33 26 simpli 
 |-  F : NN --> RR
34 33 ffvelcdmi 
 |-  ( 1 e. NN -> ( F ` 1 ) e. RR )
35 32 34 ax-mp 
 |-  ( F ` 1 ) e. RR
36 27 ffvelcdmi 
 |-  ( k e. NN -> ( G ` k ) e. RR )
37 36 adantl 
 |-  ( ( T. /\ k e. NN ) -> ( G ` k ) e. RR )
38 33 ffvelcdmi 
 |-  ( k e. NN -> ( F ` k ) e. RR )
39 38 adantl 
 |-  ( ( T. /\ k e. NN ) -> ( F ` k ) e. RR )
40 35 a1i 
 |-  ( ( T. /\ k e. NN ) -> ( F ` 1 ) e. RR )
41 fvex 
 |-  ( log ` ( 1 + ( 1 / k ) ) ) e. _V
42 9 3 41 fvmpt 
 |-  ( k e. NN -> ( H ` k ) = ( log ` ( 1 + ( 1 / k ) ) ) )
43 42 adantl 
 |-  ( ( T. /\ k e. NN ) -> ( H ` k ) = ( log ` ( 1 + ( 1 / k ) ) ) )
44 1 2 3 emcllem3 
 |-  ( k e. NN -> ( H ` k ) = ( ( F ` k ) - ( G ` k ) ) )
45 44 adantl 
 |-  ( ( T. /\ k e. NN ) -> ( H ` k ) = ( ( F ` k ) - ( G ` k ) ) )
46 43 45 eqtr3d 
 |-  ( ( T. /\ k e. NN ) -> ( log ` ( 1 + ( 1 / k ) ) ) = ( ( F ` k ) - ( G ` k ) ) )
47 1re 
 |-  1 e. RR
48 readdcl 
 |-  ( ( 1 e. RR /\ ( 1 / k ) e. RR ) -> ( 1 + ( 1 / k ) ) e. RR )
49 47 15 48 sylancr 
 |-  ( ( T. /\ k e. NN ) -> ( 1 + ( 1 / k ) ) e. RR )
50 ltaddrp 
 |-  ( ( 1 e. RR /\ ( 1 / k ) e. RR+ ) -> 1 < ( 1 + ( 1 / k ) ) )
51 47 19 50 sylancr 
 |-  ( ( T. /\ k e. NN ) -> 1 < ( 1 + ( 1 / k ) ) )
52 49 51 rplogcld 
 |-  ( ( T. /\ k e. NN ) -> ( log ` ( 1 + ( 1 / k ) ) ) e. RR+ )
53 46 52 eqeltrrd 
 |-  ( ( T. /\ k e. NN ) -> ( ( F ` k ) - ( G ` k ) ) e. RR+ )
54 53 rpge0d 
 |-  ( ( T. /\ k e. NN ) -> 0 <_ ( ( F ` k ) - ( G ` k ) ) )
55 39 37 subge0d 
 |-  ( ( T. /\ k e. NN ) -> ( 0 <_ ( ( F ` k ) - ( G ` k ) ) <-> ( G ` k ) <_ ( F ` k ) ) )
56 54 55 mpbid 
 |-  ( ( T. /\ k e. NN ) -> ( G ` k ) <_ ( F ` k ) )
57 fveq2 
 |-  ( x = 1 -> ( F ` x ) = ( F ` 1 ) )
58 57 breq1d 
 |-  ( x = 1 -> ( ( F ` x ) <_ ( F ` 1 ) <-> ( F ` 1 ) <_ ( F ` 1 ) ) )
59 fveq2 
 |-  ( x = k -> ( F ` x ) = ( F ` k ) )
60 59 breq1d 
 |-  ( x = k -> ( ( F ` x ) <_ ( F ` 1 ) <-> ( F ` k ) <_ ( F ` 1 ) ) )
61 fveq2 
 |-  ( x = ( k + 1 ) -> ( F ` x ) = ( F ` ( k + 1 ) ) )
62 61 breq1d 
 |-  ( x = ( k + 1 ) -> ( ( F ` x ) <_ ( F ` 1 ) <-> ( F ` ( k + 1 ) ) <_ ( F ` 1 ) ) )
63 35 leidi 
 |-  ( F ` 1 ) <_ ( F ` 1 )
64 29 simpld 
 |-  ( k e. NN -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )
65 peano2nn 
 |-  ( k e. NN -> ( k + 1 ) e. NN )
66 33 ffvelcdmi 
 |-  ( ( k + 1 ) e. NN -> ( F ` ( k + 1 ) ) e. RR )
67 65 66 syl 
 |-  ( k e. NN -> ( F ` ( k + 1 ) ) e. RR )
68 35 a1i 
 |-  ( k e. NN -> ( F ` 1 ) e. RR )
69 letr 
 |-  ( ( ( F ` ( k + 1 ) ) e. RR /\ ( F ` k ) e. RR /\ ( F ` 1 ) e. RR ) -> ( ( ( F ` ( k + 1 ) ) <_ ( F ` k ) /\ ( F ` k ) <_ ( F ` 1 ) ) -> ( F ` ( k + 1 ) ) <_ ( F ` 1 ) ) )
70 67 38 68 69 syl3anc 
 |-  ( k e. NN -> ( ( ( F ` ( k + 1 ) ) <_ ( F ` k ) /\ ( F ` k ) <_ ( F ` 1 ) ) -> ( F ` ( k + 1 ) ) <_ ( F ` 1 ) ) )
71 64 70 mpand 
 |-  ( k e. NN -> ( ( F ` k ) <_ ( F ` 1 ) -> ( F ` ( k + 1 ) ) <_ ( F ` 1 ) ) )
72 58 60 62 60 63 71 nnind 
 |-  ( k e. NN -> ( F ` k ) <_ ( F ` 1 ) )
73 72 adantl 
 |-  ( ( T. /\ k e. NN ) -> ( F ` k ) <_ ( F ` 1 ) )
74 37 39 40 56 73 letrd 
 |-  ( ( T. /\ k e. NN ) -> ( G ` k ) <_ ( F ` 1 ) )
75 74 ralrimiva 
 |-  ( T. -> A. k e. NN ( G ` k ) <_ ( F ` 1 ) )
76 brralrspcev 
 |-  ( ( ( F ` 1 ) e. RR /\ A. k e. NN ( G ` k ) <_ ( F ` 1 ) ) -> E. x e. RR A. k e. NN ( G ` k ) <_ x )
77 35 75 76 sylancr 
 |-  ( T. -> E. x e. RR A. k e. NN ( G ` k ) <_ x )
78 5 6 28 31 77 climsup 
 |-  ( T. -> G ~~> sup ( ran G , RR , < ) )
79 25 78 eqbrtrrid 
 |-  ( T. -> seq 1 ( + , T ) ~~> sup ( ran G , RR , < ) )
80 climrel 
 |-  Rel ~~>
81 80 releldmi 
 |-  ( seq 1 ( + , T ) ~~> sup ( ran G , RR , < ) -> seq 1 ( + , T ) e. dom ~~> )
82 79 81 syl 
 |-  ( T. -> seq 1 ( + , T ) e. dom ~~> )
83 5 6 13 24 82 isumclim2 
 |-  ( T. -> seq 1 ( + , T ) ~~> sum_ k e. NN ( ( 1 / k ) - ( log ` ( 1 + ( 1 / k ) ) ) ) )
84 df-em 
 |-  gamma = sum_ k e. NN ( ( 1 / k ) - ( log ` ( 1 + ( 1 / k ) ) ) )
85 83 25 84 3brtr4g 
 |-  ( T. -> G ~~> gamma )
86 nnex 
 |-  NN e. _V
87 86 mptex 
 |-  ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` n ) ) ) e. _V
88 1 87 eqeltri 
 |-  F e. _V
89 88 a1i 
 |-  ( T. -> F e. _V )
90 1 2 3 emcllem4 
 |-  H ~~> 0
91 90 a1i 
 |-  ( T. -> H ~~> 0 )
92 37 recnd 
 |-  ( ( T. /\ k e. NN ) -> ( G ` k ) e. CC )
93 39 37 resubcld 
 |-  ( ( T. /\ k e. NN ) -> ( ( F ` k ) - ( G ` k ) ) e. RR )
94 45 93 eqeltrd 
 |-  ( ( T. /\ k e. NN ) -> ( H ` k ) e. RR )
95 94 recnd 
 |-  ( ( T. /\ k e. NN ) -> ( H ` k ) e. CC )
96 45 oveq2d 
 |-  ( ( T. /\ k e. NN ) -> ( ( G ` k ) + ( H ` k ) ) = ( ( G ` k ) + ( ( F ` k ) - ( G ` k ) ) ) )
97 39 recnd 
 |-  ( ( T. /\ k e. NN ) -> ( F ` k ) e. CC )
98 92 97 pncan3d 
 |-  ( ( T. /\ k e. NN ) -> ( ( G ` k ) + ( ( F ` k ) - ( G ` k ) ) ) = ( F ` k ) )
99 96 98 eqtr2d 
 |-  ( ( T. /\ k e. NN ) -> ( F ` k ) = ( ( G ` k ) + ( H ` k ) ) )
100 5 6 85 89 91 92 95 99 climadd 
 |-  ( T. -> F ~~> ( gamma + 0 ) )
101 85 mptru 
 |-  G ~~> gamma
102 climcl 
 |-  ( G ~~> gamma -> gamma e. CC )
103 101 102 ax-mp 
 |-  gamma e. CC
104 103 addridi 
 |-  ( gamma + 0 ) = gamma
105 100 104 breqtrdi 
 |-  ( T. -> F ~~> gamma )
106 105 mptru 
 |-  F ~~> gamma
107 106 101 pm3.2i 
 |-  ( F ~~> gamma /\ G ~~> gamma )