Step | Hyp | Ref
| Expression |
1 | | liminflbuz2.1 |
. . . . 5
β’
β²ππ |
2 | | nfv 1909 |
. . . . 5
β’
β²π π β π |
3 | 1, 2 | nfan 1894 |
. . . 4
β’
β²π(π β§ π β π) |
4 | | simpll 765 |
. . . . 5
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π) |
5 | | liminflbuz2.4 |
. . . . . . 7
β’ π =
(β€β₯βπ) |
6 | 5 | uztrn2 12866 |
. . . . . 6
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
7 | 6 | adantll 712 |
. . . . 5
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π β π) |
8 | | liminflbuz2.5 |
. . . . . . . . . . . . 13
β’ (π β πΉ:πβΆβ*) |
9 | 8 | ffvelcdmda 7087 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (πΉβπ) β
β*) |
10 | 9 | adantr 479 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ Β¬ -β < (πΉβπ)) β (πΉβπ) β
β*) |
11 | | mnfxr 11296 |
. . . . . . . . . . . 12
β’ -β
β β* |
12 | 11 | a1i 11 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ Β¬ -β < (πΉβπ)) β -β β
β*) |
13 | | simpr 483 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ Β¬ -β < (πΉβπ)) β Β¬ -β < (πΉβπ)) |
14 | 10, 12, 13 | xrnltled 11307 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ Β¬ -β < (πΉβπ)) β (πΉβπ) β€ -β) |
15 | | xlemnf 13173 |
. . . . . . . . . . 11
β’ ((πΉβπ) β β* β ((πΉβπ) β€ -β β (πΉβπ) = -β)) |
16 | 10, 15 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ Β¬ -β < (πΉβπ)) β ((πΉβπ) β€ -β β (πΉβπ) = -β)) |
17 | 14, 16 | mpbid 231 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ Β¬ -β < (πΉβπ)) β (πΉβπ) = -β) |
18 | | xnegeq 13213 |
. . . . . . . . . 10
β’ ((πΉβπ) = -β β
-π(πΉβπ) =
-π-β) |
19 | | xnegmnf 13216 |
. . . . . . . . . 10
β’
-π-β = +β |
20 | 18, 19 | eqtrdi 2781 |
. . . . . . . . 9
β’ ((πΉβπ) = -β β
-π(πΉβπ) = +β) |
21 | 17, 20 | syl 17 |
. . . . . . . 8
β’ (((π β§ π β π) β§ Β¬ -β < (πΉβπ)) β -π(πΉβπ) = +β) |
22 | 21 | adantlr 713 |
. . . . . . 7
β’ ((((π β§ π β π) β§ -π(πΉβπ) β +β) β§ Β¬ -β <
(πΉβπ)) β -π(πΉβπ) = +β) |
23 | | neneq 2936 |
. . . . . . . 8
β’
(-π(πΉβπ) β +β β Β¬
-π(πΉβπ) = +β) |
24 | 23 | ad2antlr 725 |
. . . . . . 7
β’ ((((π β§ π β π) β§ -π(πΉβπ) β +β) β§ Β¬ -β <
(πΉβπ)) β Β¬ -π(πΉβπ) = +β) |
25 | 22, 24 | condan 816 |
. . . . . 6
β’ (((π β§ π β π) β§ -π(πΉβπ) β +β) β -β < (πΉβπ)) |
26 | 25 | ex 411 |
. . . . 5
β’ ((π β§ π β π) β (-π(πΉβπ) β +β β -β < (πΉβπ))) |
27 | 4, 7, 26 | syl2anc 582 |
. . . 4
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β
(-π(πΉβπ) β +β β -β < (πΉβπ))) |
28 | 3, 27 | ralimdaa 3248 |
. . 3
β’ ((π β§ π β π) β (βπ β (β€β₯βπ)-π(πΉβπ) β +β β βπ β
(β€β₯βπ)-β < (πΉβπ))) |
29 | 28 | imp 405 |
. 2
β’ (((π β§ π β π) β§ βπ β (β€β₯βπ)-π(πΉβπ) β +β) β βπ β
(β€β₯βπ)-β < (πΉβπ)) |
30 | 9 | xnegcld 13306 |
. . . . . . . . 9
β’ ((π β§ π β π) β -π(πΉβπ) β
β*) |
31 | 30 | adantr 479 |
. . . . . . . 8
β’ (((π β§ π β π) β§ ((π β π β¦ -π(πΉβπ))βπ) < +β) β
-π(πΉβπ) β
β*) |
32 | | pnfxr 11293 |
. . . . . . . . 9
β’ +β
β β* |
33 | 32 | a1i 11 |
. . . . . . . 8
β’ (((π β§ π β π) β§ ((π β π β¦ -π(πΉβπ))βπ) < +β) β +β β
β*) |
34 | | eqidd 2726 |
. . . . . . . . . . 11
β’ (π β (π β π β¦ -π(πΉβπ)) = (π β π β¦ -π(πΉβπ))) |
35 | 34, 30 | fvmpt2d 7011 |
. . . . . . . . . 10
β’ ((π β§ π β π) β ((π β π β¦ -π(πΉβπ))βπ) = -π(πΉβπ)) |
36 | 35 | adantr 479 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ ((π β π β¦ -π(πΉβπ))βπ) < +β) β ((π β π β¦ -π(πΉβπ))βπ) = -π(πΉβπ)) |
37 | | simpr 483 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ ((π β π β¦ -π(πΉβπ))βπ) < +β) β ((π β π β¦ -π(πΉβπ))βπ) < +β) |
38 | 36, 37 | eqbrtrrd 5168 |
. . . . . . . 8
β’ (((π β§ π β π) β§ ((π β π β¦ -π(πΉβπ))βπ) < +β) β
-π(πΉβπ) < +β) |
39 | 31, 33, 38 | xrltned 44798 |
. . . . . . 7
β’ (((π β§ π β π) β§ ((π β π β¦ -π(πΉβπ))βπ) < +β) β
-π(πΉβπ) β +β) |
40 | 39 | ex 411 |
. . . . . 6
β’ ((π β§ π β π) β (((π β π β¦ -π(πΉβπ))βπ) < +β β
-π(πΉβπ) β +β)) |
41 | 4, 7, 40 | syl2anc 582 |
. . . . 5
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β (((π β π β¦ -π(πΉβπ))βπ) < +β β
-π(πΉβπ) β +β)) |
42 | 3, 41 | ralimdaa 3248 |
. . . 4
β’ ((π β§ π β π) β (βπ β (β€β₯βπ)((π β π β¦ -π(πΉβπ))βπ) < +β β βπ β
(β€β₯βπ)-π(πΉβπ) β +β)) |
43 | 42 | imp 405 |
. . 3
β’ (((π β§ π β π) β§ βπ β (β€β₯βπ)((π β π β¦ -π(πΉβπ))βπ) < +β) β βπ β
(β€β₯βπ)-π(πΉβπ) β +β) |
44 | | nfmpt1 5252 |
. . . 4
β’
β²π(π β π β¦ -π(πΉβπ)) |
45 | | liminflbuz2.3 |
. . . 4
β’ (π β π β β€) |
46 | 1, 30 | fmptd2f 44668 |
. . . 4
β’ (π β (π β π β¦ -π(πΉβπ)):πβΆβ*) |
47 | 5 | fvexi 6904 |
. . . . . . . . . . 11
β’ π β V |
48 | 47 | a1i 11 |
. . . . . . . . . 10
β’ (π β π β V) |
49 | 8, 48 | fexd 7233 |
. . . . . . . . 9
β’ (π β πΉ β V) |
50 | 49 | liminfcld 45217 |
. . . . . . . 8
β’ (π β (lim infβπΉ) β
β*) |
51 | 50 | xnegnegd 44883 |
. . . . . . 7
β’ (π β
-π-π(lim infβπΉ) = (lim infβπΉ)) |
52 | | liminflbuz2.2 |
. . . . . . . 8
β’
β²ππΉ |
53 | 1, 52, 45, 5, 8 | liminfvaluz3 45243 |
. . . . . . 7
β’ (π β (lim infβπΉ) = -π(lim
supβ(π β π β¦
-π(πΉβπ)))) |
54 | 51, 53 | eqtr2d 2766 |
. . . . . 6
β’ (π β -π(lim
supβ(π β π β¦
-π(πΉβπ))) =
-π-π(lim infβπΉ)) |
55 | 48 | mptexd 7230 |
. . . . . . . 8
β’ (π β (π β π β¦ -π(πΉβπ)) β V) |
56 | 55 | limsupcld 45137 |
. . . . . . 7
β’ (π β (lim supβ(π β π β¦ -π(πΉβπ))) β
β*) |
57 | 50 | xnegcld 13306 |
. . . . . . 7
β’ (π β -π(lim
infβπΉ) β
β*) |
58 | | xneg11 13221 |
. . . . . . 7
β’ (((lim
supβ(π β π β¦
-π(πΉβπ))) β β* β§
-π(lim infβπΉ) β β*) β
(-π(lim supβ(π β π β¦ -π(πΉβπ))) =
-π-π(lim infβπΉ) β (lim supβ(π β π β¦ -π(πΉβπ))) = -π(lim
infβπΉ))) |
59 | 56, 57, 58 | syl2anc 582 |
. . . . . 6
β’ (π β (-π(lim
supβ(π β π β¦
-π(πΉβπ))) =
-π-π(lim infβπΉ) β (lim supβ(π β π β¦ -π(πΉβπ))) = -π(lim
infβπΉ))) |
60 | 54, 59 | mpbid 231 |
. . . . 5
β’ (π β (lim supβ(π β π β¦ -π(πΉβπ))) = -π(lim
infβπΉ)) |
61 | | nne 2934 |
. . . . . . 7
β’ (Β¬
-π(lim infβπΉ) β +β β
-π(lim infβπΉ) = +β) |
62 | 51 | eqcomd 2731 |
. . . . . . . . 9
β’ (π β (lim infβπΉ) =
-π-π(lim infβπΉ)) |
63 | 62 | adantr 479 |
. . . . . . . 8
β’ ((π β§ -π(lim
infβπΉ) = +β)
β (lim infβπΉ) =
-π-π(lim infβπΉ)) |
64 | | xnegeq 13213 |
. . . . . . . . 9
β’
(-π(lim infβπΉ) = +β β
-π-π(lim infβπΉ) =
-π+β) |
65 | 64 | adantl 480 |
. . . . . . . 8
β’ ((π β§ -π(lim
infβπΉ) = +β)
β -π-π(lim infβπΉ) =
-π+β) |
66 | | xnegpnf 13215 |
. . . . . . . . 9
β’
-π+β = -β |
67 | 66 | a1i 11 |
. . . . . . . 8
β’ ((π β§ -π(lim
infβπΉ) = +β)
β -π+β = -β) |
68 | 63, 65, 67 | 3eqtrd 2769 |
. . . . . . 7
β’ ((π β§ -π(lim
infβπΉ) = +β)
β (lim infβπΉ) =
-β) |
69 | 61, 68 | sylan2b 592 |
. . . . . 6
β’ ((π β§ Β¬
-π(lim infβπΉ) β +β) β (lim infβπΉ) = -β) |
70 | | liminflbuz2.6 |
. . . . . . . 8
β’ (π β (lim infβπΉ) β
-β) |
71 | 70 | neneqd 2935 |
. . . . . . 7
β’ (π β Β¬ (lim infβπΉ) = -β) |
72 | 71 | adantr 479 |
. . . . . 6
β’ ((π β§ Β¬
-π(lim infβπΉ) β +β) β Β¬ (lim
infβπΉ) =
-β) |
73 | 69, 72 | condan 816 |
. . . . 5
β’ (π β -π(lim
infβπΉ) β
+β) |
74 | 60, 73 | eqnetrd 2998 |
. . . 4
β’ (π β (lim supβ(π β π β¦ -π(πΉβπ))) β +β) |
75 | 1, 44, 45, 5, 46, 74 | limsupubuz2 45260 |
. . 3
β’ (π β βπ β π βπ β (β€β₯βπ)((π β π β¦ -π(πΉβπ))βπ) < +β) |
76 | 43, 75 | reximddv3 3162 |
. 2
β’ (π β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β +β) |
77 | 29, 76 | reximddv3 3162 |
1
β’ (π β βπ β π βπ β (β€β₯βπ)-β < (πΉβπ)) |