emcllem2

Description: Lemma for emcl . F is increasing, and G is decreasing. (Contributed by Mario Carneiro, 11-Jul-2014)

	Ref	Expression
Hypotheses	emcl.1	$⊢ F = (n \in ℕ ⟼ \sum_{m = 1}^{n} (\frac{1}{m}) - \log n)$
	emcl.2	$⊢ G = (n \in ℕ ⟼ \sum_{m = 1}^{n} (\frac{1}{m}) - \log (n + 1))$
Assertion	emcllem2	$⊢ N \in ℕ \to (F (N + 1) \leq F (N) \land G (N) \leq G (N + 1))$

Proof

Step	Hyp	Ref	Expression
1		emcl.1	$⊢ F = (n \in ℕ ⟼ \sum_{m = 1}^{n} (\frac{1}{m}) - \log n)$
2		emcl.2	$⊢ G = (n \in ℕ ⟼ \sum_{m = 1}^{n} (\frac{1}{m}) - \log (n + 1))$
3		peano2nn	$⊢ N \in ℕ \to N + 1 \in ℕ$
4	3	nnrecred	$⊢ N \in ℕ \to \frac{1}{N + 1} \in ℝ$
5	3	nnrpd	$⊢ N \in ℕ \to N + 1 \in ℝ^{+}$
6	5	relogcld	$⊢ N \in ℕ \to \log (N + 1) \in ℝ$
7		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
8	7	relogcld	$⊢ N \in ℕ \to \log N \in ℝ$
9	6 8	resubcld	$⊢ N \in ℕ \to \log (N + 1) - \log N \in ℝ$
10		fzfid	$⊢ N \in ℕ \to (1 \dots N) \in Fin$
11		elfznn	$⊢ m \in (1 \dots N) \to m \in ℕ$
12	11	adantl	$⊢ (N \in ℕ \land m \in (1 \dots N)) \to m \in ℕ$
13	12	nnrecred	$⊢ (N \in ℕ \land m \in (1 \dots N)) \to \frac{1}{m} \in ℝ$
14	10 13	fsumrecl	$⊢ N \in ℕ \to \sum_{m = 1}^{N} (\frac{1}{m}) \in ℝ$
15	5	rpreccld	$⊢ N \in ℕ \to \frac{1}{N + 1} \in ℝ^{+}$
16	15	rpge0d	$⊢ N \in ℕ \to 0 \leq \frac{1}{N + 1}$
17		1div1e1	$⊢ \frac{1}{1} = 1$
18		1re	$⊢ 1 \in ℝ$
19		ltaddrp	$⊢ (1 \in ℝ \land N \in ℝ^{+}) \to 1 < 1 + N$
20	18 7 19	sylancr	$⊢ N \in ℕ \to 1 < 1 + N$
21		ax-1cn	$⊢ 1 \in ℂ$
22		nncn	$⊢ N \in ℕ \to N \in ℂ$
23		addcom	$⊢ (1 \in ℂ \land N \in ℂ) \to 1 + N = N + 1$
24	21 22 23	sylancr	$⊢ N \in ℕ \to 1 + N = N + 1$
25	20 24	breqtrd	$⊢ N \in ℕ \to 1 < N + 1$
26	17 25	eqbrtrid	$⊢ N \in ℕ \to \frac{1}{1} < N + 1$
27	3	nnred	$⊢ N \in ℕ \to N + 1 \in ℝ$
28	3	nngt0d	$⊢ N \in ℕ \to 0 < N + 1$
29		0lt1	$⊢ 0 < 1$
30		ltrec1	$⊢ ((1 \in ℝ \land 0 < 1) \land (N + 1 \in ℝ \land 0 < N + 1)) \to (\frac{1}{1} < N + 1 \leftrightarrow \frac{1}{N + 1} < 1)$
31	18 29 30	mpanl12	$⊢ (N + 1 \in ℝ \land 0 < N + 1) \to (\frac{1}{1} < N + 1 \leftrightarrow \frac{1}{N + 1} < 1)$
32	27 28 31	syl2anc	$⊢ N \in ℕ \to (\frac{1}{1} < N + 1 \leftrightarrow \frac{1}{N + 1} < 1)$
33	26 32	mpbid	$⊢ N \in ℕ \to \frac{1}{N + 1} < 1$
34	4 16 33	eflegeo	$⊢ N \in ℕ \to e^{\frac{1}{N + 1}} \leq \frac{1}{1 - (\frac{1}{N + 1})}$
35	27	recnd	$⊢ N \in ℕ \to N + 1 \in ℂ$
36		nnne0	$⊢ N \in ℕ \to N \neq 0$
37	3	nnne0d	$⊢ N \in ℕ \to N + 1 \neq 0$
38	22 35 36 37	recdivd	$⊢ N \in ℕ \to \frac{1}{\frac{N}{N + 1}} = \frac{N + 1}{N}$
39		1cnd	$⊢ N \in ℕ \to 1 \in ℂ$
40	35 39 35 37	divsubdird	$⊢ N \in ℕ \to \frac{N + 1 - 1}{N + 1} = (\frac{N + 1}{N + 1}) - (\frac{1}{N + 1})$
41		pncan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N + 1 - 1 = N$
42	22 21 41	sylancl	$⊢ N \in ℕ \to N + 1 - 1 = N$
43	42	oveq1d	$⊢ N \in ℕ \to \frac{N + 1 - 1}{N + 1} = \frac{N}{N + 1}$
44	35 37	dividd	$⊢ N \in ℕ \to \frac{N + 1}{N + 1} = 1$
45	44	oveq1d	$⊢ N \in ℕ \to (\frac{N + 1}{N + 1}) - (\frac{1}{N + 1}) = 1 - (\frac{1}{N + 1})$
46	40 43 45	3eqtr3rd	$⊢ N \in ℕ \to 1 - (\frac{1}{N + 1}) = \frac{N}{N + 1}$
47	46	oveq2d	$⊢ N \in ℕ \to \frac{1}{1 - (\frac{1}{N + 1})} = \frac{1}{\frac{N}{N + 1}}$
48	5 7	rpdivcld	$⊢ N \in ℕ \to \frac{N + 1}{N} \in ℝ^{+}$
49	48	reeflogd	$⊢ N \in ℕ \to e^{\log (\frac{N + 1}{N})} = \frac{N + 1}{N}$
50	38 47 49	3eqtr4d	$⊢ N \in ℕ \to \frac{1}{1 - (\frac{1}{N + 1})} = e^{\log (\frac{N + 1}{N})}$
51	34 50	breqtrd	$⊢ N \in ℕ \to e^{\frac{1}{N + 1}} \leq e^{\log (\frac{N + 1}{N})}$
52	5 7	relogdivd	$⊢ N \in ℕ \to \log (\frac{N + 1}{N}) = \log (N + 1) - \log N$
53	52 9	eqeltrd	$⊢ N \in ℕ \to \log (\frac{N + 1}{N}) \in ℝ$
54		efle	$⊢ (\frac{1}{N + 1} \in ℝ \land \log (\frac{N + 1}{N}) \in ℝ) \to (\frac{1}{N + 1} \leq \log (\frac{N + 1}{N}) \leftrightarrow e^{\frac{1}{N + 1}} \leq e^{\log (\frac{N + 1}{N})})$
55	4 53 54	syl2anc	$⊢ N \in ℕ \to (\frac{1}{N + 1} \leq \log (\frac{N + 1}{N}) \leftrightarrow e^{\frac{1}{N + 1}} \leq e^{\log (\frac{N + 1}{N})})$
56	51 55	mpbird	$⊢ N \in ℕ \to \frac{1}{N + 1} \leq \log (\frac{N + 1}{N})$
57	56 52	breqtrd	$⊢ N \in ℕ \to \frac{1}{N + 1} \leq \log (N + 1) - \log N$
58	4 9 14 57	leadd2dd	$⊢ N \in ℕ \to \sum_{m = 1}^{N} (\frac{1}{m}) + (\frac{1}{N + 1}) \leq \sum_{m = 1}^{N} (\frac{1}{m}) + \log (N + 1) - \log N$
59		id	$⊢ N \in ℕ \to N \in ℕ$
60		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
61	59 60	eleqtrdi	$⊢ N \in ℕ \to N \in ℤ_{\geq 1}$
62		elfznn	$⊢ m \in (1 \dots N + 1) \to m \in ℕ$
63	62	adantl	$⊢ (N \in ℕ \land m \in (1 \dots N + 1)) \to m \in ℕ$
64	63	nnrecred	$⊢ (N \in ℕ \land m \in (1 \dots N + 1)) \to \frac{1}{m} \in ℝ$
65	64	recnd	$⊢ (N \in ℕ \land m \in (1 \dots N + 1)) \to \frac{1}{m} \in ℂ$
66		oveq2	$⊢ m = N + 1 \to \frac{1}{m} = \frac{1}{N + 1}$
67	61 65 66	fsump1	$⊢ N \in ℕ \to \sum_{m = 1}^{N + 1} (\frac{1}{m}) = \sum_{m = 1}^{N} (\frac{1}{m}) + (\frac{1}{N + 1})$
68	6	recnd	$⊢ N \in ℕ \to \log (N + 1) \in ℂ$
69	14	recnd	$⊢ N \in ℕ \to \sum_{m = 1}^{N} (\frac{1}{m}) \in ℂ$
70	8	recnd	$⊢ N \in ℕ \to \log N \in ℂ$
71	68 69 70	addsub12d	$⊢ N \in ℕ \to \log (N + 1) + \sum_{m = 1}^{N} (\frac{1}{m}) - \log N = \sum_{m = 1}^{N} (\frac{1}{m}) + \log (N + 1) - \log N$
72	58 67 71	3brtr4d	$⊢ N \in ℕ \to \sum_{m = 1}^{N + 1} (\frac{1}{m}) \leq \log (N + 1) + \sum_{m = 1}^{N} (\frac{1}{m}) - \log N$
73		fzfid	$⊢ N \in ℕ \to (1 \dots N + 1) \in Fin$
74	73 64	fsumrecl	$⊢ N \in ℕ \to \sum_{m = 1}^{N + 1} (\frac{1}{m}) \in ℝ$
75	14 8	resubcld	$⊢ N \in ℕ \to \sum_{m = 1}^{N} (\frac{1}{m}) - \log N \in ℝ$
76	74 6 75	lesubadd2d	$⊢ N \in ℕ \to (\sum_{m = 1}^{N + 1} (\frac{1}{m}) - \log (N + 1) \leq \sum_{m = 1}^{N} (\frac{1}{m}) - \log N \leftrightarrow \sum_{m = 1}^{N + 1} (\frac{1}{m}) \leq \log (N + 1) + \sum_{m = 1}^{N} (\frac{1}{m}) - \log N)$
77	72 76	mpbird	$⊢ N \in ℕ \to \sum_{m = 1}^{N + 1} (\frac{1}{m}) - \log (N + 1) \leq \sum_{m = 1}^{N} (\frac{1}{m}) - \log N$
78		oveq2	$⊢ n = N + 1 \to (1 \dots n) = (1 \dots N + 1)$
79	78	sumeq1d	$⊢ n = N + 1 \to \sum_{m = 1}^{n} (\frac{1}{m}) = \sum_{m = 1}^{N + 1} (\frac{1}{m})$
80		fveq2	$⊢ n = N + 1 \to \log n = \log (N + 1)$
81	79 80	oveq12d	$⊢ n = N + 1 \to \sum_{m = 1}^{n} (\frac{1}{m}) - \log n = \sum_{m = 1}^{N + 1} (\frac{1}{m}) - \log (N + 1)$
82		ovex	$⊢ \sum_{m = 1}^{N + 1} (\frac{1}{m}) - \log (N + 1) \in V$
83	81 1 82	fvmpt	$⊢ N + 1 \in ℕ \to F (N + 1) = \sum_{m = 1}^{N + 1} (\frac{1}{m}) - \log (N + 1)$
84	3 83	syl	$⊢ N \in ℕ \to F (N + 1) = \sum_{m = 1}^{N + 1} (\frac{1}{m}) - \log (N + 1)$
85		oveq2	$⊢ n = N \to (1 \dots n) = (1 \dots N)$
86	85	sumeq1d	$⊢ n = N \to \sum_{m = 1}^{n} (\frac{1}{m}) = \sum_{m = 1}^{N} (\frac{1}{m})$
87		fveq2	$⊢ n = N \to \log n = \log N$
88	86 87	oveq12d	$⊢ n = N \to \sum_{m = 1}^{n} (\frac{1}{m}) - \log n = \sum_{m = 1}^{N} (\frac{1}{m}) - \log N$
89		ovex	$⊢ \sum_{m = 1}^{N} (\frac{1}{m}) - \log N \in V$
90	88 1 89	fvmpt	$⊢ N \in ℕ \to F (N) = \sum_{m = 1}^{N} (\frac{1}{m}) - \log N$
91	77 84 90	3brtr4d	$⊢ N \in ℕ \to F (N + 1) \leq F (N)$
92		peano2nn	$⊢ N + 1 \in ℕ \to N + 1 + 1 \in ℕ$
93	3 92	syl	$⊢ N \in ℕ \to N + 1 + 1 \in ℕ$
94	93	nnrpd	$⊢ N \in ℕ \to N + 1 + 1 \in ℝ^{+}$
95	94	relogcld	$⊢ N \in ℕ \to \log (N + 1 + 1) \in ℝ$
96	95 6	resubcld	$⊢ N \in ℕ \to \log (N + 1 + 1) - \log (N + 1) \in ℝ$
97		logdifbnd	$⊢ N + 1 \in ℝ^{+} \to \log (N + 1 + 1) - \log (N + 1) \leq \frac{1}{N + 1}$
98	5 97	syl	$⊢ N \in ℕ \to \log (N + 1 + 1) - \log (N + 1) \leq \frac{1}{N + 1}$
99	96 4 14 98	leadd2dd	$⊢ N \in ℕ \to \sum_{m = 1}^{N} (\frac{1}{m}) + \log (N + 1 + 1) - \log (N + 1) \leq \sum_{m = 1}^{N} (\frac{1}{m}) + (\frac{1}{N + 1})$
100	95	recnd	$⊢ N \in ℕ \to \log (N + 1 + 1) \in ℂ$
101	69 68 100	subadd23d	$⊢ N \in ℕ \to \sum_{m = 1}^{N} (\frac{1}{m}) - \log (N + 1) + \log (N + 1 + 1) = \sum_{m = 1}^{N} (\frac{1}{m}) + \log (N + 1 + 1) - \log (N + 1)$
102	99 101 67	3brtr4d	$⊢ N \in ℕ \to \sum_{m = 1}^{N} (\frac{1}{m}) - \log (N + 1) + \log (N + 1 + 1) \leq \sum_{m = 1}^{N + 1} (\frac{1}{m})$
103	14 6	resubcld	$⊢ N \in ℕ \to \sum_{m = 1}^{N} (\frac{1}{m}) - \log (N + 1) \in ℝ$
104		leaddsub	$⊢ (\sum_{m = 1}^{N} (\frac{1}{m}) - \log (N + 1) \in ℝ \land \log (N + 1 + 1) \in ℝ \land \sum_{m = 1}^{N + 1} (\frac{1}{m}) \in ℝ) \to (\sum_{m = 1}^{N} (\frac{1}{m}) - \log (N + 1) + \log (N + 1 + 1) \leq \sum_{m = 1}^{N + 1} (\frac{1}{m}) \leftrightarrow \sum_{m = 1}^{N} (\frac{1}{m}) - \log (N + 1) \leq \sum_{m = 1}^{N + 1} (\frac{1}{m}) - \log (N + 1 + 1))$
105	103 95 74 104	syl3anc	$⊢ N \in ℕ \to (\sum_{m = 1}^{N} (\frac{1}{m}) - \log (N + 1) + \log (N + 1 + 1) \leq \sum_{m = 1}^{N + 1} (\frac{1}{m}) \leftrightarrow \sum_{m = 1}^{N} (\frac{1}{m}) - \log (N + 1) \leq \sum_{m = 1}^{N + 1} (\frac{1}{m}) - \log (N + 1 + 1))$
106	102 105	mpbid	$⊢ N \in ℕ \to \sum_{m = 1}^{N} (\frac{1}{m}) - \log (N + 1) \leq \sum_{m = 1}^{N + 1} (\frac{1}{m}) - \log (N + 1 + 1)$
107		fvoveq1	$⊢ n = N \to \log (n + 1) = \log (N + 1)$
108	86 107	oveq12d	$⊢ n = N \to \sum_{m = 1}^{n} (\frac{1}{m}) - \log (n + 1) = \sum_{m = 1}^{N} (\frac{1}{m}) - \log (N + 1)$
109		ovex	$⊢ \sum_{m = 1}^{N} (\frac{1}{m}) - \log (N + 1) \in V$
110	108 2 109	fvmpt	$⊢ N \in ℕ \to G (N) = \sum_{m = 1}^{N} (\frac{1}{m}) - \log (N + 1)$
111		fvoveq1	$⊢ n = N + 1 \to \log (n + 1) = \log (N + 1 + 1)$
112	79 111	oveq12d	$⊢ n = N + 1 \to \sum_{m = 1}^{n} (\frac{1}{m}) - \log (n + 1) = \sum_{m = 1}^{N + 1} (\frac{1}{m}) - \log (N + 1 + 1)$
113		ovex	$⊢ \sum_{m = 1}^{N + 1} (\frac{1}{m}) - \log (N + 1 + 1) \in V$
114	112 2 113	fvmpt	$⊢ N + 1 \in ℕ \to G (N + 1) = \sum_{m = 1}^{N + 1} (\frac{1}{m}) - \log (N + 1 + 1)$
115	3 114	syl	$⊢ N \in ℕ \to G (N + 1) = \sum_{m = 1}^{N + 1} (\frac{1}{m}) - \log (N + 1 + 1)$
116	106 110 115	3brtr4d	$⊢ N \in ℕ \to G (N) \leq G (N + 1)$
117	91 116	jca	$⊢ N \in ℕ \to (F (N + 1) \leq F (N) \land G (N) \leq G (N + 1))$

Metamath Proof Explorer

Theorem emcllem2

Proof