Step | Hyp | Ref
| Expression |
1 | | liminfresico.1 |
. . . . . . . . . . . . . 14
β’ (π β π β β) |
2 | 1 | rexrd 11210 |
. . . . . . . . . . . . 13
β’ (π β π β
β*) |
3 | 2 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π¦ β (π[,)+β)) β π β
β*) |
4 | | pnfxr 11214 |
. . . . . . . . . . . . 13
β’ +β
β β* |
5 | 4 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π¦ β (π[,)+β)) β +β β
β*) |
6 | | ressxr 11204 |
. . . . . . . . . . . . 13
β’ β
β β* |
7 | 4 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π β +β β
β*) |
8 | | icossre 13351 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ +β
β β*) β (π[,)+β) β
β) |
9 | 1, 7, 8 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π[,)+β) β
β) |
10 | 9 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π) β (π[,)+β) β
β) |
11 | | liminfresico.2 |
. . . . . . . . . . . . . . . . . . 19
β’ π = (π[,)+β) |
12 | 11 | eleq2i 2826 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β π β (π[,)+β)) |
13 | 12 | biimpi 215 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β π β (π[,)+β)) |
14 | 13 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π) β π β (π[,)+β)) |
15 | 10, 14 | sseldd 3946 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π) β π β β) |
16 | 15 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π) β§ π¦ β (π[,)+β)) β π β β) |
17 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π) β§ π¦ β (π[,)+β)) β π¦ β (π[,)+β)) |
18 | | elicore 13322 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π¦ β (π[,)+β)) β π¦ β β) |
19 | 16, 17, 18 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π¦ β (π[,)+β)) β π¦ β β) |
20 | 6, 19 | sselid 3943 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π¦ β (π[,)+β)) β π¦ β β*) |
21 | 1 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π¦ β (π[,)+β)) β π β β) |
22 | 2 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π) β π β
β*) |
23 | 4 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π) β +β β
β*) |
24 | 22, 23, 14 | icogelbd 43882 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π) β π β€ π) |
25 | 24 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π¦ β (π[,)+β)) β π β€ π) |
26 | 6, 16 | sselid 3943 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π) β§ π¦ β (π[,)+β)) β π β β*) |
27 | 26, 5, 17 | icogelbd 43882 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π¦ β (π[,)+β)) β π β€ π¦) |
28 | 21, 16, 19, 25, 27 | letrd 11317 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π¦ β (π[,)+β)) β π β€ π¦) |
29 | 19 | ltpnfd 13047 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π¦ β (π[,)+β)) β π¦ < +β) |
30 | 3, 5, 20, 28, 29 | elicod 13320 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π¦ β (π[,)+β)) β π¦ β (π[,)+β)) |
31 | 30, 11 | eleqtrrdi 2845 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π¦ β (π[,)+β)) β π¦ β π) |
32 | 31 | ssd 43378 |
. . . . . . . . 9
β’ ((π β§ π β π) β (π[,)+β) β π) |
33 | | resima2 5973 |
. . . . . . . . 9
β’ ((π[,)+β) β π β ((πΉ βΎ π) β (π[,)+β)) = (πΉ β (π[,)+β))) |
34 | 32, 33 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β π) β ((πΉ βΎ π) β (π[,)+β)) = (πΉ β (π[,)+β))) |
35 | 34 | ineq1d 4172 |
. . . . . . 7
β’ ((π β§ π β π) β (((πΉ βΎ π) β (π[,)+β)) β© β*) =
((πΉ β (π[,)+β)) β©
β*)) |
36 | 35 | infeq1d 9418 |
. . . . . 6
β’ ((π β§ π β π) β inf((((πΉ βΎ π) β (π[,)+β)) β© β*),
β*, < ) = inf(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
37 | 36 | mpteq2dva 5206 |
. . . . 5
β’ (π β (π β π β¦ inf((((πΉ βΎ π) β (π[,)+β)) β© β*),
β*, < )) = (π β π β¦ inf(((πΉ β (π[,)+β)) β© β*),
β*, < ))) |
38 | 37 | rneqd 5894 |
. . . 4
β’ (π β ran (π β π β¦ inf((((πΉ βΎ π) β (π[,)+β)) β© β*),
β*, < )) = ran (π β π β¦ inf(((πΉ β (π[,)+β)) β© β*),
β*, < ))) |
39 | 11, 9 | eqsstrid 3993 |
. . . . 5
β’ (π β π β β) |
40 | 39 | mptima2 43560 |
. . . 4
β’ (π β ((π β β β¦ inf((((πΉ βΎ π) β (π[,)+β)) β© β*),
β*, < )) β π) = ran (π β π β¦ inf((((πΉ βΎ π) β (π[,)+β)) β© β*),
β*, < ))) |
41 | 39 | mptima2 43560 |
. . . 4
β’ (π β ((π β β β¦ inf(((πΉ β (π[,)+β)) β© β*),
β*, < )) β π) = ran (π β π β¦ inf(((πΉ β (π[,)+β)) β© β*),
β*, < ))) |
42 | 38, 40, 41 | 3eqtr4d 2783 |
. . 3
β’ (π β ((π β β β¦ inf((((πΉ βΎ π) β (π[,)+β)) β© β*),
β*, < )) β π) = ((π β β β¦ inf(((πΉ β (π[,)+β)) β© β*),
β*, < )) β π)) |
43 | 42 | supeq1d 9387 |
. 2
β’ (π β sup(((π β β β¦ inf((((πΉ βΎ π) β (π[,)+β)) β© β*),
β*, < )) β π), β*, < ) = sup(((π β β β¦
inf(((πΉ β (π[,)+β)) β©
β*), β*, < )) β π), β*, <
)) |
44 | | eqid 2733 |
. . 3
β’ (π β β β¦
inf((((πΉ βΎ π) β (π[,)+β)) β© β*),
β*, < )) = (π β β β¦ inf((((πΉ βΎ π) β (π[,)+β)) β© β*),
β*, < )) |
45 | | liminfresico.3 |
. . . 4
β’ (π β πΉ β π) |
46 | 45 | resexd 5985 |
. . 3
β’ (π β (πΉ βΎ π) β V) |
47 | 11 | supeq1i 9388 |
. . . . 5
β’ sup(π, β*, < ) =
sup((π[,)+β),
β*, < ) |
48 | 47 | a1i 11 |
. . . 4
β’ (π β sup(π, β*, < ) = sup((π[,)+β),
β*, < )) |
49 | 1 | renepnfd 11211 |
. . . . 5
β’ (π β π β +β) |
50 | | icopnfsup 13776 |
. . . . 5
β’ ((π β β*
β§ π β +β)
β sup((π[,)+β),
β*, < ) = +β) |
51 | 2, 49, 50 | syl2anc 585 |
. . . 4
β’ (π β sup((π[,)+β), β*, < ) =
+β) |
52 | 48, 51 | eqtrd 2773 |
. . 3
β’ (π β sup(π, β*, < ) =
+β) |
53 | 44, 46, 39, 52 | liminfval2 44095 |
. 2
β’ (π β (lim infβ(πΉ βΎ π)) = sup(((π β β β¦ inf((((πΉ βΎ π) β (π[,)+β)) β© β*),
β*, < )) β π), β*, <
)) |
54 | | eqid 2733 |
. . 3
β’ (π β β β¦
inf(((πΉ β (π[,)+β)) β©
β*), β*, < )) = (π β β β¦ inf(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
55 | 54, 45, 39, 52 | liminfval2 44095 |
. 2
β’ (π β (lim infβπΉ) = sup(((π β β β¦ inf(((πΉ β (π[,)+β)) β© β*),
β*, < )) β π), β*, <
)) |
56 | 43, 53, 55 | 3eqtr4d 2783 |
1
β’ (π β (lim infβ(πΉ βΎ π)) = (lim infβπΉ)) |