Metamath Proof Explorer

Theorem basellem7

Description: Lemma for basel . The function 1 + A x. G for any fixed A goes to 1 . (Contributed by Mario Carneiro, 28-Jul-2014)

Ref Expression
Hypotheses basel.g 
|- G = ( n e. NN |-> ( 1 / ( ( 2 x. n ) + 1 ) ) )
basellem7.2 
|- A e. CC
Assertion basellem7 
|- ( ( NN X. { 1 } ) oF + ( ( NN X. { A } ) oF x. G ) ) ~~> 1

Proof

Step Hyp Ref Expression
1 basel.g 
 |-  G = ( n e. NN |-> ( 1 / ( ( 2 x. n ) + 1 ) ) )
2 basellem7.2 
 |-  A e. CC
3 nnuz 
 |-  NN = ( ZZ>= ` 1 )
4 1zzd 
 |-  ( T. -> 1 e. ZZ )
5 ax-1cn 
 |-  1 e. CC
6 3 eqimss2i 
 |-  ( ZZ>= ` 1 ) C_ NN
7 nnex 
 |-  NN e. _V
8 6 7 climconst2 
 |-  ( ( 1 e. CC /\ 1 e. ZZ ) -> ( NN X. { 1 } ) ~~> 1 )
9 5 4 8 sylancr 
 |-  ( T. -> ( NN X. { 1 } ) ~~> 1 )
10 ovexd 
 |-  ( T. -> ( ( NN X. { 1 } ) oF + ( ( NN X. { A } ) oF x. G ) ) e. _V )
11 6 7 climconst2 
 |-  ( ( A e. CC /\ 1 e. ZZ ) -> ( NN X. { A } ) ~~> A )
12 2 4 11 sylancr 
 |-  ( T. -> ( NN X. { A } ) ~~> A )
13 ovexd 
 |-  ( T. -> ( ( NN X. { A } ) oF x. G ) e. _V )
14 1 basellem6 
 |-  G ~~> 0
15 14 a1i 
 |-  ( T. -> G ~~> 0 )
16 2 elexi 
 |-  A e. _V
17 16 fconst 
 |-  ( NN X. { A } ) : NN --> { A }
18 2 a1i 
 |-  ( T. -> A e. CC )
19 18 snssd 
 |-  ( T. -> { A } C_ CC )
20 fss 
 |-  ( ( ( NN X. { A } ) : NN --> { A } /\ { A } C_ CC ) -> ( NN X. { A } ) : NN --> CC )
21 17 19 20 sylancr 
 |-  ( T. -> ( NN X. { A } ) : NN --> CC )
22 21 ffvelrnda 
 |-  ( ( T. /\ k e. NN ) -> ( ( NN X. { A } ) ` k ) e. CC )
23 2nn 
 |-  2 e. NN
24 23 a1i 
 |-  ( T. -> 2 e. NN )
25 nnmulcl 
 |-  ( ( 2 e. NN /\ n e. NN ) -> ( 2 x. n ) e. NN )
26 24 25 sylan 
 |-  ( ( T. /\ n e. NN ) -> ( 2 x. n ) e. NN )
27 26 peano2nnd 
 |-  ( ( T. /\ n e. NN ) -> ( ( 2 x. n ) + 1 ) e. NN )
28 27 nnrecred 
 |-  ( ( T. /\ n e. NN ) -> ( 1 / ( ( 2 x. n ) + 1 ) ) e. RR )
29 28 recnd 
 |-  ( ( T. /\ n e. NN ) -> ( 1 / ( ( 2 x. n ) + 1 ) ) e. CC )
30 29 1 fmptd 
 |-  ( T. -> G : NN --> CC )
31 30 ffvelrnda 
 |-  ( ( T. /\ k e. NN ) -> ( G ` k ) e. CC )
32 21 ffnd 
 |-  ( T. -> ( NN X. { A } ) Fn NN )
33 30 ffnd 
 |-  ( T. -> G Fn NN )
34 7 a1i 
 |-  ( T. -> NN e. _V )
35 inidm 
 |-  ( NN i^i NN ) = NN
36 eqidd 
 |-  ( ( T. /\ k e. NN ) -> ( ( NN X. { A } ) ` k ) = ( ( NN X. { A } ) ` k ) )
37 eqidd 
 |-  ( ( T. /\ k e. NN ) -> ( G ` k ) = ( G ` k ) )
38 32 33 34 34 35 36 37 ofval 
 |-  ( ( T. /\ k e. NN ) -> ( ( ( NN X. { A } ) oF x. G ) ` k ) = ( ( ( NN X. { A } ) ` k ) x. ( G ` k ) ) )
39 3 4 12 13 15 22 31 38 climmul 
 |-  ( T. -> ( ( NN X. { A } ) oF x. G ) ~~> ( A x. 0 ) )
40 2 mul01i 
 |-  ( A x. 0 ) = 0
41 39 40 breqtrdi 
 |-  ( T. -> ( ( NN X. { A } ) oF x. G ) ~~> 0 )
42 1ex 
 |-  1 e. _V
43 42 fconst 
 |-  ( NN X. { 1 } ) : NN --> { 1 }
44 5 a1i 
 |-  ( T. -> 1 e. CC )
45 44 snssd 
 |-  ( T. -> { 1 } C_ CC )
46 fss 
 |-  ( ( ( NN X. { 1 } ) : NN --> { 1 } /\ { 1 } C_ CC ) -> ( NN X. { 1 } ) : NN --> CC )
47 43 45 46 sylancr 
 |-  ( T. -> ( NN X. { 1 } ) : NN --> CC )
48 47 ffvelrnda 
 |-  ( ( T. /\ k e. NN ) -> ( ( NN X. { 1 } ) ` k ) e. CC )
49 mulcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x x. y ) e. CC )
50 49 adantl 
 |-  ( ( T. /\ ( x e. CC /\ y e. CC ) ) -> ( x x. y ) e. CC )
51 50 21 30 34 34 35 off 
 |-  ( T. -> ( ( NN X. { A } ) oF x. G ) : NN --> CC )
52 51 ffvelrnda 
 |-  ( ( T. /\ k e. NN ) -> ( ( ( NN X. { A } ) oF x. G ) ` k ) e. CC )
53 43 a1i 
 |-  ( T. -> ( NN X. { 1 } ) : NN --> { 1 } )
54 53 ffnd 
 |-  ( T. -> ( NN X. { 1 } ) Fn NN )
55 51 ffnd 
 |-  ( T. -> ( ( NN X. { A } ) oF x. G ) Fn NN )
56 eqidd 
 |-  ( ( T. /\ k e. NN ) -> ( ( NN X. { 1 } ) ` k ) = ( ( NN X. { 1 } ) ` k ) )
57 eqidd 
 |-  ( ( T. /\ k e. NN ) -> ( ( ( NN X. { A } ) oF x. G ) ` k ) = ( ( ( NN X. { A } ) oF x. G ) ` k ) )
58 54 55 34 34 35 56 57 ofval 
 |-  ( ( T. /\ k e. NN ) -> ( ( ( NN X. { 1 } ) oF + ( ( NN X. { A } ) oF x. G ) ) ` k ) = ( ( ( NN X. { 1 } ) ` k ) + ( ( ( NN X. { A } ) oF x. G ) ` k ) ) )
59 3 4 9 10 41 48 52 58 climadd 
 |-  ( T. -> ( ( NN X. { 1 } ) oF + ( ( NN X. { A } ) oF x. G ) ) ~~> ( 1 + 0 ) )
60 59 mptru 
 |-  ( ( NN X. { 1 } ) oF + ( ( NN X. { A } ) oF x. G ) ) ~~> ( 1 + 0 )
61 1p0e1 
 |-  ( 1 + 0 ) = 1
62 60 61 breqtri 
 |-  ( ( NN X. { 1 } ) oF + ( ( NN X. { A } ) oF x. G ) ) ~~> 1