Metamath Proof Explorer

Theorem 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∈ℕ⟼12⁢n+1
Assertion basellem6 ⊢G⇝0

Proof

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