Step | Hyp | Ref
| Expression |
1 | | fvex 6905 |
. . . . . . 7
β’ (πΉβπ€) β V |
2 | 1 | rgenw 3066 |
. . . . . 6
β’
βπ€ β dom
πΉ(πΉβπ€) β V |
3 | 2 | a1i 11 |
. . . . 5
β’ ((π β§ π¦ β β+) β
βπ€ β dom πΉ(πΉβπ€) β V) |
4 | | simpr 486 |
. . . . 5
β’ ((π β§ π¦ β β+) β π¦ β
β+) |
5 | | rlimclim1.3 |
. . . . . . . . 9
β’ (π β πΉ βπ π΄) |
6 | | rlimf 15445 |
. . . . . . . . 9
β’ (πΉ βπ
π΄ β πΉ:dom πΉβΆβ) |
7 | 5, 6 | syl 17 |
. . . . . . . 8
β’ (π β πΉ:dom πΉβΆβ) |
8 | 7 | adantr 482 |
. . . . . . 7
β’ ((π β§ π¦ β β+) β πΉ:dom πΉβΆβ) |
9 | 8 | feqmptd 6961 |
. . . . . 6
β’ ((π β§ π¦ β β+) β πΉ = (π€ β dom πΉ β¦ (πΉβπ€))) |
10 | 5 | adantr 482 |
. . . . . 6
β’ ((π β§ π¦ β β+) β πΉ βπ
π΄) |
11 | 9, 10 | eqbrtrrd 5173 |
. . . . 5
β’ ((π β§ π¦ β β+) β (π€ β dom πΉ β¦ (πΉβπ€)) βπ π΄) |
12 | 3, 4, 11 | rlimi 15457 |
. . . 4
β’ ((π β§ π¦ β β+) β
βπ§ β β
βπ€ β dom πΉ(π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦)) |
13 | | rlimclim1.2 |
. . . . . . . 8
β’ (π β π β β€) |
14 | 13 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π¦ β β+) β§ (π§ β β β§
βπ€ β dom πΉ(π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦))) β π β β€) |
15 | | flcl 13760 |
. . . . . . . . . 10
β’ (π§ β β β
(ββπ§) β
β€) |
16 | 15 | peano2zd 12669 |
. . . . . . . . 9
β’ (π§ β β β
((ββπ§) + 1)
β β€) |
17 | 16 | ad2antrl 727 |
. . . . . . . 8
β’ (((π β§ π¦ β β+) β§ (π§ β β β§
βπ€ β dom πΉ(π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦))) β ((ββπ§) + 1) β β€) |
18 | 17, 14 | ifcld 4575 |
. . . . . . 7
β’ (((π β§ π¦ β β+) β§ (π§ β β β§
βπ€ β dom πΉ(π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦))) β if(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π) β β€) |
19 | 14 | zred 12666 |
. . . . . . . 8
β’ (((π β§ π¦ β β+) β§ (π§ β β β§
βπ€ β dom πΉ(π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦))) β π β β) |
20 | 17 | zred 12666 |
. . . . . . . 8
β’ (((π β§ π¦ β β+) β§ (π§ β β β§
βπ€ β dom πΉ(π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦))) β ((ββπ§) + 1) β β) |
21 | | max1 13164 |
. . . . . . . 8
β’ ((π β β β§
((ββπ§) + 1)
β β) β π
β€ if(π β€
((ββπ§) + 1),
((ββπ§) + 1),
π)) |
22 | 19, 20, 21 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ π¦ β β+) β§ (π§ β β β§
βπ€ β dom πΉ(π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦))) β π β€ if(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π)) |
23 | | eluz2 12828 |
. . . . . . 7
β’ (if(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π) β (β€β₯βπ) β (π β β€ β§ if(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π) β β€ β§ π β€ if(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π))) |
24 | 14, 18, 22, 23 | syl3anbrc 1344 |
. . . . . 6
β’ (((π β§ π¦ β β+) β§ (π§ β β β§
βπ€ β dom πΉ(π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦))) β if(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π) β (β€β₯βπ)) |
25 | | rlimclim1.1 |
. . . . . 6
β’ π =
(β€β₯βπ) |
26 | 24, 25 | eleqtrrdi 2845 |
. . . . 5
β’ (((π β§ π¦ β β+) β§ (π§ β β β§
βπ€ β dom πΉ(π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦))) β if(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π) β π) |
27 | | simplrl 776 |
. . . . . . . 8
β’ ((((π β§ π¦ β β+) β§ (π§ β β β§
βπ€ β dom πΉ(π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦))) β§ π β
(β€β₯βif(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π))) β π§ β β) |
28 | 16 | zred 12666 |
. . . . . . . . . 10
β’ (π§ β β β
((ββπ§) + 1)
β β) |
29 | 27, 28 | syl 17 |
. . . . . . . . 9
β’ ((((π β§ π¦ β β+) β§ (π§ β β β§
βπ€ β dom πΉ(π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦))) β§ π β
(β€β₯βif(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π))) β ((ββπ§) + 1) β
β) |
30 | 19 | adantr 482 |
. . . . . . . . 9
β’ ((((π β§ π¦ β β+) β§ (π§ β β β§
βπ€ β dom πΉ(π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦))) β§ π β
(β€β₯βif(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π))) β π β β) |
31 | 29, 30 | ifcld 4575 |
. . . . . . . 8
β’ ((((π β§ π¦ β β+) β§ (π§ β β β§
βπ€ β dom πΉ(π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦))) β§ π β
(β€β₯βif(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π))) β if(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π) β β) |
32 | | eluzelre 12833 |
. . . . . . . . 9
β’ (π β
(β€β₯βif(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π)) β π β β) |
33 | 32 | adantl 483 |
. . . . . . . 8
β’ ((((π β§ π¦ β β+) β§ (π§ β β β§
βπ€ β dom πΉ(π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦))) β§ π β
(β€β₯βif(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π))) β π β β) |
34 | | fllep1 13766 |
. . . . . . . . . 10
β’ (π§ β β β π§ β€ ((ββπ§) + 1)) |
35 | 27, 34 | syl 17 |
. . . . . . . . 9
β’ ((((π β§ π¦ β β+) β§ (π§ β β β§
βπ€ β dom πΉ(π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦))) β§ π β
(β€β₯βif(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π))) β π§ β€ ((ββπ§) + 1)) |
36 | | max2 13166 |
. . . . . . . . . 10
β’ ((π β β β§
((ββπ§) + 1)
β β) β ((ββπ§) + 1) β€ if(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π)) |
37 | 30, 29, 36 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π β§ π¦ β β+) β§ (π§ β β β§
βπ€ β dom πΉ(π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦))) β§ π β
(β€β₯βif(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π))) β ((ββπ§) + 1) β€ if(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π)) |
38 | 27, 29, 31, 35, 37 | letrd 11371 |
. . . . . . . 8
β’ ((((π β§ π¦ β β+) β§ (π§ β β β§
βπ€ β dom πΉ(π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦))) β§ π β
(β€β₯βif(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π))) β π§ β€ if(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π)) |
39 | | eluzle 12835 |
. . . . . . . . 9
β’ (π β
(β€β₯βif(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π)) β if(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π) β€ π) |
40 | 39 | adantl 483 |
. . . . . . . 8
β’ ((((π β§ π¦ β β+) β§ (π§ β β β§
βπ€ β dom πΉ(π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦))) β§ π β
(β€β₯βif(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π))) β if(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π) β€ π) |
41 | 27, 31, 33, 38, 40 | letrd 11371 |
. . . . . . 7
β’ ((((π β§ π¦ β β+) β§ (π§ β β β§
βπ€ β dom πΉ(π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦))) β§ π β
(β€β₯βif(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π))) β π§ β€ π) |
42 | | breq2 5153 |
. . . . . . . . 9
β’ (π€ = π β (π§ β€ π€ β π§ β€ π)) |
43 | 42 | imbrov2fvoveq 7434 |
. . . . . . . 8
β’ (π€ = π β ((π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦) β (π§ β€ π β (absβ((πΉβπ) β π΄)) < π¦))) |
44 | | simplrr 777 |
. . . . . . . 8
β’ ((((π β§ π¦ β β+) β§ (π§ β β β§
βπ€ β dom πΉ(π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦))) β§ π β
(β€β₯βif(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π))) β βπ€ β dom πΉ(π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦)) |
45 | | rlimclim1.4 |
. . . . . . . . . 10
β’ (π β π β dom πΉ) |
46 | 45 | ad3antrrr 729 |
. . . . . . . . 9
β’ ((((π β§ π¦ β β+) β§ (π§ β β β§
βπ€ β dom πΉ(π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦))) β§ π β
(β€β₯βif(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π))) β π β dom πΉ) |
47 | 25 | uztrn2 12841 |
. . . . . . . . . 10
β’
((if(π β€
((ββπ§) + 1),
((ββπ§) + 1),
π) β π β§ π β
(β€β₯βif(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π))) β π β π) |
48 | 26, 47 | sylan 581 |
. . . . . . . . 9
β’ ((((π β§ π¦ β β+) β§ (π§ β β β§
βπ€ β dom πΉ(π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦))) β§ π β
(β€β₯βif(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π))) β π β π) |
49 | 46, 48 | sseldd 3984 |
. . . . . . . 8
β’ ((((π β§ π¦ β β+) β§ (π§ β β β§
βπ€ β dom πΉ(π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦))) β§ π β
(β€β₯βif(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π))) β π β dom πΉ) |
50 | 43, 44, 49 | rspcdva 3614 |
. . . . . . 7
β’ ((((π β§ π¦ β β+) β§ (π§ β β β§
βπ€ β dom πΉ(π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦))) β§ π β
(β€β₯βif(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π))) β (π§ β€ π β (absβ((πΉβπ) β π΄)) < π¦)) |
51 | 41, 50 | mpd 15 |
. . . . . 6
β’ ((((π β§ π¦ β β+) β§ (π§ β β β§
βπ€ β dom πΉ(π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦))) β§ π β
(β€β₯βif(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π))) β (absβ((πΉβπ) β π΄)) < π¦) |
52 | 51 | ralrimiva 3147 |
. . . . 5
β’ (((π β§ π¦ β β+) β§ (π§ β β β§
βπ€ β dom πΉ(π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦))) β βπ β
(β€β₯βif(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π))(absβ((πΉβπ) β π΄)) < π¦) |
53 | | fveq2 6892 |
. . . . . . 7
β’ (π = if(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π) β (β€β₯βπ) =
(β€β₯βif(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π))) |
54 | 53 | raleqdv 3326 |
. . . . . 6
β’ (π = if(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π) β (βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π¦ β βπ β
(β€β₯βif(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π))(absβ((πΉβπ) β π΄)) < π¦)) |
55 | 54 | rspcev 3613 |
. . . . 5
β’
((if(π β€
((ββπ§) + 1),
((ββπ§) + 1),
π) β π β§ βπ β
(β€β₯βif(π β€ ((ββπ§) + 1), ((ββπ§) + 1), π))(absβ((πΉβπ) β π΄)) < π¦) β βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π¦) |
56 | 26, 52, 55 | syl2anc 585 |
. . . 4
β’ (((π β§ π¦ β β+) β§ (π§ β β β§
βπ€ β dom πΉ(π§ β€ π€ β (absβ((πΉβπ€) β π΄)) < π¦))) β βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π¦) |
57 | 12, 56 | rexlimddv 3162 |
. . 3
β’ ((π β§ π¦ β β+) β
βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π¦) |
58 | 57 | ralrimiva 3147 |
. 2
β’ (π β βπ¦ β β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π¦) |
59 | | rlimpm 15444 |
. . . 4
β’ (πΉ βπ
π΄ β πΉ β (β βpm
β)) |
60 | 5, 59 | syl 17 |
. . 3
β’ (π β πΉ β (β βpm
β)) |
61 | | eqidd 2734 |
. . 3
β’ ((π β§ π β π) β (πΉβπ) = (πΉβπ)) |
62 | | rlimcl 15447 |
. . . 4
β’ (πΉ βπ
π΄ β π΄ β β) |
63 | 5, 62 | syl 17 |
. . 3
β’ (π β π΄ β β) |
64 | 45 | sselda 3983 |
. . . 4
β’ ((π β§ π β π) β π β dom πΉ) |
65 | 7 | ffvelcdmda 7087 |
. . . 4
β’ ((π β§ π β dom πΉ) β (πΉβπ) β β) |
66 | 64, 65 | syldan 592 |
. . 3
β’ ((π β§ π β π) β (πΉβπ) β β) |
67 | 25, 13, 60, 61, 63, 66 | clim2c 15449 |
. 2
β’ (π β (πΉ β π΄ β βπ¦ β β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π¦)) |
68 | 58, 67 | mpbird 257 |
1
β’ (π β πΉ β π΄) |