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