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 )