This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem emcllem1

Description: Lemma for emcl . The series F and G are sequences of real numbers that approach gamma from above and below, respectively. (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 emcllem1 
|- ( F : NN --> RR /\ G : NN --> RR )

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 fzfid 
 |-  ( n e. NN -> ( 1 ... n ) e. Fin )
4 elfznn 
 |-  ( m e. ( 1 ... n ) -> m e. NN )
5 4 adantl 
 |-  ( ( n e. NN /\ m e. ( 1 ... n ) ) -> m e. NN )
6 5 nnrecred 
 |-  ( ( n e. NN /\ m e. ( 1 ... n ) ) -> ( 1 / m ) e. RR )
7 3 6 fsumrecl 
 |-  ( n e. NN -> sum_ m e. ( 1 ... n ) ( 1 / m ) e. RR )
8 nnrp 
 |-  ( n e. NN -> n e. RR+ )
9 8 relogcld 
 |-  ( n e. NN -> ( log ` n ) e. RR )
10 7 9 resubcld 
 |-  ( n e. NN -> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` n ) ) e. RR )
11 1 10 fmpti 
 |-  F : NN --> RR
12 peano2nn 
 |-  ( n e. NN -> ( n + 1 ) e. NN )
13 12 nnrpd 
 |-  ( n e. NN -> ( n + 1 ) e. RR+ )
14 13 relogcld 
 |-  ( n e. NN -> ( log ` ( n + 1 ) ) e. RR )
15 7 14 resubcld 
 |-  ( n e. NN -> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` ( n + 1 ) ) ) e. RR )
16 2 15 fmpti 
 |-  G : NN --> RR
17 11 16 pm3.2i 
 |-  ( F : NN --> RR /\ G : NN --> RR )