Step | Hyp | Ref
| Expression |
1 | | cvgratnn.m |
. . . . 5
โข (๐ โ ๐ โ โ) |
2 | 1 | nnzd 9373 |
. . . 4
โข (๐ โ ๐ โ โค) |
3 | | 1zzd 9279 |
. . . 4
โข (๐ โ 1 โ
โค) |
4 | | cvgratnn.n |
. . . . . 6
โข (๐ โ ๐ โ (โคโฅโ๐)) |
5 | | eluzelz 9536 |
. . . . . 6
โข (๐ โ
(โคโฅโ๐) โ ๐ โ โค) |
6 | 4, 5 | syl 14 |
. . . . 5
โข (๐ โ ๐ โ โค) |
7 | 6, 2 | zsubcld 9379 |
. . . 4
โข (๐ โ (๐ โ ๐) โ โค) |
8 | | cvgratnn.3 |
. . . . . . 7
โข (๐ โ ๐ด โ โ) |
9 | 8 | recnd 7985 |
. . . . . 6
โข (๐ โ ๐ด โ โ) |
10 | 9 | adantr 276 |
. . . . 5
โข ((๐ โง ๐ โ (1...(๐ โ ๐))) โ ๐ด โ โ) |
11 | | elfznn 10053 |
. . . . . . 7
โข (๐ โ (1...(๐ โ ๐)) โ ๐ โ โ) |
12 | 11 | adantl 277 |
. . . . . 6
โข ((๐ โง ๐ โ (1...(๐ โ ๐))) โ ๐ โ โ) |
13 | 12 | nnnn0d 9228 |
. . . . 5
โข ((๐ โง ๐ โ (1...(๐ โ ๐))) โ ๐ โ โ0) |
14 | 10, 13 | expcld 10653 |
. . . 4
โข ((๐ โง ๐ โ (1...(๐ โ ๐))) โ (๐ดโ๐) โ โ) |
15 | | oveq2 5882 |
. . . 4
โข (๐ = (๐ โ ๐) โ (๐ดโ๐) = (๐ดโ(๐ โ ๐))) |
16 | 2, 3, 7, 14, 15 | fsumshft 11451 |
. . 3
โข (๐ โ ฮฃ๐ โ (1...(๐ โ ๐))(๐ดโ๐) = ฮฃ๐ โ ((1 + ๐)...((๐ โ ๐) + ๐))(๐ดโ(๐ โ ๐))) |
17 | | 1cnd 7972 |
. . . . . 6
โข (๐ โ 1 โ
โ) |
18 | 1 | nncnd 8932 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
19 | 17, 18 | addcomd 8107 |
. . . . 5
โข (๐ โ (1 + ๐) = (๐ + 1)) |
20 | 6 | zcnd 9375 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
21 | 20, 18 | npcand 8271 |
. . . . 5
โข (๐ โ ((๐ โ ๐) + ๐) = ๐) |
22 | 19, 21 | oveq12d 5892 |
. . . 4
โข (๐ โ ((1 + ๐)...((๐ โ ๐) + ๐)) = ((๐ + 1)...๐)) |
23 | 22 | sumeq1d 11373 |
. . 3
โข (๐ โ ฮฃ๐ โ ((1 + ๐)...((๐ โ ๐) + ๐))(๐ดโ(๐ โ ๐)) = ฮฃ๐ โ ((๐ + 1)...๐)(๐ดโ(๐ โ ๐))) |
24 | 16, 23 | eqtrd 2210 |
. 2
โข (๐ โ ฮฃ๐ โ (1...(๐ โ ๐))(๐ดโ๐) = ฮฃ๐ โ ((๐ + 1)...๐)(๐ดโ(๐ โ ๐))) |
25 | | fzval3 10203 |
. . . . 5
โข ((๐ โ ๐) โ โค โ (1...(๐ โ ๐)) = (1..^((๐ โ ๐) + 1))) |
26 | 25 | sumeq1d 11373 |
. . . 4
โข ((๐ โ ๐) โ โค โ ฮฃ๐ โ (1...(๐ โ ๐))(๐ดโ๐) = ฮฃ๐ โ (1..^((๐ โ ๐) + 1))(๐ดโ๐)) |
27 | 7, 26 | syl 14 |
. . 3
โข (๐ โ ฮฃ๐ โ (1...(๐ โ ๐))(๐ดโ๐) = ฮฃ๐ โ (1..^((๐ โ ๐) + 1))(๐ดโ๐)) |
28 | | 1red 7971 |
. . . . . 6
โข (๐ โ 1 โ
โ) |
29 | | cvgratnn.4 |
. . . . . 6
โข (๐ โ ๐ด < 1) |
30 | 8, 28, 29 | ltapd 8594 |
. . . . 5
โข (๐ โ ๐ด # 1) |
31 | | 1nn0 9191 |
. . . . . 6
โข 1 โ
โ0 |
32 | 31 | a1i 9 |
. . . . 5
โข (๐ โ 1 โ
โ0) |
33 | 7 | peano2zd 9377 |
. . . . . 6
โข (๐ โ ((๐ โ ๐) + 1) โ โค) |
34 | | eluzle 9539 |
. . . . . . . . 9
โข (๐ โ
(โคโฅโ๐) โ ๐ โค ๐) |
35 | 4, 34 | syl 14 |
. . . . . . . 8
โข (๐ โ ๐ โค ๐) |
36 | 6 | zred 9374 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
37 | 1 | nnred 8931 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
38 | 36, 37 | subge0d 8491 |
. . . . . . . 8
โข (๐ โ (0 โค (๐ โ ๐) โ ๐ โค ๐)) |
39 | 35, 38 | mpbird 167 |
. . . . . . 7
โข (๐ โ 0 โค (๐ โ ๐)) |
40 | 7 | zred 9374 |
. . . . . . . 8
โข (๐ โ (๐ โ ๐) โ โ) |
41 | 28, 40 | addge02d 8490 |
. . . . . . 7
โข (๐ โ (0 โค (๐ โ ๐) โ 1 โค ((๐ โ ๐) + 1))) |
42 | 39, 41 | mpbid 147 |
. . . . . 6
โข (๐ โ 1 โค ((๐ โ ๐) + 1)) |
43 | | eluz2 9533 |
. . . . . 6
โข (((๐ โ ๐) + 1) โ
(โคโฅโ1) โ (1 โ โค โง ((๐ โ ๐) + 1) โ โค โง 1 โค ((๐ โ ๐) + 1))) |
44 | 3, 33, 42, 43 | syl3anbrc 1181 |
. . . . 5
โข (๐ โ ((๐ โ ๐) + 1) โ
(โคโฅโ1)) |
45 | 9, 30, 32, 44 | geosergap 11513 |
. . . 4
โข (๐ โ ฮฃ๐ โ (1..^((๐ โ ๐) + 1))(๐ดโ๐) = (((๐ดโ1) โ (๐ดโ((๐ โ ๐) + 1))) / (1 โ ๐ด))) |
46 | 9 | exp1d 10648 |
. . . . . . 7
โข (๐ โ (๐ดโ1) = ๐ด) |
47 | 46, 8 | eqeltrd 2254 |
. . . . . 6
โข (๐ โ (๐ดโ1) โ โ) |
48 | | cvgratnn.gt0 |
. . . . . . . . 9
โข (๐ โ 0 < ๐ด) |
49 | 8, 48 | elrpd 9692 |
. . . . . . . 8
โข (๐ โ ๐ด โ
โ+) |
50 | 49, 33 | rpexpcld 10677 |
. . . . . . 7
โข (๐ โ (๐ดโ((๐ โ ๐) + 1)) โ
โ+) |
51 | 50 | rpred 9695 |
. . . . . 6
โข (๐ โ (๐ดโ((๐ โ ๐) + 1)) โ โ) |
52 | 47, 51 | resubcld 8337 |
. . . . 5
โข (๐ โ ((๐ดโ1) โ (๐ดโ((๐ โ ๐) + 1))) โ โ) |
53 | 28, 8 | resubcld 8337 |
. . . . . 6
โข (๐ โ (1 โ ๐ด) โ
โ) |
54 | 8, 28 | posdifd 8488 |
. . . . . . 7
โข (๐ โ (๐ด < 1 โ 0 < (1 โ ๐ด))) |
55 | 29, 54 | mpbid 147 |
. . . . . 6
โข (๐ โ 0 < (1 โ ๐ด)) |
56 | 53, 55 | elrpd 9692 |
. . . . 5
โข (๐ โ (1 โ ๐ด) โ
โ+) |
57 | 46 | oveq1d 5889 |
. . . . . 6
โข (๐ โ ((๐ดโ1) โ (๐ดโ((๐ โ ๐) + 1))) = (๐ด โ (๐ดโ((๐ โ ๐) + 1)))) |
58 | 8, 50 | ltsubrpd 9728 |
. . . . . 6
โข (๐ โ (๐ด โ (๐ดโ((๐ โ ๐) + 1))) < ๐ด) |
59 | 57, 58 | eqbrtrd 4025 |
. . . . 5
โข (๐ โ ((๐ดโ1) โ (๐ดโ((๐ โ ๐) + 1))) < ๐ด) |
60 | 52, 8, 56, 59 | ltdiv1dd 9753 |
. . . 4
โข (๐ โ (((๐ดโ1) โ (๐ดโ((๐ โ ๐) + 1))) / (1 โ ๐ด)) < (๐ด / (1 โ ๐ด))) |
61 | 45, 60 | eqbrtrd 4025 |
. . 3
โข (๐ โ ฮฃ๐ โ (1..^((๐ โ ๐) + 1))(๐ดโ๐) < (๐ด / (1 โ ๐ด))) |
62 | 27, 61 | eqbrtrd 4025 |
. 2
โข (๐ โ ฮฃ๐ โ (1...(๐ โ ๐))(๐ดโ๐) < (๐ด / (1 โ ๐ด))) |
63 | 24, 62 | eqbrtrrd 4027 |
1
โข (๐ โ ฮฃ๐ โ ((๐ + 1)...๐)(๐ดโ(๐ โ ๐)) < (๐ด / (1 โ ๐ด))) |