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 \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))$
	emcl.3	$⊢ H = (n \in ℕ ⟼ \log (1 + (\frac{1}{n})))$
	emcl.4	$⊢ T = (n \in ℕ ⟼ (\frac{1}{n}) - \log (1 + (\frac{1}{n})))$
Assertion	emcllem6	$⊢ (F ⇝ γ \land G ⇝ γ)$

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

Metamath Proof Explorer

Theorem emcllem6

Proof