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 syl5eq
 |-  ( 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 ) ) ) ) )