Step | Hyp | Ref
| Expression |
1 | | simpll 766 |
. . . . . 6
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π) |
2 | | liminflimsupxrre.2 |
. . . . . . . 8
β’ π =
(β€β₯βπ) |
3 | 2 | uztrn2 12787 |
. . . . . . 7
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
4 | 3 | adantll 713 |
. . . . . 6
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π β π) |
5 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π β π) β π β π) |
6 | | liminflimsupxrre.3 |
. . . . . . . . . . . 12
β’ (π β πΉ:πβΆβ*) |
7 | 6 | fdmd 6680 |
. . . . . . . . . . 11
β’ (π β dom πΉ = π) |
8 | 7 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β π) β dom πΉ = π) |
9 | 5, 8 | eleqtrrd 2837 |
. . . . . . . . 9
β’ ((π β§ π β π) β π β dom πΉ) |
10 | 9 | ad2antrr 725 |
. . . . . . . 8
β’ ((((π β§ π β π) β§ (πΉβπ) < +β) β§ -β < (πΉβπ)) β π β dom πΉ) |
11 | 6 | ffvelcdmda 7036 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (πΉβπ) β
β*) |
12 | 11 | ad2antrr 725 |
. . . . . . . . 9
β’ ((((π β§ π β π) β§ (πΉβπ) < +β) β§ -β < (πΉβπ)) β (πΉβπ) β
β*) |
13 | | mnfxr 11217 |
. . . . . . . . . . . 12
β’ -β
β β* |
14 | 13 | a1i 11 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ -β < (πΉβπ)) β -β β
β*) |
15 | 11 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ -β < (πΉβπ)) β (πΉβπ) β
β*) |
16 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ -β < (πΉβπ)) β -β < (πΉβπ)) |
17 | 14, 15, 16 | xrgtned 43643 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ -β < (πΉβπ)) β (πΉβπ) β -β) |
18 | 17 | adantlr 714 |
. . . . . . . . 9
β’ ((((π β§ π β π) β§ (πΉβπ) < +β) β§ -β < (πΉβπ)) β (πΉβπ) β -β) |
19 | 11 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ (πΉβπ) < +β) β (πΉβπ) β
β*) |
20 | | pnfxr 11214 |
. . . . . . . . . . . 12
β’ +β
β β* |
21 | 20 | a1i 11 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ (πΉβπ) < +β) β +β β
β*) |
22 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ (πΉβπ) < +β) β (πΉβπ) < +β) |
23 | 19, 21, 22 | xrltned 43678 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ (πΉβπ) < +β) β (πΉβπ) β +β) |
24 | 23 | adantr 482 |
. . . . . . . . 9
β’ ((((π β§ π β π) β§ (πΉβπ) < +β) β§ -β < (πΉβπ)) β (πΉβπ) β +β) |
25 | 12, 18, 24 | xrred 43686 |
. . . . . . . 8
β’ ((((π β§ π β π) β§ (πΉβπ) < +β) β§ -β < (πΉβπ)) β (πΉβπ) β β) |
26 | 10, 25 | jca 513 |
. . . . . . 7
β’ ((((π β§ π β π) β§ (πΉβπ) < +β) β§ -β < (πΉβπ)) β (π β dom πΉ β§ (πΉβπ) β β)) |
27 | 26 | expl 459 |
. . . . . 6
β’ ((π β§ π β π) β (((πΉβπ) < +β β§ -β < (πΉβπ)) β (π β dom πΉ β§ (πΉβπ) β β))) |
28 | 1, 4, 27 | syl2anc 585 |
. . . . 5
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β (((πΉβπ) < +β β§ -β < (πΉβπ)) β (π β dom πΉ β§ (πΉβπ) β β))) |
29 | 28 | ralimdva 3161 |
. . . 4
β’ ((π β§ π β π) β (βπ β (β€β₯βπ)((πΉβπ) < +β β§ -β < (πΉβπ)) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β))) |
30 | 29 | imp 408 |
. . 3
β’ (((π β§ π β π) β§ βπ β (β€β₯βπ)((πΉβπ) < +β β§ -β < (πΉβπ))) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β)) |
31 | 6 | ffund 6673 |
. . . . 5
β’ (π β Fun πΉ) |
32 | | ffvresb 7073 |
. . . . 5
β’ (Fun
πΉ β ((πΉ βΎ
(β€β₯βπ)):(β€β₯βπ)βΆβ β
βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β))) |
33 | 31, 32 | syl 17 |
. . . 4
β’ (π β ((πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ β
βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β))) |
34 | 33 | ad2antrr 725 |
. . 3
β’ (((π β§ π β π) β§ βπ β (β€β₯βπ)((πΉβπ) < +β β§ -β < (πΉβπ))) β ((πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ β
βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β))) |
35 | 30, 34 | mpbird 257 |
. 2
β’ (((π β§ π β π) β§ βπ β (β€β₯βπ)((πΉβπ) < +β β§ -β < (πΉβπ))) β (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) |
36 | | nfv 1918 |
. . . 4
β’
β²ππ |
37 | | nfcv 2904 |
. . . 4
β’
β²ππΉ |
38 | | liminflimsupxrre.1 |
. . . 4
β’ (π β π β β€) |
39 | | liminflimsupxrre.4 |
. . . 4
β’ (π β (lim supβπΉ) β
+β) |
40 | 36, 37, 38, 2, 6, 39 | limsupubuz2 44140 |
. . 3
β’ (π β βπ β π βπ β (β€β₯βπ)(πΉβπ) < +β) |
41 | | liminflimsupxrre.5 |
. . . 4
β’ (π β (lim infβπΉ) β
-β) |
42 | 36, 37, 38, 2, 6, 41 | liminflbuz2 44142 |
. . 3
β’ (π β βπ β π βπ β (β€β₯βπ)-β < (πΉβπ)) |
43 | 2 | rexanuz2 15240 |
. . 3
β’
(βπ β
π βπ β
(β€β₯βπ)((πΉβπ) < +β β§ -β < (πΉβπ)) β (βπ β π βπ β (β€β₯βπ)(πΉβπ) < +β β§ βπ β π βπ β (β€β₯βπ)-β < (πΉβπ))) |
44 | 40, 42, 43 | sylanbrc 584 |
. 2
β’ (π β βπ β π βπ β (β€β₯βπ)((πΉβπ) < +β β§ -β < (πΉβπ))) |
45 | 35, 44 | reximddv3 43449 |
1
β’ (π β βπ β π (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) |