Step | Hyp | Ref
| Expression |
1 | | nfv 1918 |
. . . . . 6
β’
β²π(π β§ π β π) |
2 | | nfra1 3268 |
. . . . . 6
β’
β²πβπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β ( β βπΉ))) < 1) |
3 | 1, 2 | nfan 1903 |
. . . . 5
β’
β²π((π β§ π β π) β§ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β ( β βπΉ))) < 1)) |
4 | | climrescn.z |
. . . . . . . . . 10
β’ π =
(β€β₯βπ) |
5 | 4 | uztrn2 12783 |
. . . . . . . . 9
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
6 | 5 | adantll 713 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π β π) |
7 | | climrescn.f |
. . . . . . . . . 10
β’ (π β πΉ Fn π) |
8 | 7 | fndmd 6608 |
. . . . . . . . 9
β’ (π β dom πΉ = π) |
9 | 8 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β dom πΉ = π) |
10 | 6, 9 | eleqtrrd 2841 |
. . . . . . 7
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π β dom πΉ) |
11 | 10 | adantlr 714 |
. . . . . 6
β’ ((((π β§ π β π) β§ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β ( β βπΉ))) < 1)) β§ π β (β€β₯βπ)) β π β dom πΉ) |
12 | | rspa 3232 |
. . . . . . . . 9
β’
((βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β ( β βπΉ))) < 1) β§ π β (β€β₯βπ)) β ((πΉβπ) β β β§ (absβ((πΉβπ) β ( β βπΉ))) < 1)) |
13 | 12 | adantll 713 |
. . . . . . . 8
β’ (((π β π β§ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β ( β βπΉ))) < 1)) β§ π β (β€β₯βπ)) β ((πΉβπ) β β β§ (absβ((πΉβπ) β ( β βπΉ))) < 1)) |
14 | 13 | simpld 496 |
. . . . . . 7
β’ (((π β π β§ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β ( β βπΉ))) < 1)) β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
15 | 14 | adantlll 717 |
. . . . . 6
β’ ((((π β§ π β π) β§ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β ( β βπΉ))) < 1)) β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
16 | 11, 15 | jca 513 |
. . . . 5
β’ ((((π β§ π β π) β§ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β ( β βπΉ))) < 1)) β§ π β (β€β₯βπ)) β (π β dom πΉ β§ (πΉβπ) β β)) |
17 | 3, 16 | ralrimia 3242 |
. . . 4
β’ (((π β§ π β π) β§ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β ( β βπΉ))) < 1)) β βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β)) |
18 | | fnfun 6603 |
. . . . . 6
β’ (πΉ Fn π β Fun πΉ) |
19 | | ffvresb 7073 |
. . . . . 6
β’ (Fun
πΉ β ((πΉ βΎ
(β€β₯βπ)):(β€β₯βπ)βΆβ β
βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β))) |
20 | 7, 18, 19 | 3syl 18 |
. . . . 5
β’ (π β ((πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ β
βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β))) |
21 | 20 | ad2antrr 725 |
. . . 4
β’ (((π β§ π β π) β§ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β ( β βπΉ))) < 1)) β ((πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ β
βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β))) |
22 | 17, 21 | mpbird 257 |
. . 3
β’ (((π β§ π β π) β§ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β ( β βπΉ))) < 1)) β (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) |
23 | | breq2 5110 |
. . . . . . 7
β’ (π₯ = 1 β ((absβ((πΉβπ) β ( β βπΉ))) < π₯ β (absβ((πΉβπ) β ( β βπΉ))) < 1)) |
24 | 23 | anbi2d 630 |
. . . . . 6
β’ (π₯ = 1 β (((πΉβπ) β β β§ (absβ((πΉβπ) β ( β βπΉ))) < π₯) β ((πΉβπ) β β β§ (absβ((πΉβπ) β ( β βπΉ))) < 1))) |
25 | 24 | rexralbidv 3215 |
. . . . 5
β’ (π₯ = 1 β (βπ β β€ βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β ( β βπΉ))) < π₯) β βπ β β€ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β ( β βπΉ))) < 1))) |
26 | | climrescn.c |
. . . . . . . 8
β’ (π β πΉ β dom β ) |
27 | | climdm 15437 |
. . . . . . . 8
β’ (πΉ β dom β β πΉ β ( β βπΉ)) |
28 | 26, 27 | sylib 217 |
. . . . . . 7
β’ (π β πΉ β ( β βπΉ)) |
29 | | eqidd 2738 |
. . . . . . . 8
β’ ((π β§ π β β€) β (πΉβπ) = (πΉβπ)) |
30 | 26, 29 | clim 15377 |
. . . . . . 7
β’ (π β (πΉ β ( β βπΉ) β (( β βπΉ) β β β§ βπ₯ β β+
βπ β β€
βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β ( β βπΉ))) < π₯)))) |
31 | 28, 30 | mpbid 231 |
. . . . . 6
β’ (π β (( β βπΉ) β β β§
βπ₯ β
β+ βπ β β€ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β ( β βπΉ))) < π₯))) |
32 | 31 | simprd 497 |
. . . . 5
β’ (π β βπ₯ β β+ βπ β β€ βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β ( β βπΉ))) < π₯)) |
33 | | 1rp 12920 |
. . . . . 6
β’ 1 β
β+ |
34 | 33 | a1i 11 |
. . . . 5
β’ (π β 1 β
β+) |
35 | 25, 32, 34 | rspcdva 3583 |
. . . 4
β’ (π β βπ β β€ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β ( β βπΉ))) < 1)) |
36 | | climrescn.m |
. . . . 5
β’ (π β π β β€) |
37 | 4 | rexuz3 15234 |
. . . . 5
β’ (π β β€ β
(βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β ( β βπΉ))) < 1) β βπ β β€ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β ( β βπΉ))) < 1))) |
38 | 36, 37 | syl 17 |
. . . 4
β’ (π β (βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β ( β βπΉ))) < 1) β βπ β β€ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β ( β βπΉ))) < 1))) |
39 | 35, 38 | mpbird 257 |
. . 3
β’ (π β βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β ( β βπΉ))) < 1)) |
40 | 22, 39 | reximddv3 43368 |
. 2
β’ (π β βπ β π (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) |
41 | | fveq2 6843 |
. . . . 5
β’ (π = π β (β€β₯βπ) =
(β€β₯βπ)) |
42 | 41 | reseq2d 5938 |
. . . 4
β’ (π = π β (πΉ βΎ (β€β₯βπ)) = (πΉ βΎ (β€β₯βπ))) |
43 | 42, 41 | feq12d 6657 |
. . 3
β’ (π = π β ((πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ β (πΉ βΎ
(β€β₯βπ)):(β€β₯βπ)βΆβ)) |
44 | 43 | cbvrexvw 3227 |
. 2
β’
(βπ β
π (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ β
βπ β π (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) |
45 | 40, 44 | sylibr 233 |
1
β’ (π β βπ β π (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) |