Step |
Hyp |
Ref |
Expression |
1 |
|
rlimcxp.1 |
โข ( ( ๐ โง ๐ โ ๐ด ) โ ๐ต โ ๐ ) |
2 |
|
rlimcxp.2 |
โข ( ๐ โ ( ๐ โ ๐ด โฆ ๐ต ) โ๐ 0 ) |
3 |
|
rlimcxp.3 |
โข ( ๐ โ ๐ถ โ โ+ ) |
4 |
|
rlimf |
โข ( ( ๐ โ ๐ด โฆ ๐ต ) โ๐ 0 โ ( ๐ โ ๐ด โฆ ๐ต ) : dom ( ๐ โ ๐ด โฆ ๐ต ) โถ โ ) |
5 |
2 4
|
syl |
โข ( ๐ โ ( ๐ โ ๐ด โฆ ๐ต ) : dom ( ๐ โ ๐ด โฆ ๐ต ) โถ โ ) |
6 |
1
|
ralrimiva |
โข ( ๐ โ โ ๐ โ ๐ด ๐ต โ ๐ ) |
7 |
|
dmmptg |
โข ( โ ๐ โ ๐ด ๐ต โ ๐ โ dom ( ๐ โ ๐ด โฆ ๐ต ) = ๐ด ) |
8 |
6 7
|
syl |
โข ( ๐ โ dom ( ๐ โ ๐ด โฆ ๐ต ) = ๐ด ) |
9 |
8
|
feq2d |
โข ( ๐ โ ( ( ๐ โ ๐ด โฆ ๐ต ) : dom ( ๐ โ ๐ด โฆ ๐ต ) โถ โ โ ( ๐ โ ๐ด โฆ ๐ต ) : ๐ด โถ โ ) ) |
10 |
5 9
|
mpbid |
โข ( ๐ โ ( ๐ โ ๐ด โฆ ๐ต ) : ๐ด โถ โ ) |
11 |
|
eqid |
โข ( ๐ โ ๐ด โฆ ๐ต ) = ( ๐ โ ๐ด โฆ ๐ต ) |
12 |
11
|
fmpt |
โข ( โ ๐ โ ๐ด ๐ต โ โ โ ( ๐ โ ๐ด โฆ ๐ต ) : ๐ด โถ โ ) |
13 |
10 12
|
sylibr |
โข ( ๐ โ โ ๐ โ ๐ด ๐ต โ โ ) |
14 |
13
|
adantr |
โข ( ( ๐ โง ๐ฅ โ โ+ ) โ โ ๐ โ ๐ด ๐ต โ โ ) |
15 |
|
simpr |
โข ( ( ๐ โง ๐ฅ โ โ+ ) โ ๐ฅ โ โ+ ) |
16 |
3
|
adantr |
โข ( ( ๐ โง ๐ฅ โ โ+ ) โ ๐ถ โ โ+ ) |
17 |
16
|
rprecred |
โข ( ( ๐ โง ๐ฅ โ โ+ ) โ ( 1 / ๐ถ ) โ โ ) |
18 |
15 17
|
rpcxpcld |
โข ( ( ๐ โง ๐ฅ โ โ+ ) โ ( ๐ฅ โ๐ ( 1 / ๐ถ ) ) โ โ+ ) |
19 |
2
|
adantr |
โข ( ( ๐ โง ๐ฅ โ โ+ ) โ ( ๐ โ ๐ด โฆ ๐ต ) โ๐ 0 ) |
20 |
14 18 19
|
rlimi |
โข ( ( ๐ โง ๐ฅ โ โ+ ) โ โ ๐ฆ โ โ โ ๐ โ ๐ด ( ๐ฆ โค ๐ โ ( abs โ ( ๐ต โ 0 ) ) < ( ๐ฅ โ๐ ( 1 / ๐ถ ) ) ) ) |
21 |
1 2
|
rlimmptrcl |
โข ( ( ๐ โง ๐ โ ๐ด ) โ ๐ต โ โ ) |
22 |
21
|
adantlr |
โข ( ( ( ๐ โง ๐ฅ โ โ+ ) โง ๐ โ ๐ด ) โ ๐ต โ โ ) |
23 |
22
|
abscld |
โข ( ( ( ๐ โง ๐ฅ โ โ+ ) โง ๐ โ ๐ด ) โ ( abs โ ๐ต ) โ โ ) |
24 |
22
|
absge0d |
โข ( ( ( ๐ โง ๐ฅ โ โ+ ) โง ๐ โ ๐ด ) โ 0 โค ( abs โ ๐ต ) ) |
25 |
18
|
adantr |
โข ( ( ( ๐ โง ๐ฅ โ โ+ ) โง ๐ โ ๐ด ) โ ( ๐ฅ โ๐ ( 1 / ๐ถ ) ) โ โ+ ) |
26 |
25
|
rpred |
โข ( ( ( ๐ โง ๐ฅ โ โ+ ) โง ๐ โ ๐ด ) โ ( ๐ฅ โ๐ ( 1 / ๐ถ ) ) โ โ ) |
27 |
25
|
rpge0d |
โข ( ( ( ๐ โง ๐ฅ โ โ+ ) โง ๐ โ ๐ด ) โ 0 โค ( ๐ฅ โ๐ ( 1 / ๐ถ ) ) ) |
28 |
3
|
ad2antrr |
โข ( ( ( ๐ โง ๐ฅ โ โ+ ) โง ๐ โ ๐ด ) โ ๐ถ โ โ+ ) |
29 |
23 24 26 27 28
|
cxplt2d |
โข ( ( ( ๐ โง ๐ฅ โ โ+ ) โง ๐ โ ๐ด ) โ ( ( abs โ ๐ต ) < ( ๐ฅ โ๐ ( 1 / ๐ถ ) ) โ ( ( abs โ ๐ต ) โ๐ ๐ถ ) < ( ( ๐ฅ โ๐ ( 1 / ๐ถ ) ) โ๐ ๐ถ ) ) ) |
30 |
22
|
subid1d |
โข ( ( ( ๐ โง ๐ฅ โ โ+ ) โง ๐ โ ๐ด ) โ ( ๐ต โ 0 ) = ๐ต ) |
31 |
30
|
fveq2d |
โข ( ( ( ๐ โง ๐ฅ โ โ+ ) โง ๐ โ ๐ด ) โ ( abs โ ( ๐ต โ 0 ) ) = ( abs โ ๐ต ) ) |
32 |
31
|
breq1d |
โข ( ( ( ๐ โง ๐ฅ โ โ+ ) โง ๐ โ ๐ด ) โ ( ( abs โ ( ๐ต โ 0 ) ) < ( ๐ฅ โ๐ ( 1 / ๐ถ ) ) โ ( abs โ ๐ต ) < ( ๐ฅ โ๐ ( 1 / ๐ถ ) ) ) ) |
33 |
28
|
rpred |
โข ( ( ( ๐ โง ๐ฅ โ โ+ ) โง ๐ โ ๐ด ) โ ๐ถ โ โ ) |
34 |
|
abscxp2 |
โข ( ( ๐ต โ โ โง ๐ถ โ โ ) โ ( abs โ ( ๐ต โ๐ ๐ถ ) ) = ( ( abs โ ๐ต ) โ๐ ๐ถ ) ) |
35 |
22 33 34
|
syl2anc |
โข ( ( ( ๐ โง ๐ฅ โ โ+ ) โง ๐ โ ๐ด ) โ ( abs โ ( ๐ต โ๐ ๐ถ ) ) = ( ( abs โ ๐ต ) โ๐ ๐ถ ) ) |
36 |
28
|
rpcnd |
โข ( ( ( ๐ โง ๐ฅ โ โ+ ) โง ๐ โ ๐ด ) โ ๐ถ โ โ ) |
37 |
28
|
rpne0d |
โข ( ( ( ๐ โง ๐ฅ โ โ+ ) โง ๐ โ ๐ด ) โ ๐ถ โ 0 ) |
38 |
36 37
|
recid2d |
โข ( ( ( ๐ โง ๐ฅ โ โ+ ) โง ๐ โ ๐ด ) โ ( ( 1 / ๐ถ ) ยท ๐ถ ) = 1 ) |
39 |
38
|
oveq2d |
โข ( ( ( ๐ โง ๐ฅ โ โ+ ) โง ๐ โ ๐ด ) โ ( ๐ฅ โ๐ ( ( 1 / ๐ถ ) ยท ๐ถ ) ) = ( ๐ฅ โ๐ 1 ) ) |
40 |
|
simplr |
โข ( ( ( ๐ โง ๐ฅ โ โ+ ) โง ๐ โ ๐ด ) โ ๐ฅ โ โ+ ) |
41 |
17
|
adantr |
โข ( ( ( ๐ โง ๐ฅ โ โ+ ) โง ๐ โ ๐ด ) โ ( 1 / ๐ถ ) โ โ ) |
42 |
40 41 36
|
cxpmuld |
โข ( ( ( ๐ โง ๐ฅ โ โ+ ) โง ๐ โ ๐ด ) โ ( ๐ฅ โ๐ ( ( 1 / ๐ถ ) ยท ๐ถ ) ) = ( ( ๐ฅ โ๐ ( 1 / ๐ถ ) ) โ๐ ๐ถ ) ) |
43 |
40
|
rpcnd |
โข ( ( ( ๐ โง ๐ฅ โ โ+ ) โง ๐ โ ๐ด ) โ ๐ฅ โ โ ) |
44 |
43
|
cxp1d |
โข ( ( ( ๐ โง ๐ฅ โ โ+ ) โง ๐ โ ๐ด ) โ ( ๐ฅ โ๐ 1 ) = ๐ฅ ) |
45 |
39 42 44
|
3eqtr3rd |
โข ( ( ( ๐ โง ๐ฅ โ โ+ ) โง ๐ โ ๐ด ) โ ๐ฅ = ( ( ๐ฅ โ๐ ( 1 / ๐ถ ) ) โ๐ ๐ถ ) ) |
46 |
35 45
|
breq12d |
โข ( ( ( ๐ โง ๐ฅ โ โ+ ) โง ๐ โ ๐ด ) โ ( ( abs โ ( ๐ต โ๐ ๐ถ ) ) < ๐ฅ โ ( ( abs โ ๐ต ) โ๐ ๐ถ ) < ( ( ๐ฅ โ๐ ( 1 / ๐ถ ) ) โ๐ ๐ถ ) ) ) |
47 |
29 32 46
|
3bitr4d |
โข ( ( ( ๐ โง ๐ฅ โ โ+ ) โง ๐ โ ๐ด ) โ ( ( abs โ ( ๐ต โ 0 ) ) < ( ๐ฅ โ๐ ( 1 / ๐ถ ) ) โ ( abs โ ( ๐ต โ๐ ๐ถ ) ) < ๐ฅ ) ) |
48 |
47
|
biimpd |
โข ( ( ( ๐ โง ๐ฅ โ โ+ ) โง ๐ โ ๐ด ) โ ( ( abs โ ( ๐ต โ 0 ) ) < ( ๐ฅ โ๐ ( 1 / ๐ถ ) ) โ ( abs โ ( ๐ต โ๐ ๐ถ ) ) < ๐ฅ ) ) |
49 |
48
|
imim2d |
โข ( ( ( ๐ โง ๐ฅ โ โ+ ) โง ๐ โ ๐ด ) โ ( ( ๐ฆ โค ๐ โ ( abs โ ( ๐ต โ 0 ) ) < ( ๐ฅ โ๐ ( 1 / ๐ถ ) ) ) โ ( ๐ฆ โค ๐ โ ( abs โ ( ๐ต โ๐ ๐ถ ) ) < ๐ฅ ) ) ) |
50 |
49
|
ralimdva |
โข ( ( ๐ โง ๐ฅ โ โ+ ) โ ( โ ๐ โ ๐ด ( ๐ฆ โค ๐ โ ( abs โ ( ๐ต โ 0 ) ) < ( ๐ฅ โ๐ ( 1 / ๐ถ ) ) ) โ โ ๐ โ ๐ด ( ๐ฆ โค ๐ โ ( abs โ ( ๐ต โ๐ ๐ถ ) ) < ๐ฅ ) ) ) |
51 |
50
|
reximdv |
โข ( ( ๐ โง ๐ฅ โ โ+ ) โ ( โ ๐ฆ โ โ โ ๐ โ ๐ด ( ๐ฆ โค ๐ โ ( abs โ ( ๐ต โ 0 ) ) < ( ๐ฅ โ๐ ( 1 / ๐ถ ) ) ) โ โ ๐ฆ โ โ โ ๐ โ ๐ด ( ๐ฆ โค ๐ โ ( abs โ ( ๐ต โ๐ ๐ถ ) ) < ๐ฅ ) ) ) |
52 |
20 51
|
mpd |
โข ( ( ๐ โง ๐ฅ โ โ+ ) โ โ ๐ฆ โ โ โ ๐ โ ๐ด ( ๐ฆ โค ๐ โ ( abs โ ( ๐ต โ๐ ๐ถ ) ) < ๐ฅ ) ) |
53 |
52
|
ralrimiva |
โข ( ๐ โ โ ๐ฅ โ โ+ โ ๐ฆ โ โ โ ๐ โ ๐ด ( ๐ฆ โค ๐ โ ( abs โ ( ๐ต โ๐ ๐ถ ) ) < ๐ฅ ) ) |
54 |
3
|
rpcnd |
โข ( ๐ โ ๐ถ โ โ ) |
55 |
54
|
adantr |
โข ( ( ๐ โง ๐ โ ๐ด ) โ ๐ถ โ โ ) |
56 |
21 55
|
cxpcld |
โข ( ( ๐ โง ๐ โ ๐ด ) โ ( ๐ต โ๐ ๐ถ ) โ โ ) |
57 |
56
|
ralrimiva |
โข ( ๐ โ โ ๐ โ ๐ด ( ๐ต โ๐ ๐ถ ) โ โ ) |
58 |
|
rlimss |
โข ( ( ๐ โ ๐ด โฆ ๐ต ) โ๐ 0 โ dom ( ๐ โ ๐ด โฆ ๐ต ) โ โ ) |
59 |
2 58
|
syl |
โข ( ๐ โ dom ( ๐ โ ๐ด โฆ ๐ต ) โ โ ) |
60 |
8 59
|
eqsstrrd |
โข ( ๐ โ ๐ด โ โ ) |
61 |
57 60
|
rlim0 |
โข ( ๐ โ ( ( ๐ โ ๐ด โฆ ( ๐ต โ๐ ๐ถ ) ) โ๐ 0 โ โ ๐ฅ โ โ+ โ ๐ฆ โ โ โ ๐ โ ๐ด ( ๐ฆ โค ๐ โ ( abs โ ( ๐ต โ๐ ๐ถ ) ) < ๐ฅ ) ) ) |
62 |
53 61
|
mpbird |
โข ( ๐ โ ( ๐ โ ๐ด โฆ ( ๐ต โ๐ ๐ถ ) ) โ๐ 0 ) |