# 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 )`
` |-  ( ( 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 )`