Step | Hyp | Ref
| Expression |
1 | | geoserg.3 |
. . . . . . 7
โข (๐ โ ๐ โ
โ0) |
2 | 1 | nn0zd 9372 |
. . . . . 6
โข (๐ โ ๐ โ โค) |
3 | | geoserg.4 |
. . . . . . 7
โข (๐ โ ๐ โ (โคโฅโ๐)) |
4 | | eluzelz 9536 |
. . . . . . 7
โข (๐ โ
(โคโฅโ๐) โ ๐ โ โค) |
5 | 3, 4 | syl 14 |
. . . . . 6
โข (๐ โ ๐ โ โค) |
6 | | fzofig 10431 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โค) โ (๐..^๐) โ Fin) |
7 | 2, 5, 6 | syl2anc 411 |
. . . . 5
โข (๐ โ (๐..^๐) โ Fin) |
8 | | ax-1cn 7903 |
. . . . . 6
โข 1 โ
โ |
9 | | geoserg.1 |
. . . . . 6
โข (๐ โ ๐ด โ โ) |
10 | | subcl 8155 |
. . . . . 6
โข ((1
โ โ โง ๐ด
โ โ) โ (1 โ ๐ด) โ โ) |
11 | 8, 9, 10 | sylancr 414 |
. . . . 5
โข (๐ โ (1 โ ๐ด) โ
โ) |
12 | 9 | adantr 276 |
. . . . . 6
โข ((๐ โง ๐ โ (๐..^๐)) โ ๐ด โ โ) |
13 | | elfzouz 10150 |
. . . . . . 7
โข (๐ โ (๐..^๐) โ ๐ โ (โคโฅโ๐)) |
14 | | eluznn0 9598 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ๐ โ โ0) |
15 | 1, 13, 14 | syl2an 289 |
. . . . . 6
โข ((๐ โง ๐ โ (๐..^๐)) โ ๐ โ โ0) |
16 | 12, 15 | expcld 10653 |
. . . . 5
โข ((๐ โง ๐ โ (๐..^๐)) โ (๐ดโ๐) โ โ) |
17 | 7, 11, 16 | fsummulc1 11456 |
. . . 4
โข (๐ โ (ฮฃ๐ โ (๐..^๐)(๐ดโ๐) ยท (1 โ ๐ด)) = ฮฃ๐ โ (๐..^๐)((๐ดโ๐) ยท (1 โ ๐ด))) |
18 | | 1cnd 7972 |
. . . . . . 7
โข ((๐ โง ๐ โ (๐..^๐)) โ 1 โ โ) |
19 | 16, 18, 12 | subdid 8370 |
. . . . . 6
โข ((๐ โง ๐ โ (๐..^๐)) โ ((๐ดโ๐) ยท (1 โ ๐ด)) = (((๐ดโ๐) ยท 1) โ ((๐ดโ๐) ยท ๐ด))) |
20 | 16 | mulridd 7973 |
. . . . . . 7
โข ((๐ โง ๐ โ (๐..^๐)) โ ((๐ดโ๐) ยท 1) = (๐ดโ๐)) |
21 | 12, 15 | expp1d 10654 |
. . . . . . . 8
โข ((๐ โง ๐ โ (๐..^๐)) โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
22 | 21 | eqcomd 2183 |
. . . . . . 7
โข ((๐ โง ๐ โ (๐..^๐)) โ ((๐ดโ๐) ยท ๐ด) = (๐ดโ(๐ + 1))) |
23 | 20, 22 | oveq12d 5892 |
. . . . . 6
โข ((๐ โง ๐ โ (๐..^๐)) โ (((๐ดโ๐) ยท 1) โ ((๐ดโ๐) ยท ๐ด)) = ((๐ดโ๐) โ (๐ดโ(๐ + 1)))) |
24 | 19, 23 | eqtrd 2210 |
. . . . 5
โข ((๐ โง ๐ โ (๐..^๐)) โ ((๐ดโ๐) ยท (1 โ ๐ด)) = ((๐ดโ๐) โ (๐ดโ(๐ + 1)))) |
25 | 24 | sumeq2dv 11375 |
. . . 4
โข (๐ โ ฮฃ๐ โ (๐..^๐)((๐ดโ๐) ยท (1 โ ๐ด)) = ฮฃ๐ โ (๐..^๐)((๐ดโ๐) โ (๐ดโ(๐ + 1)))) |
26 | | oveq2 5882 |
. . . . 5
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
27 | | oveq2 5882 |
. . . . 5
โข (๐ = (๐ + 1) โ (๐ดโ๐) = (๐ดโ(๐ + 1))) |
28 | | oveq2 5882 |
. . . . 5
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
29 | | oveq2 5882 |
. . . . 5
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
30 | 9 | adantr 276 |
. . . . . 6
โข ((๐ โง ๐ โ (๐...๐)) โ ๐ด โ โ) |
31 | | elfzuz 10020 |
. . . . . . 7
โข (๐ โ (๐...๐) โ ๐ โ (โคโฅโ๐)) |
32 | | eluznn0 9598 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ๐ โ โ0) |
33 | 1, 31, 32 | syl2an 289 |
. . . . . 6
โข ((๐ โง ๐ โ (๐...๐)) โ ๐ โ โ0) |
34 | 30, 33 | expcld 10653 |
. . . . 5
โข ((๐ โง ๐ โ (๐...๐)) โ (๐ดโ๐) โ โ) |
35 | 26, 27, 28, 29, 3, 34 | telfsumo 11473 |
. . . 4
โข (๐ โ ฮฃ๐ โ (๐..^๐)((๐ดโ๐) โ (๐ดโ(๐ + 1))) = ((๐ดโ๐) โ (๐ดโ๐))) |
36 | 17, 25, 35 | 3eqtrrd 2215 |
. . 3
โข (๐ โ ((๐ดโ๐) โ (๐ดโ๐)) = (ฮฃ๐ โ (๐..^๐)(๐ดโ๐) ยท (1 โ ๐ด))) |
37 | 9, 1 | expcld 10653 |
. . . . 5
โข (๐ โ (๐ดโ๐) โ โ) |
38 | | eluznn0 9598 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ๐ โ
โ0) |
39 | 1, 3, 38 | syl2anc 411 |
. . . . . 6
โข (๐ โ ๐ โ
โ0) |
40 | 9, 39 | expcld 10653 |
. . . . 5
โข (๐ โ (๐ดโ๐) โ โ) |
41 | 37, 40 | subcld 8267 |
. . . 4
โข (๐ โ ((๐ดโ๐) โ (๐ดโ๐)) โ โ) |
42 | 7, 16 | fsumcl 11407 |
. . . 4
โข (๐ โ ฮฃ๐ โ (๐..^๐)(๐ดโ๐) โ โ) |
43 | | geosergap.2 |
. . . . . . 7
โข (๐ โ ๐ด # 1) |
44 | | 1cnd 7972 |
. . . . . . . 8
โข (๐ โ 1 โ
โ) |
45 | | apneg 8567 |
. . . . . . . 8
โข ((๐ด โ โ โง 1 โ
โ) โ (๐ด # 1
โ -๐ด #
-1)) |
46 | 9, 44, 45 | syl2anc 411 |
. . . . . . 7
โข (๐ โ (๐ด # 1 โ -๐ด # -1)) |
47 | 43, 46 | mpbid 147 |
. . . . . 6
โข (๐ โ -๐ด # -1) |
48 | 9 | negcld 8254 |
. . . . . . 7
โข (๐ โ -๐ด โ โ) |
49 | 44 | negcld 8254 |
. . . . . . 7
โข (๐ โ -1 โ
โ) |
50 | | apadd2 8565 |
. . . . . . 7
โข ((-๐ด โ โ โง -1 โ
โ โง 1 โ โ) โ (-๐ด # -1 โ (1 + -๐ด) # (1 + -1))) |
51 | 48, 49, 44, 50 | syl3anc 1238 |
. . . . . 6
โข (๐ โ (-๐ด # -1 โ (1 + -๐ด) # (1 + -1))) |
52 | 47, 51 | mpbid 147 |
. . . . 5
โข (๐ โ (1 + -๐ด) # (1 + -1)) |
53 | 44, 9 | negsubd 8273 |
. . . . 5
โข (๐ โ (1 + -๐ด) = (1 โ ๐ด)) |
54 | | 1pneg1e0 9029 |
. . . . . 6
โข (1 + -1)
= 0 |
55 | 54 | a1i 9 |
. . . . 5
โข (๐ โ (1 + -1) =
0) |
56 | 52, 53, 55 | 3brtr3d 4034 |
. . . 4
โข (๐ โ (1 โ ๐ด) # 0) |
57 | 41, 42, 11, 56 | divmulap3d 8781 |
. . 3
โข (๐ โ ((((๐ดโ๐) โ (๐ดโ๐)) / (1 โ ๐ด)) = ฮฃ๐ โ (๐..^๐)(๐ดโ๐) โ ((๐ดโ๐) โ (๐ดโ๐)) = (ฮฃ๐ โ (๐..^๐)(๐ดโ๐) ยท (1 โ ๐ด)))) |
58 | 36, 57 | mpbird 167 |
. 2
โข (๐ โ (((๐ดโ๐) โ (๐ดโ๐)) / (1 โ ๐ด)) = ฮฃ๐ โ (๐..^๐)(๐ดโ๐)) |
59 | 58 | eqcomd 2183 |
1
โข (๐ โ ฮฃ๐ โ (๐..^๐)(๐ดโ๐) = (((๐ดโ๐) โ (๐ดโ๐)) / (1 โ ๐ด))) |