Step | Hyp | Ref
| Expression |
1 | | nfv 1918 |
. . . . 5
β’
β²ππ |
2 | | liminfreuzlem.1 |
. . . . 5
β’
β²ππΉ |
3 | | liminfreuzlem.2 |
. . . . 5
β’ (π β π β β€) |
4 | | liminfreuzlem.3 |
. . . . 5
β’ π =
(β€β₯βπ) |
5 | | liminfreuzlem.4 |
. . . . 5
β’ (π β πΉ:πβΆβ) |
6 | 1, 2, 3, 4, 5 | liminfvaluz4 44126 |
. . . 4
β’ (π β (lim infβπΉ) = -π(lim
supβ(π β π β¦ -(πΉβπ)))) |
7 | 6 | eleq1d 2819 |
. . 3
β’ (π β ((lim infβπΉ) β β β
-π(lim supβ(π β π β¦ -(πΉβπ))) β β)) |
8 | 4 | fvexi 6857 |
. . . . . . 7
β’ π β V |
9 | 8 | mptex 7174 |
. . . . . 6
β’ (π β π β¦ -(πΉβπ)) β V |
10 | | limsupcl 15361 |
. . . . . 6
β’ ((π β π β¦ -(πΉβπ)) β V β (lim supβ(π β π β¦ -(πΉβπ))) β
β*) |
11 | 9, 10 | ax-mp 5 |
. . . . 5
β’ (lim
supβ(π β π β¦ -(πΉβπ))) β
β* |
12 | 11 | a1i 11 |
. . . 4
β’ (π β (lim supβ(π β π β¦ -(πΉβπ))) β
β*) |
13 | 12 | xnegred 43791 |
. . 3
β’ (π β ((lim supβ(π β π β¦ -(πΉβπ))) β β β
-π(lim supβ(π β π β¦ -(πΉβπ))) β β)) |
14 | 7, 13 | bitr4d 282 |
. 2
β’ (π β ((lim infβπΉ) β β β (lim
supβ(π β π β¦ -(πΉβπ))) β β)) |
15 | 5 | ffvelcdmda 7036 |
. . . . 5
β’ ((π β§ π β π) β (πΉβπ) β β) |
16 | 15 | renegcld 11587 |
. . . 4
β’ ((π β§ π β π) β -(πΉβπ) β β) |
17 | 1, 3, 4, 16 | limsupreuzmpt 44066 |
. . 3
β’ (π β ((lim supβ(π β π β¦ -(πΉβπ))) β β β (βπ¦ β β βπ β π βπ β (β€β₯βπ)π¦ β€ -(πΉβπ) β§ βπ¦ β β βπ β π -(πΉβπ) β€ π¦))) |
18 | | renegcl 11469 |
. . . . . . . 8
β’ (π¦ β β β -π¦ β
β) |
19 | 18 | ad2antlr 726 |
. . . . . . 7
β’ (((π β§ π¦ β β) β§ βπ β π βπ β (β€β₯βπ)π¦ β€ -(πΉβπ)) β -π¦ β β) |
20 | | simpllr 775 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β β) β§ π β π) β§ π β (β€β₯βπ)) β π¦ β β) |
21 | 5 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β πΉ:πβΆβ) |
22 | 4 | uztrn2 12787 |
. . . . . . . . . . . . . . 15
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
23 | 22 | adantll 713 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π β π) |
24 | 21, 23 | ffvelcdmd 7037 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
25 | 24 | adantllr 718 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β β) β§ π β π) β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
26 | 20, 25 | leneg2d 43769 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β β) β§ π β π) β§ π β (β€β₯βπ)) β (π¦ β€ -(πΉβπ) β (πΉβπ) β€ -π¦)) |
27 | 26 | rexbidva 3170 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β) β§ π β π) β (βπ β (β€β₯βπ)π¦ β€ -(πΉβπ) β βπ β (β€β₯βπ)(πΉβπ) β€ -π¦)) |
28 | 27 | ralbidva 3169 |
. . . . . . . . 9
β’ ((π β§ π¦ β β) β (βπ β π βπ β (β€β₯βπ)π¦ β€ -(πΉβπ) β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ -π¦)) |
29 | 28 | biimpd 228 |
. . . . . . . 8
β’ ((π β§ π¦ β β) β (βπ β π βπ β (β€β₯βπ)π¦ β€ -(πΉβπ) β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ -π¦)) |
30 | 29 | imp 408 |
. . . . . . 7
β’ (((π β§ π¦ β β) β§ βπ β π βπ β (β€β₯βπ)π¦ β€ -(πΉβπ)) β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ -π¦) |
31 | | breq2 5110 |
. . . . . . . . . 10
β’ (π₯ = -π¦ β ((πΉβπ) β€ π₯ β (πΉβπ) β€ -π¦)) |
32 | 31 | rexbidv 3172 |
. . . . . . . . 9
β’ (π₯ = -π¦ β (βπ β (β€β₯βπ)(πΉβπ) β€ π₯ β βπ β (β€β₯βπ)(πΉβπ) β€ -π¦)) |
33 | 32 | ralbidv 3171 |
. . . . . . . 8
β’ (π₯ = -π¦ β (βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ -π¦)) |
34 | 33 | rspcev 3580 |
. . . . . . 7
β’ ((-π¦ β β β§
βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ -π¦) β βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) |
35 | 19, 30, 34 | syl2anc 585 |
. . . . . 6
β’ (((π β§ π¦ β β) β§ βπ β π βπ β (β€β₯βπ)π¦ β€ -(πΉβπ)) β βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) |
36 | 35 | rexlimdva2 3151 |
. . . . 5
β’ (π β (βπ¦ β β βπ β π βπ β (β€β₯βπ)π¦ β€ -(πΉβπ) β βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) |
37 | | renegcl 11469 |
. . . . . . . 8
β’ (π₯ β β β -π₯ β
β) |
38 | 37 | ad2antlr 726 |
. . . . . . 7
β’ (((π β§ π₯ β β) β§ βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β -π₯ β β) |
39 | 24 | adantllr 718 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β β) β§ π β π) β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
40 | | simpllr 775 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β β) β§ π β π) β§ π β (β€β₯βπ)) β π₯ β β) |
41 | 39, 40 | lenegd 11739 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β) β§ π β π) β§ π β (β€β₯βπ)) β ((πΉβπ) β€ π₯ β -π₯ β€ -(πΉβπ))) |
42 | 41 | rexbidva 3170 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ π β π) β (βπ β (β€β₯βπ)(πΉβπ) β€ π₯ β βπ β (β€β₯βπ)-π₯ β€ -(πΉβπ))) |
43 | 42 | ralbidva 3169 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β (βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯ β βπ β π βπ β (β€β₯βπ)-π₯ β€ -(πΉβπ))) |
44 | 43 | biimpd 228 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β (βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯ β βπ β π βπ β (β€β₯βπ)-π₯ β€ -(πΉβπ))) |
45 | 44 | imp 408 |
. . . . . . 7
β’ (((π β§ π₯ β β) β§ βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β βπ β π βπ β (β€β₯βπ)-π₯ β€ -(πΉβπ)) |
46 | | breq1 5109 |
. . . . . . . . . 10
β’ (π¦ = -π₯ β (π¦ β€ -(πΉβπ) β -π₯ β€ -(πΉβπ))) |
47 | 46 | rexbidv 3172 |
. . . . . . . . 9
β’ (π¦ = -π₯ β (βπ β (β€β₯βπ)π¦ β€ -(πΉβπ) β βπ β (β€β₯βπ)-π₯ β€ -(πΉβπ))) |
48 | 47 | ralbidv 3171 |
. . . . . . . 8
β’ (π¦ = -π₯ β (βπ β π βπ β (β€β₯βπ)π¦ β€ -(πΉβπ) β βπ β π βπ β (β€β₯βπ)-π₯ β€ -(πΉβπ))) |
49 | 48 | rspcev 3580 |
. . . . . . 7
β’ ((-π₯ β β β§
βπ β π βπ β (β€β₯βπ)-π₯ β€ -(πΉβπ)) β βπ¦ β β βπ β π βπ β (β€β₯βπ)π¦ β€ -(πΉβπ)) |
50 | 38, 45, 49 | syl2anc 585 |
. . . . . 6
β’ (((π β§ π₯ β β) β§ βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β βπ¦ β β βπ β π βπ β (β€β₯βπ)π¦ β€ -(πΉβπ)) |
51 | 50 | rexlimdva2 3151 |
. . . . 5
β’ (π β (βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯ β βπ¦ β β βπ β π βπ β (β€β₯βπ)π¦ β€ -(πΉβπ))) |
52 | 36, 51 | impbid 211 |
. . . 4
β’ (π β (βπ¦ β β βπ β π βπ β (β€β₯βπ)π¦ β€ -(πΉβπ) β βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) |
53 | 18 | ad2antlr 726 |
. . . . . . 7
β’ (((π β§ π¦ β β) β§ βπ β π -(πΉβπ) β€ π¦) β -π¦ β β) |
54 | 15 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β) β§ π β π) β (πΉβπ) β β) |
55 | | simplr 768 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β) β§ π β π) β π¦ β β) |
56 | 54, 55 | leneg3d 43778 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β) β§ π β π) β (-(πΉβπ) β€ π¦ β -π¦ β€ (πΉβπ))) |
57 | 56 | ralbidva 3169 |
. . . . . . . . 9
β’ ((π β§ π¦ β β) β (βπ β π -(πΉβπ) β€ π¦ β βπ β π -π¦ β€ (πΉβπ))) |
58 | 57 | biimpd 228 |
. . . . . . . 8
β’ ((π β§ π¦ β β) β (βπ β π -(πΉβπ) β€ π¦ β βπ β π -π¦ β€ (πΉβπ))) |
59 | 58 | imp 408 |
. . . . . . 7
β’ (((π β§ π¦ β β) β§ βπ β π -(πΉβπ) β€ π¦) β βπ β π -π¦ β€ (πΉβπ)) |
60 | | breq1 5109 |
. . . . . . . . 9
β’ (π₯ = -π¦ β (π₯ β€ (πΉβπ) β -π¦ β€ (πΉβπ))) |
61 | 60 | ralbidv 3171 |
. . . . . . . 8
β’ (π₯ = -π¦ β (βπ β π π₯ β€ (πΉβπ) β βπ β π -π¦ β€ (πΉβπ))) |
62 | 61 | rspcev 3580 |
. . . . . . 7
β’ ((-π¦ β β β§
βπ β π -π¦ β€ (πΉβπ)) β βπ₯ β β βπ β π π₯ β€ (πΉβπ)) |
63 | 53, 59, 62 | syl2anc 585 |
. . . . . 6
β’ (((π β§ π¦ β β) β§ βπ β π -(πΉβπ) β€ π¦) β βπ₯ β β βπ β π π₯ β€ (πΉβπ)) |
64 | 63 | rexlimdva2 3151 |
. . . . 5
β’ (π β (βπ¦ β β βπ β π -(πΉβπ) β€ π¦ β βπ₯ β β βπ β π π₯ β€ (πΉβπ))) |
65 | 37 | ad2antlr 726 |
. . . . . . 7
β’ (((π β§ π₯ β β) β§ βπ β π π₯ β€ (πΉβπ)) β -π₯ β β) |
66 | | simplr 768 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β) β§ π β π) β π₯ β β) |
67 | 15 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β) β§ π β π) β (πΉβπ) β β) |
68 | 66, 67 | lenegd 11739 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ π β π) β (π₯ β€ (πΉβπ) β -(πΉβπ) β€ -π₯)) |
69 | 68 | ralbidva 3169 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β (βπ β π π₯ β€ (πΉβπ) β βπ β π -(πΉβπ) β€ -π₯)) |
70 | 69 | biimpd 228 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β (βπ β π π₯ β€ (πΉβπ) β βπ β π -(πΉβπ) β€ -π₯)) |
71 | 70 | imp 408 |
. . . . . . 7
β’ (((π β§ π₯ β β) β§ βπ β π π₯ β€ (πΉβπ)) β βπ β π -(πΉβπ) β€ -π₯) |
72 | | brralrspcev 5166 |
. . . . . . 7
β’ ((-π₯ β β β§
βπ β π -(πΉβπ) β€ -π₯) β βπ¦ β β βπ β π -(πΉβπ) β€ π¦) |
73 | 65, 71, 72 | syl2anc 585 |
. . . . . 6
β’ (((π β§ π₯ β β) β§ βπ β π π₯ β€ (πΉβπ)) β βπ¦ β β βπ β π -(πΉβπ) β€ π¦) |
74 | 73 | rexlimdva2 3151 |
. . . . 5
β’ (π β (βπ₯ β β βπ β π π₯ β€ (πΉβπ) β βπ¦ β β βπ β π -(πΉβπ) β€ π¦)) |
75 | 64, 74 | impbid 211 |
. . . 4
β’ (π β (βπ¦ β β βπ β π -(πΉβπ) β€ π¦ β βπ₯ β β βπ β π π₯ β€ (πΉβπ))) |
76 | 52, 75 | anbi12d 632 |
. . 3
β’ (π β ((βπ¦ β β βπ β π βπ β (β€β₯βπ)π¦ β€ -(πΉβπ) β§ βπ¦ β β βπ β π -(πΉβπ) β€ π¦) β (βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯ β§ βπ₯ β β βπ β π π₯ β€ (πΉβπ)))) |
77 | 17, 76 | bitrd 279 |
. 2
β’ (π β ((lim supβ(π β π β¦ -(πΉβπ))) β β β (βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯ β§ βπ₯ β β βπ β π π₯ β€ (πΉβπ)))) |
78 | 14, 77 | bitrd 279 |
1
β’ (π β ((lim infβπΉ) β β β
(βπ₯ β β
βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯ β§ βπ₯ β β βπ β π π₯ β€ (πΉβπ)))) |