Step | Hyp | Ref
| Expression |
1 | | limsupval2.1 |
. . 3
β’ (π β πΉ β π) |
2 | | limsupval.1 |
. . . 4
β’ πΊ = (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
3 | 2 | limsupval 15420 |
. . 3
β’ (πΉ β π β (lim supβπΉ) = inf(ran πΊ, β*, <
)) |
4 | 1, 3 | syl 17 |
. 2
β’ (π β (lim supβπΉ) = inf(ran πΊ, β*, <
)) |
5 | | imassrn 6070 |
. . . . 5
β’ (πΊ β π΄) β ran πΊ |
6 | 2 | limsupgf 15421 |
. . . . . . 7
β’ πΊ:ββΆβ* |
7 | | frn 6724 |
. . . . . . 7
β’ (πΊ:ββΆβ* β
ran πΊ β
β*) |
8 | 6, 7 | ax-mp 5 |
. . . . . 6
β’ ran πΊ β
β* |
9 | | infxrlb 13315 |
. . . . . . 7
β’ ((ran
πΊ β
β* β§ π₯
β ran πΊ) β
inf(ran πΊ,
β*, < ) β€ π₯) |
10 | 9 | ralrimiva 3146 |
. . . . . 6
β’ (ran
πΊ β
β* β βπ₯ β ran πΊinf(ran πΊ, β*, < ) β€ π₯) |
11 | 8, 10 | mp1i 13 |
. . . . 5
β’ (π β βπ₯ β ran πΊinf(ran πΊ, β*, < ) β€ π₯) |
12 | | ssralv 4050 |
. . . . 5
β’ ((πΊ β π΄) β ran πΊ β (βπ₯ β ran πΊinf(ran πΊ, β*, < ) β€ π₯ β βπ₯ β (πΊ β π΄)inf(ran πΊ, β*, < ) β€ π₯)) |
13 | 5, 11, 12 | mpsyl 68 |
. . . 4
β’ (π β βπ₯ β (πΊ β π΄)inf(ran πΊ, β*, < ) β€ π₯) |
14 | 5, 8 | sstri 3991 |
. . . . 5
β’ (πΊ β π΄) β
β* |
15 | | infxrcl 13314 |
. . . . . 6
β’ (ran
πΊ β
β* β inf(ran πΊ, β*, < ) β
β*) |
16 | 8, 15 | ax-mp 5 |
. . . . 5
β’ inf(ran
πΊ, β*,
< ) β β* |
17 | | infxrgelb 13316 |
. . . . 5
β’ (((πΊ β π΄) β β* β§ inf(ran
πΊ, β*,
< ) β β*) β (inf(ran πΊ, β*, < ) β€
inf((πΊ β π΄), β*, < )
β βπ₯ β
(πΊ β π΄)inf(ran πΊ, β*, < ) β€ π₯)) |
18 | 14, 16, 17 | mp2an 690 |
. . . 4
β’ (inf(ran
πΊ, β*,
< ) β€ inf((πΊ β
π΄), β*,
< ) β βπ₯
β (πΊ β π΄)inf(ran πΊ, β*, < ) β€ π₯) |
19 | 13, 18 | sylibr 233 |
. . 3
β’ (π β inf(ran πΊ, β*, < ) β€
inf((πΊ β π΄), β*, <
)) |
20 | | limsupval2.3 |
. . . . . . 7
β’ (π β sup(π΄, β*, < ) =
+β) |
21 | | limsupval2.2 |
. . . . . . . . 9
β’ (π β π΄ β β) |
22 | | ressxr 11260 |
. . . . . . . . 9
β’ β
β β* |
23 | 21, 22 | sstrdi 3994 |
. . . . . . . 8
β’ (π β π΄ β
β*) |
24 | | supxrunb1 13300 |
. . . . . . . 8
β’ (π΄ β β*
β (βπ β
β βπ₯ β
π΄ π β€ π₯ β sup(π΄, β*, < ) =
+β)) |
25 | 23, 24 | syl 17 |
. . . . . . 7
β’ (π β (βπ β β βπ₯ β π΄ π β€ π₯ β sup(π΄, β*, < ) =
+β)) |
26 | 20, 25 | mpbird 256 |
. . . . . 6
β’ (π β βπ β β βπ₯ β π΄ π β€ π₯) |
27 | | infxrcl 13314 |
. . . . . . . . . 10
β’ ((πΊ β π΄) β β* β
inf((πΊ β π΄), β*, < )
β β*) |
28 | 14, 27 | mp1i 13 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ (π₯ β π΄ β§ π β€ π₯)) β inf((πΊ β π΄), β*, < ) β
β*) |
29 | 21 | sselda 3982 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β π₯ β β) |
30 | 29 | ad2ant2r 745 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (π₯ β π΄ β§ π β€ π₯)) β π₯ β β) |
31 | 6 | ffvelcdmi 7085 |
. . . . . . . . . 10
β’ (π₯ β β β (πΊβπ₯) β
β*) |
32 | 30, 31 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ (π₯ β π΄ β§ π β€ π₯)) β (πΊβπ₯) β
β*) |
33 | 6 | ffvelcdmi 7085 |
. . . . . . . . . 10
β’ (π β β β (πΊβπ) β
β*) |
34 | 33 | ad2antlr 725 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ (π₯ β π΄ β§ π β€ π₯)) β (πΊβπ) β
β*) |
35 | | ffn 6717 |
. . . . . . . . . . . 12
β’ (πΊ:ββΆβ* β
πΊ Fn
β) |
36 | 6, 35 | mp1i 13 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ (π₯ β π΄ β§ π β€ π₯)) β πΊ Fn β) |
37 | 21 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ (π₯ β π΄ β§ π β€ π₯)) β π΄ β β) |
38 | | simprl 769 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ (π₯ β π΄ β§ π β€ π₯)) β π₯ β π΄) |
39 | | fnfvima 7237 |
. . . . . . . . . . 11
β’ ((πΊ Fn β β§ π΄ β β β§ π₯ β π΄) β (πΊβπ₯) β (πΊ β π΄)) |
40 | 36, 37, 38, 39 | syl3anc 1371 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (π₯ β π΄ β§ π β€ π₯)) β (πΊβπ₯) β (πΊ β π΄)) |
41 | | infxrlb 13315 |
. . . . . . . . . 10
β’ (((πΊ β π΄) β β* β§ (πΊβπ₯) β (πΊ β π΄)) β inf((πΊ β π΄), β*, < ) β€ (πΊβπ₯)) |
42 | 14, 40, 41 | sylancr 587 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ (π₯ β π΄ β§ π β€ π₯)) β inf((πΊ β π΄), β*, < ) β€ (πΊβπ₯)) |
43 | | simplr 767 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ (π₯ β π΄ β§ π β€ π₯)) β π β β) |
44 | | simprr 771 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ (π₯ β π΄ β§ π β€ π₯)) β π β€ π₯) |
45 | | limsupgord 15418 |
. . . . . . . . . . 11
β’ ((π β β β§ π₯ β β β§ π β€ π₯) β sup(((πΉ β (π₯[,)+β)) β© β*),
β*, < ) β€ sup(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
46 | 43, 30, 44, 45 | syl3anc 1371 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (π₯ β π΄ β§ π β€ π₯)) β sup(((πΉ β (π₯[,)+β)) β© β*),
β*, < ) β€ sup(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
47 | 2 | limsupgval 15422 |
. . . . . . . . . . 11
β’ (π₯ β β β (πΊβπ₯) = sup(((πΉ β (π₯[,)+β)) β© β*),
β*, < )) |
48 | 30, 47 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (π₯ β π΄ β§ π β€ π₯)) β (πΊβπ₯) = sup(((πΉ β (π₯[,)+β)) β© β*),
β*, < )) |
49 | 2 | limsupgval 15422 |
. . . . . . . . . . 11
β’ (π β β β (πΊβπ) = sup(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
50 | 49 | ad2antlr 725 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (π₯ β π΄ β§ π β€ π₯)) β (πΊβπ) = sup(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
51 | 46, 48, 50 | 3brtr4d 5180 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ (π₯ β π΄ β§ π β€ π₯)) β (πΊβπ₯) β€ (πΊβπ)) |
52 | 28, 32, 34, 42, 51 | xrletrd 13143 |
. . . . . . . 8
β’ (((π β§ π β β) β§ (π₯ β π΄ β§ π β€ π₯)) β inf((πΊ β π΄), β*, < ) β€ (πΊβπ)) |
53 | 52 | rexlimdvaa 3156 |
. . . . . . 7
β’ ((π β§ π β β) β (βπ₯ β π΄ π β€ π₯ β inf((πΊ β π΄), β*, < ) β€ (πΊβπ))) |
54 | 53 | ralimdva 3167 |
. . . . . 6
β’ (π β (βπ β β βπ₯ β π΄ π β€ π₯ β βπ β β inf((πΊ β π΄), β*, < ) β€ (πΊβπ))) |
55 | 26, 54 | mpd 15 |
. . . . 5
β’ (π β βπ β β inf((πΊ β π΄), β*, < ) β€ (πΊβπ)) |
56 | 6, 35 | ax-mp 5 |
. . . . . 6
β’ πΊ Fn β |
57 | | breq2 5152 |
. . . . . . 7
β’ (π₯ = (πΊβπ) β (inf((πΊ β π΄), β*, < ) β€ π₯ β inf((πΊ β π΄), β*, < ) β€ (πΊβπ))) |
58 | 57 | ralrn 7089 |
. . . . . 6
β’ (πΊ Fn β β
(βπ₯ β ran πΊinf((πΊ β π΄), β*, < ) β€ π₯ β βπ β β inf((πΊ β π΄), β*, < ) β€ (πΊβπ))) |
59 | 56, 58 | ax-mp 5 |
. . . . 5
β’
(βπ₯ β
ran πΊinf((πΊ β π΄), β*, < ) β€ π₯ β βπ β β inf((πΊ β π΄), β*, < ) β€ (πΊβπ)) |
60 | 55, 59 | sylibr 233 |
. . . 4
β’ (π β βπ₯ β ran πΊinf((πΊ β π΄), β*, < ) β€ π₯) |
61 | 14, 27 | ax-mp 5 |
. . . . 5
β’
inf((πΊ β π΄), β*, < )
β β* |
62 | | infxrgelb 13316 |
. . . . 5
β’ ((ran
πΊ β
β* β§ inf((πΊ β π΄), β*, < ) β
β*) β (inf((πΊ β π΄), β*, < ) β€ inf(ran
πΊ, β*,
< ) β βπ₯
β ran πΊinf((πΊ β π΄), β*, < ) β€ π₯)) |
63 | 8, 61, 62 | mp2an 690 |
. . . 4
β’
(inf((πΊ β
π΄), β*,
< ) β€ inf(ran πΊ,
β*, < ) β βπ₯ β ran πΊinf((πΊ β π΄), β*, < ) β€ π₯) |
64 | 60, 63 | sylibr 233 |
. . 3
β’ (π β inf((πΊ β π΄), β*, < ) β€ inf(ran
πΊ, β*,
< )) |
65 | | xrletri3 13135 |
. . . 4
β’ ((inf(ran
πΊ, β*,
< ) β β* β§ inf((πΊ β π΄), β*, < ) β
β*) β (inf(ran πΊ, β*, < ) = inf((πΊ β π΄), β*, < ) β
(inf(ran πΊ,
β*, < ) β€ inf((πΊ β π΄), β*, < ) β§
inf((πΊ β π΄), β*, < )
β€ inf(ran πΊ,
β*, < )))) |
66 | 16, 61, 65 | mp2an 690 |
. . 3
β’ (inf(ran
πΊ, β*,
< ) = inf((πΊ β
π΄), β*,
< ) β (inf(ran πΊ,
β*, < ) β€ inf((πΊ β π΄), β*, < ) β§
inf((πΊ β π΄), β*, < )
β€ inf(ran πΊ,
β*, < ))) |
67 | 19, 64, 66 | sylanbrc 583 |
. 2
β’ (π β inf(ran πΊ, β*, < ) = inf((πΊ β π΄), β*, <
)) |
68 | 4, 67 | eqtrd 2772 |
1
β’ (π β (lim supβπΉ) = inf((πΊ β π΄), β*, <
)) |