Step | Hyp | Ref
| Expression |
1 | | geolim3.f |
. . 3
โข ๐น = (๐ โ (โคโฅโ๐ด) โฆ (๐ถ ยท (๐ตโ(๐ โ ๐ด)))) |
2 | | seqeq3 13918 |
. . 3
โข (๐น = (๐ โ (โคโฅโ๐ด) โฆ (๐ถ ยท (๐ตโ(๐ โ ๐ด)))) โ seq๐ด( + , ๐น) = seq๐ด( + , (๐ โ (โคโฅโ๐ด) โฆ (๐ถ ยท (๐ตโ(๐ โ ๐ด)))))) |
3 | 1, 2 | ax-mp 5 |
. 2
โข seq๐ด( + , ๐น) = seq๐ด( + , (๐ โ (โคโฅโ๐ด) โฆ (๐ถ ยท (๐ตโ(๐ โ ๐ด))))) |
4 | | nn0uz 12812 |
. . . . 5
โข
โ0 = (โคโฅโ0) |
5 | | 0zd 12518 |
. . . . 5
โข (๐ โ 0 โ
โค) |
6 | | geolim3.c |
. . . . 5
โข (๐ โ ๐ถ โ โ) |
7 | | geolim3.b1 |
. . . . . 6
โข (๐ โ ๐ต โ โ) |
8 | | geolim3.b2 |
. . . . . 6
โข (๐ โ (absโ๐ต) < 1) |
9 | | oveq2 7370 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ตโ๐) = (๐ตโ๐)) |
10 | | eqid 2737 |
. . . . . . . 8
โข (๐ โ โ0
โฆ (๐ตโ๐)) = (๐ โ โ0 โฆ (๐ตโ๐)) |
11 | | ovex 7395 |
. . . . . . . 8
โข (๐ตโ๐) โ V |
12 | 9, 10, 11 | fvmpt 6953 |
. . . . . . 7
โข (๐ โ โ0
โ ((๐ โ
โ0 โฆ (๐ตโ๐))โ๐) = (๐ตโ๐)) |
13 | 12 | adantl 483 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ ((๐ โ โ0
โฆ (๐ตโ๐))โ๐) = (๐ตโ๐)) |
14 | 7, 8, 13 | geolim 15762 |
. . . . 5
โข (๐ โ seq0( + , (๐ โ โ0
โฆ (๐ตโ๐))) โ (1 / (1 โ
๐ต))) |
15 | | expcl 13992 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ โ โ0)
โ (๐ตโ๐) โ
โ) |
16 | 7, 15 | sylan 581 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ (๐ตโ๐) โ โ) |
17 | 13, 16 | eqeltrd 2838 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ ((๐ โ โ0
โฆ (๐ตโ๐))โ๐) โ โ) |
18 | | geolim3.a |
. . . . . . . 8
โข (๐ โ ๐ด โ โค) |
19 | 18 | zcnd 12615 |
. . . . . . 7
โข (๐ โ ๐ด โ โ) |
20 | | nn0cn 12430 |
. . . . . . 7
โข (๐ โ โ0
โ ๐ โ
โ) |
21 | | fvex 6860 |
. . . . . . . . 9
โข
(โคโฅโ๐ด) โ V |
22 | 21 | mptex 7178 |
. . . . . . . 8
โข (๐ โ
(โคโฅโ๐ด) โฆ (๐ถ ยท (๐ตโ(๐ โ ๐ด)))) โ V |
23 | 22 | shftval4 14969 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ) โ (((๐ โ
(โคโฅโ๐ด) โฆ (๐ถ ยท (๐ตโ(๐ โ ๐ด)))) shift -๐ด)โ๐) = ((๐ โ (โคโฅโ๐ด) โฆ (๐ถ ยท (๐ตโ(๐ โ ๐ด))))โ(๐ด + ๐))) |
24 | 19, 20, 23 | syl2an 597 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ (((๐ โ
(โคโฅโ๐ด) โฆ (๐ถ ยท (๐ตโ(๐ โ ๐ด)))) shift -๐ด)โ๐) = ((๐ โ (โคโฅโ๐ด) โฆ (๐ถ ยท (๐ตโ(๐ โ ๐ด))))โ(๐ด + ๐))) |
25 | | uzid 12785 |
. . . . . . . . 9
โข (๐ด โ โค โ ๐ด โ
(โคโฅโ๐ด)) |
26 | 18, 25 | syl 17 |
. . . . . . . 8
โข (๐ โ ๐ด โ (โคโฅโ๐ด)) |
27 | | uzaddcl 12836 |
. . . . . . . 8
โข ((๐ด โ
(โคโฅโ๐ด) โง ๐ โ โ0) โ (๐ด + ๐) โ (โคโฅโ๐ด)) |
28 | 26, 27 | sylan 581 |
. . . . . . 7
โข ((๐ โง ๐ โ โ0) โ (๐ด + ๐) โ (โคโฅโ๐ด)) |
29 | | oveq1 7369 |
. . . . . . . . . 10
โข (๐ = (๐ด + ๐) โ (๐ โ ๐ด) = ((๐ด + ๐) โ ๐ด)) |
30 | 29 | oveq2d 7378 |
. . . . . . . . 9
โข (๐ = (๐ด + ๐) โ (๐ตโ(๐ โ ๐ด)) = (๐ตโ((๐ด + ๐) โ ๐ด))) |
31 | 30 | oveq2d 7378 |
. . . . . . . 8
โข (๐ = (๐ด + ๐) โ (๐ถ ยท (๐ตโ(๐ โ ๐ด))) = (๐ถ ยท (๐ตโ((๐ด + ๐) โ ๐ด)))) |
32 | | eqid 2737 |
. . . . . . . 8
โข (๐ โ
(โคโฅโ๐ด) โฆ (๐ถ ยท (๐ตโ(๐ โ ๐ด)))) = (๐ โ (โคโฅโ๐ด) โฆ (๐ถ ยท (๐ตโ(๐ โ ๐ด)))) |
33 | | ovex 7395 |
. . . . . . . 8
โข (๐ถ ยท (๐ตโ((๐ด + ๐) โ ๐ด))) โ V |
34 | 31, 32, 33 | fvmpt 6953 |
. . . . . . 7
โข ((๐ด + ๐) โ (โคโฅโ๐ด) โ ((๐ โ (โคโฅโ๐ด) โฆ (๐ถ ยท (๐ตโ(๐ โ ๐ด))))โ(๐ด + ๐)) = (๐ถ ยท (๐ตโ((๐ด + ๐) โ ๐ด)))) |
35 | 28, 34 | syl 17 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ ((๐ โ
(โคโฅโ๐ด) โฆ (๐ถ ยท (๐ตโ(๐ โ ๐ด))))โ(๐ด + ๐)) = (๐ถ ยท (๐ตโ((๐ด + ๐) โ ๐ด)))) |
36 | | pncan2 11415 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ โ) โ ((๐ด + ๐) โ ๐ด) = ๐) |
37 | 19, 20, 36 | syl2an 597 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ0) โ ((๐ด + ๐) โ ๐ด) = ๐) |
38 | 37 | oveq2d 7378 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ (๐ตโ((๐ด + ๐) โ ๐ด)) = (๐ตโ๐)) |
39 | 38, 13 | eqtr4d 2780 |
. . . . . . 7
โข ((๐ โง ๐ โ โ0) โ (๐ตโ((๐ด + ๐) โ ๐ด)) = ((๐ โ โ0 โฆ (๐ตโ๐))โ๐)) |
40 | 39 | oveq2d 7378 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ (๐ถ ยท (๐ตโ((๐ด + ๐) โ ๐ด))) = (๐ถ ยท ((๐ โ โ0 โฆ (๐ตโ๐))โ๐))) |
41 | 24, 35, 40 | 3eqtrd 2781 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ (((๐ โ
(โคโฅโ๐ด) โฆ (๐ถ ยท (๐ตโ(๐ โ ๐ด)))) shift -๐ด)โ๐) = (๐ถ ยท ((๐ โ โ0 โฆ (๐ตโ๐))โ๐))) |
42 | 4, 5, 6, 14, 17, 41 | isermulc2 15549 |
. . . 4
โข (๐ โ seq0( + , ((๐ โ
(โคโฅโ๐ด) โฆ (๐ถ ยท (๐ตโ(๐ โ ๐ด)))) shift -๐ด)) โ (๐ถ ยท (1 / (1 โ ๐ต)))) |
43 | 19 | negidd 11509 |
. . . . 5
โข (๐ โ (๐ด + -๐ด) = 0) |
44 | 43 | seqeq1d 13919 |
. . . 4
โข (๐ โ seq(๐ด + -๐ด)( + , ((๐ โ (โคโฅโ๐ด) โฆ (๐ถ ยท (๐ตโ(๐ โ ๐ด)))) shift -๐ด)) = seq0( + , ((๐ โ (โคโฅโ๐ด) โฆ (๐ถ ยท (๐ตโ(๐ โ ๐ด)))) shift -๐ด))) |
45 | | ax-1cn 11116 |
. . . . . 6
โข 1 โ
โ |
46 | | subcl 11407 |
. . . . . 6
โข ((1
โ โ โง ๐ต
โ โ) โ (1 โ ๐ต) โ โ) |
47 | 45, 7, 46 | sylancr 588 |
. . . . 5
โข (๐ โ (1 โ ๐ต) โ
โ) |
48 | | abs1 15189 |
. . . . . . . . 9
โข
(absโ1) = 1 |
49 | 48 | a1i 11 |
. . . . . . . 8
โข (๐ โ (absโ1) =
1) |
50 | 7 | abscld 15328 |
. . . . . . . . 9
โข (๐ โ (absโ๐ต) โ
โ) |
51 | 50, 8 | gtned 11297 |
. . . . . . . 8
โข (๐ โ 1 โ (absโ๐ต)) |
52 | 49, 51 | eqnetrd 3012 |
. . . . . . 7
โข (๐ โ (absโ1) โ
(absโ๐ต)) |
53 | | fveq2 6847 |
. . . . . . . 8
โข (1 =
๐ต โ (absโ1) =
(absโ๐ต)) |
54 | 53 | necon3i 2977 |
. . . . . . 7
โข
((absโ1) โ (absโ๐ต) โ 1 โ ๐ต) |
55 | 52, 54 | syl 17 |
. . . . . 6
โข (๐ โ 1 โ ๐ต) |
56 | | subeq0 11434 |
. . . . . . . 8
โข ((1
โ โ โง ๐ต
โ โ) โ ((1 โ ๐ต) = 0 โ 1 = ๐ต)) |
57 | 45, 7, 56 | sylancr 588 |
. . . . . . 7
โข (๐ โ ((1 โ ๐ต) = 0 โ 1 = ๐ต)) |
58 | 57 | necon3bid 2989 |
. . . . . 6
โข (๐ โ ((1 โ ๐ต) โ 0 โ 1 โ ๐ต)) |
59 | 55, 58 | mpbird 257 |
. . . . 5
โข (๐ โ (1 โ ๐ต) โ 0) |
60 | 6, 47, 59 | divrecd 11941 |
. . . 4
โข (๐ โ (๐ถ / (1 โ ๐ต)) = (๐ถ ยท (1 / (1 โ ๐ต)))) |
61 | 42, 44, 60 | 3brtr4d 5142 |
. . 3
โข (๐ โ seq(๐ด + -๐ด)( + , ((๐ โ (โคโฅโ๐ด) โฆ (๐ถ ยท (๐ตโ(๐ โ ๐ด)))) shift -๐ด)) โ (๐ถ / (1 โ ๐ต))) |
62 | 18 | znegcld 12616 |
. . . 4
โข (๐ โ -๐ด โ โค) |
63 | 22 | isershft 15555 |
. . . 4
โข ((๐ด โ โค โง -๐ด โ โค) โ
(seq๐ด( + , (๐ โ
(โคโฅโ๐ด) โฆ (๐ถ ยท (๐ตโ(๐ โ ๐ด))))) โ (๐ถ / (1 โ ๐ต)) โ seq(๐ด + -๐ด)( + , ((๐ โ (โคโฅโ๐ด) โฆ (๐ถ ยท (๐ตโ(๐ โ ๐ด)))) shift -๐ด)) โ (๐ถ / (1 โ ๐ต)))) |
64 | 18, 62, 63 | syl2anc 585 |
. . 3
โข (๐ โ (seq๐ด( + , (๐ โ (โคโฅโ๐ด) โฆ (๐ถ ยท (๐ตโ(๐ โ ๐ด))))) โ (๐ถ / (1 โ ๐ต)) โ seq(๐ด + -๐ด)( + , ((๐ โ (โคโฅโ๐ด) โฆ (๐ถ ยท (๐ตโ(๐ โ ๐ด)))) shift -๐ด)) โ (๐ถ / (1 โ ๐ต)))) |
65 | 61, 64 | mpbird 257 |
. 2
โข (๐ โ seq๐ด( + , (๐ โ (โคโฅโ๐ด) โฆ (๐ถ ยท (๐ตโ(๐ โ ๐ด))))) โ (๐ถ / (1 โ ๐ต))) |
66 | 3, 65 | eqbrtrid 5145 |
1
โข (๐ โ seq๐ด( + , ๐น) โ (๐ถ / (1 โ ๐ต))) |