Step | Hyp | Ref
| Expression |
1 | | nfv 1918 |
. . . . 5
β’
β²ππ |
2 | | nfcv 2904 |
. . . . 5
β’
β²ππΉ |
3 | | liminfpnfuz.2 |
. . . . 5
β’ (π β π β β€) |
4 | | liminfpnfuz.3 |
. . . . 5
β’ π =
(β€β₯βπ) |
5 | | liminfpnfuz.4 |
. . . . 5
β’ (π β πΉ:πβΆβ*) |
6 | 1, 2, 3, 4, 5 | liminfvaluz3 44123 |
. . . 4
β’ (π β (lim infβπΉ) = -π(lim
supβ(π β π β¦
-π(πΉβπ)))) |
7 | | liminfpnfuz.1 |
. . . . . . . . 9
β’
β²ππΉ |
8 | | nfcv 2904 |
. . . . . . . . 9
β’
β²ππ |
9 | 7, 8 | nffv 6853 |
. . . . . . . 8
β’
β²π(πΉβπ) |
10 | 9 | nfxneg 43782 |
. . . . . . 7
β’
β²π-π(πΉβπ) |
11 | | nfcv 2904 |
. . . . . . 7
β’
β²π-π(πΉβπ) |
12 | | fveq2 6843 |
. . . . . . . 8
β’ (π = π β (πΉβπ) = (πΉβπ)) |
13 | 12 | xnegeqd 43758 |
. . . . . . 7
β’ (π = π β -π(πΉβπ) = -π(πΉβπ)) |
14 | 10, 11, 13 | cbvmpt 5217 |
. . . . . 6
β’ (π β π β¦ -π(πΉβπ)) = (π β π β¦ -π(πΉβπ)) |
15 | 14 | fveq2i 6846 |
. . . . 5
β’ (lim
supβ(π β π β¦
-π(πΉβπ))) = (lim supβ(π β π β¦ -π(πΉβπ))) |
16 | 15 | xnegeqi 43761 |
. . . 4
β’
-π(lim supβ(π β π β¦ -π(πΉβπ))) = -π(lim
supβ(π β π β¦
-π(πΉβπ))) |
17 | 6, 16 | eqtrdi 2789 |
. . 3
β’ (π β (lim infβπΉ) = -π(lim
supβ(π β π β¦
-π(πΉβπ)))) |
18 | 17 | eqeq1d 2735 |
. 2
β’ (π β ((lim infβπΉ) = +β β
-π(lim supβ(π β π β¦ -π(πΉβπ))) = +β)) |
19 | | xnegmnf 13135 |
. . . . . 6
β’
-π-β = +β |
20 | 19 | eqcomi 2742 |
. . . . 5
β’ +β
= -π-β |
21 | 20 | a1i 11 |
. . . 4
β’ (π β +β =
-π-β) |
22 | 21 | eqeq2d 2744 |
. . 3
β’ (π β (-π(lim
supβ(π β π β¦
-π(πΉβπ))) = +β β
-π(lim supβ(π β π β¦ -π(πΉβπ))) =
-π-β)) |
23 | 4 | fvexi 6857 |
. . . . . . 7
β’ π β V |
24 | 23 | mptex 7174 |
. . . . . 6
β’ (π β π β¦ -π(πΉβπ)) β V |
25 | 24 | a1i 11 |
. . . . 5
β’ (π β (π β π β¦ -π(πΉβπ)) β V) |
26 | 25 | limsupcld 44017 |
. . . 4
β’ (π β (lim supβ(π β π β¦ -π(πΉβπ))) β
β*) |
27 | | mnfxr 11217 |
. . . 4
β’ -β
β β* |
28 | | xneg11 13140 |
. . . 4
β’ (((lim
supβ(π β π β¦
-π(πΉβπ))) β β* β§ -β
β β*) β (-π(lim supβ(π β π β¦ -π(πΉβπ))) = -π-β β
(lim supβ(π β
π β¦
-π(πΉβπ))) = -β)) |
29 | 26, 27, 28 | sylancl 587 |
. . 3
β’ (π β (-π(lim
supβ(π β π β¦
-π(πΉβπ))) = -π-β β
(lim supβ(π β
π β¦
-π(πΉβπ))) = -β)) |
30 | 22, 29 | bitrd 279 |
. 2
β’ (π β (-π(lim
supβ(π β π β¦
-π(πΉβπ))) = +β β (lim supβ(π β π β¦ -π(πΉβπ))) = -β)) |
31 | 4 | uztrn2 12787 |
. . . . . . . . 9
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
32 | | xnegex 13133 |
. . . . . . . . 9
β’
-π(πΉβπ) β V |
33 | | fvmpt4 43551 |
. . . . . . . . 9
β’ ((π β π β§ -π(πΉβπ) β V) β ((π β π β¦ -π(πΉβπ))βπ) = -π(πΉβπ)) |
34 | 31, 32, 33 | sylancl 587 |
. . . . . . . 8
β’ ((π β π β§ π β (β€β₯βπ)) β ((π β π β¦ -π(πΉβπ))βπ) = -π(πΉβπ)) |
35 | 34 | breq1d 5116 |
. . . . . . 7
β’ ((π β π β§ π β (β€β₯βπ)) β (((π β π β¦ -π(πΉβπ))βπ) β€ π₯ β -π(πΉβπ) β€ π₯)) |
36 | 35 | ralbidva 3169 |
. . . . . 6
β’ (π β π β (βπ β (β€β₯βπ)((π β π β¦ -π(πΉβπ))βπ) β€ π₯ β βπ β (β€β₯βπ)-π(πΉβπ) β€ π₯)) |
37 | 36 | rexbiia 3092 |
. . . . 5
β’
(βπ β
π βπ β
(β€β₯βπ)((π β π β¦ -π(πΉβπ))βπ) β€ π₯ β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π₯) |
38 | 37 | ralbii 3093 |
. . . 4
β’
(βπ₯ β
β βπ β
π βπ β
(β€β₯βπ)((π β π β¦ -π(πΉβπ))βπ) β€ π₯ β βπ₯ β β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π₯) |
39 | 38 | a1i 11 |
. . 3
β’ (π β (βπ₯ β β βπ β π βπ β (β€β₯βπ)((π β π β¦ -π(πΉβπ))βπ) β€ π₯ β βπ₯ β β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π₯)) |
40 | | nfmpt1 5214 |
. . . 4
β’
β²π(π β π β¦ -π(πΉβπ)) |
41 | 5 | ffvelcdmda 7036 |
. . . . . 6
β’ ((π β§ π β π) β (πΉβπ) β
β*) |
42 | 41 | xnegcld 13225 |
. . . . 5
β’ ((π β§ π β π) β -π(πΉβπ) β
β*) |
43 | 14 | eqcomi 2742 |
. . . . 5
β’ (π β π β¦ -π(πΉβπ)) = (π β π β¦ -π(πΉβπ)) |
44 | 42, 43 | fmptd 7063 |
. . . 4
β’ (π β (π β π β¦ -π(πΉβπ)):πβΆβ*) |
45 | 40, 3, 4, 44 | limsupmnfuz 44054 |
. . 3
β’ (π β ((lim supβ(π β π β¦ -π(πΉβπ))) = -β β βπ₯ β β βπ β π βπ β (β€β₯βπ)((π β π β¦ -π(πΉβπ))βπ) β€ π₯)) |
46 | 7, 4, 5 | xlimpnfxnegmnf 44141 |
. . 3
β’ (π β (βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ) β βπ₯ β β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π₯)) |
47 | 39, 45, 46 | 3bitr4d 311 |
. 2
β’ (π β ((lim supβ(π β π β¦ -π(πΉβπ))) = -β β βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ))) |
48 | 18, 30, 47 | 3bitrd 305 |
1
β’ (π β ((lim infβπΉ) = +β β
βπ₯ β β
βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ))) |