Step |
Hyp |
Ref |
Expression |
1 |
|
aaliou3lem.a |
|- G = ( c e. ( ZZ>= ` A ) |-> ( ( 2 ^ -u ( ! ` A ) ) x. ( ( 1 / 2 ) ^ ( c - A ) ) ) ) |
2 |
|
aaliou3lem.b |
|- F = ( a e. NN |-> ( 2 ^ -u ( ! ` a ) ) ) |
3 |
|
eqid |
|- ( ZZ>= ` A ) = ( ZZ>= ` A ) |
4 |
|
nnz |
|- ( A e. NN -> A e. ZZ ) |
5 |
|
uzid |
|- ( A e. ZZ -> A e. ( ZZ>= ` A ) ) |
6 |
4 5
|
syl |
|- ( A e. NN -> A e. ( ZZ>= ` A ) ) |
7 |
1
|
aaliou3lem1 |
|- ( ( A e. NN /\ b e. ( ZZ>= ` A ) ) -> ( G ` b ) e. RR ) |
8 |
1 2
|
aaliou3lem2 |
|- ( ( A e. NN /\ b e. ( ZZ>= ` A ) ) -> ( F ` b ) e. ( 0 (,] ( G ` b ) ) ) |
9 |
|
0xr |
|- 0 e. RR* |
10 |
|
elioc2 |
|- ( ( 0 e. RR* /\ ( G ` b ) e. RR ) -> ( ( F ` b ) e. ( 0 (,] ( G ` b ) ) <-> ( ( F ` b ) e. RR /\ 0 < ( F ` b ) /\ ( F ` b ) <_ ( G ` b ) ) ) ) |
11 |
9 7 10
|
sylancr |
|- ( ( A e. NN /\ b e. ( ZZ>= ` A ) ) -> ( ( F ` b ) e. ( 0 (,] ( G ` b ) ) <-> ( ( F ` b ) e. RR /\ 0 < ( F ` b ) /\ ( F ` b ) <_ ( G ` b ) ) ) ) |
12 |
8 11
|
mpbid |
|- ( ( A e. NN /\ b e. ( ZZ>= ` A ) ) -> ( ( F ` b ) e. RR /\ 0 < ( F ` b ) /\ ( F ` b ) <_ ( G ` b ) ) ) |
13 |
12
|
simp1d |
|- ( ( A e. NN /\ b e. ( ZZ>= ` A ) ) -> ( F ` b ) e. RR ) |
14 |
|
halfcn |
|- ( 1 / 2 ) e. CC |
15 |
14
|
a1i |
|- ( A e. NN -> ( 1 / 2 ) e. CC ) |
16 |
|
halfre |
|- ( 1 / 2 ) e. RR |
17 |
|
halfgt0 |
|- 0 < ( 1 / 2 ) |
18 |
16 17
|
elrpii |
|- ( 1 / 2 ) e. RR+ |
19 |
|
rprege0 |
|- ( ( 1 / 2 ) e. RR+ -> ( ( 1 / 2 ) e. RR /\ 0 <_ ( 1 / 2 ) ) ) |
20 |
|
absid |
|- ( ( ( 1 / 2 ) e. RR /\ 0 <_ ( 1 / 2 ) ) -> ( abs ` ( 1 / 2 ) ) = ( 1 / 2 ) ) |
21 |
18 19 20
|
mp2b |
|- ( abs ` ( 1 / 2 ) ) = ( 1 / 2 ) |
22 |
|
halflt1 |
|- ( 1 / 2 ) < 1 |
23 |
21 22
|
eqbrtri |
|- ( abs ` ( 1 / 2 ) ) < 1 |
24 |
23
|
a1i |
|- ( A e. NN -> ( abs ` ( 1 / 2 ) ) < 1 ) |
25 |
|
2rp |
|- 2 e. RR+ |
26 |
|
nnnn0 |
|- ( A e. NN -> A e. NN0 ) |
27 |
26
|
faccld |
|- ( A e. NN -> ( ! ` A ) e. NN ) |
28 |
27
|
nnzd |
|- ( A e. NN -> ( ! ` A ) e. ZZ ) |
29 |
28
|
znegcld |
|- ( A e. NN -> -u ( ! ` A ) e. ZZ ) |
30 |
|
rpexpcl |
|- ( ( 2 e. RR+ /\ -u ( ! ` A ) e. ZZ ) -> ( 2 ^ -u ( ! ` A ) ) e. RR+ ) |
31 |
25 29 30
|
sylancr |
|- ( A e. NN -> ( 2 ^ -u ( ! ` A ) ) e. RR+ ) |
32 |
31
|
rpcnd |
|- ( A e. NN -> ( 2 ^ -u ( ! ` A ) ) e. CC ) |
33 |
4 15 24 32 1
|
geolim3 |
|- ( A e. NN -> seq A ( + , G ) ~~> ( ( 2 ^ -u ( ! ` A ) ) / ( 1 - ( 1 / 2 ) ) ) ) |
34 |
|
seqex |
|- seq A ( + , G ) e. _V |
35 |
|
ovex |
|- ( ( 2 ^ -u ( ! ` A ) ) / ( 1 - ( 1 / 2 ) ) ) e. _V |
36 |
34 35
|
breldm |
|- ( seq A ( + , G ) ~~> ( ( 2 ^ -u ( ! ` A ) ) / ( 1 - ( 1 / 2 ) ) ) -> seq A ( + , G ) e. dom ~~> ) |
37 |
33 36
|
syl |
|- ( A e. NN -> seq A ( + , G ) e. dom ~~> ) |
38 |
12
|
simp2d |
|- ( ( A e. NN /\ b e. ( ZZ>= ` A ) ) -> 0 < ( F ` b ) ) |
39 |
13 38
|
elrpd |
|- ( ( A e. NN /\ b e. ( ZZ>= ` A ) ) -> ( F ` b ) e. RR+ ) |
40 |
39
|
rpge0d |
|- ( ( A e. NN /\ b e. ( ZZ>= ` A ) ) -> 0 <_ ( F ` b ) ) |
41 |
12
|
simp3d |
|- ( ( A e. NN /\ b e. ( ZZ>= ` A ) ) -> ( F ` b ) <_ ( G ` b ) ) |
42 |
3 6 7 13 37 40 41
|
cvgcmp |
|- ( A e. NN -> seq A ( + , F ) e. dom ~~> ) |
43 |
|
eqidd |
|- ( ( A e. NN /\ b e. ( ZZ>= ` A ) ) -> ( F ` b ) = ( F ` b ) ) |
44 |
3 3 6 43 39 42
|
isumrpcl |
|- ( A e. NN -> sum_ b e. ( ZZ>= ` A ) ( F ` b ) e. RR+ ) |
45 |
|
eqidd |
|- ( ( A e. NN /\ b e. ( ZZ>= ` A ) ) -> ( G ` b ) = ( G ` b ) ) |
46 |
3 4 43 13 45 7 41 42 37
|
isumle |
|- ( A e. NN -> sum_ b e. ( ZZ>= ` A ) ( F ` b ) <_ sum_ b e. ( ZZ>= ` A ) ( G ` b ) ) |
47 |
7
|
recnd |
|- ( ( A e. NN /\ b e. ( ZZ>= ` A ) ) -> ( G ` b ) e. CC ) |
48 |
3 4 45 47 33
|
isumclim |
|- ( A e. NN -> sum_ b e. ( ZZ>= ` A ) ( G ` b ) = ( ( 2 ^ -u ( ! ` A ) ) / ( 1 - ( 1 / 2 ) ) ) ) |
49 |
|
1mhlfehlf |
|- ( 1 - ( 1 / 2 ) ) = ( 1 / 2 ) |
50 |
49
|
oveq2i |
|- ( ( 2 ^ -u ( ! ` A ) ) / ( 1 - ( 1 / 2 ) ) ) = ( ( 2 ^ -u ( ! ` A ) ) / ( 1 / 2 ) ) |
51 |
|
2cn |
|- 2 e. CC |
52 |
|
mulcl |
|- ( ( ( 2 ^ -u ( ! ` A ) ) e. CC /\ 2 e. CC ) -> ( ( 2 ^ -u ( ! ` A ) ) x. 2 ) e. CC ) |
53 |
32 51 52
|
sylancl |
|- ( A e. NN -> ( ( 2 ^ -u ( ! ` A ) ) x. 2 ) e. CC ) |
54 |
53
|
div1d |
|- ( A e. NN -> ( ( ( 2 ^ -u ( ! ` A ) ) x. 2 ) / 1 ) = ( ( 2 ^ -u ( ! ` A ) ) x. 2 ) ) |
55 |
|
1rp |
|- 1 e. RR+ |
56 |
|
rpcnne0 |
|- ( 1 e. RR+ -> ( 1 e. CC /\ 1 =/= 0 ) ) |
57 |
55 56
|
ax-mp |
|- ( 1 e. CC /\ 1 =/= 0 ) |
58 |
|
2cnne0 |
|- ( 2 e. CC /\ 2 =/= 0 ) |
59 |
|
divdiv2 |
|- ( ( ( 2 ^ -u ( ! ` A ) ) e. CC /\ ( 1 e. CC /\ 1 =/= 0 ) /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( 2 ^ -u ( ! ` A ) ) / ( 1 / 2 ) ) = ( ( ( 2 ^ -u ( ! ` A ) ) x. 2 ) / 1 ) ) |
60 |
57 58 59
|
mp3an23 |
|- ( ( 2 ^ -u ( ! ` A ) ) e. CC -> ( ( 2 ^ -u ( ! ` A ) ) / ( 1 / 2 ) ) = ( ( ( 2 ^ -u ( ! ` A ) ) x. 2 ) / 1 ) ) |
61 |
32 60
|
syl |
|- ( A e. NN -> ( ( 2 ^ -u ( ! ` A ) ) / ( 1 / 2 ) ) = ( ( ( 2 ^ -u ( ! ` A ) ) x. 2 ) / 1 ) ) |
62 |
|
mulcom |
|- ( ( 2 e. CC /\ ( 2 ^ -u ( ! ` A ) ) e. CC ) -> ( 2 x. ( 2 ^ -u ( ! ` A ) ) ) = ( ( 2 ^ -u ( ! ` A ) ) x. 2 ) ) |
63 |
51 32 62
|
sylancr |
|- ( A e. NN -> ( 2 x. ( 2 ^ -u ( ! ` A ) ) ) = ( ( 2 ^ -u ( ! ` A ) ) x. 2 ) ) |
64 |
54 61 63
|
3eqtr4d |
|- ( A e. NN -> ( ( 2 ^ -u ( ! ` A ) ) / ( 1 / 2 ) ) = ( 2 x. ( 2 ^ -u ( ! ` A ) ) ) ) |
65 |
50 64
|
syl5eq |
|- ( A e. NN -> ( ( 2 ^ -u ( ! ` A ) ) / ( 1 - ( 1 / 2 ) ) ) = ( 2 x. ( 2 ^ -u ( ! ` A ) ) ) ) |
66 |
48 65
|
eqtrd |
|- ( A e. NN -> sum_ b e. ( ZZ>= ` A ) ( G ` b ) = ( 2 x. ( 2 ^ -u ( ! ` A ) ) ) ) |
67 |
46 66
|
breqtrd |
|- ( A e. NN -> sum_ b e. ( ZZ>= ` A ) ( F ` b ) <_ ( 2 x. ( 2 ^ -u ( ! ` A ) ) ) ) |
68 |
42 44 67
|
3jca |
|- ( A e. NN -> ( seq A ( + , F ) e. dom ~~> /\ sum_ b e. ( ZZ>= ` A ) ( F ` b ) e. RR+ /\ sum_ b e. ( ZZ>= ` A ) ( F ` b ) <_ ( 2 x. ( 2 ^ -u ( ! ` A ) ) ) ) ) |