Step | Hyp | Ref
| Expression |
1 | | fzofi 13886 |
. . . . . 6
โข (๐..^๐) โ Fin |
2 | 1 | a1i 11 |
. . . . 5
โข (๐ โ (๐..^๐) โ Fin) |
3 | | ax-1cn 11116 |
. . . . . 6
โข 1 โ
โ |
4 | | geoserg.1 |
. . . . . 6
โข (๐ โ ๐ด โ โ) |
5 | | subcl 11407 |
. . . . . 6
โข ((1
โ โ โง ๐ด
โ โ) โ (1 โ ๐ด) โ โ) |
6 | 3, 4, 5 | sylancr 588 |
. . . . 5
โข (๐ โ (1 โ ๐ด) โ
โ) |
7 | 4 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ โ (๐..^๐)) โ ๐ด โ โ) |
8 | | geoserg.3 |
. . . . . . 7
โข (๐ โ ๐ โ
โ0) |
9 | | elfzouz 13583 |
. . . . . . 7
โข (๐ โ (๐..^๐) โ ๐ โ (โคโฅโ๐)) |
10 | | eluznn0 12849 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ๐ โ โ0) |
11 | 8, 9, 10 | syl2an 597 |
. . . . . 6
โข ((๐ โง ๐ โ (๐..^๐)) โ ๐ โ โ0) |
12 | 7, 11 | expcld 14058 |
. . . . 5
โข ((๐ โง ๐ โ (๐..^๐)) โ (๐ดโ๐) โ โ) |
13 | 2, 6, 12 | fsummulc1 15677 |
. . . 4
โข (๐ โ (ฮฃ๐ โ (๐..^๐)(๐ดโ๐) ยท (1 โ ๐ด)) = ฮฃ๐ โ (๐..^๐)((๐ดโ๐) ยท (1 โ ๐ด))) |
14 | 3 | a1i 11 |
. . . . . . 7
โข ((๐ โง ๐ โ (๐..^๐)) โ 1 โ โ) |
15 | 12, 14, 7 | subdid 11618 |
. . . . . 6
โข ((๐ โง ๐ โ (๐..^๐)) โ ((๐ดโ๐) ยท (1 โ ๐ด)) = (((๐ดโ๐) ยท 1) โ ((๐ดโ๐) ยท ๐ด))) |
16 | 12 | mulid1d 11179 |
. . . . . . 7
โข ((๐ โง ๐ โ (๐..^๐)) โ ((๐ดโ๐) ยท 1) = (๐ดโ๐)) |
17 | 7, 11 | expp1d 14059 |
. . . . . . . 8
โข ((๐ โง ๐ โ (๐..^๐)) โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
18 | 17 | eqcomd 2743 |
. . . . . . 7
โข ((๐ โง ๐ โ (๐..^๐)) โ ((๐ดโ๐) ยท ๐ด) = (๐ดโ(๐ + 1))) |
19 | 16, 18 | oveq12d 7380 |
. . . . . 6
โข ((๐ โง ๐ โ (๐..^๐)) โ (((๐ดโ๐) ยท 1) โ ((๐ดโ๐) ยท ๐ด)) = ((๐ดโ๐) โ (๐ดโ(๐ + 1)))) |
20 | 15, 19 | eqtrd 2777 |
. . . . 5
โข ((๐ โง ๐ โ (๐..^๐)) โ ((๐ดโ๐) ยท (1 โ ๐ด)) = ((๐ดโ๐) โ (๐ดโ(๐ + 1)))) |
21 | 20 | sumeq2dv 15595 |
. . . 4
โข (๐ โ ฮฃ๐ โ (๐..^๐)((๐ดโ๐) ยท (1 โ ๐ด)) = ฮฃ๐ โ (๐..^๐)((๐ดโ๐) โ (๐ดโ(๐ + 1)))) |
22 | | oveq2 7370 |
. . . . 5
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
23 | | oveq2 7370 |
. . . . 5
โข (๐ = (๐ + 1) โ (๐ดโ๐) = (๐ดโ(๐ + 1))) |
24 | | oveq2 7370 |
. . . . 5
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
25 | | oveq2 7370 |
. . . . 5
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
26 | | geoserg.4 |
. . . . 5
โข (๐ โ ๐ โ (โคโฅโ๐)) |
27 | 4 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ โ (๐...๐)) โ ๐ด โ โ) |
28 | | elfzuz 13444 |
. . . . . . 7
โข (๐ โ (๐...๐) โ ๐ โ (โคโฅโ๐)) |
29 | | eluznn0 12849 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ๐ โ โ0) |
30 | 8, 28, 29 | syl2an 597 |
. . . . . 6
โข ((๐ โง ๐ โ (๐...๐)) โ ๐ โ โ0) |
31 | 27, 30 | expcld 14058 |
. . . . 5
โข ((๐ โง ๐ โ (๐...๐)) โ (๐ดโ๐) โ โ) |
32 | 22, 23, 24, 25, 26, 31 | telfsumo 15694 |
. . . 4
โข (๐ โ ฮฃ๐ โ (๐..^๐)((๐ดโ๐) โ (๐ดโ(๐ + 1))) = ((๐ดโ๐) โ (๐ดโ๐))) |
33 | 13, 21, 32 | 3eqtrrd 2782 |
. . 3
โข (๐ โ ((๐ดโ๐) โ (๐ดโ๐)) = (ฮฃ๐ โ (๐..^๐)(๐ดโ๐) ยท (1 โ ๐ด))) |
34 | 4, 8 | expcld 14058 |
. . . . 5
โข (๐ โ (๐ดโ๐) โ โ) |
35 | | eluznn0 12849 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ๐ โ
โ0) |
36 | 8, 26, 35 | syl2anc 585 |
. . . . . 6
โข (๐ โ ๐ โ
โ0) |
37 | 4, 36 | expcld 14058 |
. . . . 5
โข (๐ โ (๐ดโ๐) โ โ) |
38 | 34, 37 | subcld 11519 |
. . . 4
โข (๐ โ ((๐ดโ๐) โ (๐ดโ๐)) โ โ) |
39 | 2, 12 | fsumcl 15625 |
. . . 4
โข (๐ โ ฮฃ๐ โ (๐..^๐)(๐ดโ๐) โ โ) |
40 | | geoserg.2 |
. . . . . 6
โข (๐ โ ๐ด โ 1) |
41 | 40 | necomd 3000 |
. . . . 5
โข (๐ โ 1 โ ๐ด) |
42 | | subeq0 11434 |
. . . . . . 7
โข ((1
โ โ โง ๐ด
โ โ) โ ((1 โ ๐ด) = 0 โ 1 = ๐ด)) |
43 | 3, 4, 42 | sylancr 588 |
. . . . . 6
โข (๐ โ ((1 โ ๐ด) = 0 โ 1 = ๐ด)) |
44 | 43 | necon3bid 2989 |
. . . . 5
โข (๐ โ ((1 โ ๐ด) โ 0 โ 1 โ ๐ด)) |
45 | 41, 44 | mpbird 257 |
. . . 4
โข (๐ โ (1 โ ๐ด) โ 0) |
46 | 38, 39, 6, 45 | divmul3d 11972 |
. . 3
โข (๐ โ ((((๐ดโ๐) โ (๐ดโ๐)) / (1 โ ๐ด)) = ฮฃ๐ โ (๐..^๐)(๐ดโ๐) โ ((๐ดโ๐) โ (๐ดโ๐)) = (ฮฃ๐ โ (๐..^๐)(๐ดโ๐) ยท (1 โ ๐ด)))) |
47 | 33, 46 | mpbird 257 |
. 2
โข (๐ โ (((๐ดโ๐) โ (๐ดโ๐)) / (1 โ ๐ด)) = ฮฃ๐ โ (๐..^๐)(๐ดโ๐)) |
48 | 47 | eqcomd 2743 |
1
โข (๐ โ ฮฃ๐ โ (๐..^๐)(๐ดโ๐) = (((๐ดโ๐) โ (๐ดโ๐)) / (1 โ ๐ด))) |