Step | Hyp | Ref
| Expression |
1 | | rlimclim.1 |
. . 3
β’ π =
(β€β₯βπ) |
2 | | rlimclim.2 |
. . . 4
β’ (π β π β β€) |
3 | 2 | adantr 482 |
. . 3
β’ ((π β§ πΉ βπ π΄) β π β β€) |
4 | | simpr 486 |
. . 3
β’ ((π β§ πΉ βπ π΄) β πΉ βπ π΄) |
5 | | rlimclim.3 |
. . . . 5
β’ (π β πΉ:πβΆβ) |
6 | | fdm 6727 |
. . . . 5
β’ (πΉ:πβΆβ β dom πΉ = π) |
7 | | eqimss2 4042 |
. . . . 5
β’ (dom
πΉ = π β π β dom πΉ) |
8 | 5, 6, 7 | 3syl 18 |
. . . 4
β’ (π β π β dom πΉ) |
9 | 8 | adantr 482 |
. . 3
β’ ((π β§ πΉ βπ π΄) β π β dom πΉ) |
10 | 1, 3, 4, 9 | rlimclim1 15489 |
. 2
β’ ((π β§ πΉ βπ π΄) β πΉ β π΄) |
11 | | climcl 15443 |
. . . 4
β’ (πΉ β π΄ β π΄ β β) |
12 | 11 | adantl 483 |
. . 3
β’ ((π β§ πΉ β π΄) β π΄ β β) |
13 | 2 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ πΉ β π΄) β§ π¦ β β+) β π β
β€) |
14 | | simpr 486 |
. . . . . 6
β’ (((π β§ πΉ β π΄) β§ π¦ β β+) β π¦ β
β+) |
15 | | eqidd 2734 |
. . . . . 6
β’ ((((π β§ πΉ β π΄) β§ π¦ β β+) β§ π β π) β (πΉβπ) = (πΉβπ)) |
16 | | simplr 768 |
. . . . . 6
β’ (((π β§ πΉ β π΄) β§ π¦ β β+) β πΉ β π΄) |
17 | 1, 13, 14, 15, 16 | climi2 15455 |
. . . . 5
β’ (((π β§ πΉ β π΄) β§ π¦ β β+) β
βπ§ β π βπ β (β€β₯βπ§)(absβ((πΉβπ) β π΄)) < π¦) |
18 | | uzssz 12843 |
. . . . . . . 8
β’
(β€β₯βπ) β β€ |
19 | 1, 18 | eqsstri 4017 |
. . . . . . 7
β’ π β
β€ |
20 | | zssre 12565 |
. . . . . . 7
β’ β€
β β |
21 | 19, 20 | sstri 3992 |
. . . . . 6
β’ π β
β |
22 | | fveq2 6892 |
. . . . . . . . . . . . 13
β’ (π = π€ β (πΉβπ) = (πΉβπ€)) |
23 | 22 | fvoveq1d 7431 |
. . . . . . . . . . . 12
β’ (π = π€ β (absβ((πΉβπ) β π΄)) = (absβ((πΉβπ€) β π΄))) |
24 | 23 | breq1d 5159 |
. . . . . . . . . . 11
β’ (π = π€ β ((absβ((πΉβπ) β π΄)) < π¦ β (absβ((πΉβπ€) β π΄)) < π¦)) |
25 | | simplrr 777 |
. . . . . . . . . . 11
β’
(((((π β§ πΉ β π΄) β§ π¦ β β+) β§ (π§ β π β§ βπ β (β€β₯βπ§)(absβ((πΉβπ) β π΄)) < π¦)) β§ (π€ β π β§ π§ β€ π€)) β βπ β (β€β₯βπ§)(absβ((πΉβπ) β π΄)) < π¦) |
26 | | simplrl 776 |
. . . . . . . . . . . . 13
β’
(((((π β§ πΉ β π΄) β§ π¦ β β+) β§ (π§ β π β§ βπ β (β€β₯βπ§)(absβ((πΉβπ) β π΄)) < π¦)) β§ (π€ β π β§ π§ β€ π€)) β π§ β π) |
27 | 19, 26 | sselid 3981 |
. . . . . . . . . . . 12
β’
(((((π β§ πΉ β π΄) β§ π¦ β β+) β§ (π§ β π β§ βπ β (β€β₯βπ§)(absβ((πΉβπ) β π΄)) < π¦)) β§ (π€ β π β§ π§ β€ π€)) β π§ β β€) |
28 | | simprl 770 |
. . . . . . . . . . . . 13
β’
(((((π β§ πΉ β π΄) β§ π¦ β β+) β§ (π§ β π β§ βπ β (β€β₯βπ§)(absβ((πΉβπ) β π΄)) < π¦)) β§ (π€ β π β§ π§ β€ π€)) β π€ β π) |
29 | 19, 28 | sselid 3981 |
. . . . . . . . . . . 12
β’
(((((π β§ πΉ β π΄) β§ π¦ β β+) β§ (π§ β π β§ βπ β (β€β₯βπ§)(absβ((πΉβπ) β π΄)) < π¦)) β§ (π€ β π β§ π§ β€ π€)) β π€ β β€) |
30 | | simprr 772 |
. . . . . . . . . . . 12
β’
(((((π β§ πΉ β π΄) β§ π¦ β β+) β§ (π§ β π β§ βπ β (β€β₯βπ§)(absβ((πΉβπ) β π΄)) < π¦)) β§ (π€ β π β§ π§ β€ π€)) β π§ β€ π€) |
31 | | eluz2 12828 |
. . . . . . . . . . . 12
β’ (π€ β
(β€β₯βπ§) β (π§ β β€ β§ π€ β β€ β§ π§ β€ π€)) |
32 | 27, 29, 30, 31 | syl3anbrc 1344 |
. . . . . . . . . . 11
β’
(((((π β§ πΉ β π΄) β§ π¦ β β+) β§ (π§ β π β§ βπ β (β€β₯βπ§)(absβ((πΉβπ) β π΄)) < π¦)) β§ (π€ β π β§ π§ β€ π€)) β π€ β (β€β₯βπ§)) |
33 | 24, 25, 32 | rspcdva 3614 |
. . . . . . . . . 10
β’
(((((π β§ πΉ β π΄) β§ π¦ β β+) β§ (π§ β π β§ βπ β (β€β₯βπ§)(absβ((πΉβπ) β π΄)) < π¦)) β§ (π€ β π β§ π§ β€ π€)) β (absβ((πΉβπ€) β π΄)) < π¦) |
34 | 33 | expr 458 |
. . . . . . . . 9
β’
(((((π β§ πΉ β π΄) β§ π¦ β β+) β§ (π§ β π β§ βπ β (β€β₯βπ§)(absβ((πΉβπ) β π΄)) < π¦)) β§ π€ β π) β (π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦)) |
35 | 34 | ralrimiva 3147 |
. . . . . . . 8
β’ ((((π β§ πΉ β π΄) β§ π¦ β β+) β§ (π§ β π β§ βπ β (β€β₯βπ§)(absβ((πΉβπ) β π΄)) < π¦)) β βπ€ β π (π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦)) |
36 | 35 | expr 458 |
. . . . . . 7
β’ ((((π β§ πΉ β π΄) β§ π¦ β β+) β§ π§ β π) β (βπ β (β€β₯βπ§)(absβ((πΉβπ) β π΄)) < π¦ β βπ€ β π (π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦))) |
37 | 36 | reximdva 3169 |
. . . . . 6
β’ (((π β§ πΉ β π΄) β§ π¦ β β+) β
(βπ§ β π βπ β (β€β₯βπ§)(absβ((πΉβπ) β π΄)) < π¦ β βπ§ β π βπ€ β π (π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦))) |
38 | | ssrexv 4052 |
. . . . . 6
β’ (π β β β
(βπ§ β π βπ€ β π (π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦) β βπ§ β β βπ€ β π (π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦))) |
39 | 21, 37, 38 | mpsylsyld 69 |
. . . . 5
β’ (((π β§ πΉ β π΄) β§ π¦ β β+) β
(βπ§ β π βπ β (β€β₯βπ§)(absβ((πΉβπ) β π΄)) < π¦ β βπ§ β β βπ€ β π (π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦))) |
40 | 17, 39 | mpd 15 |
. . . 4
β’ (((π β§ πΉ β π΄) β§ π¦ β β+) β
βπ§ β β
βπ€ β π (π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦)) |
41 | 40 | ralrimiva 3147 |
. . 3
β’ ((π β§ πΉ β π΄) β βπ¦ β β+ βπ§ β β βπ€ β π (π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦)) |
42 | 5 | adantr 482 |
. . . 4
β’ ((π β§ πΉ β π΄) β πΉ:πβΆβ) |
43 | 21 | a1i 11 |
. . . 4
β’ ((π β§ πΉ β π΄) β π β β) |
44 | | eqidd 2734 |
. . . 4
β’ (((π β§ πΉ β π΄) β§ π€ β π) β (πΉβπ€) = (πΉβπ€)) |
45 | 42, 43, 44 | rlim 15439 |
. . 3
β’ ((π β§ πΉ β π΄) β (πΉ βπ π΄ β (π΄ β β β§ βπ¦ β β+
βπ§ β β
βπ€ β π (π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦)))) |
46 | 12, 41, 45 | mpbir2and 712 |
. 2
β’ ((π β§ πΉ β π΄) β πΉ βπ π΄) |
47 | 10, 46 | impbida 800 |
1
β’ (π β (πΉ βπ π΄ β πΉ β π΄)) |