Step | Hyp | Ref
| Expression |
1 | | simpll 765 |
. . . . . 6
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π) |
2 | | liminflimsupxrre.2 |
. . . . . . . 8
β’ π =
(β€β₯βπ) |
3 | 2 | uztrn2 12840 |
. . . . . . 7
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
4 | 3 | adantll 712 |
. . . . . 6
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π β π) |
5 | | simpr 485 |
. . . . . . . . . 10
β’ ((π β§ π β π) β π β π) |
6 | | liminflimsupxrre.3 |
. . . . . . . . . . . 12
β’ (π β πΉ:πβΆβ*) |
7 | 6 | fdmd 6728 |
. . . . . . . . . . 11
β’ (π β dom πΉ = π) |
8 | 7 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β π) β dom πΉ = π) |
9 | 5, 8 | eleqtrrd 2836 |
. . . . . . . . 9
β’ ((π β§ π β π) β π β dom πΉ) |
10 | 9 | ad2antrr 724 |
. . . . . . . 8
β’ ((((π β§ π β π) β§ (πΉβπ) < +β) β§ -β < (πΉβπ)) β π β dom πΉ) |
11 | 6 | ffvelcdmda 7086 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (πΉβπ) β
β*) |
12 | 11 | ad2antrr 724 |
. . . . . . . . 9
β’ ((((π β§ π β π) β§ (πΉβπ) < +β) β§ -β < (πΉβπ)) β (πΉβπ) β
β*) |
13 | | mnfxr 11270 |
. . . . . . . . . . . 12
β’ -β
β β* |
14 | 13 | a1i 11 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ -β < (πΉβπ)) β -β β
β*) |
15 | 11 | adantr 481 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ -β < (πΉβπ)) β (πΉβπ) β
β*) |
16 | | simpr 485 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ -β < (πΉβπ)) β -β < (πΉβπ)) |
17 | 14, 15, 16 | xrgtned 44022 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ -β < (πΉβπ)) β (πΉβπ) β -β) |
18 | 17 | adantlr 713 |
. . . . . . . . 9
β’ ((((π β§ π β π) β§ (πΉβπ) < +β) β§ -β < (πΉβπ)) β (πΉβπ) β -β) |
19 | 11 | adantr 481 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ (πΉβπ) < +β) β (πΉβπ) β
β*) |
20 | | pnfxr 11267 |
. . . . . . . . . . . 12
β’ +β
β β* |
21 | 20 | a1i 11 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ (πΉβπ) < +β) β +β β
β*) |
22 | | simpr 485 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ (πΉβπ) < +β) β (πΉβπ) < +β) |
23 | 19, 21, 22 | xrltned 44057 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ (πΉβπ) < +β) β (πΉβπ) β +β) |
24 | 23 | adantr 481 |
. . . . . . . . 9
β’ ((((π β§ π β π) β§ (πΉβπ) < +β) β§ -β < (πΉβπ)) β (πΉβπ) β +β) |
25 | 12, 18, 24 | xrred 44065 |
. . . . . . . 8
β’ ((((π β§ π β π) β§ (πΉβπ) < +β) β§ -β < (πΉβπ)) β (πΉβπ) β β) |
26 | 10, 25 | jca 512 |
. . . . . . 7
β’ ((((π β§ π β π) β§ (πΉβπ) < +β) β§ -β < (πΉβπ)) β (π β dom πΉ β§ (πΉβπ) β β)) |
27 | 26 | expl 458 |
. . . . . 6
β’ ((π β§ π β π) β (((πΉβπ) < +β β§ -β < (πΉβπ)) β (π β dom πΉ β§ (πΉβπ) β β))) |
28 | 1, 4, 27 | syl2anc 584 |
. . . . 5
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β (((πΉβπ) < +β β§ -β < (πΉβπ)) β (π β dom πΉ β§ (πΉβπ) β β))) |
29 | 28 | ralimdva 3167 |
. . . 4
β’ ((π β§ π β π) β (βπ β (β€β₯βπ)((πΉβπ) < +β β§ -β < (πΉβπ)) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β))) |
30 | 29 | imp 407 |
. . 3
β’ (((π β§ π β π) β§ βπ β (β€β₯βπ)((πΉβπ) < +β β§ -β < (πΉβπ))) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β)) |
31 | 6 | ffund 6721 |
. . . . 5
β’ (π β Fun πΉ) |
32 | | ffvresb 7123 |
. . . . 5
β’ (Fun
πΉ β ((πΉ βΎ
(β€β₯βπ)):(β€β₯βπ)βΆβ β
βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β))) |
33 | 31, 32 | syl 17 |
. . . 4
β’ (π β ((πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ β
βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β))) |
34 | 33 | ad2antrr 724 |
. . 3
β’ (((π β§ π β π) β§ βπ β (β€β₯βπ)((πΉβπ) < +β β§ -β < (πΉβπ))) β ((πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ β
βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β))) |
35 | 30, 34 | mpbird 256 |
. 2
β’ (((π β§ π β π) β§ βπ β (β€β₯βπ)((πΉβπ) < +β β§ -β < (πΉβπ))) β (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) |
36 | | nfv 1917 |
. . . 4
β’
β²ππ |
37 | | nfcv 2903 |
. . . 4
β’
β²ππΉ |
38 | | liminflimsupxrre.1 |
. . . 4
β’ (π β π β β€) |
39 | | liminflimsupxrre.4 |
. . . 4
β’ (π β (lim supβπΉ) β
+β) |
40 | 36, 37, 38, 2, 6, 39 | limsupubuz2 44519 |
. . 3
β’ (π β βπ β π βπ β (β€β₯βπ)(πΉβπ) < +β) |
41 | | liminflimsupxrre.5 |
. . . 4
β’ (π β (lim infβπΉ) β
-β) |
42 | 36, 37, 38, 2, 6, 41 | liminflbuz2 44521 |
. . 3
β’ (π β βπ β π βπ β (β€β₯βπ)-β < (πΉβπ)) |
43 | 2 | rexanuz2 15295 |
. . 3
β’
(βπ β
π βπ β
(β€β₯βπ)((πΉβπ) < +β β§ -β < (πΉβπ)) β (βπ β π βπ β (β€β₯βπ)(πΉβπ) < +β β§ βπ β π βπ β (β€β₯βπ)-β < (πΉβπ))) |
44 | 40, 42, 43 | sylanbrc 583 |
. 2
β’ (π β βπ β π βπ β (β€β₯βπ)((πΉβπ) < +β β§ -β < (πΉβπ))) |
45 | 35, 44 | reximddv3 43830 |
1
β’ (π β βπ β π (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) |