Step | Hyp | Ref
| Expression |
1 | | climrec.1 |
. . 3
โข ๐ =
(โคโฅโ๐) |
2 | | climrec.2 |
. . 3
โข (๐ โ ๐ โ โค) |
3 | | climrec.3 |
. . . . 5
โข (๐ โ ๐บ โ ๐ด) |
4 | | climcl 15382 |
. . . . 5
โข (๐บ โ ๐ด โ ๐ด โ โ) |
5 | 3, 4 | syl 17 |
. . . 4
โข (๐ โ ๐ด โ โ) |
6 | | climrec.4 |
. . . . . 6
โข (๐ โ ๐ด โ 0) |
7 | 6 | neneqd 2949 |
. . . . 5
โข (๐ โ ยฌ ๐ด = 0) |
8 | | c0ex 11150 |
. . . . . 6
โข 0 โ
V |
9 | 8 | elsn2 4626 |
. . . . 5
โข (๐ด โ {0} โ ๐ด = 0) |
10 | 7, 9 | sylnibr 329 |
. . . 4
โข (๐ โ ยฌ ๐ด โ {0}) |
11 | 5, 10 | eldifd 3922 |
. . 3
โข (๐ โ ๐ด โ (โ โ
{0})) |
12 | | eqidd 2738 |
. . . . 5
โข ((๐ โง ๐ง โ (โ โ {0})) โ (๐ค โ (โ โ {0})
โฆ (1 / ๐ค)) = (๐ค โ (โ โ {0})
โฆ (1 / ๐ค))) |
13 | | simpr 486 |
. . . . . 6
โข (((๐ โง ๐ง โ (โ โ {0})) โง ๐ค = ๐ง) โ ๐ค = ๐ง) |
14 | 13 | oveq2d 7374 |
. . . . 5
โข (((๐ โง ๐ง โ (โ โ {0})) โง ๐ค = ๐ง) โ (1 / ๐ค) = (1 / ๐ง)) |
15 | | simpr 486 |
. . . . 5
โข ((๐ โง ๐ง โ (โ โ {0})) โ ๐ง โ (โ โ
{0})) |
16 | 15 | eldifad 3923 |
. . . . . 6
โข ((๐ โง ๐ง โ (โ โ {0})) โ ๐ง โ
โ) |
17 | | eldifsni 4751 |
. . . . . . 7
โข (๐ง โ (โ โ {0})
โ ๐ง โ
0) |
18 | 17 | adantl 483 |
. . . . . 6
โข ((๐ โง ๐ง โ (โ โ {0})) โ ๐ง โ 0) |
19 | 16, 18 | reccld 11925 |
. . . . 5
โข ((๐ โง ๐ง โ (โ โ {0})) โ (1 /
๐ง) โ
โ) |
20 | 12, 14, 15, 19 | fvmptd 6956 |
. . . 4
โข ((๐ โง ๐ง โ (โ โ {0})) โ ((๐ค โ (โ โ {0})
โฆ (1 / ๐ค))โ๐ง) = (1 / ๐ง)) |
21 | 20, 19 | eqeltrd 2838 |
. . 3
โข ((๐ โง ๐ง โ (โ โ {0})) โ ((๐ค โ (โ โ {0})
โฆ (1 / ๐ค))โ๐ง) โ โ) |
22 | | climrec.7 |
. . 3
โข (๐ โ ๐ป โ ๐) |
23 | | eqid 2737 |
. . . . . 6
โข (if(1
โค ((absโ๐ด)
ยท ๐ฅ), 1,
((absโ๐ด) ยท
๐ฅ)) ยท
((absโ๐ด) / 2)) =
(if(1 โค ((absโ๐ด)
ยท ๐ฅ), 1,
((absโ๐ด) ยท
๐ฅ)) ยท
((absโ๐ด) /
2)) |
24 | 23 | reccn2 15480 |
. . . . 5
โข ((๐ด โ (โ โ {0})
โง ๐ฅ โ
โ+) โ โ๐ฆ โ โ+ โ๐ง โ (โ โ
{0})((absโ(๐ง โ
๐ด)) < ๐ฆ โ (absโ((1 / ๐ง) โ (1 / ๐ด))) < ๐ฅ)) |
25 | 11, 24 | sylan 581 |
. . . 4
โข ((๐ โง ๐ฅ โ โ+) โ
โ๐ฆ โ
โ+ โ๐ง โ (โ โ
{0})((absโ(๐ง โ
๐ด)) < ๐ฆ โ (absโ((1 / ๐ง) โ (1 / ๐ด))) < ๐ฅ)) |
26 | | eqidd 2738 |
. . . . . . . . . . . 12
โข (๐ง โ (โ โ {0})
โ (๐ค โ (โ
โ {0}) โฆ (1 / ๐ค)) = (๐ค โ (โ โ {0}) โฆ (1 /
๐ค))) |
27 | | simpr 486 |
. . . . . . . . . . . . 13
โข ((๐ง โ (โ โ {0})
โง ๐ค = ๐ง) โ ๐ค = ๐ง) |
28 | 27 | oveq2d 7374 |
. . . . . . . . . . . 12
โข ((๐ง โ (โ โ {0})
โง ๐ค = ๐ง) โ (1 / ๐ค) = (1 / ๐ง)) |
29 | | id 22 |
. . . . . . . . . . . 12
โข (๐ง โ (โ โ {0})
โ ๐ง โ (โ
โ {0})) |
30 | | eldifi 4087 |
. . . . . . . . . . . . 13
โข (๐ง โ (โ โ {0})
โ ๐ง โ
โ) |
31 | 30, 17 | reccld 11925 |
. . . . . . . . . . . 12
โข (๐ง โ (โ โ {0})
โ (1 / ๐ง) โ
โ) |
32 | 26, 28, 29, 31 | fvmptd 6956 |
. . . . . . . . . . 11
โข (๐ง โ (โ โ {0})
โ ((๐ค โ (โ
โ {0}) โฆ (1 / ๐ค))โ๐ง) = (1 / ๐ง)) |
33 | 32 | ad2antlr 726 |
. . . . . . . . . 10
โข
(((((๐ โง ๐ฅ โ โ+)
โง (๐ง โ (โ
โ {0}) โ ((absโ(๐ง โ ๐ด)) < ๐ฆ โ (absโ((1 / ๐ง) โ (1 / ๐ด))) < ๐ฅ))) โง ๐ง โ (โ โ {0})) โง
(absโ(๐ง โ ๐ด)) < ๐ฆ) โ ((๐ค โ (โ โ {0}) โฆ (1 /
๐ค))โ๐ง) = (1 / ๐ง)) |
34 | | eqidd 2738 |
. . . . . . . . . . . 12
โข (๐ โ (๐ค โ (โ โ {0}) โฆ (1 /
๐ค)) = (๐ค โ (โ โ {0}) โฆ (1 /
๐ค))) |
35 | | simpr 486 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ค = ๐ด) โ ๐ค = ๐ด) |
36 | 35 | oveq2d 7374 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ค = ๐ด) โ (1 / ๐ค) = (1 / ๐ด)) |
37 | 5, 6 | reccld 11925 |
. . . . . . . . . . . 12
โข (๐ โ (1 / ๐ด) โ โ) |
38 | 34, 36, 11, 37 | fvmptd 6956 |
. . . . . . . . . . 11
โข (๐ โ ((๐ค โ (โ โ {0}) โฆ (1 /
๐ค))โ๐ด) = (1 / ๐ด)) |
39 | 38 | ad4antr 731 |
. . . . . . . . . 10
โข
(((((๐ โง ๐ฅ โ โ+)
โง (๐ง โ (โ
โ {0}) โ ((absโ(๐ง โ ๐ด)) < ๐ฆ โ (absโ((1 / ๐ง) โ (1 / ๐ด))) < ๐ฅ))) โง ๐ง โ (โ โ {0})) โง
(absโ(๐ง โ ๐ด)) < ๐ฆ) โ ((๐ค โ (โ โ {0}) โฆ (1 /
๐ค))โ๐ด) = (1 / ๐ด)) |
40 | 33, 39 | oveq12d 7376 |
. . . . . . . . 9
โข
(((((๐ โง ๐ฅ โ โ+)
โง (๐ง โ (โ
โ {0}) โ ((absโ(๐ง โ ๐ด)) < ๐ฆ โ (absโ((1 / ๐ง) โ (1 / ๐ด))) < ๐ฅ))) โง ๐ง โ (โ โ {0})) โง
(absโ(๐ง โ ๐ด)) < ๐ฆ) โ (((๐ค โ (โ โ {0}) โฆ (1 /
๐ค))โ๐ง) โ ((๐ค โ (โ โ {0}) โฆ (1 /
๐ค))โ๐ด)) = ((1 / ๐ง) โ (1 / ๐ด))) |
41 | 40 | fveq2d 6847 |
. . . . . . . 8
โข
(((((๐ โง ๐ฅ โ โ+)
โง (๐ง โ (โ
โ {0}) โ ((absโ(๐ง โ ๐ด)) < ๐ฆ โ (absโ((1 / ๐ง) โ (1 / ๐ด))) < ๐ฅ))) โง ๐ง โ (โ โ {0})) โง
(absโ(๐ง โ ๐ด)) < ๐ฆ) โ (absโ(((๐ค โ (โ โ {0}) โฆ (1 /
๐ค))โ๐ง) โ ((๐ค โ (โ โ {0}) โฆ (1 /
๐ค))โ๐ด))) = (absโ((1 / ๐ง) โ (1 / ๐ด)))) |
42 | 29 | ad2antlr 726 |
. . . . . . . . 9
โข
(((((๐ โง ๐ฅ โ โ+)
โง (๐ง โ (โ
โ {0}) โ ((absโ(๐ง โ ๐ด)) < ๐ฆ โ (absโ((1 / ๐ง) โ (1 / ๐ด))) < ๐ฅ))) โง ๐ง โ (โ โ {0})) โง
(absโ(๐ง โ ๐ด)) < ๐ฆ) โ ๐ง โ (โ โ
{0})) |
43 | | simpr 486 |
. . . . . . . . 9
โข
(((((๐ โง ๐ฅ โ โ+)
โง (๐ง โ (โ
โ {0}) โ ((absโ(๐ง โ ๐ด)) < ๐ฆ โ (absโ((1 / ๐ง) โ (1 / ๐ด))) < ๐ฅ))) โง ๐ง โ (โ โ {0})) โง
(absโ(๐ง โ ๐ด)) < ๐ฆ) โ (absโ(๐ง โ ๐ด)) < ๐ฆ) |
44 | | simpllr 775 |
. . . . . . . . 9
โข
(((((๐ โง ๐ฅ โ โ+)
โง (๐ง โ (โ
โ {0}) โ ((absโ(๐ง โ ๐ด)) < ๐ฆ โ (absโ((1 / ๐ง) โ (1 / ๐ด))) < ๐ฅ))) โง ๐ง โ (โ โ {0})) โง
(absโ(๐ง โ ๐ด)) < ๐ฆ) โ (๐ง โ (โ โ {0}) โ
((absโ(๐ง โ
๐ด)) < ๐ฆ โ (absโ((1 / ๐ง) โ (1 / ๐ด))) < ๐ฅ))) |
45 | 42, 43, 44 | mp2d 49 |
. . . . . . . 8
โข
(((((๐ โง ๐ฅ โ โ+)
โง (๐ง โ (โ
โ {0}) โ ((absโ(๐ง โ ๐ด)) < ๐ฆ โ (absโ((1 / ๐ง) โ (1 / ๐ด))) < ๐ฅ))) โง ๐ง โ (โ โ {0})) โง
(absโ(๐ง โ ๐ด)) < ๐ฆ) โ (absโ((1 / ๐ง) โ (1 / ๐ด))) < ๐ฅ) |
46 | 41, 45 | eqbrtrd 5128 |
. . . . . . 7
โข
(((((๐ โง ๐ฅ โ โ+)
โง (๐ง โ (โ
โ {0}) โ ((absโ(๐ง โ ๐ด)) < ๐ฆ โ (absโ((1 / ๐ง) โ (1 / ๐ด))) < ๐ฅ))) โง ๐ง โ (โ โ {0})) โง
(absโ(๐ง โ ๐ด)) < ๐ฆ) โ (absโ(((๐ค โ (โ โ {0}) โฆ (1 /
๐ค))โ๐ง) โ ((๐ค โ (โ โ {0}) โฆ (1 /
๐ค))โ๐ด))) < ๐ฅ) |
47 | 46 | exp41 436 |
. . . . . 6
โข ((๐ โง ๐ฅ โ โ+) โ ((๐ง โ (โ โ {0})
โ ((absโ(๐ง
โ ๐ด)) < ๐ฆ โ (absโ((1 / ๐ง) โ (1 / ๐ด))) < ๐ฅ)) โ (๐ง โ (โ โ {0}) โ
((absโ(๐ง โ
๐ด)) < ๐ฆ โ (absโ(((๐ค โ (โ โ {0}) โฆ (1 /
๐ค))โ๐ง) โ ((๐ค โ (โ โ {0}) โฆ (1 /
๐ค))โ๐ด))) < ๐ฅ)))) |
48 | 47 | ralimdv2 3161 |
. . . . 5
โข ((๐ โง ๐ฅ โ โ+) โ
(โ๐ง โ (โ
โ {0})((absโ(๐ง
โ ๐ด)) < ๐ฆ โ (absโ((1 / ๐ง) โ (1 / ๐ด))) < ๐ฅ) โ โ๐ง โ (โ โ
{0})((absโ(๐ง โ
๐ด)) < ๐ฆ โ (absโ(((๐ค โ (โ โ {0}) โฆ (1 /
๐ค))โ๐ง) โ ((๐ค โ (โ โ {0}) โฆ (1 /
๐ค))โ๐ด))) < ๐ฅ))) |
49 | 48 | reximdv 3168 |
. . . 4
โข ((๐ โง ๐ฅ โ โ+) โ
(โ๐ฆ โ
โ+ โ๐ง โ (โ โ
{0})((absโ(๐ง โ
๐ด)) < ๐ฆ โ (absโ((1 / ๐ง) โ (1 / ๐ด))) < ๐ฅ) โ โ๐ฆ โ โ+ โ๐ง โ (โ โ
{0})((absโ(๐ง โ
๐ด)) < ๐ฆ โ (absโ(((๐ค โ (โ โ {0}) โฆ (1 /
๐ค))โ๐ง) โ ((๐ค โ (โ โ {0}) โฆ (1 /
๐ค))โ๐ด))) < ๐ฅ))) |
50 | 25, 49 | mpd 15 |
. . 3
โข ((๐ โง ๐ฅ โ โ+) โ
โ๐ฆ โ
โ+ โ๐ง โ (โ โ
{0})((absโ(๐ง โ
๐ด)) < ๐ฆ โ (absโ(((๐ค โ (โ โ {0}) โฆ (1 /
๐ค))โ๐ง) โ ((๐ค โ (โ โ {0}) โฆ (1 /
๐ค))โ๐ด))) < ๐ฅ)) |
51 | | climrec.5 |
. . 3
โข ((๐ โง ๐ โ ๐) โ (๐บโ๐) โ (โ โ
{0})) |
52 | | climrec.6 |
. . . 4
โข ((๐ โง ๐ โ ๐) โ (๐ปโ๐) = (1 / (๐บโ๐))) |
53 | | eqidd 2738 |
. . . . 5
โข ((๐ โง ๐ โ ๐) โ (๐ค โ (โ โ {0}) โฆ (1 /
๐ค)) = (๐ค โ (โ โ {0}) โฆ (1 /
๐ค))) |
54 | | oveq2 7366 |
. . . . . 6
โข (๐ค = (๐บโ๐) โ (1 / ๐ค) = (1 / (๐บโ๐))) |
55 | 54 | adantl 483 |
. . . . 5
โข (((๐ โง ๐ โ ๐) โง ๐ค = (๐บโ๐)) โ (1 / ๐ค) = (1 / (๐บโ๐))) |
56 | 51 | eldifad 3923 |
. . . . . 6
โข ((๐ โง ๐ โ ๐) โ (๐บโ๐) โ โ) |
57 | | eldifsni 4751 |
. . . . . . 7
โข ((๐บโ๐) โ (โ โ {0}) โ (๐บโ๐) โ 0) |
58 | 51, 57 | syl 17 |
. . . . . 6
โข ((๐ โง ๐ โ ๐) โ (๐บโ๐) โ 0) |
59 | 56, 58 | reccld 11925 |
. . . . 5
โข ((๐ โง ๐ โ ๐) โ (1 / (๐บโ๐)) โ โ) |
60 | 53, 55, 51, 59 | fvmptd 6956 |
. . . 4
โข ((๐ โง ๐ โ ๐) โ ((๐ค โ (โ โ {0}) โฆ (1 /
๐ค))โ(๐บโ๐)) = (1 / (๐บโ๐))) |
61 | 52, 60 | eqtr4d 2780 |
. . 3
โข ((๐ โง ๐ โ ๐) โ (๐ปโ๐) = ((๐ค โ (โ โ {0}) โฆ (1 /
๐ค))โ(๐บโ๐))) |
62 | 1, 2, 11, 21, 3, 22, 50, 51, 61 | climcn1 15475 |
. 2
โข (๐ โ ๐ป โ ((๐ค โ (โ โ {0}) โฆ (1 /
๐ค))โ๐ด)) |
63 | 62, 38 | breqtrd 5132 |
1
โข (๐ โ ๐ป โ (1 / ๐ด)) |