Metamath Proof Explorer

Theorem log2tlbnd

Description: Bound the error term in the series of log2cnv . (Contributed by Mario Carneiro, 7-Apr-2015)

Ref Expression
Assertion log2tlbnd 
|- ( N e. NN0 -> ( ( log ` 2 ) - sum_ n e. ( 0 ... ( N - 1 ) ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) ) e. ( 0 [,] ( 3 / ( ( 4 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fzfid 
 |-  ( N e. NN0 -> ( 0 ... ( N - 1 ) ) e. Fin )
2 elfznn0 
 |-  ( n e. ( 0 ... ( N - 1 ) ) -> n e. NN0 )
3 2re 
 |-  2 e. RR
4 3nn 
 |-  3 e. NN
5 2nn0 
 |-  2 e. NN0
6 simpr 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> n e. NN0 )
7 nn0mulcl 
 |-  ( ( 2 e. NN0 /\ n e. NN0 ) -> ( 2 x. n ) e. NN0 )
8 5 6 7 sylancr 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> ( 2 x. n ) e. NN0 )
9 nn0p1nn 
 |-  ( ( 2 x. n ) e. NN0 -> ( ( 2 x. n ) + 1 ) e. NN )
10 8 9 syl 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> ( ( 2 x. n ) + 1 ) e. NN )
11 nnmulcl 
 |-  ( ( 3 e. NN /\ ( ( 2 x. n ) + 1 ) e. NN ) -> ( 3 x. ( ( 2 x. n ) + 1 ) ) e. NN )
12 4 10 11 sylancr 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> ( 3 x. ( ( 2 x. n ) + 1 ) ) e. NN )
13 9nn 
 |-  9 e. NN
14 nnexpcl 
 |-  ( ( 9 e. NN /\ n e. NN0 ) -> ( 9 ^ n ) e. NN )
15 13 6 14 sylancr 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> ( 9 ^ n ) e. NN )
16 12 15 nnmulcld 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) e. NN )
17 nndivre 
 |-  ( ( 2 e. RR /\ ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) e. NN ) -> ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) e. RR )
18 3 16 17 sylancr 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) e. RR )
19 18 recnd 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) e. CC )
20 2 19 sylan2 
 |-  ( ( N e. NN0 /\ n e. ( 0 ... ( N - 1 ) ) ) -> ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) e. CC )
21 1 20 fsumcl 
 |-  ( N e. NN0 -> sum_ n e. ( 0 ... ( N - 1 ) ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) e. CC )
22 eqid 
 |-  ( ZZ>= ` N ) = ( ZZ>= ` N )
23 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
24 eluznn0 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> n e. NN0 )
25 oveq2 
 |-  ( k = n -> ( 2 x. k ) = ( 2 x. n ) )
26 25 oveq1d 
 |-  ( k = n -> ( ( 2 x. k ) + 1 ) = ( ( 2 x. n ) + 1 ) )
27 26 oveq2d 
 |-  ( k = n -> ( 3 x. ( ( 2 x. k ) + 1 ) ) = ( 3 x. ( ( 2 x. n ) + 1 ) ) )
28 oveq2 
 |-  ( k = n -> ( 9 ^ k ) = ( 9 ^ n ) )
29 27 28 oveq12d 
 |-  ( k = n -> ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) = ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) )
30 29 oveq2d 
 |-  ( k = n -> ( 2 / ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) ) = ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) )
31 eqid 
 |-  ( k e. NN0 |-> ( 2 / ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) ) ) = ( k e. NN0 |-> ( 2 / ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) ) )
32 ovex 
 |-  ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) e. _V
33 30 31 32 fvmpt 
 |-  ( n e. NN0 -> ( ( k e. NN0 |-> ( 2 / ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) ) ) ` n ) = ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) )
34 24 33 syl 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( ( k e. NN0 |-> ( 2 / ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) ) ) ` n ) = ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) )
35 24 18 syldan 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) e. RR )
36 31 log2cnv 
 |-  seq 0 ( + , ( k e. NN0 |-> ( 2 / ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) ) ) ) ~~> ( log ` 2 )
37 seqex 
 |-  seq 0 ( + , ( k e. NN0 |-> ( 2 / ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) ) ) ) e. _V
38 fvex 
 |-  ( log ` 2 ) e. _V
39 37 38 breldm 
 |-  ( seq 0 ( + , ( k e. NN0 |-> ( 2 / ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) ) ) ) ~~> ( log ` 2 ) -> seq 0 ( + , ( k e. NN0 |-> ( 2 / ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) ) ) ) e. dom ~~> )
40 36 39 mp1i 
 |-  ( N e. NN0 -> seq 0 ( + , ( k e. NN0 |-> ( 2 / ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) ) ) ) e. dom ~~> )
41 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
42 id 
 |-  ( N e. NN0 -> N e. NN0 )
43 33 adantl 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> ( ( k e. NN0 |-> ( 2 / ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) ) ) ` n ) = ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) )
44 43 19 eqeltrd 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> ( ( k e. NN0 |-> ( 2 / ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) ) ) ` n ) e. CC )
45 41 42 44 iserex 
 |-  ( N e. NN0 -> ( seq 0 ( + , ( k e. NN0 |-> ( 2 / ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) ) ) ) e. dom ~~> <-> seq N ( + , ( k e. NN0 |-> ( 2 / ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) ) ) ) e. dom ~~> ) )
46 40 45 mpbid 
 |-  ( N e. NN0 -> seq N ( + , ( k e. NN0 |-> ( 2 / ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) ) ) ) e. dom ~~> )
47 22 23 34 35 46 isumrecl 
 |-  ( N e. NN0 -> sum_ n e. ( ZZ>= ` N ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) e. RR )
48 47 recnd 
 |-  ( N e. NN0 -> sum_ n e. ( ZZ>= ` N ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) e. CC )
49 0zd 
 |-  ( N e. NN0 -> 0 e. ZZ )
50 36 a1i 
 |-  ( N e. NN0 -> seq 0 ( + , ( k e. NN0 |-> ( 2 / ( ( 3 x. ( ( 2 x. k ) + 1 ) ) x. ( 9 ^ k ) ) ) ) ) ~~> ( log ` 2 ) )
51 41 49 43 19 50 isumclim 
 |-  ( N e. NN0 -> sum_ n e. NN0 ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) = ( log ` 2 ) )
52 41 22 42 43 19 40 isumsplit 
 |-  ( N e. NN0 -> sum_ n e. NN0 ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) = ( sum_ n e. ( 0 ... ( N - 1 ) ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) + sum_ n e. ( ZZ>= ` N ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) ) )
53 51 52 eqtr3d 
 |-  ( N e. NN0 -> ( log ` 2 ) = ( sum_ n e. ( 0 ... ( N - 1 ) ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) + sum_ n e. ( ZZ>= ` N ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) ) )
54 21 48 53 mvrladdd 
 |-  ( N e. NN0 -> ( ( log ` 2 ) - sum_ n e. ( 0 ... ( N - 1 ) ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) ) = sum_ n e. ( ZZ>= ` N ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) )
55 3 a1i 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> 2 e. RR )
56 0le2 
 |-  0 <_ 2
57 56 a1i 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> 0 <_ 2 )
58 16 nnred 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) e. RR )
59 16 nngt0d 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> 0 < ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) )
60 divge0 
 |-  ( ( ( 2 e. RR /\ 0 <_ 2 ) /\ ( ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) e. RR /\ 0 < ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) ) -> 0 <_ ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) )
61 55 57 58 59 60 syl22anc 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> 0 <_ ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) )
62 24 61 syldan 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> 0 <_ ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) )
63 22 23 34 35 46 62 isumge0 
 |-  ( N e. NN0 -> 0 <_ sum_ n e. ( ZZ>= ` N ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) )
64 oveq2 
 |-  ( k = n -> ( ( 1 / 9 ) ^ k ) = ( ( 1 / 9 ) ^ n ) )
65 64 oveq2d 
 |-  ( k = n -> ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( ( 1 / 9 ) ^ k ) ) = ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( ( 1 / 9 ) ^ n ) ) )
66 eqid 
 |-  ( k e. NN0 |-> ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( ( 1 / 9 ) ^ k ) ) ) = ( k e. NN0 |-> ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( ( 1 / 9 ) ^ k ) ) )
67 ovex 
 |-  ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( ( 1 / 9 ) ^ n ) ) e. _V
68 65 66 67 fvmpt 
 |-  ( n e. NN0 -> ( ( k e. NN0 |-> ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( ( 1 / 9 ) ^ k ) ) ) ` n ) = ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( ( 1 / 9 ) ^ n ) ) )
69 68 adantl 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> ( ( k e. NN0 |-> ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( ( 1 / 9 ) ^ k ) ) ) ` n ) = ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( ( 1 / 9 ) ^ n ) ) )
70 9cn 
 |-  9 e. CC
71 70 a1i 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> 9 e. CC )
72 13 nnne0i 
 |-  9 =/= 0
73 72 a1i 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> 9 =/= 0 )
74 nn0z 
 |-  ( n e. NN0 -> n e. ZZ )
75 74 adantl 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> n e. ZZ )
76 71 73 75 exprecd 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> ( ( 1 / 9 ) ^ n ) = ( 1 / ( 9 ^ n ) ) )
77 76 oveq2d 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( ( 1 / 9 ) ^ n ) ) = ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( 1 / ( 9 ^ n ) ) ) )
78 nn0mulcl 
 |-  ( ( 2 e. NN0 /\ N e. NN0 ) -> ( 2 x. N ) e. NN0 )
79 5 78 mpan 
 |-  ( N e. NN0 -> ( 2 x. N ) e. NN0 )
80 nn0p1nn 
 |-  ( ( 2 x. N ) e. NN0 -> ( ( 2 x. N ) + 1 ) e. NN )
81 79 80 syl 
 |-  ( N e. NN0 -> ( ( 2 x. N ) + 1 ) e. NN )
82 nnmulcl 
 |-  ( ( 3 e. NN /\ ( ( 2 x. N ) + 1 ) e. NN ) -> ( 3 x. ( ( 2 x. N ) + 1 ) ) e. NN )
83 4 81 82 sylancr 
 |-  ( N e. NN0 -> ( 3 x. ( ( 2 x. N ) + 1 ) ) e. NN )
84 nndivre 
 |-  ( ( 2 e. RR /\ ( 3 x. ( ( 2 x. N ) + 1 ) ) e. NN ) -> ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) e. RR )
85 3 83 84 sylancr 
 |-  ( N e. NN0 -> ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) e. RR )
86 85 recnd 
 |-  ( N e. NN0 -> ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) e. CC )
87 86 adantr 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) e. CC )
88 15 nncnd 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> ( 9 ^ n ) e. CC )
89 15 nnne0d 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> ( 9 ^ n ) =/= 0 )
90 87 88 89 divrecd 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) / ( 9 ^ n ) ) = ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( 1 / ( 9 ^ n ) ) ) )
91 2cnd 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> 2 e. CC )
92 83 adantr 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> ( 3 x. ( ( 2 x. N ) + 1 ) ) e. NN )
93 92 nncnd 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> ( 3 x. ( ( 2 x. N ) + 1 ) ) e. CC )
94 92 nnne0d 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> ( 3 x. ( ( 2 x. N ) + 1 ) ) =/= 0 )
95 91 93 88 94 89 divdiv1d 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) / ( 9 ^ n ) ) = ( 2 / ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ n ) ) ) )
96 77 90 95 3eqtr2d 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( ( 1 / 9 ) ^ n ) ) = ( 2 / ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ n ) ) ) )
97 69 96 eqtrd 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> ( ( k e. NN0 |-> ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( ( 1 / 9 ) ^ k ) ) ) ` n ) = ( 2 / ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ n ) ) ) )
98 24 97 syldan 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( ( k e. NN0 |-> ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( ( 1 / 9 ) ^ k ) ) ) ` n ) = ( 2 / ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ n ) ) ) )
99 92 15 nnmulcld 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ n ) ) e. NN )
100 nndivre 
 |-  ( ( 2 e. RR /\ ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ n ) ) e. NN ) -> ( 2 / ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ n ) ) ) e. RR )
101 3 99 100 sylancr 
 |-  ( ( N e. NN0 /\ n e. NN0 ) -> ( 2 / ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ n ) ) ) e. RR )
102 24 101 syldan 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( 2 / ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ n ) ) ) e. RR )
103 79 adantr 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( 2 x. N ) e. NN0 )
104 103 nn0red 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( 2 x. N ) e. RR )
105 5 24 7 sylancr 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( 2 x. n ) e. NN0 )
106 105 nn0red 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( 2 x. n ) e. RR )
107 1red 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> 1 e. RR )
108 eluzle 
 |-  ( n e. ( ZZ>= ` N ) -> N <_ n )
109 108 adantl 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> N <_ n )
110 nn0re 
 |-  ( N e. NN0 -> N e. RR )
111 110 adantr 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> N e. RR )
112 24 nn0red 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> n e. RR )
113 3 a1i 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> 2 e. RR )
114 2pos 
 |-  0 < 2
115 114 a1i 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> 0 < 2 )
116 lemul2 
 |-  ( ( N e. RR /\ n e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( N <_ n <-> ( 2 x. N ) <_ ( 2 x. n ) ) )
117 111 112 113 115 116 syl112anc 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( N <_ n <-> ( 2 x. N ) <_ ( 2 x. n ) ) )
118 109 117 mpbid 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( 2 x. N ) <_ ( 2 x. n ) )
119 104 106 107 118 leadd1dd 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( ( 2 x. N ) + 1 ) <_ ( ( 2 x. n ) + 1 ) )
120 81 adantr 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( ( 2 x. N ) + 1 ) e. NN )
121 120 nnred 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( ( 2 x. N ) + 1 ) e. RR )
122 24 10 syldan 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( ( 2 x. n ) + 1 ) e. NN )
123 122 nnred 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( ( 2 x. n ) + 1 ) e. RR )
124 3re 
 |-  3 e. RR
125 124 a1i 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> 3 e. RR )
126 3pos 
 |-  0 < 3
127 126 a1i 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> 0 < 3 )
128 lemul2 
 |-  ( ( ( ( 2 x. N ) + 1 ) e. RR /\ ( ( 2 x. n ) + 1 ) e. RR /\ ( 3 e. RR /\ 0 < 3 ) ) -> ( ( ( 2 x. N ) + 1 ) <_ ( ( 2 x. n ) + 1 ) <-> ( 3 x. ( ( 2 x. N ) + 1 ) ) <_ ( 3 x. ( ( 2 x. n ) + 1 ) ) ) )
129 121 123 125 127 128 syl112anc 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( ( ( 2 x. N ) + 1 ) <_ ( ( 2 x. n ) + 1 ) <-> ( 3 x. ( ( 2 x. N ) + 1 ) ) <_ ( 3 x. ( ( 2 x. n ) + 1 ) ) ) )
130 119 129 mpbid 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( 3 x. ( ( 2 x. N ) + 1 ) ) <_ ( 3 x. ( ( 2 x. n ) + 1 ) ) )
131 83 adantr 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( 3 x. ( ( 2 x. N ) + 1 ) ) e. NN )
132 131 nnred 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( 3 x. ( ( 2 x. N ) + 1 ) ) e. RR )
133 24 12 syldan 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( 3 x. ( ( 2 x. n ) + 1 ) ) e. NN )
134 133 nnred 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( 3 x. ( ( 2 x. n ) + 1 ) ) e. RR )
135 13 24 14 sylancr 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( 9 ^ n ) e. NN )
136 135 nnred 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( 9 ^ n ) e. RR )
137 135 nngt0d 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> 0 < ( 9 ^ n ) )
138 lemul1 
 |-  ( ( ( 3 x. ( ( 2 x. N ) + 1 ) ) e. RR /\ ( 3 x. ( ( 2 x. n ) + 1 ) ) e. RR /\ ( ( 9 ^ n ) e. RR /\ 0 < ( 9 ^ n ) ) ) -> ( ( 3 x. ( ( 2 x. N ) + 1 ) ) <_ ( 3 x. ( ( 2 x. n ) + 1 ) ) <-> ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ n ) ) <_ ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) )
139 132 134 136 137 138 syl112anc 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( ( 3 x. ( ( 2 x. N ) + 1 ) ) <_ ( 3 x. ( ( 2 x. n ) + 1 ) ) <-> ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ n ) ) <_ ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) )
140 130 139 mpbid 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ n ) ) <_ ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) )
141 24 99 syldan 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ n ) ) e. NN )
142 141 nnred 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ n ) ) e. RR )
143 141 nngt0d 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> 0 < ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ n ) ) )
144 24 58 syldan 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) e. RR )
145 24 59 syldan 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> 0 < ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) )
146 lediv2 
 |-  ( ( ( ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ n ) ) e. RR /\ 0 < ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ n ) ) ) /\ ( ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) e. RR /\ 0 < ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ n ) ) <_ ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) <-> ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) <_ ( 2 / ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ n ) ) ) ) )
147 142 143 144 145 113 115 146 syl222anc 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ n ) ) <_ ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) <-> ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) <_ ( 2 / ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ n ) ) ) ) )
148 140 147 mpbid 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) <_ ( 2 / ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ n ) ) ) )
149 9re 
 |-  9 e. RR
150 149 72 rereccli 
 |-  ( 1 / 9 ) e. RR
151 150 recni 
 |-  ( 1 / 9 ) e. CC
152 151 a1i 
 |-  ( N e. NN0 -> ( 1 / 9 ) e. CC )
153 0re 
 |-  0 e. RR
154 9pos 
 |-  0 < 9
155 149 154 recgt0ii 
 |-  0 < ( 1 / 9 )
156 153 150 155 ltleii 
 |-  0 <_ ( 1 / 9 )
157 absid 
 |-  ( ( ( 1 / 9 ) e. RR /\ 0 <_ ( 1 / 9 ) ) -> ( abs ` ( 1 / 9 ) ) = ( 1 / 9 ) )
158 150 156 157 mp2an 
 |-  ( abs ` ( 1 / 9 ) ) = ( 1 / 9 )
159 1lt9 
 |-  1 < 9
160 recgt1i 
 |-  ( ( 9 e. RR /\ 1 < 9 ) -> ( 0 < ( 1 / 9 ) /\ ( 1 / 9 ) < 1 ) )
161 149 159 160 mp2an 
 |-  ( 0 < ( 1 / 9 ) /\ ( 1 / 9 ) < 1 )
162 161 simpri 
 |-  ( 1 / 9 ) < 1
163 158 162 eqbrtri 
 |-  ( abs ` ( 1 / 9 ) ) < 1
164 163 a1i 
 |-  ( N e. NN0 -> ( abs ` ( 1 / 9 ) ) < 1 )
165 eqid 
 |-  ( k e. NN0 |-> ( ( 1 / 9 ) ^ k ) ) = ( k e. NN0 |-> ( ( 1 / 9 ) ^ k ) )
166 ovex 
 |-  ( ( 1 / 9 ) ^ n ) e. _V
167 64 165 166 fvmpt 
 |-  ( n e. NN0 -> ( ( k e. NN0 |-> ( ( 1 / 9 ) ^ k ) ) ` n ) = ( ( 1 / 9 ) ^ n ) )
168 24 167 syl 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( ( k e. NN0 |-> ( ( 1 / 9 ) ^ k ) ) ` n ) = ( ( 1 / 9 ) ^ n ) )
169 152 164 42 168 geolim2 
 |-  ( N e. NN0 -> seq N ( + , ( k e. NN0 |-> ( ( 1 / 9 ) ^ k ) ) ) ~~> ( ( ( 1 / 9 ) ^ N ) / ( 1 - ( 1 / 9 ) ) ) )
170 70 a1i 
 |-  ( N e. NN0 -> 9 e. CC )
171 72 a1i 
 |-  ( N e. NN0 -> 9 =/= 0 )
172 170 171 23 exprecd 
 |-  ( N e. NN0 -> ( ( 1 / 9 ) ^ N ) = ( 1 / ( 9 ^ N ) ) )
173 70 72 dividi 
 |-  ( 9 / 9 ) = 1
174 173 oveq1i 
 |-  ( ( 9 / 9 ) - ( 1 / 9 ) ) = ( 1 - ( 1 / 9 ) )
175 ax-1cn 
 |-  1 e. CC
176 70 72 pm3.2i 
 |-  ( 9 e. CC /\ 9 =/= 0 )
177 divsubdir 
 |-  ( ( 9 e. CC /\ 1 e. CC /\ ( 9 e. CC /\ 9 =/= 0 ) ) -> ( ( 9 - 1 ) / 9 ) = ( ( 9 / 9 ) - ( 1 / 9 ) ) )
178 70 175 176 177 mp3an 
 |-  ( ( 9 - 1 ) / 9 ) = ( ( 9 / 9 ) - ( 1 / 9 ) )
179 9m1e8 
 |-  ( 9 - 1 ) = 8
180 179 oveq1i 
 |-  ( ( 9 - 1 ) / 9 ) = ( 8 / 9 )
181 178 180 eqtr3i 
 |-  ( ( 9 / 9 ) - ( 1 / 9 ) ) = ( 8 / 9 )
182 174 181 eqtr3i 
 |-  ( 1 - ( 1 / 9 ) ) = ( 8 / 9 )
183 182 a1i 
 |-  ( N e. NN0 -> ( 1 - ( 1 / 9 ) ) = ( 8 / 9 ) )
184 172 183 oveq12d 
 |-  ( N e. NN0 -> ( ( ( 1 / 9 ) ^ N ) / ( 1 - ( 1 / 9 ) ) ) = ( ( 1 / ( 9 ^ N ) ) / ( 8 / 9 ) ) )
185 175 a1i 
 |-  ( N e. NN0 -> 1 e. CC )
186 nnexpcl 
 |-  ( ( 9 e. NN /\ N e. NN0 ) -> ( 9 ^ N ) e. NN )
187 13 186 mpan 
 |-  ( N e. NN0 -> ( 9 ^ N ) e. NN )
188 187 nncnd 
 |-  ( N e. NN0 -> ( 9 ^ N ) e. CC )
189 8cn 
 |-  8 e. CC
190 189 70 72 divcli 
 |-  ( 8 / 9 ) e. CC
191 190 a1i 
 |-  ( N e. NN0 -> ( 8 / 9 ) e. CC )
192 187 nnne0d 
 |-  ( N e. NN0 -> ( 9 ^ N ) =/= 0 )
193 8nn 
 |-  8 e. NN
194 193 nnne0i 
 |-  8 =/= 0
195 189 70 194 72 divne0i 
 |-  ( 8 / 9 ) =/= 0
196 195 a1i 
 |-  ( N e. NN0 -> ( 8 / 9 ) =/= 0 )
197 185 188 191 192 196 divdiv32d 
 |-  ( N e. NN0 -> ( ( 1 / ( 9 ^ N ) ) / ( 8 / 9 ) ) = ( ( 1 / ( 8 / 9 ) ) / ( 9 ^ N ) ) )
198 recdiv 
 |-  ( ( ( 8 e. CC /\ 8 =/= 0 ) /\ ( 9 e. CC /\ 9 =/= 0 ) ) -> ( 1 / ( 8 / 9 ) ) = ( 9 / 8 ) )
199 189 194 70 72 198 mp4an 
 |-  ( 1 / ( 8 / 9 ) ) = ( 9 / 8 )
200 199 oveq1i 
 |-  ( ( 1 / ( 8 / 9 ) ) / ( 9 ^ N ) ) = ( ( 9 / 8 ) / ( 9 ^ N ) )
201 189 a1i 
 |-  ( N e. NN0 -> 8 e. CC )
202 194 a1i 
 |-  ( N e. NN0 -> 8 =/= 0 )
203 170 201 188 202 192 divdiv1d 
 |-  ( N e. NN0 -> ( ( 9 / 8 ) / ( 9 ^ N ) ) = ( 9 / ( 8 x. ( 9 ^ N ) ) ) )
204 200 203 eqtrid 
 |-  ( N e. NN0 -> ( ( 1 / ( 8 / 9 ) ) / ( 9 ^ N ) ) = ( 9 / ( 8 x. ( 9 ^ N ) ) ) )
205 184 197 204 3eqtrd 
 |-  ( N e. NN0 -> ( ( ( 1 / 9 ) ^ N ) / ( 1 - ( 1 / 9 ) ) ) = ( 9 / ( 8 x. ( 9 ^ N ) ) ) )
206 169 205 breqtrd 
 |-  ( N e. NN0 -> seq N ( + , ( k e. NN0 |-> ( ( 1 / 9 ) ^ k ) ) ) ~~> ( 9 / ( 8 x. ( 9 ^ N ) ) ) )
207 expcl 
 |-  ( ( ( 1 / 9 ) e. CC /\ n e. NN0 ) -> ( ( 1 / 9 ) ^ n ) e. CC )
208 151 24 207 sylancr 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( ( 1 / 9 ) ^ n ) e. CC )
209 168 208 eqeltrd 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( ( k e. NN0 |-> ( ( 1 / 9 ) ^ k ) ) ` n ) e. CC )
210 24 68 syl 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( ( k e. NN0 |-> ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( ( 1 / 9 ) ^ k ) ) ) ` n ) = ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( ( 1 / 9 ) ^ n ) ) )
211 168 oveq2d 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( ( k e. NN0 |-> ( ( 1 / 9 ) ^ k ) ) ` n ) ) = ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( ( 1 / 9 ) ^ n ) ) )
212 210 211 eqtr4d 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( ( k e. NN0 |-> ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( ( 1 / 9 ) ^ k ) ) ) ` n ) = ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( ( k e. NN0 |-> ( ( 1 / 9 ) ^ k ) ) ` n ) ) )
213 22 23 86 206 209 212 isermulc2 
 |-  ( N e. NN0 -> seq N ( + , ( k e. NN0 |-> ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( ( 1 / 9 ) ^ k ) ) ) ) ~~> ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( 9 / ( 8 x. ( 9 ^ N ) ) ) ) )
214 seqex 
 |-  seq N ( + , ( k e. NN0 |-> ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( ( 1 / 9 ) ^ k ) ) ) ) e. _V
215 ovex 
 |-  ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( 9 / ( 8 x. ( 9 ^ N ) ) ) ) e. _V
216 214 215 breldm 
 |-  ( seq N ( + , ( k e. NN0 |-> ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( ( 1 / 9 ) ^ k ) ) ) ) ~~> ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( 9 / ( 8 x. ( 9 ^ N ) ) ) ) -> seq N ( + , ( k e. NN0 |-> ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( ( 1 / 9 ) ^ k ) ) ) ) e. dom ~~> )
217 213 216 syl 
 |-  ( N e. NN0 -> seq N ( + , ( k e. NN0 |-> ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( ( 1 / 9 ) ^ k ) ) ) ) e. dom ~~> )
218 22 23 34 35 98 102 148 46 217 isumle 
 |-  ( N e. NN0 -> sum_ n e. ( ZZ>= ` N ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) <_ sum_ n e. ( ZZ>= ` N ) ( 2 / ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ n ) ) ) )
219 102 recnd 
 |-  ( ( N e. NN0 /\ n e. ( ZZ>= ` N ) ) -> ( 2 / ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ n ) ) ) e. CC )
220 3cn 
 |-  3 e. CC
221 4cn 
 |-  4 e. CC
222 2cn 
 |-  2 e. CC
223 4ne0 
 |-  4 =/= 0
224 3ne0 
 |-  3 =/= 0
225 2ne0 
 |-  2 =/= 0
226 220 221 222 220 223 224 225 divdivdivi 
 |-  ( ( 3 / 4 ) / ( 2 / 3 ) ) = ( ( 3 x. 3 ) / ( 4 x. 2 ) )
227 3t3e9 
 |-  ( 3 x. 3 ) = 9
228 4t2e8 
 |-  ( 4 x. 2 ) = 8
229 227 228 oveq12i 
 |-  ( ( 3 x. 3 ) / ( 4 x. 2 ) ) = ( 9 / 8 )
230 226 229 eqtri 
 |-  ( ( 3 / 4 ) / ( 2 / 3 ) ) = ( 9 / 8 )
231 230 oveq2i 
 |-  ( ( 2 / 3 ) x. ( ( 3 / 4 ) / ( 2 / 3 ) ) ) = ( ( 2 / 3 ) x. ( 9 / 8 ) )
232 220 221 223 divcli 
 |-  ( 3 / 4 ) e. CC
233 222 220 224 divcli 
 |-  ( 2 / 3 ) e. CC
234 222 220 225 224 divne0i 
 |-  ( 2 / 3 ) =/= 0
235 232 233 234 divcan2i 
 |-  ( ( 2 / 3 ) x. ( ( 3 / 4 ) / ( 2 / 3 ) ) ) = ( 3 / 4 )
236 231 235 eqtr3i 
 |-  ( ( 2 / 3 ) x. ( 9 / 8 ) ) = ( 3 / 4 )
237 236 oveq1i 
 |-  ( ( ( 2 / 3 ) x. ( 9 / 8 ) ) / ( ( ( 2 x. N ) + 1 ) x. ( 9 ^ N ) ) ) = ( ( 3 / 4 ) / ( ( ( 2 x. N ) + 1 ) x. ( 9 ^ N ) ) )
238 2cnd 
 |-  ( N e. NN0 -> 2 e. CC )
239 220 a1i 
 |-  ( N e. NN0 -> 3 e. CC )
240 81 nncnd 
 |-  ( N e. NN0 -> ( ( 2 x. N ) + 1 ) e. CC )
241 224 a1i 
 |-  ( N e. NN0 -> 3 =/= 0 )
242 81 nnne0d 
 |-  ( N e. NN0 -> ( ( 2 x. N ) + 1 ) =/= 0 )
243 238 239 240 241 242 divdiv1d 
 |-  ( N e. NN0 -> ( ( 2 / 3 ) / ( ( 2 x. N ) + 1 ) ) = ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) )
244 243 203 oveq12d 
 |-  ( N e. NN0 -> ( ( ( 2 / 3 ) / ( ( 2 x. N ) + 1 ) ) x. ( ( 9 / 8 ) / ( 9 ^ N ) ) ) = ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( 9 / ( 8 x. ( 9 ^ N ) ) ) ) )
245 233 a1i 
 |-  ( N e. NN0 -> ( 2 / 3 ) e. CC )
246 70 189 194 divcli 
 |-  ( 9 / 8 ) e. CC
247 246 a1i 
 |-  ( N e. NN0 -> ( 9 / 8 ) e. CC )
248 245 240 247 188 242 192 divmuldivd 
 |-  ( N e. NN0 -> ( ( ( 2 / 3 ) / ( ( 2 x. N ) + 1 ) ) x. ( ( 9 / 8 ) / ( 9 ^ N ) ) ) = ( ( ( 2 / 3 ) x. ( 9 / 8 ) ) / ( ( ( 2 x. N ) + 1 ) x. ( 9 ^ N ) ) ) )
249 244 248 eqtr3d 
 |-  ( N e. NN0 -> ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( 9 / ( 8 x. ( 9 ^ N ) ) ) ) = ( ( ( 2 / 3 ) x. ( 9 / 8 ) ) / ( ( ( 2 x. N ) + 1 ) x. ( 9 ^ N ) ) ) )
250 221 a1i 
 |-  ( N e. NN0 -> 4 e. CC )
251 250 240 188 mulassd 
 |-  ( N e. NN0 -> ( ( 4 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) = ( 4 x. ( ( ( 2 x. N ) + 1 ) x. ( 9 ^ N ) ) ) )
252 251 oveq2d 
 |-  ( N e. NN0 -> ( 3 / ( ( 4 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) ) = ( 3 / ( 4 x. ( ( ( 2 x. N ) + 1 ) x. ( 9 ^ N ) ) ) ) )
253 81 187 nnmulcld 
 |-  ( N e. NN0 -> ( ( ( 2 x. N ) + 1 ) x. ( 9 ^ N ) ) e. NN )
254 253 nncnd 
 |-  ( N e. NN0 -> ( ( ( 2 x. N ) + 1 ) x. ( 9 ^ N ) ) e. CC )
255 223 a1i 
 |-  ( N e. NN0 -> 4 =/= 0 )
256 253 nnne0d 
 |-  ( N e. NN0 -> ( ( ( 2 x. N ) + 1 ) x. ( 9 ^ N ) ) =/= 0 )
257 239 250 254 255 256 divdiv1d 
 |-  ( N e. NN0 -> ( ( 3 / 4 ) / ( ( ( 2 x. N ) + 1 ) x. ( 9 ^ N ) ) ) = ( 3 / ( 4 x. ( ( ( 2 x. N ) + 1 ) x. ( 9 ^ N ) ) ) ) )
258 252 257 eqtr4d 
 |-  ( N e. NN0 -> ( 3 / ( ( 4 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) ) = ( ( 3 / 4 ) / ( ( ( 2 x. N ) + 1 ) x. ( 9 ^ N ) ) ) )
259 237 249 258 3eqtr4a 
 |-  ( N e. NN0 -> ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( 9 / ( 8 x. ( 9 ^ N ) ) ) ) = ( 3 / ( ( 4 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) ) )
260 213 259 breqtrd 
 |-  ( N e. NN0 -> seq N ( + , ( k e. NN0 |-> ( ( 2 / ( 3 x. ( ( 2 x. N ) + 1 ) ) ) x. ( ( 1 / 9 ) ^ k ) ) ) ) ~~> ( 3 / ( ( 4 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) ) )
261 22 23 98 219 260 isumclim 
 |-  ( N e. NN0 -> sum_ n e. ( ZZ>= ` N ) ( 2 / ( ( 3 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ n ) ) ) = ( 3 / ( ( 4 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) ) )
262 218 261 breqtrd 
 |-  ( N e. NN0 -> sum_ n e. ( ZZ>= ` N ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) <_ ( 3 / ( ( 4 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) ) )
263 4nn 
 |-  4 e. NN
264 nnmulcl 
 |-  ( ( 4 e. NN /\ ( ( 2 x. N ) + 1 ) e. NN ) -> ( 4 x. ( ( 2 x. N ) + 1 ) ) e. NN )
265 263 81 264 sylancr 
 |-  ( N e. NN0 -> ( 4 x. ( ( 2 x. N ) + 1 ) ) e. NN )
266 265 187 nnmulcld 
 |-  ( N e. NN0 -> ( ( 4 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) e. NN )
267 nndivre 
 |-  ( ( 3 e. RR /\ ( ( 4 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) e. NN ) -> ( 3 / ( ( 4 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) ) e. RR )
268 124 266 267 sylancr 
 |-  ( N e. NN0 -> ( 3 / ( ( 4 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) ) e. RR )
269 elicc2 
 |-  ( ( 0 e. RR /\ ( 3 / ( ( 4 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) ) e. RR ) -> ( sum_ n e. ( ZZ>= ` N ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) e. ( 0 [,] ( 3 / ( ( 4 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) ) ) <-> ( sum_ n e. ( ZZ>= ` N ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) e. RR /\ 0 <_ sum_ n e. ( ZZ>= ` N ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) /\ sum_ n e. ( ZZ>= ` N ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) <_ ( 3 / ( ( 4 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) ) ) ) )
270 153 268 269 sylancr 
 |-  ( N e. NN0 -> ( sum_ n e. ( ZZ>= ` N ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) e. ( 0 [,] ( 3 / ( ( 4 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) ) ) <-> ( sum_ n e. ( ZZ>= ` N ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) e. RR /\ 0 <_ sum_ n e. ( ZZ>= ` N ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) /\ sum_ n e. ( ZZ>= ` N ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) <_ ( 3 / ( ( 4 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) ) ) ) )
271 47 63 262 270 mpbir3and 
 |-  ( N e. NN0 -> sum_ n e. ( ZZ>= ` N ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) e. ( 0 [,] ( 3 / ( ( 4 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) ) ) )
272 54 271 eqeltrd 
 |-  ( N e. NN0 -> ( ( log ` 2 ) - sum_ n e. ( 0 ... ( N - 1 ) ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) ) e. ( 0 [,] ( 3 / ( ( 4 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) ) ) )