Step | Hyp | Ref
| Expression |
1 | | liminflbuz2.1 |
. . . . 5
β’
β²ππ |
2 | | nfv 1917 |
. . . . 5
β’
β²π π β π |
3 | 1, 2 | nfan 1902 |
. . . 4
β’
β²π(π β§ π β π) |
4 | | simpll 765 |
. . . . 5
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π) |
5 | | liminflbuz2.4 |
. . . . . . 7
β’ π =
(β€β₯βπ) |
6 | 5 | uztrn2 12837 |
. . . . . 6
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
7 | 6 | adantll 712 |
. . . . 5
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π β π) |
8 | | liminflbuz2.5 |
. . . . . . . . . . . . 13
β’ (π β πΉ:πβΆβ*) |
9 | 8 | ffvelcdmda 7083 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (πΉβπ) β
β*) |
10 | 9 | adantr 481 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ Β¬ -β < (πΉβπ)) β (πΉβπ) β
β*) |
11 | | mnfxr 11267 |
. . . . . . . . . . . 12
β’ -β
β β* |
12 | 11 | a1i 11 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ Β¬ -β < (πΉβπ)) β -β β
β*) |
13 | | simpr 485 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ Β¬ -β < (πΉβπ)) β Β¬ -β < (πΉβπ)) |
14 | 10, 12, 13 | xrnltled 11278 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ Β¬ -β < (πΉβπ)) β (πΉβπ) β€ -β) |
15 | | xlemnf 13142 |
. . . . . . . . . . 11
β’ ((πΉβπ) β β* β ((πΉβπ) β€ -β β (πΉβπ) = -β)) |
16 | 10, 15 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ Β¬ -β < (πΉβπ)) β ((πΉβπ) β€ -β β (πΉβπ) = -β)) |
17 | 14, 16 | mpbid 231 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ Β¬ -β < (πΉβπ)) β (πΉβπ) = -β) |
18 | | xnegeq 13182 |
. . . . . . . . . 10
β’ ((πΉβπ) = -β β
-π(πΉβπ) =
-π-β) |
19 | | xnegmnf 13185 |
. . . . . . . . . 10
β’
-π-β = +β |
20 | 18, 19 | eqtrdi 2788 |
. . . . . . . . 9
β’ ((πΉβπ) = -β β
-π(πΉβπ) = +β) |
21 | 17, 20 | syl 17 |
. . . . . . . 8
β’ (((π β§ π β π) β§ Β¬ -β < (πΉβπ)) β -π(πΉβπ) = +β) |
22 | 21 | adantlr 713 |
. . . . . . 7
β’ ((((π β§ π β π) β§ -π(πΉβπ) β +β) β§ Β¬ -β <
(πΉβπ)) β -π(πΉβπ) = +β) |
23 | | neneq 2946 |
. . . . . . . 8
β’
(-π(πΉβπ) β +β β Β¬
-π(πΉβπ) = +β) |
24 | 23 | ad2antlr 725 |
. . . . . . 7
β’ ((((π β§ π β π) β§ -π(πΉβπ) β +β) β§ Β¬ -β <
(πΉβπ)) β Β¬ -π(πΉβπ) = +β) |
25 | 22, 24 | condan 816 |
. . . . . 6
β’ (((π β§ π β π) β§ -π(πΉβπ) β +β) β -β < (πΉβπ)) |
26 | 25 | ex 413 |
. . . . 5
β’ ((π β§ π β π) β (-π(πΉβπ) β +β β -β < (πΉβπ))) |
27 | 4, 7, 26 | syl2anc 584 |
. . . 4
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β
(-π(πΉβπ) β +β β -β < (πΉβπ))) |
28 | 3, 27 | ralimdaa 3257 |
. . 3
β’ ((π β§ π β π) β (βπ β (β€β₯βπ)-π(πΉβπ) β +β β βπ β
(β€β₯βπ)-β < (πΉβπ))) |
29 | 28 | imp 407 |
. 2
β’ (((π β§ π β π) β§ βπ β (β€β₯βπ)-π(πΉβπ) β +β) β βπ β
(β€β₯βπ)-β < (πΉβπ)) |
30 | 9 | xnegcld 13275 |
. . . . . . . . 9
β’ ((π β§ π β π) β -π(πΉβπ) β
β*) |
31 | 30 | adantr 481 |
. . . . . . . 8
β’ (((π β§ π β π) β§ ((π β π β¦ -π(πΉβπ))βπ) < +β) β
-π(πΉβπ) β
β*) |
32 | | pnfxr 11264 |
. . . . . . . . 9
β’ +β
β β* |
33 | 32 | a1i 11 |
. . . . . . . 8
β’ (((π β§ π β π) β§ ((π β π β¦ -π(πΉβπ))βπ) < +β) β +β β
β*) |
34 | | eqidd 2733 |
. . . . . . . . . . 11
β’ (π β (π β π β¦ -π(πΉβπ)) = (π β π β¦ -π(πΉβπ))) |
35 | 34, 30 | fvmpt2d 7008 |
. . . . . . . . . 10
β’ ((π β§ π β π) β ((π β π β¦ -π(πΉβπ))βπ) = -π(πΉβπ)) |
36 | 35 | adantr 481 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ ((π β π β¦ -π(πΉβπ))βπ) < +β) β ((π β π β¦ -π(πΉβπ))βπ) = -π(πΉβπ)) |
37 | | simpr 485 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ ((π β π β¦ -π(πΉβπ))βπ) < +β) β ((π β π β¦ -π(πΉβπ))βπ) < +β) |
38 | 36, 37 | eqbrtrrd 5171 |
. . . . . . . 8
β’ (((π β§ π β π) β§ ((π β π β¦ -π(πΉβπ))βπ) < +β) β
-π(πΉβπ) < +β) |
39 | 31, 33, 38 | xrltned 44053 |
. . . . . . 7
β’ (((π β§ π β π) β§ ((π β π β¦ -π(πΉβπ))βπ) < +β) β
-π(πΉβπ) β +β) |
40 | 39 | ex 413 |
. . . . . 6
β’ ((π β§ π β π) β (((π β π β¦ -π(πΉβπ))βπ) < +β β
-π(πΉβπ) β +β)) |
41 | 4, 7, 40 | syl2anc 584 |
. . . . 5
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β (((π β π β¦ -π(πΉβπ))βπ) < +β β
-π(πΉβπ) β +β)) |
42 | 3, 41 | ralimdaa 3257 |
. . . 4
β’ ((π β§ π β π) β (βπ β (β€β₯βπ)((π β π β¦ -π(πΉβπ))βπ) < +β β βπ β
(β€β₯βπ)-π(πΉβπ) β +β)) |
43 | 42 | imp 407 |
. . 3
β’ (((π β§ π β π) β§ βπ β (β€β₯βπ)((π β π β¦ -π(πΉβπ))βπ) < +β) β βπ β
(β€β₯βπ)-π(πΉβπ) β +β) |
44 | | nfmpt1 5255 |
. . . 4
β’
β²π(π β π β¦ -π(πΉβπ)) |
45 | | liminflbuz2.3 |
. . . 4
β’ (π β π β β€) |
46 | 1, 30 | fmptd2f 43922 |
. . . 4
β’ (π β (π β π β¦ -π(πΉβπ)):πβΆβ*) |
47 | 5 | fvexi 6902 |
. . . . . . . . . . 11
β’ π β V |
48 | 47 | a1i 11 |
. . . . . . . . . 10
β’ (π β π β V) |
49 | 8, 48 | fexd 7225 |
. . . . . . . . 9
β’ (π β πΉ β V) |
50 | 49 | liminfcld 44472 |
. . . . . . . 8
β’ (π β (lim infβπΉ) β
β*) |
51 | 50 | xnegnegd 44138 |
. . . . . . 7
β’ (π β
-π-π(lim infβπΉ) = (lim infβπΉ)) |
52 | | liminflbuz2.2 |
. . . . . . . 8
β’
β²ππΉ |
53 | 1, 52, 45, 5, 8 | liminfvaluz3 44498 |
. . . . . . 7
β’ (π β (lim infβπΉ) = -π(lim
supβ(π β π β¦
-π(πΉβπ)))) |
54 | 51, 53 | eqtr2d 2773 |
. . . . . 6
β’ (π β -π(lim
supβ(π β π β¦
-π(πΉβπ))) =
-π-π(lim infβπΉ)) |
55 | 48 | mptexd 7222 |
. . . . . . . 8
β’ (π β (π β π β¦ -π(πΉβπ)) β V) |
56 | 55 | limsupcld 44392 |
. . . . . . 7
β’ (π β (lim supβ(π β π β¦ -π(πΉβπ))) β
β*) |
57 | 50 | xnegcld 13275 |
. . . . . . 7
β’ (π β -π(lim
infβπΉ) β
β*) |
58 | | xneg11 13190 |
. . . . . . 7
β’ (((lim
supβ(π β π β¦
-π(πΉβπ))) β β* β§
-π(lim infβπΉ) β β*) β
(-π(lim supβ(π β π β¦ -π(πΉβπ))) =
-π-π(lim infβπΉ) β (lim supβ(π β π β¦ -π(πΉβπ))) = -π(lim
infβπΉ))) |
59 | 56, 57, 58 | syl2anc 584 |
. . . . . 6
β’ (π β (-π(lim
supβ(π β π β¦
-π(πΉβπ))) =
-π-π(lim infβπΉ) β (lim supβ(π β π β¦ -π(πΉβπ))) = -π(lim
infβπΉ))) |
60 | 54, 59 | mpbid 231 |
. . . . 5
β’ (π β (lim supβ(π β π β¦ -π(πΉβπ))) = -π(lim
infβπΉ)) |
61 | | nne 2944 |
. . . . . . 7
β’ (Β¬
-π(lim infβπΉ) β +β β
-π(lim infβπΉ) = +β) |
62 | 51 | eqcomd 2738 |
. . . . . . . . 9
β’ (π β (lim infβπΉ) =
-π-π(lim infβπΉ)) |
63 | 62 | adantr 481 |
. . . . . . . 8
β’ ((π β§ -π(lim
infβπΉ) = +β)
β (lim infβπΉ) =
-π-π(lim infβπΉ)) |
64 | | xnegeq 13182 |
. . . . . . . . 9
β’
(-π(lim infβπΉ) = +β β
-π-π(lim infβπΉ) =
-π+β) |
65 | 64 | adantl 482 |
. . . . . . . 8
β’ ((π β§ -π(lim
infβπΉ) = +β)
β -π-π(lim infβπΉ) =
-π+β) |
66 | | xnegpnf 13184 |
. . . . . . . . 9
β’
-π+β = -β |
67 | 66 | a1i 11 |
. . . . . . . 8
β’ ((π β§ -π(lim
infβπΉ) = +β)
β -π+β = -β) |
68 | 63, 65, 67 | 3eqtrd 2776 |
. . . . . . 7
β’ ((π β§ -π(lim
infβπΉ) = +β)
β (lim infβπΉ) =
-β) |
69 | 61, 68 | sylan2b 594 |
. . . . . 6
β’ ((π β§ Β¬
-π(lim infβπΉ) β +β) β (lim infβπΉ) = -β) |
70 | | liminflbuz2.6 |
. . . . . . . 8
β’ (π β (lim infβπΉ) β
-β) |
71 | 70 | neneqd 2945 |
. . . . . . 7
β’ (π β Β¬ (lim infβπΉ) = -β) |
72 | 71 | adantr 481 |
. . . . . 6
β’ ((π β§ Β¬
-π(lim infβπΉ) β +β) β Β¬ (lim
infβπΉ) =
-β) |
73 | 69, 72 | condan 816 |
. . . . 5
β’ (π β -π(lim
infβπΉ) β
+β) |
74 | 60, 73 | eqnetrd 3008 |
. . . 4
β’ (π β (lim supβ(π β π β¦ -π(πΉβπ))) β +β) |
75 | 1, 44, 45, 5, 46, 74 | limsupubuz2 44515 |
. . 3
β’ (π β βπ β π βπ β (β€β₯βπ)((π β π β¦ -π(πΉβπ))βπ) < +β) |
76 | 43, 75 | reximddv3 43825 |
. 2
β’ (π β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β +β) |
77 | 29, 76 | reximddv3 43825 |
1
β’ (π β βπ β π βπ β (β€β₯βπ)-β < (πΉβπ)) |