Step | Hyp | Ref
| Expression |
1 | | simp1 998 |
. . 3
โข ((๐ด โ โ โง ๐
โ โ โง
(absโ๐
) < 1)
โ ๐ด โ
โ) |
2 | | simp2 999 |
. . 3
โข ((๐ด โ โ โง ๐
โ โ โง
(absโ๐
) < 1)
โ ๐
โ
โ) |
3 | | 1cnd 7986 |
. . . 4
โข ((๐ด โ โ โง ๐
โ โ โง
(absโ๐
) < 1)
โ 1 โ โ) |
4 | 3, 2 | subcld 8281 |
. . 3
โข ((๐ด โ โ โง ๐
โ โ โง
(absโ๐
) < 1)
โ (1 โ ๐
) โ
โ) |
5 | | 1red 7985 |
. . . . . 6
โข ((๐ด โ โ โง ๐
โ โ โง
(absโ๐
) < 1)
โ 1 โ โ) |
6 | | simp3 1000 |
. . . . . 6
โข ((๐ด โ โ โง ๐
โ โ โง
(absโ๐
) < 1)
โ (absโ๐
) <
1) |
7 | 2, 5, 6 | absltap 11530 |
. . . . 5
โข ((๐ด โ โ โง ๐
โ โ โง
(absโ๐
) < 1)
โ ๐
#
1) |
8 | | apsym 8576 |
. . . . . 6
โข ((๐
โ โ โง 1 โ
โ) โ (๐
# 1
โ 1 # ๐
)) |
9 | 2, 3, 8 | syl2anc 411 |
. . . . 5
โข ((๐ด โ โ โง ๐
โ โ โง
(absโ๐
) < 1)
โ (๐
# 1 โ 1 #
๐
)) |
10 | 7, 9 | mpbid 147 |
. . . 4
โข ((๐ด โ โ โง ๐
โ โ โง
(absโ๐
) < 1)
โ 1 # ๐
) |
11 | 3, 2, 10 | subap0d 8614 |
. . 3
โข ((๐ด โ โ โง ๐
โ โ โง
(absโ๐
) < 1)
โ (1 โ ๐
) #
0) |
12 | 1, 2, 4, 11 | divassapd 8796 |
. 2
โข ((๐ด โ โ โง ๐
โ โ โง
(absโ๐
) < 1)
โ ((๐ด ยท ๐
) / (1 โ ๐
)) = (๐ด ยท (๐
/ (1 โ ๐
)))) |
13 | | geoisum1 11540 |
. . . 4
โข ((๐
โ โ โง
(absโ๐
) < 1)
โ ฮฃ๐ โ
โ (๐
โ๐) = (๐
/ (1 โ ๐
))) |
14 | 13 | 3adant1 1016 |
. . 3
โข ((๐ด โ โ โง ๐
โ โ โง
(absโ๐
) < 1)
โ ฮฃ๐ โ
โ (๐
โ๐) = (๐
/ (1 โ ๐
))) |
15 | 14 | oveq2d 5904 |
. 2
โข ((๐ด โ โ โง ๐
โ โ โง
(absโ๐
) < 1)
โ (๐ด ยท
ฮฃ๐ โ โ
(๐
โ๐)) = (๐ด ยท (๐
/ (1 โ ๐
)))) |
16 | | nnuz 9576 |
. . 3
โข โ =
(โคโฅโ1) |
17 | | 1zzd 9293 |
. . 3
โข ((๐ด โ โ โง ๐
โ โ โง
(absโ๐
) < 1)
โ 1 โ โค) |
18 | | simpr 110 |
. . . 4
โข (((๐ด โ โ โง ๐
โ โ โง
(absโ๐
) < 1) โง
๐ โ โ) โ
๐ โ
โ) |
19 | | simpl2 1002 |
. . . . 5
โข (((๐ด โ โ โง ๐
โ โ โง
(absโ๐
) < 1) โง
๐ โ โ) โ
๐
โ
โ) |
20 | 18 | nnnn0d 9242 |
. . . . 5
โข (((๐ด โ โ โง ๐
โ โ โง
(absโ๐
) < 1) โง
๐ โ โ) โ
๐ โ
โ0) |
21 | 19, 20 | expcld 10667 |
. . . 4
โข (((๐ด โ โ โง ๐
โ โ โง
(absโ๐
) < 1) โง
๐ โ โ) โ
(๐
โ๐) โ โ) |
22 | | oveq2 5896 |
. . . . 5
โข (๐ = ๐ โ (๐
โ๐) = (๐
โ๐)) |
23 | | eqid 2187 |
. . . . 5
โข (๐ โ โ โฆ (๐
โ๐)) = (๐ โ โ โฆ (๐
โ๐)) |
24 | 22, 23 | fvmptg 5605 |
. . . 4
โข ((๐ โ โ โง (๐
โ๐) โ โ) โ ((๐ โ โ โฆ (๐
โ๐))โ๐) = (๐
โ๐)) |
25 | 18, 21, 24 | syl2anc 411 |
. . 3
โข (((๐ด โ โ โง ๐
โ โ โง
(absโ๐
) < 1) โง
๐ โ โ) โ
((๐ โ โ โฆ
(๐
โ๐))โ๐) = (๐
โ๐)) |
26 | | nnnn0 9196 |
. . . . 5
โข (๐ โ โ โ ๐ โ
โ0) |
27 | 26 | adantl 277 |
. . . 4
โข (((๐ด โ โ โง ๐
โ โ โง
(absโ๐
) < 1) โง
๐ โ โ) โ
๐ โ
โ0) |
28 | 19, 27 | expcld 10667 |
. . 3
โข (((๐ด โ โ โง ๐
โ โ โง
(absโ๐
) < 1) โง
๐ โ โ) โ
(๐
โ๐) โ โ) |
29 | | seqex 10460 |
. . . 4
โข seq1( + ,
(๐ โ โ โฆ
(๐
โ๐))) โ V |
30 | | 1nn0 9205 |
. . . . . . 7
โข 1 โ
โ0 |
31 | 30 | a1i 9 |
. . . . . 6
โข ((๐ด โ โ โง ๐
โ โ โง
(absโ๐
) < 1)
โ 1 โ โ0) |
32 | | elnnuz 9577 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
(โคโฅโ1)) |
33 | 32, 25 | sylan2br 288 |
. . . . . 6
โข (((๐ด โ โ โง ๐
โ โ โง
(absโ๐
) < 1) โง
๐ โ
(โคโฅโ1)) โ ((๐ โ โ โฆ (๐
โ๐))โ๐) = (๐
โ๐)) |
34 | 2, 6, 31, 33 | geolim2 11533 |
. . . . 5
โข ((๐ด โ โ โง ๐
โ โ โง
(absโ๐
) < 1)
โ seq1( + , (๐ โ
โ โฆ (๐
โ๐))) โ ((๐
โ1) / (1 โ ๐
))) |
35 | | climcl 11303 |
. . . . 5
โข (seq1( +
, (๐ โ โ โฆ
(๐
โ๐))) โ ((๐
โ1) / (1 โ ๐
)) โ ((๐
โ1) / (1 โ ๐
)) โ โ) |
36 | 34, 35 | syl 14 |
. . . 4
โข ((๐ด โ โ โง ๐
โ โ โง
(absโ๐
) < 1)
โ ((๐
โ1) / (1
โ ๐
)) โ
โ) |
37 | | breldmg 4845 |
. . . 4
โข ((seq1( +
, (๐ โ โ โฆ
(๐
โ๐))) โ V โง ((๐
โ1) / (1 โ ๐
)) โ โ โง seq1( + , (๐ โ โ โฆ (๐
โ๐))) โ ((๐
โ1) / (1 โ ๐
))) โ seq1( + , (๐ โ โ โฆ (๐
โ๐))) โ dom โ ) |
38 | 29, 36, 34, 37 | mp3an2i 1352 |
. . 3
โข ((๐ด โ โ โง ๐
โ โ โง
(absโ๐
) < 1)
โ seq1( + , (๐ โ
โ โฆ (๐
โ๐))) โ dom โ ) |
39 | 16, 17, 25, 28, 38, 1 | isummulc2 11447 |
. 2
โข ((๐ด โ โ โง ๐
โ โ โง
(absโ๐
) < 1)
โ (๐ด ยท
ฮฃ๐ โ โ
(๐
โ๐)) = ฮฃ๐ โ โ (๐ด ยท (๐
โ๐))) |
40 | 12, 15, 39 | 3eqtr2rd 2227 |
1
โข ((๐ด โ โ โง ๐
โ โ โง
(absโ๐
) < 1)
โ ฮฃ๐ โ
โ (๐ด ยท (๐
โ๐)) = ((๐ด ยท ๐
) / (1 โ ๐
))) |