Step | Hyp | Ref
| Expression |
1 | | nn0uz 9564 |
. . 3
โข
โ0 = (โคโฅโ0) |
2 | | 0zd 9267 |
. . 3
โข (๐ โ 0 โ
โค) |
3 | | geolim.1 |
. . . . . 6
โข (๐ โ ๐ด โ โ) |
4 | | geolim.2 |
. . . . . 6
โข (๐ โ (absโ๐ด) < 1) |
5 | 3, 4 | expcnv 11514 |
. . . . 5
โข (๐ โ (๐ โ โ0 โฆ (๐ดโ๐)) โ 0) |
6 | | ax-1cn 7906 |
. . . . . . 7
โข 1 โ
โ |
7 | | subcl 8158 |
. . . . . . 7
โข ((1
โ โ โง ๐ด
โ โ) โ (1 โ ๐ด) โ โ) |
8 | 6, 3, 7 | sylancr 414 |
. . . . . 6
โข (๐ โ (1 โ ๐ด) โ
โ) |
9 | | 1cnd 7975 |
. . . . . . 7
โข (๐ โ 1 โ
โ) |
10 | | 1red 7974 |
. . . . . . . . 9
โข (๐ โ 1 โ
โ) |
11 | 3, 10, 4 | absltap 11519 |
. . . . . . . 8
โข (๐ โ ๐ด # 1) |
12 | | apsym 8565 |
. . . . . . . . 9
โข ((๐ด โ โ โง 1 โ
โ) โ (๐ด # 1
โ 1 # ๐ด)) |
13 | 3, 6, 12 | sylancl 413 |
. . . . . . . 8
โข (๐ โ (๐ด # 1 โ 1 # ๐ด)) |
14 | 11, 13 | mpbid 147 |
. . . . . . 7
โข (๐ โ 1 # ๐ด) |
15 | 9, 3, 14 | subap0d 8603 |
. . . . . 6
โข (๐ โ (1 โ ๐ด) # 0) |
16 | 3, 8, 15 | divclapd 8749 |
. . . . 5
โข (๐ โ (๐ด / (1 โ ๐ด)) โ โ) |
17 | | nn0ex 9184 |
. . . . . . 7
โข
โ0 โ V |
18 | 17 | mptex 5744 |
. . . . . 6
โข (๐ โ โ0
โฆ ((๐ดโ(๐ + 1)) / (1 โ ๐ด))) โ V |
19 | 18 | a1i 9 |
. . . . 5
โข (๐ โ (๐ โ โ0 โฆ ((๐ดโ(๐ + 1)) / (1 โ ๐ด))) โ V) |
20 | | simpr 110 |
. . . . . . 7
โข ((๐ โง ๐ โ โ0) โ ๐ โ
โ0) |
21 | 3 | adantr 276 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ ๐ด โ
โ) |
22 | 21, 20 | expcld 10656 |
. . . . . . 7
โข ((๐ โง ๐ โ โ0) โ (๐ดโ๐) โ โ) |
23 | | oveq2 5885 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
24 | | eqid 2177 |
. . . . . . . 8
โข (๐ โ โ0
โฆ (๐ดโ๐)) = (๐ โ โ0 โฆ (๐ดโ๐)) |
25 | 23, 24 | fvmptg 5594 |
. . . . . . 7
โข ((๐ โ โ0
โง (๐ดโ๐) โ โ) โ ((๐ โ โ0
โฆ (๐ดโ๐))โ๐) = (๐ดโ๐)) |
26 | 20, 22, 25 | syl2anc 411 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ ((๐ โ โ0
โฆ (๐ดโ๐))โ๐) = (๐ดโ๐)) |
27 | | expcl 10540 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ๐) โ
โ) |
28 | 3, 27 | sylan 283 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ (๐ดโ๐) โ โ) |
29 | 26, 28 | eqeltrd 2254 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ ((๐ โ โ0
โฆ (๐ดโ๐))โ๐) โ โ) |
30 | | expp1 10529 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
31 | 3, 30 | sylan 283 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ0) โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
32 | 28, 21 | mulcomd 7981 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ0) โ ((๐ดโ๐) ยท ๐ด) = (๐ด ยท (๐ดโ๐))) |
33 | 31, 32 | eqtrd 2210 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ (๐ดโ(๐ + 1)) = (๐ด ยท (๐ดโ๐))) |
34 | 33 | oveq1d 5892 |
. . . . . . 7
โข ((๐ โง ๐ โ โ0) โ ((๐ดโ(๐ + 1)) / (1 โ ๐ด)) = ((๐ด ยท (๐ดโ๐)) / (1 โ ๐ด))) |
35 | 8 | adantr 276 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ (1
โ ๐ด) โ
โ) |
36 | 15 | adantr 276 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ (1
โ ๐ด) #
0) |
37 | 21, 28, 35, 36 | div23apd 8787 |
. . . . . . 7
โข ((๐ โง ๐ โ โ0) โ ((๐ด ยท (๐ดโ๐)) / (1 โ ๐ด)) = ((๐ด / (1 โ ๐ด)) ยท (๐ดโ๐))) |
38 | 34, 37 | eqtrd 2210 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ ((๐ดโ(๐ + 1)) / (1 โ ๐ด)) = ((๐ด / (1 โ ๐ด)) ยท (๐ดโ๐))) |
39 | | peano2nn0 9218 |
. . . . . . . . . 10
โข (๐ โ โ0
โ (๐ + 1) โ
โ0) |
40 | 39 | adantl 277 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ0) โ (๐ + 1) โ
โ0) |
41 | 21, 40 | expcld 10656 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ (๐ดโ(๐ + 1)) โ โ) |
42 | 41, 35, 36 | divclapd 8749 |
. . . . . . 7
โข ((๐ โง ๐ โ โ0) โ ((๐ดโ(๐ + 1)) / (1 โ ๐ด)) โ โ) |
43 | | oveq1 5884 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐ + 1) = (๐ + 1)) |
44 | 43 | oveq2d 5893 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ดโ(๐ + 1)) = (๐ดโ(๐ + 1))) |
45 | 44 | oveq1d 5892 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐ดโ(๐ + 1)) / (1 โ ๐ด)) = ((๐ดโ(๐ + 1)) / (1 โ ๐ด))) |
46 | | eqid 2177 |
. . . . . . . 8
โข (๐ โ โ0
โฆ ((๐ดโ(๐ + 1)) / (1 โ ๐ด))) = (๐ โ โ0 โฆ ((๐ดโ(๐ + 1)) / (1 โ ๐ด))) |
47 | 45, 46 | fvmptg 5594 |
. . . . . . 7
โข ((๐ โ โ0
โง ((๐ดโ(๐ + 1)) / (1 โ ๐ด)) โ โ) โ
((๐ โ
โ0 โฆ ((๐ดโ(๐ + 1)) / (1 โ ๐ด)))โ๐) = ((๐ดโ(๐ + 1)) / (1 โ ๐ด))) |
48 | 20, 42, 47 | syl2anc 411 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ ((๐ โ โ0
โฆ ((๐ดโ(๐ + 1)) / (1 โ ๐ด)))โ๐) = ((๐ดโ(๐ + 1)) / (1 โ ๐ด))) |
49 | 26 | oveq2d 5893 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ ((๐ด / (1 โ ๐ด)) ยท ((๐ โ โ0 โฆ (๐ดโ๐))โ๐)) = ((๐ด / (1 โ ๐ด)) ยท (๐ดโ๐))) |
50 | 38, 48, 49 | 3eqtr4d 2220 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ ((๐ โ โ0
โฆ ((๐ดโ(๐ + 1)) / (1 โ ๐ด)))โ๐) = ((๐ด / (1 โ ๐ด)) ยท ((๐ โ โ0 โฆ (๐ดโ๐))โ๐))) |
51 | 1, 2, 5, 16, 19, 29, 50 | climmulc2 11341 |
. . . 4
โข (๐ โ (๐ โ โ0 โฆ ((๐ดโ(๐ + 1)) / (1 โ ๐ด))) โ ((๐ด / (1 โ ๐ด)) ยท 0)) |
52 | 16 | mul01d 8352 |
. . . 4
โข (๐ โ ((๐ด / (1 โ ๐ด)) ยท 0) = 0) |
53 | 51, 52 | breqtrd 4031 |
. . 3
โข (๐ โ (๐ โ โ0 โฆ ((๐ดโ(๐ + 1)) / (1 โ ๐ด))) โ 0) |
54 | 8, 15 | recclapd 8740 |
. . 3
โข (๐ โ (1 / (1 โ ๐ด)) โ
โ) |
55 | | seqex 10449 |
. . . 4
โข seq0( + ,
๐น) โ
V |
56 | 55 | a1i 9 |
. . 3
โข (๐ โ seq0( + , ๐น) โ V) |
57 | | expcl 10540 |
. . . . . 6
โข ((๐ด โ โ โง (๐ + 1) โ
โ0) โ (๐ดโ(๐ + 1)) โ โ) |
58 | 3, 39, 57 | syl2an 289 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ (๐ดโ(๐ + 1)) โ โ) |
59 | 58, 35, 36 | divclapd 8749 |
. . . 4
โข ((๐ โง ๐ โ โ0) โ ((๐ดโ(๐ + 1)) / (1 โ ๐ด)) โ โ) |
60 | 48, 59 | eqeltrd 2254 |
. . 3
โข ((๐ โง ๐ โ โ0) โ ((๐ โ โ0
โฆ ((๐ดโ(๐ + 1)) / (1 โ ๐ด)))โ๐) โ โ) |
61 | | nn0cn 9188 |
. . . . . . . 8
โข (๐ โ โ0
โ ๐ โ
โ) |
62 | 61 | adantl 277 |
. . . . . . 7
โข ((๐ โง ๐ โ โ0) โ ๐ โ
โ) |
63 | | pncan 8165 |
. . . . . . 7
โข ((๐ โ โ โง 1 โ
โ) โ ((๐ + 1)
โ 1) = ๐) |
64 | 62, 6, 63 | sylancl 413 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ ((๐ + 1) โ 1) = ๐) |
65 | 64 | oveq2d 5893 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ
(0...((๐ + 1) โ 1)) =
(0...๐)) |
66 | 65 | sumeq1d 11376 |
. . . 4
โข ((๐ โง ๐ โ โ0) โ
ฮฃ๐ โ
(0...((๐ + 1) โ
1))(๐ดโ๐) = ฮฃ๐ โ (0...๐)(๐ดโ๐)) |
67 | | 1cnd 7975 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ 1 โ
โ) |
68 | 67, 58, 35, 36 | divsubdirapd 8789 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ ((1
โ (๐ดโ(๐ + 1))) / (1 โ ๐ด)) = ((1 / (1 โ ๐ด)) โ ((๐ดโ(๐ + 1)) / (1 โ ๐ด)))) |
69 | 11 | adantr 276 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ ๐ด # 1) |
70 | 21, 69, 40 | geoserap 11517 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ
ฮฃ๐ โ
(0...((๐ + 1) โ
1))(๐ดโ๐) = ((1 โ (๐ดโ(๐ + 1))) / (1 โ ๐ด))) |
71 | 48 | oveq2d 5893 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ ((1 / (1
โ ๐ด)) โ ((๐ โ โ0
โฆ ((๐ดโ(๐ + 1)) / (1 โ ๐ด)))โ๐)) = ((1 / (1 โ ๐ด)) โ ((๐ดโ(๐ + 1)) / (1 โ ๐ด)))) |
72 | 68, 70, 71 | 3eqtr4d 2220 |
. . . 4
โข ((๐ โง ๐ โ โ0) โ
ฮฃ๐ โ
(0...((๐ + 1) โ
1))(๐ดโ๐) = ((1 / (1 โ ๐ด)) โ ((๐ โ โ0 โฆ ((๐ดโ(๐ + 1)) / (1 โ ๐ด)))โ๐))) |
73 | | simpll 527 |
. . . . . 6
โข (((๐ โง ๐ โ โ0) โง ๐ โ
(โคโฅโ0)) โ ๐) |
74 | | elnn0uz 9567 |
. . . . . . . 8
โข (๐ โ โ0
โ ๐ โ
(โคโฅโ0)) |
75 | 74 | biimpri 133 |
. . . . . . 7
โข (๐ โ
(โคโฅโ0) โ ๐ โ โ0) |
76 | 75 | adantl 277 |
. . . . . 6
โข (((๐ โง ๐ โ โ0) โง ๐ โ
(โคโฅโ0)) โ ๐ โ โ0) |
77 | | geolim.3 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ (๐นโ๐) = (๐ดโ๐)) |
78 | 73, 76, 77 | syl2anc 411 |
. . . . 5
โข (((๐ โง ๐ โ โ0) โง ๐ โ
(โคโฅโ0)) โ (๐นโ๐) = (๐ดโ๐)) |
79 | 20, 1 | eleqtrdi 2270 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ ๐ โ
(โคโฅโ0)) |
80 | 21 | adantr 276 |
. . . . . 6
โข (((๐ โง ๐ โ โ0) โง ๐ โ
(โคโฅโ0)) โ ๐ด โ โ) |
81 | 80, 76 | expcld 10656 |
. . . . 5
โข (((๐ โง ๐ โ โ0) โง ๐ โ
(โคโฅโ0)) โ (๐ดโ๐) โ โ) |
82 | 78, 79, 81 | fsum3ser 11407 |
. . . 4
โข ((๐ โง ๐ โ โ0) โ
ฮฃ๐ โ (0...๐)(๐ดโ๐) = (seq0( + , ๐น)โ๐)) |
83 | 66, 72, 82 | 3eqtr3rd 2219 |
. . 3
โข ((๐ โง ๐ โ โ0) โ (seq0( +
, ๐น)โ๐) = ((1 / (1 โ ๐ด)) โ ((๐ โ โ0 โฆ ((๐ดโ(๐ + 1)) / (1 โ ๐ด)))โ๐))) |
84 | 1, 2, 53, 54, 56, 60, 83 | climsubc2 11343 |
. 2
โข (๐ โ seq0( + , ๐น) โ ((1 / (1 โ ๐ด)) โ 0)) |
85 | 54 | subid1d 8259 |
. 2
โข (๐ โ ((1 / (1 โ ๐ด)) โ 0) = (1 / (1 โ
๐ด))) |
86 | 84, 85 | breqtrd 4031 |
1
โข (๐ โ seq0( + , ๐น) โ (1 / (1 โ ๐ด))) |