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 e. NN |-> ( 1 / ( ( 2 x. n ) + 1 ) ) )
Assertion basellem6 
|- G ~~> 0

Proof

Step Hyp Ref Expression
1 basel.g 
 |-  G = ( n e. NN |-> ( 1 / ( ( 2 x. n ) + 1 ) ) )
2 nnuz 
 |-  NN = ( ZZ>= ` 1 )
3 1zzd 
 |-  ( T. -> 1 e. ZZ )
4 ax-1cn 
 |-  1 e. CC
5 divcnv 
 |-  ( 1 e. CC -> ( n e. NN |-> ( 1 / n ) ) ~~> 0 )
6 4 5 mp1i 
 |-  ( T. -> ( n e. NN |-> ( 1 / n ) ) ~~> 0 )
7 nnex 
 |-  NN e. _V
8 7 mptex 
 |-  ( n e. NN |-> ( 1 / ( ( 2 x. n ) + 1 ) ) ) e. _V
9 1 8 eqeltri 
 |-  G e. _V
10 9 a1i 
 |-  ( T. -> G e. _V )
11 oveq2 
 |-  ( n = k -> ( 1 / n ) = ( 1 / k ) )
12 eqid 
 |-  ( n e. NN |-> ( 1 / n ) ) = ( n e. NN |-> ( 1 / n ) )
13 ovex 
 |-  ( 1 / k ) e. _V
14 11 12 13 fvmpt 
 |-  ( k e. NN -> ( ( n e. NN |-> ( 1 / n ) ) ` k ) = ( 1 / k ) )
15 14 adantl 
 |-  ( ( T. /\ k e. NN ) -> ( ( n e. NN |-> ( 1 / n ) ) ` k ) = ( 1 / k ) )
16 nnrecre 
 |-  ( k e. NN -> ( 1 / k ) e. RR )
17 16 adantl 
 |-  ( ( T. /\ k e. NN ) -> ( 1 / k ) e. RR )
18 15 17 eqeltrd 
 |-  ( ( T. /\ k e. NN ) -> ( ( n e. NN |-> ( 1 / n ) ) ` k ) e. RR )
19 oveq2 
 |-  ( n = k -> ( 2 x. n ) = ( 2 x. k ) )
20 19 oveq1d 
 |-  ( n = k -> ( ( 2 x. n ) + 1 ) = ( ( 2 x. k ) + 1 ) )
21 20 oveq2d 
 |-  ( n = k -> ( 1 / ( ( 2 x. n ) + 1 ) ) = ( 1 / ( ( 2 x. k ) + 1 ) ) )
22 ovex 
 |-  ( 1 / ( ( 2 x. k ) + 1 ) ) e. _V
23 21 1 22 fvmpt 
 |-  ( k e. NN -> ( G ` k ) = ( 1 / ( ( 2 x. k ) + 1 ) ) )
24 23 adantl 
 |-  ( ( T. /\ k e. NN ) -> ( G ` k ) = ( 1 / ( ( 2 x. k ) + 1 ) ) )
25 2nn 
 |-  2 e. NN
26 25 a1i 
 |-  ( T. -> 2 e. NN )
27 nnmulcl 
 |-  ( ( 2 e. NN /\ k e. NN ) -> ( 2 x. k ) e. NN )
28 26 27 sylan 
 |-  ( ( T. /\ k e. NN ) -> ( 2 x. k ) e. NN )
29 28 peano2nnd 
 |-  ( ( T. /\ k e. NN ) -> ( ( 2 x. k ) + 1 ) e. NN )
30 29 nnrecred 
 |-  ( ( T. /\ k e. NN ) -> ( 1 / ( ( 2 x. k ) + 1 ) ) e. RR )
31 24 30 eqeltrd 
 |-  ( ( T. /\ k e. NN ) -> ( G ` k ) e. RR )
32 nnre 
 |-  ( k e. NN -> k e. RR )
33 32 adantl 
 |-  ( ( T. /\ k e. NN ) -> k e. RR )
34 28 nnred 
 |-  ( ( T. /\ k e. NN ) -> ( 2 x. k ) e. RR )
35 29 nnred 
 |-  ( ( T. /\ k e. NN ) -> ( ( 2 x. k ) + 1 ) e. RR )
36 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
37 36 adantl 
 |-  ( ( T. /\ k e. NN ) -> k e. NN0 )
38 nn0addge1 
 |-  ( ( k e. RR /\ k e. NN0 ) -> k <_ ( k + k ) )
39 33 37 38 syl2anc 
 |-  ( ( T. /\ k e. NN ) -> k <_ ( k + k ) )
40 33 recnd 
 |-  ( ( T. /\ k e. NN ) -> k e. CC )
41 40 2timesd 
 |-  ( ( T. /\ k e. NN ) -> ( 2 x. k ) = ( k + k ) )
42 39 41 breqtrrd 
 |-  ( ( T. /\ k e. NN ) -> k <_ ( 2 x. k ) )
43 34 lep1d 
 |-  ( ( T. /\ k e. NN ) -> ( 2 x. k ) <_ ( ( 2 x. k ) + 1 ) )
44 33 34 35 42 43 letrd 
 |-  ( ( T. /\ k e. NN ) -> k <_ ( ( 2 x. k ) + 1 ) )
45 nngt0 
 |-  ( k e. NN -> 0 < k )
46 45 adantl 
 |-  ( ( T. /\ k e. NN ) -> 0 < k )
47 29 nngt0d 
 |-  ( ( T. /\ k e. NN ) -> 0 < ( ( 2 x. k ) + 1 ) )
48 lerec 
 |-  ( ( ( k e. RR /\ 0 < k ) /\ ( ( ( 2 x. k ) + 1 ) e. RR /\ 0 < ( ( 2 x. k ) + 1 ) ) ) -> ( k <_ ( ( 2 x. k ) + 1 ) <-> ( 1 / ( ( 2 x. k ) + 1 ) ) <_ ( 1 / k ) ) )
49 33 46 35 47 48 syl22anc 
 |-  ( ( T. /\ k e. NN ) -> ( k <_ ( ( 2 x. k ) + 1 ) <-> ( 1 / ( ( 2 x. k ) + 1 ) ) <_ ( 1 / k ) ) )
50 44 49 mpbid 
 |-  ( ( T. /\ k e. NN ) -> ( 1 / ( ( 2 x. k ) + 1 ) ) <_ ( 1 / k ) )
51 50 24 15 3brtr4d 
 |-  ( ( T. /\ k e. NN ) -> ( G ` k ) <_ ( ( n e. NN |-> ( 1 / n ) ) ` k ) )
52 29 nnrpd 
 |-  ( ( T. /\ k e. NN ) -> ( ( 2 x. k ) + 1 ) e. RR+ )
53 52 rpreccld 
 |-  ( ( T. /\ k e. NN ) -> ( 1 / ( ( 2 x. k ) + 1 ) ) e. RR+ )
54 53 rpge0d 
 |-  ( ( T. /\ k e. NN ) -> 0 <_ ( 1 / ( ( 2 x. k ) + 1 ) ) )
55 54 24 breqtrrd 
 |-  ( ( T. /\ k e. NN ) -> 0 <_ ( G ` k ) )
56 2 3 6 10 18 31 51 55 climsqz2 
 |-  ( T. -> G ~~> 0 )
57 56 mptru 
 |-  G ~~> 0