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 ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) )
Assertion basellem6 𝐺 ⇝ 0

Proof

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