basellem6

Description: Lemma for basel . The function G goes to zero because it is bounded by 1 / n . (Contributed by Mario Carneiro, 28-Jul-2014)

		Ref	Expression
	Hypothesis	basel.g	$⊢ G = (n \in ℕ ⟼ \frac{1}{2 n + 1})$
	Assertion	basellem6	$⊢ G ⇝ 0$

Proof

Step	Hyp	Ref	Expression
1		basel.g	$⊢ G = (n \in ℕ ⟼ \frac{1}{2 n + 1})$
2		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
3		1zzd	$⊢ ⊤ \to 1 \in ℤ$
4		ax-1cn	$⊢ 1 \in ℂ$
5		divcnv	$⊢ 1 \in ℂ \to (n \in ℕ ⟼ \frac{1}{n}) ⇝ 0$
6	4 5	mp1i	$⊢ ⊤ \to (n \in ℕ ⟼ \frac{1}{n}) ⇝ 0$
7		nnex	$⊢ ℕ \in V$
8	7	mptex	$⊢ (n \in ℕ ⟼ \frac{1}{2 n + 1}) \in V$
9	1 8	eqeltri	$⊢ G \in V$
10	9	a1i	$⊢ ⊤ \to G \in V$
11		oveq2	$⊢ n = k \to \frac{1}{n} = \frac{1}{k}$
12		eqid	$⊢ (n \in ℕ ⟼ \frac{1}{n}) = (n \in ℕ ⟼ \frac{1}{n})$
13		ovex	$⊢ \frac{1}{k} \in V$
14	11 12 13	fvmpt	$⊢ k \in ℕ \to (n \in ℕ ⟼ \frac{1}{n}) (k) = \frac{1}{k}$
15	14	adantl	$⊢ (⊤ \land k \in ℕ) \to (n \in ℕ ⟼ \frac{1}{n}) (k) = \frac{1}{k}$
16		nnrecre	$⊢ k \in ℕ \to \frac{1}{k} \in ℝ$
17	16	adantl	$⊢ (⊤ \land k \in ℕ) \to \frac{1}{k} \in ℝ$
18	15 17	eqeltrd	$⊢ (⊤ \land k \in ℕ) \to (n \in ℕ ⟼ \frac{1}{n}) (k) \in ℝ$
19		oveq2	$⊢ n = k \to 2 n = 2 k$
20	19	oveq1d	$⊢ n = k \to 2 n + 1 = 2 k + 1$
21	20	oveq2d	$⊢ n = k \to \frac{1}{2 n + 1} = \frac{1}{2 k + 1}$
22		ovex	$⊢ \frac{1}{2 k + 1} \in V$
23	21 1 22	fvmpt	$⊢ k \in ℕ \to G (k) = \frac{1}{2 k + 1}$
24	23	adantl	$⊢ (⊤ \land k \in ℕ) \to G (k) = \frac{1}{2 k + 1}$
25		2nn	$⊢ 2 \in ℕ$
26	25	a1i	$⊢ ⊤ \to 2 \in ℕ$
27		nnmulcl	$⊢ (2 \in ℕ \land k \in ℕ) \to 2 k \in ℕ$
28	26 27	sylan	$⊢ (⊤ \land k \in ℕ) \to 2 k \in ℕ$
29	28	peano2nnd	$⊢ (⊤ \land k \in ℕ) \to 2 k + 1 \in ℕ$
30	29	nnrecred	$⊢ (⊤ \land k \in ℕ) \to \frac{1}{2 k + 1} \in ℝ$
31	24 30	eqeltrd	$⊢ (⊤ \land k \in ℕ) \to G (k) \in ℝ$
32		nnre	$⊢ k \in ℕ \to k \in ℝ$
33	32	adantl	$⊢ (⊤ \land k \in ℕ) \to k \in ℝ$
34	28	nnred	$⊢ (⊤ \land k \in ℕ) \to 2 k \in ℝ$
35	29	nnred	$⊢ (⊤ \land k \in ℕ) \to 2 k + 1 \in ℝ$
36		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
37	36	adantl	$⊢ (⊤ \land k \in ℕ) \to k \in ℕ_{0}$
38		nn0addge1	$⊢ (k \in ℝ \land k \in ℕ_{0}) \to k \leq k + k$
39	33 37 38	syl2anc	$⊢ (⊤ \land k \in ℕ) \to k \leq k + k$
40	33	recnd	$⊢ (⊤ \land k \in ℕ) \to k \in ℂ$
41	40	2timesd	$⊢ (⊤ \land k \in ℕ) \to 2 k = k + k$
42	39 41	breqtrrd	$⊢ (⊤ \land k \in ℕ) \to k \leq 2 k$
43	34	lep1d	$⊢ (⊤ \land k \in ℕ) \to 2 k \leq 2 k + 1$
44	33 34 35 42 43	letrd	$⊢ (⊤ \land k \in ℕ) \to k \leq 2 k + 1$
45		nngt0	$⊢ k \in ℕ \to 0 < k$
46	45	adantl	$⊢ (⊤ \land k \in ℕ) \to 0 < k$
47	29	nngt0d	$⊢ (⊤ \land k \in ℕ) \to 0 < 2 k + 1$
48		lerec	$⊢ ((k \in ℝ \land 0 < k) \land (2 k + 1 \in ℝ \land 0 < 2 k + 1)) \to (k \leq 2 k + 1 \leftrightarrow \frac{1}{2 k + 1} \leq \frac{1}{k})$
49	33 46 35 47 48	syl22anc	$⊢ (⊤ \land k \in ℕ) \to (k \leq 2 k + 1 \leftrightarrow \frac{1}{2 k + 1} \leq \frac{1}{k})$
50	44 49	mpbid	$⊢ (⊤ \land k \in ℕ) \to \frac{1}{2 k + 1} \leq \frac{1}{k}$
51	50 24 15	3brtr4d	$⊢ (⊤ \land k \in ℕ) \to G (k) \leq (n \in ℕ ⟼ \frac{1}{n}) (k)$
52	29	nnrpd	$⊢ (⊤ \land k \in ℕ) \to 2 k + 1 \in ℝ^{+}$
53	52	rpreccld	$⊢ (⊤ \land k \in ℕ) \to \frac{1}{2 k + 1} \in ℝ^{+}$
54	53	rpge0d	$⊢ (⊤ \land k \in ℕ) \to 0 \leq \frac{1}{2 k + 1}$
55	54 24	breqtrrd	$⊢ (⊤ \land k \in ℕ) \to 0 \leq G (k)$
56	2 3 6 10 18 31 51 55	climsqz2	$⊢ ⊤ \to G ⇝ 0$
57	56	mptru	$⊢ G ⇝ 0$

Metamath Proof Explorer

Theorem basellem6

Proof