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