Step | Hyp | Ref
| Expression |
1 | | nn0uz 12812 |
. . 3
โข
โ0 = (โคโฅโ0) |
2 | | 0zd 12518 |
. . 3
โข (๐ โ 0 โ
โค) |
3 | | geolim.1 |
. . . . . 6
โข (๐ โ ๐ด โ โ) |
4 | | geolim.2 |
. . . . . 6
โข (๐ โ (absโ๐ด) < 1) |
5 | 3, 4 | expcnv 15756 |
. . . . 5
โข (๐ โ (๐ โ โ0 โฆ (๐ดโ๐)) โ 0) |
6 | | ax-1cn 11116 |
. . . . . . 7
โข 1 โ
โ |
7 | | subcl 11407 |
. . . . . . 7
โข ((1
โ โ โง ๐ด
โ โ) โ (1 โ ๐ด) โ โ) |
8 | 6, 3, 7 | sylancr 588 |
. . . . . 6
โข (๐ โ (1 โ ๐ด) โ
โ) |
9 | | 1re 11162 |
. . . . . . . . . . . 12
โข 1 โ
โ |
10 | 9 | ltnri 11271 |
. . . . . . . . . . 11
โข ยฌ 1
< 1 |
11 | | fveq2 6847 |
. . . . . . . . . . . . 13
โข (๐ด = 1 โ (absโ๐ด) =
(absโ1)) |
12 | | abs1 15189 |
. . . . . . . . . . . . 13
โข
(absโ1) = 1 |
13 | 11, 12 | eqtrdi 2793 |
. . . . . . . . . . . 12
โข (๐ด = 1 โ (absโ๐ด) = 1) |
14 | 13 | breq1d 5120 |
. . . . . . . . . . 11
โข (๐ด = 1 โ ((absโ๐ด) < 1 โ 1 <
1)) |
15 | 10, 14 | mtbiri 327 |
. . . . . . . . . 10
โข (๐ด = 1 โ ยฌ
(absโ๐ด) <
1) |
16 | 15 | necon2ai 2974 |
. . . . . . . . 9
โข
((absโ๐ด) <
1 โ ๐ด โ
1) |
17 | 4, 16 | syl 17 |
. . . . . . . 8
โข (๐ โ ๐ด โ 1) |
18 | 17 | necomd 3000 |
. . . . . . 7
โข (๐ โ 1 โ ๐ด) |
19 | | subeq0 11434 |
. . . . . . . . 9
โข ((1
โ โ โง ๐ด
โ โ) โ ((1 โ ๐ด) = 0 โ 1 = ๐ด)) |
20 | 6, 3, 19 | sylancr 588 |
. . . . . . . 8
โข (๐ โ ((1 โ ๐ด) = 0 โ 1 = ๐ด)) |
21 | 20 | necon3bid 2989 |
. . . . . . 7
โข (๐ โ ((1 โ ๐ด) โ 0 โ 1 โ ๐ด)) |
22 | 18, 21 | mpbird 257 |
. . . . . 6
โข (๐ โ (1 โ ๐ด) โ 0) |
23 | 3, 8, 22 | divcld 11938 |
. . . . 5
โข (๐ โ (๐ด / (1 โ ๐ด)) โ โ) |
24 | | nn0ex 12426 |
. . . . . . 7
โข
โ0 โ V |
25 | 24 | mptex 7178 |
. . . . . 6
โข (๐ โ โ0
โฆ ((๐ดโ(๐ + 1)) / (1 โ ๐ด))) โ V |
26 | 25 | a1i 11 |
. . . . 5
โข (๐ โ (๐ โ โ0 โฆ ((๐ดโ(๐ + 1)) / (1 โ ๐ด))) โ V) |
27 | | oveq2 7370 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
28 | | eqid 2737 |
. . . . . . . 8
โข (๐ โ โ0
โฆ (๐ดโ๐)) = (๐ โ โ0 โฆ (๐ดโ๐)) |
29 | | ovex 7395 |
. . . . . . . 8
โข (๐ดโ๐) โ V |
30 | 27, 28, 29 | fvmpt 6953 |
. . . . . . 7
โข (๐ โ โ0
โ ((๐ โ
โ0 โฆ (๐ดโ๐))โ๐) = (๐ดโ๐)) |
31 | 30 | adantl 483 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ ((๐ โ โ0
โฆ (๐ดโ๐))โ๐) = (๐ดโ๐)) |
32 | | expcl 13992 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ๐) โ
โ) |
33 | 3, 32 | sylan 581 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ (๐ดโ๐) โ โ) |
34 | 31, 33 | eqeltrd 2838 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ ((๐ โ โ0
โฆ (๐ดโ๐))โ๐) โ โ) |
35 | | expp1 13981 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
36 | 3, 35 | sylan 581 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ0) โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
37 | 3 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ0) โ ๐ด โ
โ) |
38 | 33, 37 | mulcomd 11183 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ0) โ ((๐ดโ๐) ยท ๐ด) = (๐ด ยท (๐ดโ๐))) |
39 | 36, 38 | eqtrd 2777 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ (๐ดโ(๐ + 1)) = (๐ด ยท (๐ดโ๐))) |
40 | 39 | oveq1d 7377 |
. . . . . . 7
โข ((๐ โง ๐ โ โ0) โ ((๐ดโ(๐ + 1)) / (1 โ ๐ด)) = ((๐ด ยท (๐ดโ๐)) / (1 โ ๐ด))) |
41 | 8 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ (1
โ ๐ด) โ
โ) |
42 | 22 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ (1
โ ๐ด) โ
0) |
43 | 37, 33, 41, 42 | div23d 11975 |
. . . . . . 7
โข ((๐ โง ๐ โ โ0) โ ((๐ด ยท (๐ดโ๐)) / (1 โ ๐ด)) = ((๐ด / (1 โ ๐ด)) ยท (๐ดโ๐))) |
44 | 40, 43 | eqtrd 2777 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ ((๐ดโ(๐ + 1)) / (1 โ ๐ด)) = ((๐ด / (1 โ ๐ด)) ยท (๐ดโ๐))) |
45 | | oveq1 7369 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐ + 1) = (๐ + 1)) |
46 | 45 | oveq2d 7378 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ดโ(๐ + 1)) = (๐ดโ(๐ + 1))) |
47 | 46 | oveq1d 7377 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐ดโ(๐ + 1)) / (1 โ ๐ด)) = ((๐ดโ(๐ + 1)) / (1 โ ๐ด))) |
48 | | eqid 2737 |
. . . . . . . 8
โข (๐ โ โ0
โฆ ((๐ดโ(๐ + 1)) / (1 โ ๐ด))) = (๐ โ โ0 โฆ ((๐ดโ(๐ + 1)) / (1 โ ๐ด))) |
49 | | ovex 7395 |
. . . . . . . 8
โข ((๐ดโ(๐ + 1)) / (1 โ ๐ด)) โ V |
50 | 47, 48, 49 | fvmpt 6953 |
. . . . . . 7
โข (๐ โ โ0
โ ((๐ โ
โ0 โฆ ((๐ดโ(๐ + 1)) / (1 โ ๐ด)))โ๐) = ((๐ดโ(๐ + 1)) / (1 โ ๐ด))) |
51 | 50 | adantl 483 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ ((๐ โ โ0
โฆ ((๐ดโ(๐ + 1)) / (1 โ ๐ด)))โ๐) = ((๐ดโ(๐ + 1)) / (1 โ ๐ด))) |
52 | 31 | oveq2d 7378 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ ((๐ด / (1 โ ๐ด)) ยท ((๐ โ โ0 โฆ (๐ดโ๐))โ๐)) = ((๐ด / (1 โ ๐ด)) ยท (๐ดโ๐))) |
53 | 44, 51, 52 | 3eqtr4d 2787 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ ((๐ โ โ0
โฆ ((๐ดโ(๐ + 1)) / (1 โ ๐ด)))โ๐) = ((๐ด / (1 โ ๐ด)) ยท ((๐ โ โ0 โฆ (๐ดโ๐))โ๐))) |
54 | 1, 2, 5, 23, 26, 34, 53 | climmulc2 15526 |
. . . 4
โข (๐ โ (๐ โ โ0 โฆ ((๐ดโ(๐ + 1)) / (1 โ ๐ด))) โ ((๐ด / (1 โ ๐ด)) ยท 0)) |
55 | 23 | mul01d 11361 |
. . . 4
โข (๐ โ ((๐ด / (1 โ ๐ด)) ยท 0) = 0) |
56 | 54, 55 | breqtrd 5136 |
. . 3
โข (๐ โ (๐ โ โ0 โฆ ((๐ดโ(๐ + 1)) / (1 โ ๐ด))) โ 0) |
57 | 8, 22 | reccld 11931 |
. . 3
โข (๐ โ (1 / (1 โ ๐ด)) โ
โ) |
58 | | seqex 13915 |
. . . 4
โข seq0( + ,
๐น) โ
V |
59 | 58 | a1i 11 |
. . 3
โข (๐ โ seq0( + , ๐น) โ V) |
60 | | peano2nn0 12460 |
. . . . . 6
โข (๐ โ โ0
โ (๐ + 1) โ
โ0) |
61 | | expcl 13992 |
. . . . . 6
โข ((๐ด โ โ โง (๐ + 1) โ
โ0) โ (๐ดโ(๐ + 1)) โ โ) |
62 | 3, 60, 61 | syl2an 597 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ (๐ดโ(๐ + 1)) โ โ) |
63 | 62, 41, 42 | divcld 11938 |
. . . 4
โข ((๐ โง ๐ โ โ0) โ ((๐ดโ(๐ + 1)) / (1 โ ๐ด)) โ โ) |
64 | 51, 63 | eqeltrd 2838 |
. . 3
โข ((๐ โง ๐ โ โ0) โ ((๐ โ โ0
โฆ ((๐ดโ(๐ + 1)) / (1 โ ๐ด)))โ๐) โ โ) |
65 | | nn0cn 12430 |
. . . . . . . 8
โข (๐ โ โ0
โ ๐ โ
โ) |
66 | 65 | adantl 483 |
. . . . . . 7
โข ((๐ โง ๐ โ โ0) โ ๐ โ
โ) |
67 | | pncan 11414 |
. . . . . . 7
โข ((๐ โ โ โง 1 โ
โ) โ ((๐ + 1)
โ 1) = ๐) |
68 | 66, 6, 67 | sylancl 587 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ ((๐ + 1) โ 1) = ๐) |
69 | 68 | oveq2d 7378 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ
(0...((๐ + 1) โ 1)) =
(0...๐)) |
70 | 69 | sumeq1d 15593 |
. . . 4
โข ((๐ โง ๐ โ โ0) โ
ฮฃ๐ โ
(0...((๐ + 1) โ
1))(๐ดโ๐) = ฮฃ๐ โ (0...๐)(๐ดโ๐)) |
71 | 6 | a1i 11 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ 1 โ
โ) |
72 | 71, 62, 41, 42 | divsubdird 11977 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ ((1
โ (๐ดโ(๐ + 1))) / (1 โ ๐ด)) = ((1 / (1 โ ๐ด)) โ ((๐ดโ(๐ + 1)) / (1 โ ๐ด)))) |
73 | 17 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ ๐ด โ 1) |
74 | 60 | adantl 483 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ (๐ + 1) โ
โ0) |
75 | 37, 73, 74 | geoser 15759 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ
ฮฃ๐ โ
(0...((๐ + 1) โ
1))(๐ดโ๐) = ((1 โ (๐ดโ(๐ + 1))) / (1 โ ๐ด))) |
76 | 51 | oveq2d 7378 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ ((1 / (1
โ ๐ด)) โ ((๐ โ โ0
โฆ ((๐ดโ(๐ + 1)) / (1 โ ๐ด)))โ๐)) = ((1 / (1 โ ๐ด)) โ ((๐ดโ(๐ + 1)) / (1 โ ๐ด)))) |
77 | 72, 75, 76 | 3eqtr4d 2787 |
. . . 4
โข ((๐ โง ๐ โ โ0) โ
ฮฃ๐ โ
(0...((๐ + 1) โ
1))(๐ดโ๐) = ((1 / (1 โ ๐ด)) โ ((๐ โ โ0 โฆ ((๐ดโ(๐ + 1)) / (1 โ ๐ด)))โ๐))) |
78 | | simpll 766 |
. . . . . 6
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ ๐) |
79 | | elfznn0 13541 |
. . . . . . 7
โข (๐ โ (0...๐) โ ๐ โ โ0) |
80 | 79 | adantl 483 |
. . . . . 6
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ ๐ โ โ0) |
81 | | geolim.3 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ (๐นโ๐) = (๐ดโ๐)) |
82 | 78, 80, 81 | syl2anc 585 |
. . . . 5
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (๐นโ๐) = (๐ดโ๐)) |
83 | | simpr 486 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ ๐ โ
โ0) |
84 | 83, 1 | eleqtrdi 2848 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ ๐ โ
(โคโฅโ0)) |
85 | 78, 3 | syl 17 |
. . . . . 6
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ ๐ด โ โ) |
86 | 85, 80 | expcld 14058 |
. . . . 5
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (๐ดโ๐) โ โ) |
87 | 82, 84, 86 | fsumser 15622 |
. . . 4
โข ((๐ โง ๐ โ โ0) โ
ฮฃ๐ โ (0...๐)(๐ดโ๐) = (seq0( + , ๐น)โ๐)) |
88 | 70, 77, 87 | 3eqtr3rd 2786 |
. . 3
โข ((๐ โง ๐ โ โ0) โ (seq0( +
, ๐น)โ๐) = ((1 / (1 โ ๐ด)) โ ((๐ โ โ0 โฆ ((๐ดโ(๐ + 1)) / (1 โ ๐ด)))โ๐))) |
89 | 1, 2, 56, 57, 59, 64, 88 | climsubc2 15528 |
. 2
โข (๐ โ seq0( + , ๐น) โ ((1 / (1 โ ๐ด)) โ 0)) |
90 | 57 | subid1d 11508 |
. 2
โข (๐ โ ((1 / (1 โ ๐ด)) โ 0) = (1 / (1 โ
๐ด))) |
91 | 89, 90 | breqtrd 5136 |
1
โข (๐ โ seq0( + , ๐น) โ (1 / (1 โ ๐ด))) |