Step | Hyp | Ref
| Expression |
1 | | smfliminflem.g |
. . . 4
β’ πΊ = (π₯ β π· β¦ (lim infβ(π β π β¦ ((πΉβπ)βπ₯)))) |
2 | 1 | a1i 11 |
. . 3
β’ (π β πΊ = (π₯ β π· β¦ (lim infβ(π β π β¦ ((πΉβπ)βπ₯))))) |
3 | | smfliminflem.d |
. . . . . . . . . 10
β’ π· = {π₯ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (lim infβ(π β π β¦ ((πΉβπ)βπ₯))) β β} |
4 | | ssrab2 4041 |
. . . . . . . . . 10
β’ {π₯ β βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (lim infβ(π β π β¦ ((πΉβπ)βπ₯))) β β} β βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) |
5 | 3, 4 | eqsstri 3982 |
. . . . . . . . 9
β’ π· β βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) |
6 | | id 22 |
. . . . . . . . 9
β’ (π₯ β π· β π₯ β π·) |
7 | 5, 6 | sselid 3946 |
. . . . . . . 8
β’ (π₯ β π· β π₯ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ)) |
8 | | smfliminflem.z |
. . . . . . . . 9
β’ π =
(β€β₯βπ) |
9 | | eqid 2733 |
. . . . . . . . 9
β’ βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) = βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) |
10 | 8, 9 | allbutfi 43718 |
. . . . . . . 8
β’ (π₯ β βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) β βπ β π βπ β (β€β₯βπ)π₯ β dom (πΉβπ)) |
11 | 7, 10 | sylib 217 |
. . . . . . 7
β’ (π₯ β π· β βπ β π βπ β (β€β₯βπ)π₯ β dom (πΉβπ)) |
12 | 11 | adantl 483 |
. . . . . 6
β’ ((π β§ π₯ β π·) β βπ β π βπ β (β€β₯βπ)π₯ β dom (πΉβπ)) |
13 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π(π β§ π β π) |
14 | | nfra1 3266 |
. . . . . . . . . 10
β’
β²πβπ β (β€β₯βπ)π₯ β dom (πΉβπ) |
15 | 13, 14 | nfan 1903 |
. . . . . . . . 9
β’
β²π((π β§ π β π) β§ βπ β (β€β₯βπ)π₯ β dom (πΉβπ)) |
16 | 8 | fvexi 6860 |
. . . . . . . . . 10
β’ π β V |
17 | 16 | a1i 11 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ βπ β (β€β₯βπ)π₯ β dom (πΉβπ)) β π β V) |
18 | 8 | eluzelz2 43728 |
. . . . . . . . . . 11
β’ (π β π β π β β€) |
19 | 18 | zred 12615 |
. . . . . . . . . 10
β’ (π β π β π β β) |
20 | 19 | ad2antlr 726 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ βπ β (β€β₯βπ)π₯ β dom (πΉβπ)) β π β β) |
21 | | simpll 766 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ βπ β (β€β₯βπ)π₯ β dom (πΉβπ)) β π) |
22 | | elinel1 4159 |
. . . . . . . . . . 11
β’ (π β (π β© (π[,)+β)) β π β π) |
23 | | smfliminflem.s |
. . . . . . . . . . . . 13
β’ (π β π β SAlg) |
24 | 23 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β π β SAlg) |
25 | | smfliminflem.f |
. . . . . . . . . . . . 13
β’ (π β πΉ:πβΆ(SMblFnβπ)) |
26 | 25 | ffvelcdmda 7039 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (πΉβπ) β (SMblFnβπ)) |
27 | | eqid 2733 |
. . . . . . . . . . . 12
β’ dom
(πΉβπ) = dom (πΉβπ) |
28 | 24, 26, 27 | smff 45063 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (πΉβπ):dom (πΉβπ)βΆβ) |
29 | 21, 22, 28 | syl2an 597 |
. . . . . . . . . 10
β’ ((((π β§ π β π) β§ βπ β (β€β₯βπ)π₯ β dom (πΉβπ)) β§ π β (π β© (π[,)+β))) β (πΉβπ):dom (πΉβπ)βΆβ) |
30 | | simplr 768 |
. . . . . . . . . . . 12
β’ (((π β π β§ βπ β (β€β₯βπ)π₯ β dom (πΉβπ)) β§ π β (π β© (π[,)+β))) β βπ β
(β€β₯βπ)π₯ β dom (πΉβπ)) |
31 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(β€β₯βπ) = (β€β₯βπ) |
32 | 18 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ π β (π β© (π[,)+β))) β π β β€) |
33 | 8, 22 | eluzelz2d 43738 |
. . . . . . . . . . . . . . 15
β’ (π β (π β© (π[,)+β)) β π β β€) |
34 | 33 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ π β (π β© (π[,)+β))) β π β β€) |
35 | 19 | rexrd 11213 |
. . . . . . . . . . . . . . . 16
β’ (π β π β π β β*) |
36 | 35 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β π β§ π β (π β© (π[,)+β))) β π β β*) |
37 | | pnfxr 11217 |
. . . . . . . . . . . . . . . 16
β’ +β
β β* |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β π β§ π β (π β© (π[,)+β))) β +β β
β*) |
39 | | elinel2 4160 |
. . . . . . . . . . . . . . . 16
β’ (π β (π β© (π[,)+β)) β π β (π[,)+β)) |
40 | 39 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β π β§ π β (π β© (π[,)+β))) β π β (π[,)+β)) |
41 | 36, 38, 40 | icogelbd 43886 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ π β (π β© (π[,)+β))) β π β€ π) |
42 | 31, 32, 34, 41 | eluzd 43734 |
. . . . . . . . . . . . 13
β’ ((π β π β§ π β (π β© (π[,)+β))) β π β (β€β₯βπ)) |
43 | 42 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β π β§ βπ β (β€β₯βπ)π₯ β dom (πΉβπ)) β§ π β (π β© (π[,)+β))) β π β (β€β₯βπ)) |
44 | | rspa 3230 |
. . . . . . . . . . . 12
β’
((βπ β
(β€β₯βπ)π₯ β dom (πΉβπ) β§ π β (β€β₯βπ)) β π₯ β dom (πΉβπ)) |
45 | 30, 43, 44 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β π β§ βπ β (β€β₯βπ)π₯ β dom (πΉβπ)) β§ π β (π β© (π[,)+β))) β π₯ β dom (πΉβπ)) |
46 | 45 | adantlll 717 |
. . . . . . . . . 10
β’ ((((π β§ π β π) β§ βπ β (β€β₯βπ)π₯ β dom (πΉβπ)) β§ π β (π β© (π[,)+β))) β π₯ β dom (πΉβπ)) |
47 | 29, 46 | ffvelcdmd 7040 |
. . . . . . . . 9
β’ ((((π β§ π β π) β§ βπ β (β€β₯βπ)π₯ β dom (πΉβπ)) β§ π β (π β© (π[,)+β))) β ((πΉβπ)βπ₯) β β) |
48 | 15, 17, 20, 47 | liminfval4 44120 |
. . . . . . . 8
β’ (((π β§ π β π) β§ βπ β (β€β₯βπ)π₯ β dom (πΉβπ)) β (lim infβ(π β π β¦ ((πΉβπ)βπ₯))) = -π(lim
supβ(π β π β¦ -((πΉβπ)βπ₯)))) |
49 | 48 | rexlimdva2 3151 |
. . . . . . 7
β’ (π β (βπ β π βπ β (β€β₯βπ)π₯ β dom (πΉβπ) β (lim infβ(π β π β¦ ((πΉβπ)βπ₯))) = -π(lim
supβ(π β π β¦ -((πΉβπ)βπ₯))))) |
50 | 49 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β π·) β (βπ β π βπ β (β€β₯βπ)π₯ β dom (πΉβπ) β (lim infβ(π β π β¦ ((πΉβπ)βπ₯))) = -π(lim
supβ(π β π β¦ -((πΉβπ)βπ₯))))) |
51 | 12, 50 | mpd 15 |
. . . . 5
β’ ((π β§ π₯ β π·) β (lim infβ(π β π β¦ ((πΉβπ)βπ₯))) = -π(lim
supβ(π β π β¦ -((πΉβπ)βπ₯)))) |
52 | 51 | xnegeqd 43762 |
. . . . . . . . 9
β’ ((π β§ π₯ β π·) β -π(lim
infβ(π β π β¦ ((πΉβπ)βπ₯))) =
-π-π(lim supβ(π β π β¦ -((πΉβπ)βπ₯)))) |
53 | 16 | mptex 7177 |
. . . . . . . . . . . 12
β’ (π β π β¦ -((πΉβπ)βπ₯)) β V |
54 | 53 | limsupcli 44088 |
. . . . . . . . . . 11
β’ (lim
supβ(π β π β¦ -((πΉβπ)βπ₯))) β
β* |
55 | 54 | xnegnegi 43764 |
. . . . . . . . . 10
β’
-π-π(lim supβ(π β π β¦ -((πΉβπ)βπ₯))) = (lim supβ(π β π β¦ -((πΉβπ)βπ₯))) |
56 | 55 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π₯ β π·) β
-π-π(lim supβ(π β π β¦ -((πΉβπ)βπ₯))) = (lim supβ(π β π β¦ -((πΉβπ)βπ₯)))) |
57 | 52, 56 | eqtr2d 2774 |
. . . . . . . 8
β’ ((π β§ π₯ β π·) β (lim supβ(π β π β¦ -((πΉβπ)βπ₯))) = -π(lim
infβ(π β π β¦ ((πΉβπ)βπ₯)))) |
58 | 3 | reqabi 3428 |
. . . . . . . . . . 11
β’ (π₯ β π· β (π₯ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ) β§ (lim infβ(π β π β¦ ((πΉβπ)βπ₯))) β β)) |
59 | 58 | simprbi 498 |
. . . . . . . . . 10
β’ (π₯ β π· β (lim infβ(π β π β¦ ((πΉβπ)βπ₯))) β β) |
60 | 59 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π₯ β π·) β (lim infβ(π β π β¦ ((πΉβπ)βπ₯))) β β) |
61 | 60 | rexnegd 43445 |
. . . . . . . 8
β’ ((π β§ π₯ β π·) β -π(lim
infβ(π β π β¦ ((πΉβπ)βπ₯))) = -(lim infβ(π β π β¦ ((πΉβπ)βπ₯)))) |
62 | 57, 61 | eqtr2d 2774 |
. . . . . . 7
β’ ((π β§ π₯ β π·) β -(lim infβ(π β π β¦ ((πΉβπ)βπ₯))) = (lim supβ(π β π β¦ -((πΉβπ)βπ₯)))) |
63 | 60 | renegcld 11590 |
. . . . . . 7
β’ ((π β§ π₯ β π·) β -(lim infβ(π β π β¦ ((πΉβπ)βπ₯))) β β) |
64 | 62, 63 | eqeltrrd 2835 |
. . . . . 6
β’ ((π β§ π₯ β π·) β (lim supβ(π β π β¦ -((πΉβπ)βπ₯))) β β) |
65 | 64 | rexnegd 43445 |
. . . . 5
β’ ((π β§ π₯ β π·) β -π(lim
supβ(π β π β¦ -((πΉβπ)βπ₯))) = -(lim supβ(π β π β¦ -((πΉβπ)βπ₯)))) |
66 | 51, 65 | eqtrd 2773 |
. . . 4
β’ ((π β§ π₯ β π·) β (lim infβ(π β π β¦ ((πΉβπ)βπ₯))) = -(lim supβ(π β π β¦ -((πΉβπ)βπ₯)))) |
67 | 66 | mpteq2dva 5209 |
. . 3
β’ (π β (π₯ β π· β¦ (lim infβ(π β π β¦ ((πΉβπ)βπ₯)))) = (π₯ β π· β¦ -(lim supβ(π β π β¦ -((πΉβπ)βπ₯))))) |
68 | 2, 67 | eqtrd 2773 |
. 2
β’ (π β πΊ = (π₯ β π· β¦ -(lim supβ(π β π β¦ -((πΉβπ)βπ₯))))) |
69 | | nfv 1918 |
. . 3
β’
β²π₯π |
70 | 18, 31 | uzn0d 43750 |
. . . . . . . 8
β’ (π β π β (β€β₯βπ) β β
) |
71 | | fvex 6859 |
. . . . . . . . . . 11
β’ (πΉβπ) β V |
72 | 71 | dmex 7852 |
. . . . . . . . . 10
β’ dom
(πΉβπ) β V |
73 | 72 | rgenw 3065 |
. . . . . . . . 9
β’
βπ β
(β€β₯βπ)dom (πΉβπ) β V |
74 | 73 | a1i 11 |
. . . . . . . 8
β’ (π β π β βπ β (β€β₯βπ)dom (πΉβπ) β V) |
75 | | iinexg 5302 |
. . . . . . . 8
β’
(((β€β₯βπ) β β
β§ βπ β
(β€β₯βπ)dom (πΉβπ) β V) β β© π β (β€β₯βπ)dom (πΉβπ) β V) |
76 | 70, 74, 75 | syl2anc 585 |
. . . . . . 7
β’ (π β π β β©
π β
(β€β₯βπ)dom (πΉβπ) β V) |
77 | 76 | rgen 3063 |
. . . . . 6
β’
βπ β
π β© π β (β€β₯βπ)dom (πΉβπ) β V |
78 | | iunexg 7900 |
. . . . . 6
β’ ((π β V β§ βπ β π β© π β
(β€β₯βπ)dom (πΉβπ) β V) β βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) β V) |
79 | 16, 77, 78 | mp2an 691 |
. . . . 5
β’ βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) β V |
80 | 79, 5 | ssexi 5283 |
. . . 4
β’ π· β V |
81 | 80 | a1i 11 |
. . 3
β’ (π β π· β V) |
82 | 3 | a1i 11 |
. . . . . 6
β’ (π β π· = {π₯ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (lim infβ(π β π β¦ ((πΉβπ)βπ₯))) β β}) |
83 | 10 | biimpi 215 |
. . . . . . . . 9
β’ (π₯ β βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) β βπ β π βπ β (β€β₯βπ)π₯ β dom (πΉβπ)) |
84 | 49 | imp 408 |
. . . . . . . . 9
β’ ((π β§ βπ β π βπ β (β€β₯βπ)π₯ β dom (πΉβπ)) β (lim infβ(π β π β¦ ((πΉβπ)βπ₯))) = -π(lim
supβ(π β π β¦ -((πΉβπ)βπ₯)))) |
85 | 83, 84 | sylan2 594 |
. . . . . . . 8
β’ ((π β§ π₯ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ)) β (lim infβ(π β π β¦ ((πΉβπ)βπ₯))) = -π(lim
supβ(π β π β¦ -((πΉβπ)βπ₯)))) |
86 | 54 | a1i 11 |
. . . . . . . . . 10
β’ (((lim
infβ(π β π β¦ ((πΉβπ)βπ₯))) = -π(lim
supβ(π β π β¦ -((πΉβπ)βπ₯))) β§ (lim infβ(π β π β¦ ((πΉβπ)βπ₯))) β β) β (lim
supβ(π β π β¦ -((πΉβπ)βπ₯))) β
β*) |
87 | | simpl 484 |
. . . . . . . . . . 11
β’ (((lim
infβ(π β π β¦ ((πΉβπ)βπ₯))) = -π(lim
supβ(π β π β¦ -((πΉβπ)βπ₯))) β§ (lim infβ(π β π β¦ ((πΉβπ)βπ₯))) β β) β (lim
infβ(π β π β¦ ((πΉβπ)βπ₯))) = -π(lim
supβ(π β π β¦ -((πΉβπ)βπ₯)))) |
88 | | simpr 486 |
. . . . . . . . . . 11
β’ (((lim
infβ(π β π β¦ ((πΉβπ)βπ₯))) = -π(lim
supβ(π β π β¦ -((πΉβπ)βπ₯))) β§ (lim infβ(π β π β¦ ((πΉβπ)βπ₯))) β β) β (lim
infβ(π β π β¦ ((πΉβπ)βπ₯))) β β) |
89 | 87, 88 | eqeltrrd 2835 |
. . . . . . . . . 10
β’ (((lim
infβ(π β π β¦ ((πΉβπ)βπ₯))) = -π(lim
supβ(π β π β¦ -((πΉβπ)βπ₯))) β§ (lim infβ(π β π β¦ ((πΉβπ)βπ₯))) β β) β
-π(lim supβ(π β π β¦ -((πΉβπ)βπ₯))) β β) |
90 | | xnegrecl2 43785 |
. . . . . . . . . 10
β’ (((lim
supβ(π β π β¦ -((πΉβπ)βπ₯))) β β* β§
-π(lim supβ(π β π β¦ -((πΉβπ)βπ₯))) β β) β (lim
supβ(π β π β¦ -((πΉβπ)βπ₯))) β β) |
91 | 86, 89, 90 | syl2anc 585 |
. . . . . . . . 9
β’ (((lim
infβ(π β π β¦ ((πΉβπ)βπ₯))) = -π(lim
supβ(π β π β¦ -((πΉβπ)βπ₯))) β§ (lim infβ(π β π β¦ ((πΉβπ)βπ₯))) β β) β (lim
supβ(π β π β¦ -((πΉβπ)βπ₯))) β β) |
92 | | simpl 484 |
. . . . . . . . . 10
β’ (((lim
infβ(π β π β¦ ((πΉβπ)βπ₯))) = -π(lim
supβ(π β π β¦ -((πΉβπ)βπ₯))) β§ (lim supβ(π β π β¦ -((πΉβπ)βπ₯))) β β) β (lim
infβ(π β π β¦ ((πΉβπ)βπ₯))) = -π(lim
supβ(π β π β¦ -((πΉβπ)βπ₯)))) |
93 | | xnegrecl 43763 |
. . . . . . . . . . 11
β’ ((lim
supβ(π β π β¦ -((πΉβπ)βπ₯))) β β β
-π(lim supβ(π β π β¦ -((πΉβπ)βπ₯))) β β) |
94 | 93 | adantl 483 |
. . . . . . . . . 10
β’ (((lim
infβ(π β π β¦ ((πΉβπ)βπ₯))) = -π(lim
supβ(π β π β¦ -((πΉβπ)βπ₯))) β§ (lim supβ(π β π β¦ -((πΉβπ)βπ₯))) β β) β
-π(lim supβ(π β π β¦ -((πΉβπ)βπ₯))) β β) |
95 | 92, 94 | eqeltrd 2834 |
. . . . . . . . 9
β’ (((lim
infβ(π β π β¦ ((πΉβπ)βπ₯))) = -π(lim
supβ(π β π β¦ -((πΉβπ)βπ₯))) β§ (lim supβ(π β π β¦ -((πΉβπ)βπ₯))) β β) β (lim
infβ(π β π β¦ ((πΉβπ)βπ₯))) β β) |
96 | 91, 95 | impbida 800 |
. . . . . . . 8
β’ ((lim
infβ(π β π β¦ ((πΉβπ)βπ₯))) = -π(lim
supβ(π β π β¦ -((πΉβπ)βπ₯))) β ((lim infβ(π β π β¦ ((πΉβπ)βπ₯))) β β β (lim
supβ(π β π β¦ -((πΉβπ)βπ₯))) β β)) |
97 | 85, 96 | syl 17 |
. . . . . . 7
β’ ((π β§ π₯ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ)) β ((lim infβ(π β π β¦ ((πΉβπ)βπ₯))) β β β (lim
supβ(π β π β¦ -((πΉβπ)βπ₯))) β β)) |
98 | 97 | rabbidva 3413 |
. . . . . 6
β’ (π β {π₯ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (lim infβ(π β π β¦ ((πΉβπ)βπ₯))) β β} = {π₯ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (lim supβ(π β π β¦ -((πΉβπ)βπ₯))) β β}) |
99 | 82, 98 | eqtrd 2773 |
. . . . 5
β’ (π β π· = {π₯ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (lim supβ(π β π β¦ -((πΉβπ)βπ₯))) β β}) |
100 | 69, 99 | mpteq1df 43552 |
. . . 4
β’ (π β (π₯ β π· β¦ (lim supβ(π β π β¦ -((πΉβπ)βπ₯)))) = (π₯ β {π₯ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (lim supβ(π β π β¦ -((πΉβπ)βπ₯))) β β} β¦ (lim
supβ(π β π β¦ -((πΉβπ)βπ₯))))) |
101 | | nfv 1918 |
. . . . 5
β’
β²ππ |
102 | | nfv 1918 |
. . . . 5
β’
β²ππ |
103 | | smfliminflem.m |
. . . . 5
β’ (π β π β β€) |
104 | | negex 11407 |
. . . . . 6
β’ -((πΉβπ)βπ₯) β V |
105 | 104 | a1i 11 |
. . . . 5
β’ ((π β§ π β π β§ π₯ β dom (πΉβπ)) β -((πΉβπ)βπ₯) β V) |
106 | | nfv 1918 |
. . . . . 6
β’
β²π₯(π β§ π β π) |
107 | 72 | a1i 11 |
. . . . . 6
β’ ((π β§ π β π) β dom (πΉβπ) β V) |
108 | 28 | ffvelcdmda 7039 |
. . . . . 6
β’ (((π β§ π β π) β§ π₯ β dom (πΉβπ)) β ((πΉβπ)βπ₯) β β) |
109 | 28 | feqmptd 6914 |
. . . . . . 7
β’ ((π β§ π β π) β (πΉβπ) = (π₯ β dom (πΉβπ) β¦ ((πΉβπ)βπ₯))) |
110 | 109, 26 | eqeltrrd 2835 |
. . . . . 6
β’ ((π β§ π β π) β (π₯ β dom (πΉβπ) β¦ ((πΉβπ)βπ₯)) β (SMblFnβπ)) |
111 | 106, 24, 107, 108, 110 | smfneg 45134 |
. . . . 5
β’ ((π β§ π β π) β (π₯ β dom (πΉβπ) β¦ -((πΉβπ)βπ₯)) β (SMblFnβπ)) |
112 | | eqid 2733 |
. . . . 5
β’ {π₯ β βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (lim supβ(π β π β¦ -((πΉβπ)βπ₯))) β β} = {π₯ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (lim supβ(π β π β¦ -((πΉβπ)βπ₯))) β β} |
113 | | eqid 2733 |
. . . . 5
β’ (π₯ β {π₯ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (lim supβ(π β π β¦ -((πΉβπ)βπ₯))) β β} β¦ (lim
supβ(π β π β¦ -((πΉβπ)βπ₯)))) = (π₯ β {π₯ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (lim supβ(π β π β¦ -((πΉβπ)βπ₯))) β β} β¦ (lim
supβ(π β π β¦ -((πΉβπ)βπ₯)))) |
114 | 101, 69, 102, 103, 8, 23, 105, 111, 112, 113 | smflimsupmpt 45160 |
. . . 4
β’ (π β (π₯ β {π₯ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (lim supβ(π β π β¦ -((πΉβπ)βπ₯))) β β} β¦ (lim
supβ(π β π β¦ -((πΉβπ)βπ₯)))) β (SMblFnβπ)) |
115 | 100, 114 | eqeltrd 2834 |
. . 3
β’ (π β (π₯ β π· β¦ (lim supβ(π β π β¦ -((πΉβπ)βπ₯)))) β (SMblFnβπ)) |
116 | 69, 23, 81, 64, 115 | smfneg 45134 |
. 2
β’ (π β (π₯ β π· β¦ -(lim supβ(π β π β¦ -((πΉβπ)βπ₯)))) β (SMblFnβπ)) |
117 | 68, 116 | eqeltrd 2834 |
1
β’ (π β πΊ β (SMblFnβπ)) |